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.

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

1. 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.
2. If the bottom cards of each pile are equal, take one of the cards and move (rotate) it to the top of that pile.
3. Riffle both piles. Note that the shuffle does not need to be perfect.
4. 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).

• 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.

• 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.

• 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)