NuITP

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:

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

Download

Everything related to this example -the Maude specifications, the NuITP proof scripts, and the proof reports and snapshots- is bundled in the zip file below. Alternatively, each of these files can also be downloaded separately from the links throughout the rest of this page.

Download Example (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