diff --git a/Gilbreath_Card_Trick.ipynb b/Gilbreath_Card_Trick.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..88f29eb99c09416e2a5be7091e2b487a4aefb1e1
--- /dev/null
+++ b/Gilbreath_Card_Trick.ipynb
@@ -0,0 +1,502 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Gilbreath Card Trick\n",
+ "\n",
+ "A while ago a member of the research group that created ProB and ProB2 stumbled across a short article [Unraveling a Card Trick](https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10) by Tony Hoare and Natarajan Shankar in the Dagstuhl library. In memory of Amir Pnueli they decided to model the problem as described in the article.\n",
+ "\n",
+ "The article unravels a card trick by Gilbreath that has several phases:\n",
+ "\n",
+ "* first you arrange 16 cards into a sequence of quartets with one card from each suit (Spade, Club, Heart, Diamond) in the same order. The example in the article is as follows: ⟨5♠⟩,⟨3♡⟩,⟨Q♣⟩,⟨8♢⟩, ⟨K♠⟩,⟨2♡⟩,⟨7♣⟩,⟨4♢⟩, ⟨8♠⟩,⟨J♡⟩,⟨9♣⟩,⟨A♢⟩\n",
+ "\n",
+ "* you split the cards into two sequences. The example in the article is: ⟨5♠⟩,⟨3♡⟩,⟨Q♣⟩,⟨8♢⟩,⟨K♠⟩ and ⟨2♡⟩,⟨7♣⟩,⟨4♢⟩,⟨8♠⟩,⟨J♡⟩,⟨9♣⟩,⟨A♢⟩ .\n",
+ "\n",
+ "* you reverse one of the sequences\n",
+ "\n",
+ "* you perform a (not necessarily perfect) riffle shuffle of the two sequences\n",
+ "\n",
+ "* the resulting final sequence is guaranteed to consist of a sequence of four quartets with one card from each suite.\n",
+ "\n",
+ "In this notebook we are going to use the B machine they have created and visualise it."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: CardTrick"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE CardTrick\n",
+ "/* Translation by Michael Leuschel of Example in\n",
+ " \"Unraveling a Card Trick\" by Tony Hoare and Natarajan Shankar\n",
+ " in LNCS 6200, pp. 195-201, 2010.\n",
+ " DOI: 10.1007/978-3-642-13754-9_10\n",
+ " https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10\n",
+ " */\n",
+ "SETS\n",
+ " SUIT={spade,club,heart,diamond}\n",
+ "DEFINITIONS\n",
+ " all == [spade,club,heart,diamond]; /* an arbitrary permutation of the suits */\n",
+ "\n",
+ " /* check that in dst we can partition the deck into quartets where every suit occurs once: */\n",
+ " ok(dst) == #(a,b,c,d).(dst = a^b^c^d & size(a)=4 & size(b)=4 & size(c)=4 & size(d)=4 &\n",
+ " a : perm(SUIT) & b:perm(SUIT) & c:perm(SUIT) & d:perm(SUIT));\n",
+ " ANIMATION_FUNCTION_DEFAULT == {(1,0,\"x\"),(2,0,\"y\"),(3,0,\"dest\")};\n",
+ " ANIMATION_FUNCTION == ( {r,c,i| r=1 & c|->i:x} \\/ {r,c,i| r=2 & c|->i:y} \\/ {r,c,i| r=3 & c|->i:dest} );\n",
+ " ANIMATION_IMG1 == \"images/French_suits_Spade.gif\";\n",
+ " ANIMATION_IMG2 == \"images/French_suits_Club.gif\";\n",
+ " ANIMATION_IMG3 == \"images/French_suits_Heart.gif\";\n",
+ " ANIMATION_IMG4 == \"images/French_suits_Diamond.gif\";\n",
+ "CONSTANTS\n",
+ " initial\n",
+ "PROPERTIES\n",
+ " initial = all^all^all^all /* we fix the sequence; i.e., we perform symmetry reduction by hand; it should be possible to achieve this by ProB's symmetry reduction itself using a deferred set */\n",
+ "VARIABLES x,y,dest,reversed\n",
+ "INVARIANT\n",
+ " x:seq(SUIT) & y:seq(SUIT) & dest:seq(SUIT) & reversed:BOOL &\n",
+ " ((x=<> & y=<>) => ok(dest)) /* the property we are interested in: after the riffle shuffle the sequence consists of four quartets, each containing every suit */\n",
+ "INITIALISATION\n",
+ " x,y : (x^y = initial) /* split the initial sequence into two: x and y */\n",
+ " || dest := <> || reversed := FALSE\n",
+ "OPERATIONS\n",
+ "\n",
+ " /* reverse one of the two decks */\n",
+ " Reverse = PRE reversed=FALSE THEN CHOICE x := rev(x) OR y := rev(y) END || reversed := TRUE END;\n",
+ "\n",
+ " /* perform the riffle shuffle: transfer one card from either x or y to dest */\n",
+ " Shuffle1 = PRE x/=<> & reversed=TRUE THEN dest := dest<-last(x) || x:= front(x) END;\n",
+ " Shuffle2 = PRE y/=<> & reversed=TRUE THEN dest := dest<-last(y) || y:= front(y) END\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "First of all, we will make some observations. \n",
+ "In this machine, symmetry reduction is perfomed by hand, by forcing a particular order of the cards initially. You can find a version of this model without the symmetry reduction in our [Modelling Examples](https://www3.hhu.de/stups/handbook/prob2/modelling_examples.html#gilbreath-card-trick). For the purpose of this notebook, we will use this model however, because arguably model checking gives less insight into why the trick works than proof does.\n",
+ "A longer Why3 encoding can be found [here](http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html). A version of the model that can be run in TLC was additionally created and can be found in our [Modelling Examples](https://www3.hhu.de/stups/handbook/prob2/modelling_examples.html#gilbreath-card-trick), as well.\n",
+ "\n",
+ "**Note:** To see the graphical visualisation, you will need to have the images for the `ANIMATION_FUNCTION` in your images folder.\n",
+ "\n",
+ "Now we will set up the constants and initialize the machine. As you can see below, our machine has a lot of initialization options, you can use `card(x)=NUMBER` to quickly set a number of cards that should be initialized in x."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: CardTrick\n",
+ "Sets: SUIT\n",
+ "Constants: initial\n",
+ "Variables: x, y, dest, reversed\n",
+ "Operations: \n",
+ "INITIALISATION()\n",
+ "INITIALISATION()\n",
+ "INITIALISATION()\n",
+ "INITIALISATION()\n",
+ "More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 5: $initialise_machine()"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init card(x)=4"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Here we can take a look at our options with the `:browse` command. You will see, that we can execute the reverse operation by typing in `:exec Reverse` and executing that command."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: CardTrick\n",
+ "Sets: SUIT\n",
+ "Constants: initial\n",
+ "Variables: x, y, dest, reversed\n",
+ "Operations: \n",
+ "Reverse()\n",
+ "Reverse()"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Reverse()"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Reverse"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "If we take another look at out options here, we can see, that we can now execute the Shuffle2 command. From here on you can try out the visualisation for yourself. Chose as many Shuffles as you want and look at the visualisation by using the `:show` command."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: CardTrick\n",
+ "Sets: SUIT\n",
+ "Constants: initial\n",
+ "Variables: x, y, dest, reversed\n",
+ "Operations: \n",
+ "Shuffle1()\n",
+ "Shuffle2()"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Shuffle2()"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Shuffle2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/French_suits_Diamond.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/French_suits_Heart.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/French_suits_Club.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/French_suits_Spade.gif\"/></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/French_suits_Spade.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/French_suits_Club.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/French_suits_Heart.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/French_suits_Diamond.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/French_suits_Spade.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/French_suits_Club.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/French_suits_Heart.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/French_suits_Diamond.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/French_suits_Spade.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/French_suits_Club.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/French_suits_Heart.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">dest</td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/French_suits_Diamond.gif\"/></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: CardTrick\n",
+ "Sets: SUIT\n",
+ "Constants: initial\n",
+ "Variables: x, y, dest, reversed\n",
+ "Operations: \n",
+ "Shuffle1()\n",
+ "Shuffle2()"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Shuffle1()"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Shuffle1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/French_suits_Diamond.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/French_suits_Heart.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/French_suits_Club.gif\"/></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/French_suits_Spade.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/French_suits_Club.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/French_suits_Heart.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/French_suits_Diamond.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/French_suits_Spade.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/French_suits_Club.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/French_suits_Heart.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/French_suits_Diamond.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/French_suits_Spade.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/French_suits_Club.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/French_suits_Heart.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">dest</td>\n",
+ "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/French_suits_Diamond.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/French_suits_Spade.gif\"/></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: CardTrick\n",
+ "Sets: SUIT\n",
+ "Constants: initial\n",
+ "Variables: x, y, dest, reversed\n",
+ "Operations: \n",
+ "Shuffle1()\n",
+ "Shuffle2()"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/images/French_suits_Club.gif b/images/French_suits_Club.gif
new file mode 100644
index 0000000000000000000000000000000000000000..665f6407c8ad8ba49334e2174fc46a9490f98751
Binary files /dev/null and b/images/French_suits_Club.gif differ
diff --git a/images/French_suits_Diamond.gif b/images/French_suits_Diamond.gif
new file mode 100644
index 0000000000000000000000000000000000000000..b414772dc0e6fcffc993ec3653c11035e50ee22c
Binary files /dev/null and b/images/French_suits_Diamond.gif differ
diff --git a/images/French_suits_Heart.gif b/images/French_suits_Heart.gif
new file mode 100644
index 0000000000000000000000000000000000000000..772b7e93989c20e22cabcd56f2aee2ccef9a9df4
Binary files /dev/null and b/images/French_suits_Heart.gif differ
diff --git a/images/French_suits_Spade.gif b/images/French_suits_Spade.gif
new file mode 100644
index 0000000000000000000000000000000000000000..08d12e3de5c7dc6bf3af7668b028ca7949627131
Binary files /dev/null and b/images/French_suits_Spade.gif differ