Example

Gilbreath's Card Trick

The Gilbreath's card trick is a popular card trick based on Norman L. Gilbreath's principle stating that, given an initial deck of cards with some adequate properties, after a random shuffle the resulting deck will preserve some of those properties. For example, in the Gilbreath's card trick, given an initial deck of cards with alternating (e.g., red and black) colors, after shuffling it once, if we deal the resulting deck in pairs, each pair will always contain one card of each color. Note that the trick can be generalized for n colors.

How the Trick Works

Schematically, the trick can be achieved by following the next steps.

Consider an initial, even deck of cards so that they are sorted alternating colors (e.g., red and black) and split the deck in two, not necessarily equal piles.
If the bottom cards of each pile are equal, take one of the cards and move (rotate) it to the top of that pile.
Riffle both piles. Note that the shuffle does not need to be perfect.
Deal the resulting deck in pairs. All pairs will always have a card of each color (e.g., either red-black or black-red cards).

Download

Complete example

Gilbreath bundle

The Maude specifications, the NuITP proof scripts, and the proof reports and snapshots. Every file is also linked separately further down this page.

Download ZIP

Equational Theories

The original GILBREATH-ACU Maude specification of the Gilbreath's Card Trick can be found here.
The enriched GILBREATH-ACU-ENRICHED Maude specification of the Gilbreath's Card Trick can be found here.

Proof Scripts

The following NuITP proof scripts require NuITP Alpha 30 running in Maude Alpha 160 or later.

A detailed proof script with explicit proofs and internalization of the simplification lemmas can be found here.
A simpler proof script with the simplification lemmas already internalized as Maude equations can be found here.

Proof Reports and Snapshots

Simplification Lemmas

Internalized as Maude equations in the enriched specification above.

alter(L1 C1 C1 L2) = False Proof report Snapshot
(paired(C1,C2) = True) → alter(L1 C1 C2 C1 L2) = alter(L1 C1 L2) Proof report Snapshot
(paired(C1,C2) = True) → alter(L1 C1 C2) = alter(L1 C1) Proof report Snapshot
even(L1 red L2) = even(black L1 L2) Proof report Snapshot
shuffle(nil, nil, L) = False Proof report Snapshot
shuffle(nil, C1 L, C2) = False Proof report Snapshot
shuffle(C1 L, nil, C2) = False Proof report Snapshot
shuffle(L1, L2, C) = False Proof report Snapshot
(paired(C1,C2) = True) → shuffle(C1 L1, C2 L2, C1 L3) = shuffle(L1, C2 L2, L3) Proof report Snapshot
(paired(C1,C2) = True) → shuffle(C1 L1, C2 L2, C2 L3) = shuffle(C1 L1, L2, L3) Proof report Snapshot

Non-executable Lemma

((alter(L1 C L2 C L3) = True) /\ (even(L2) = True)) → false Proof report Snapshot

Main Goal 1

((alter(L1 L2) = True) /\ (even((L1 L2)) = True) /\ (opposite(L1, L2) = True) /\ (shuffle(L1, L2, L3) = True)) → (pairedList(L3) = True) Proof report Snapshot

Main Goal 2

((alter(L1 L2) = True) /\ (even(L1 L2) = True) /\ (opposite(L1, L2) = False) /\ (shuffle(L1, L2, L3) = True)) → (pairedList(rotate(L3)) = True) Proof report Snapshot