Initial commit

8c1dd15c · penguinn · 8c1dd15c · 8c1dd15c · 8c1dd15c · 8c1dd15c
Commit 8c1dd15c authored 6 years ago by penguinn
--- a/.ipynb_checkpoints/Apples_and_Oranges-checkpoint.ipynb
+++ b/.ipynb_checkpoints/Apples_and_Oranges-checkpoint.ipynb
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Apples and Oranges\n",
+    "\n",
+    "Use `:help` to get an overview for the jupyter notebook commands.\n",
+    "\n",
+    "This puzzle is [apparently an Interview question at Apple](https://bgr.com/2015/11/20/apple-interview-questions/). Quoting from\n",
+    "[1](https://bgr.com/2015/11/20/apple-interview-questions/) we have the\n",
+    "following information:\n",
+    "\n",
+    "* (1) There are three boxes, one contains only apples, one contains only oranges, and one contains both apples and oranges.\n",
+    "* (2) The boxes have been incorrectly labeled such that no label identifies the actual contents of the box it labels.\n",
+    "* (3) Opening just one box, and without looking in the box, you take out one piece of fruit.\n",
+    "* (4) By looking at the fruit, how can you immediately label all of the boxes correctly?\n",
+    "\n",
+    "Here is one encoding of this puzzle in B:\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: ApplesOranges"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE ApplesOranges\n",
+    "SETS\n",
+    " Fruit={apple,orange}; // possible content for the boxes\n",
+    " Label={A,O,Both} // labels for the boxes\n",
+    "CONSTANTS a,o,b,  // a,o,b are the three boxes\n",
+    "          Take,  // which box should we open (the label of that box)\n",
+    "          DecisionFunction // given the fruit we pick from Take: what are the contents of the boxes labeled A,O,Both\n",
+    "PROPERTIES\n",
+    "  a = {apple} & o={orange} & b={apple,orange} // (1)\n",
+    "  &\n",
+    "  Take : Label //3\n",
+    "  &\n",
+    "  DecisionFunction : Fruit --> (Label >->> {a,o,b}) & //4\n",
+    "  !label. ( // the decision function has to work for all allowed labelings\n",
+    "  ( label : {a,o,b} >->> Label &\n",
+    "    label(a) /= A & label(o) /= O & label(b) /= Both // (2)\n",
+    "  )\n",
+    "   =>\n",
+    "  !f.(f: label~(Take)\n",
+    "      => DecisionFunction(f)=label~ // the function should tell us what is behind label A,O,Both\n",
+    "     )\n",
+    "  )\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "We have abstracted the box of apples `a` by the set containing `apple`.\n",
+    "Ditto for `o` and `b`, which are abstracted by `{orange}` and\n",
+    "`{apple,orange}` respectively.\n",
+    "\n",
+    "NOTE: You need a recent version of ProB 1.5.1-beta3 or newer to load the above model on your own computer with its one-line comments. If you have an older version of ProB, simply use the normal comments `/* ... */`.\n",
+    "\n",
+    "`:goto Number` jumps to the state with the given number. \n",
+    "\n",
+    "With the `:trace` command, you will get the information of your current trace.\n",
+    "\n",
+    "There is an autocompletion tool, which allows you to see the possible commands, simply use TAB after you type in your `:`. \n",
+    "\n",
+    "This model gives you just one solution, after setting up the constants with `:constants`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Changed to state with index -1"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":goto -1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "* -1: Root state\n",
+       "* 0: `SETUP_CONSTANTS()` **(current)**"
+      ],
+      "text/plain": [
+       "-1: Root state\n",
+       "0: SETUP_CONSTANTS() (current)"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":trace"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{Both}$"
+      ],
+      "text/plain": [
+       "Both"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "Take"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "As we can see, the only solution is to open the box labelled with\n",
+    "\"Both\". We can inspect the decision function by using the jupyter notebook code block, like follows:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(\\mathit{A}\\mapsto\\{\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{apple}\\})\\}$"
+      ],
+      "text/plain": [
+       "{(A↦{orange}),(O↦{apple,orange}),(Both↦{apple})}"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "DecisionFunction(apple)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(\\mathit{A}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{orange}\\})\\}$"
+      ],
+      "text/plain": [
+       "{(A↦{apple,orange}),(O↦{apple}),(Both↦{orange})}"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "DecisionFunction(orange)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "In other words, when we pick an apple out of the box labelled with\n",
+    "\"Both\", then it contains only apples and the box labelled \"O\"ranges\n",
+    "contains both apples and oranges. The box labelled \"A\"pples contains\n",
+    "just oranges. Similarly, if we pick up an orange out of the box labelled\n",
+    "with \"Both\", then it contains only oranges and the box labelled with\n",
+    "\"A\"pples contains contains both apples and oranges. The box labelled\n",
+    "\"O\"ranges contains just apples.\n",
+    "\n",
+    "NOTE: You can use `:table Expression` to get values or expressions in a tabular form."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|prj1|prj2|\n",
+       "|---|---|\n",
+       "|$\\mathit{apple}$|$\\{(\\mathit{A}\\mapsto\\{\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{apple}\\})\\}$|\n",
+       "|$\\mathit{orange}$|$\\{(\\mathit{A}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{orange}\\})\\}$|\n"
+      ],
+      "text/plain": [
+       "prj1\tprj2\n",
+       "apple\t{(A|->{orange}),(O|->{apple,orange}),(Both|->{apple})}\n",
+       "orange\t{(A|->{apple,orange}),(O|->{apple}),(Both|->{orange})}\n"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":table DecisionFunction"
+   ]
+  },
+  {
+   "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
+}
+%% Cell type:markdown id: tags:
+
+# Apples and Oranges
+
+Use `:help` to get an overview for the jupyter notebook commands.
+
+This puzzle is [apparently an Interview question at Apple](https://bgr.com/2015/11/20/apple-interview-questions/). Quoting from
+[1](https://bgr.com/2015/11/20/apple-interview-questions/) we have the
+following information:
+
+* (1) There are three boxes, one contains only apples, one contains only oranges, and one contains both apples and oranges.
+* (2) The boxes have been incorrectly labeled such that no label identifies the actual contents of the box it labels.
+* (3) Opening just one box, and without looking in the box, you take out one piece of fruit.
+* (4) By looking at the fruit, how can you immediately label all of the boxes correctly?
+
+Here is one encoding of this puzzle in B:
+
+%% Cell type:code id: tags:
+
+``` prob
+::load
+MACHINE ApplesOranges
+SETS
+ Fruit={apple,orange}; // possible content for the boxes
+ Label={A,O,Both} // labels for the boxes
+CONSTANTS a,o,b,  // a,o,b are the three boxes
+          Take,  // which box should we open (the label of that box)
+          DecisionFunction // given the fruit we pick from Take: what are the contents of the boxes labeled A,O,Both
+PROPERTIES
+  a = {apple} & o={orange} & b={apple,orange} // (1)
+  &
+  Take : Label //3
+  &
+  DecisionFunction : Fruit --> (Label >->> {a,o,b}) & //4
+  !label. ( // the decision function has to work for all allowed labelings
+  ( label : {a,o,b} >->> Label &
+    label(a) /= A & label(o) /= O & label(b) /= Both // (2)
+  )
+   =>
+  !f.(f: label~(Take)
+      => DecisionFunction(f)=label~ // the function should tell us what is behind label A,O,Both
+     )
+  )
+END
+```
+
+%% Output
+
+    Loaded machine: ApplesOranges
+
+%% Cell type:markdown id: tags:
+
+We have abstracted the box of apples `a` by the set containing `apple`.
+Ditto for `o` and `b`, which are abstracted by `{orange}` and
+`{apple,orange}` respectively.
+
+NOTE: You need a recent version of ProB 1.5.1-beta3 or newer to load the above model on your own computer with its one-line comments. If you have an older version of ProB, simply use the normal comments `/* ... */`.
+
+`:goto Number` jumps to the state with the given number.
+
+With the `:trace` command, you will get the information of your current trace.
+
+There is an autocompletion tool, which allows you to see the possible commands, simply use TAB after you type in your `:`.
+
+This model gives you just one solution, after setting up the constants with `:constants`.
+
+%% Cell type:code id: tags:
+
+``` prob
+:goto -1
+```
+
+%% Output
+
+    Changed to state with index -1
+
+%% Cell type:code id: tags:
+
+``` prob
+:trace
+```
+
+%% Output
+
+    * -1: Root state
+    * 0: `SETUP_CONSTANTS()` **(current)**
+    -1: Root state
+    0: SETUP_CONSTANTS() (current)
+
+%% Cell type:code id: tags:
+
+``` prob
+:constants
+```
+
+%% Output
+
+    Machine constants set up using operation 0: $setup_constants()
+
+%% Cell type:code id: tags:
+
+``` prob
+Take
+```
+
+%% Output
+
+    $\mathit{Both}$
+    Both
+
+%% Cell type:markdown id: tags:
+
+As we can see, the only solution is to open the box labelled with
+"Both". We can inspect the decision function by using the jupyter notebook code block, like follows:
+
+%% Cell type:code id: tags:
+
+``` prob
+DecisionFunction(apple)
+```
+
+%% Output
+
+    $\{(\mathit{A}\mapsto\{\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{Both}\mapsto\{\mathit{apple}\})\}$
+    {(A↦{orange}),(O↦{apple,orange}),(Both↦{apple})}
+
+%% Cell type:code id: tags:
+
+``` prob
+DecisionFunction(orange)
+```
+
+%% Output
+
+    $\{(\mathit{A}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple}\}),(\mathit{Both}\mapsto\{\mathit{orange}\})\}$
+    {(A↦{apple,orange}),(O↦{apple}),(Both↦{orange})}
+
+%% Cell type:markdown id: tags:
+
+In other words, when we pick an apple out of the box labelled with
+"Both", then it contains only apples and the box labelled "O"ranges
+contains both apples and oranges. The box labelled "A"pples contains
+just oranges. Similarly, if we pick up an orange out of the box labelled
+with "Both", then it contains only oranges and the box labelled with
+"A"pples contains contains both apples and oranges. The box labelled
+"O"ranges contains just apples.
+
+NOTE: You can use `:table Expression` to get values or expressions in a tabular form.
+
+%% Cell type:code id: tags:
+
+``` prob
+:table DecisionFunction
+```
+
+%% Output
+
+    |prj1|prj2|
+    |---|---|
+    |$\mathit{apple}$|$\{(\mathit{A}\mapsto\{\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{Both}\mapsto\{\mathit{apple}\})\}$|
+    |$\mathit{orange}$|$\{(\mathit{A}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple}\}),(\mathit{Both}\mapsto\{\mathit{orange}\})\}$|
+    prj1	prj2
+    apple	{(A|->{orange}),(O|->{apple,orange}),(Both|->{apple})}
+    orange	{(A|->{apple,orange}),(O|->{apple}),(Both|->{orange})}
+
+%% Cell type:code id: tags:
+
+``` prob
+```
--- a/.ipynb_checkpoints/Argumentation_Theory-checkpoint.ipynb
+++ b/.ipynb_checkpoints/Argumentation_Theory-checkpoint.ipynb
--- a/Apples_and_Oranges.ipynb
+++ b/Apples_and_Oranges.ipynb
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Apples and Oranges\n",
+    "\n",
+    "Use `:help` to get an overview for the jupyter notebook commands.\n",
+    "\n",
+    "This puzzle is [apparently an Interview question at Apple](https://bgr.com/2015/11/20/apple-interview-questions/). Quoting from\n",
+    "[1](https://bgr.com/2015/11/20/apple-interview-questions/) we have the\n",
+    "following information:\n",
+    "\n",
+    "* (1) There are three boxes, one contains only apples, one contains only oranges, and one contains both apples and oranges.\n",
+    "* (2) The boxes have been incorrectly labeled such that no label identifies the actual contents of the box it labels.\n",
+    "* (3) Opening just one box, and without looking in the box, you take out one piece of fruit.\n",
+    "* (4) By looking at the fruit, how can you immediately label all of the boxes correctly?\n",
+    "\n",
+    "Here is one encoding of this puzzle in B:\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: ApplesOranges"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE ApplesOranges\n",
+    "SETS\n",
+    " Fruit={apple,orange}; // possible content for the boxes\n",
+    " Label={A,O,Both} // labels for the boxes\n",
+    "CONSTANTS a,o,b,  // a,o,b are the three boxes\n",
+    "          Take,  // which box should we open (the label of that box)\n",
+    "          DecisionFunction // given the fruit we pick from Take: what are the contents of the boxes labeled A,O,Both\n",
+    "PROPERTIES\n",
+    "  a = {apple} & o={orange} & b={apple,orange} // (1)\n",
+    "  &\n",
+    "  Take : Label //3\n",
+    "  &\n",
+    "  DecisionFunction : Fruit --> (Label >->> {a,o,b}) & //4\n",
+    "  !label. ( // the decision function has to work for all allowed labelings\n",
+    "  ( label : {a,o,b} >->> Label &\n",
+    "    label(a) /= A & label(o) /= O & label(b) /= Both // (2)\n",
+    "  )\n",
+    "   =>\n",
+    "  !f.(f: label~(Take)\n",
+    "      => DecisionFunction(f)=label~ // the function should tell us what is behind label A,O,Both\n",
+    "     )\n",
+    "  )\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "We have abstracted the box of apples `a` by the set containing `apple`.\n",
+    "Ditto for `o` and `b`, which are abstracted by `{orange}` and\n",
+    "`{apple,orange}` respectively.\n",
+    "\n",
+    "NOTE: You need a recent version of ProB 1.5.1-beta3 or newer to load the above model on your own computer with its one-line comments. If you have an older version of ProB, simply use the normal comments `/* ... */`.\n",
+    "\n",
+    "`:goto Number` jumps to the state with the given number. \n",
+    "\n",
+    "With the `:trace` command, you will get the information of your current trace.\n",
+    "\n",
+    "There is an autocompletion tool, which allows you to see the possible commands, simply use TAB after you type in your `:`. \n",
+    "\n",
+    "This model gives you just one solution, after setting up the constants with `:constants`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Changed to state with index -1"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":goto -1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "* -1: Root state\n",
+       "* 0: `SETUP_CONSTANTS()` **(current)**"
+      ],
+      "text/plain": [
+       "-1: Root state\n",
+       "0: SETUP_CONSTANTS() (current)"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":trace"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{Both}$"
+      ],
+      "text/plain": [
+       "Both"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "Take"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "As we can see, the only solution is to open the box labelled with\n",
+    "\"Both\". We can inspect the decision function by using the jupyter notebook code block, like follows:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(\\mathit{A}\\mapsto\\{\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{apple}\\})\\}$"
+      ],
+      "text/plain": [
+       "{(A↦{orange}),(O↦{apple,orange}),(Both↦{apple})}"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "DecisionFunction(apple)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(\\mathit{A}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{orange}\\})\\}$"
+      ],
+      "text/plain": [
+       "{(A↦{apple,orange}),(O↦{apple}),(Both↦{orange})}"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "DecisionFunction(orange)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "In other words, when we pick an apple out of the box labelled with\n",
+    "\"Both\", then it contains only apples and the box labelled \"O\"ranges\n",
+    "contains both apples and oranges. The box labelled \"A\"pples contains\n",
+    "just oranges. Similarly, if we pick up an orange out of the box labelled\n",
+    "with \"Both\", then it contains only oranges and the box labelled with\n",
+    "\"A\"pples contains contains both apples and oranges. The box labelled\n",
+    "\"O\"ranges contains just apples.\n",
+    "\n",
+    "NOTE: You can use `:table Expression` to get values or expressions in a tabular form."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|prj1|prj2|\n",
+       "|---|---|\n",
+       "|$\\mathit{apple}$|$\\{(\\mathit{A}\\mapsto\\{\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{apple}\\})\\}$|\n",
+       "|$\\mathit{orange}$|$\\{(\\mathit{A}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{orange}\\})\\}$|\n"
+      ],
+      "text/plain": [
+       "prj1\tprj2\n",
+       "apple\t{(A|->{orange}),(O|->{apple,orange}),(Both|->{apple})}\n",
+       "orange\t{(A|->{apple,orange}),(O|->{apple}),(Both|->{orange})}\n"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":table DecisionFunction"
+   ]
+  },
+  {
+   "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
+}
+%% Cell type:markdown id: tags:
+
+# Apples and Oranges
+
+Use `:help` to get an overview for the jupyter notebook commands.
+
+This puzzle is [apparently an Interview question at Apple](https://bgr.com/2015/11/20/apple-interview-questions/). Quoting from
+[1](https://bgr.com/2015/11/20/apple-interview-questions/) we have the
+following information:
+
+* (1) There are three boxes, one contains only apples, one contains only oranges, and one contains both apples and oranges.
+* (2) The boxes have been incorrectly labeled such that no label identifies the actual contents of the box it labels.
+* (3) Opening just one box, and without looking in the box, you take out one piece of fruit.
+* (4) By looking at the fruit, how can you immediately label all of the boxes correctly?
+
+Here is one encoding of this puzzle in B:
+
+%% Cell type:code id: tags:
+
+``` prob
+::load
+MACHINE ApplesOranges
+SETS
+ Fruit={apple,orange}; // possible content for the boxes
+ Label={A,O,Both} // labels for the boxes
+CONSTANTS a,o,b,  // a,o,b are the three boxes
+          Take,  // which box should we open (the label of that box)
+          DecisionFunction // given the fruit we pick from Take: what are the contents of the boxes labeled A,O,Both
+PROPERTIES
+  a = {apple} & o={orange} & b={apple,orange} // (1)
+  &
+  Take : Label //3
+  &
+  DecisionFunction : Fruit --> (Label >->> {a,o,b}) & //4
+  !label. ( // the decision function has to work for all allowed labelings
+  ( label : {a,o,b} >->> Label &
+    label(a) /= A & label(o) /= O & label(b) /= Both // (2)
+  )
+   =>
+  !f.(f: label~(Take)
+      => DecisionFunction(f)=label~ // the function should tell us what is behind label A,O,Both
+     )
+  )
+END
+```
+
+%% Output
+
+    Loaded machine: ApplesOranges
+
+%% Cell type:markdown id: tags:
+
+We have abstracted the box of apples `a` by the set containing `apple`.
+Ditto for `o` and `b`, which are abstracted by `{orange}` and
+`{apple,orange}` respectively.
+
+NOTE: You need a recent version of ProB 1.5.1-beta3 or newer to load the above model on your own computer with its one-line comments. If you have an older version of ProB, simply use the normal comments `/* ... */`.
+
+`:goto Number` jumps to the state with the given number.
+
+With the `:trace` command, you will get the information of your current trace.
+
+There is an autocompletion tool, which allows you to see the possible commands, simply use TAB after you type in your `:`.
+
+This model gives you just one solution, after setting up the constants with `:constants`.
+
+%% Cell type:code id: tags:
+
+``` prob
+:goto -1
+```
+
+%% Output
+
+    Changed to state with index -1
+
+%% Cell type:code id: tags:
+
+``` prob
+:trace
+```
+
+%% Output
+
+    * -1: Root state
+    * 0: `SETUP_CONSTANTS()` **(current)**
+    -1: Root state
+    0: SETUP_CONSTANTS() (current)
+
+%% Cell type:code id: tags:
+
+``` prob
+:constants
+```
+
+%% Output
+
+    Machine constants set up using operation 0: $setup_constants()
+
+%% Cell type:code id: tags:
+
+``` prob
+Take
+```
+
+%% Output
+
+    $\mathit{Both}$
+    Both
+
+%% Cell type:markdown id: tags:
+
+As we can see, the only solution is to open the box labelled with
+"Both". We can inspect the decision function by using the jupyter notebook code block, like follows:
+
+%% Cell type:code id: tags:
+
+``` prob
+DecisionFunction(apple)
+```
+
+%% Output
+
+    $\{(\mathit{A}\mapsto\{\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{Both}\mapsto\{\mathit{apple}\})\}$
+    {(A↦{orange}),(O↦{apple,orange}),(Both↦{apple})}
+
+%% Cell type:code id: tags:
+
+``` prob
+DecisionFunction(orange)
+```
+
+%% Output
+
+    $\{(\mathit{A}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple}\}),(\mathit{Both}\mapsto\{\mathit{orange}\})\}$
+    {(A↦{apple,orange}),(O↦{apple}),(Both↦{orange})}
+
+%% Cell type:markdown id: tags:
+
+In other words, when we pick an apple out of the box labelled with
+"Both", then it contains only apples and the box labelled "O"ranges
+contains both apples and oranges. The box labelled "A"pples contains
+just oranges. Similarly, if we pick up an orange out of the box labelled
+with "Both", then it contains only oranges and the box labelled with
+"A"pples contains contains both apples and oranges. The box labelled
+"O"ranges contains just apples.
+
+NOTE: You can use `:table Expression` to get values or expressions in a tabular form.
+
+%% Cell type:code id: tags:
+
+``` prob
+:table DecisionFunction
+```
+
+%% Output
+
+    |prj1|prj2|
+    |---|---|
+    |$\mathit{apple}$|$\{(\mathit{A}\mapsto\{\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{Both}\mapsto\{\mathit{apple}\})\}$|
+    |$\mathit{orange}$|$\{(\mathit{A}\mapsto\{\mathit{apple},\mathit{orange}\}),(\mathit{O}\mapsto\{\mathit{apple}\}),(\mathit{Both}\mapsto\{\mathit{orange}\})\}$|
+    prj1	prj2
+    apple	{(A|->{orange}),(O|->{apple,orange}),(Both|->{apple})}
+    orange	{(A|->{apple,orange}),(O|->{apple}),(Both|->{orange})}
+
+%% Cell type:code id: tags:
+
+``` prob
+```
--- a/Argumentation_Theory.ipynb
+++ b/Argumentation_Theory.ipynb
--- a/images/ProBRodinArgumentationState.png
+++ b/images/ProBRodinArgumentationState.png
--- a/images/ProB_ApplesOranges_Sol.png
+++ b/images/ProB_ApplesOranges_Sol.png
--- a/images/ProB_ApplesOranges_Table.png
+++ b/images/ProB_ApplesOranges_Table.png