add miracle Sudoku example

puzzles/Sudoku_Miracle.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Sudoku - The Miracle\n",
+    "\n",
+    "\n",
+    "Here we show how to solve a variation of the Sudoku puzzle, called \"The Miracle\", desigen by Mitchell Lee.\n",
+    "Some links are:\n",
+    "* https://www.reddit.com/r/sudoku/comments/ghkkwp/the_miracle_sudoku/\n",
+    "* https://www.youtube.com/watch?v=yKf9aUIxdb4 */\n",
+    "* https://www.popularmechanics.com/science/a32605317/miracle-sudoku-hardest-puzzle-ever/\n",
+    "\n",
+    "In this puzzle the standard Sudoku rules apply, but in addition there are additional constraints.\n",
+    "The puzzle states that in row 5 and column 3 there is a 1 and in row 6 at column 7 a 2.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: SudokuAsConstantMiracle"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE Sudoku_Setup\n",
+    "DEFINITIONS DOM == 1..9;\n",
+    "      ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};\n",
+    "      ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM &  i = Board(r)(c)} );\n",
+    "      ANIMATION_IMG0 == \"images/sm_empty_box.gif\";\n",
+    "      ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+    "      ANIMATION_IMG2 == \"images/sm_2.gif\";\n",
+    "      ANIMATION_IMG3 == \"images/sm_3.gif\";\n",
+    "      ANIMATION_IMG4 == \"images/sm_4.gif\";\n",
+    "      ANIMATION_IMG5 == \"images/sm_5.gif\";\n",
+    "      ANIMATION_IMG6 == \"images/sm_6.gif\";\n",
+    "      ANIMATION_IMG7 == \"images/sm_7.gif\";\n",
+    "      ANIMATION_IMG8 == \"images/sm_8.gif\";\n",
+    "      ANIMATION_IMG9 == \"images/sm_9.gif\"\n",
+    "CONSTANTS Board\n",
+    "PROPERTIES\n",
+    "  Board : DOM +-> (DOM +-> DOM)   &\n",
+    "\n",
+    " /* PUZZLE CONSTRAINTS : */\n",
+    "   Board(5)(3)=1 & Board(6)(7)=2\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "<table style=\"font-family:monospace\"><tbody>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_empty_box.gif\"/></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Let us gradually solve this puzzle. First we need to stipulate that ```Board``` is totally defined over the domain of numbers from 1..9 and that on all columns and rows the numbers must be distinct."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: Sudoku_Horizontal_Vertical"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE Sudoku_Horizontal_Vertical\n",
+    "DEFINITIONS DOM == 1..9; D1 == 1..8; D2 == 2..9;\n",
+    "      ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};\n",
+    "      ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM &  i = Board(r)(c)} );\n",
+    "      ANIMATION_IMG0 == \"images/sm_empty_box.gif\";\n",
+    "      ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+    "      ANIMATION_IMG2 == \"images/sm_2.gif\";\n",
+    "      ANIMATION_IMG3 == \"images/sm_3.gif\";\n",
+    "      ANIMATION_IMG4 == \"images/sm_4.gif\";\n",
+    "      ANIMATION_IMG5 == \"images/sm_5.gif\";\n",
+    "      ANIMATION_IMG6 == \"images/sm_6.gif\";\n",
+    "      ANIMATION_IMG7 == \"images/sm_7.gif\";\n",
+    "      ANIMATION_IMG8 == \"images/sm_8.gif\";\n",
+    "      ANIMATION_IMG9 == \"images/sm_9.gif\"\n",
+    "CONSTANTS Board\n",
+    "PROPERTIES\n",
+    "  Board ∈ DOM --> (DOM --> DOM)\n",
+    "  ∧\n",
+    "  /*@label \"Horizontal and vertical lines\" */\n",
+    "  ∀y.(y:DOM ⇒ ∀(x1,x2).(x1∈D1 ∧ x1<x2 ∧ x2∈D2  ⇒ (Board(x1)(y) ≠ Board(x2)(y) ∧\n",
+    "                                                    Board(y)(x1) ≠ Board(y)(x2))))\n",
+    "     /*@desc \"within a vertical or horizontal line all numbers must be different\" */\n",
+    "  ∧\n",
+    " /* PUZZLE CONSTRAINTS : */\n",
+    "   Board(5)(3)=1 ∧ Board(6)(7)=2\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "<table style=\"font-family:monospace\"><tbody>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Now let us stipulate that within each sub-square the numbers must also be distinct.\n",
+    "For this we introduce the possible indices for the subsquares ```SUBSQ```."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: Sudoku_Horizontal_Vertical"
+      ]
+     },
+     "execution_count": 16,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE Sudoku_Horizontal_Vertical\n",
+    "DEFINITIONS DOM == 1..9; D1 == 1..8; D2 == 2..9;\n",
+    "      SUBSQ == { {1,2,3}, {4,5,6}, {7,8,9} };\n",
+    "      ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};\n",
+    "      ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM &  i = Board(r)(c)} );\n",
+    "      ANIMATION_IMG0 == \"images/sm_empty_box.gif\";\n",
+    "      ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+    "      ANIMATION_IMG2 == \"images/sm_2.gif\";\n",
+    "      ANIMATION_IMG3 == \"images/sm_3.gif\";\n",
+    "      ANIMATION_IMG4 == \"images/sm_4.gif\";\n",
+    "      ANIMATION_IMG5 == \"images/sm_5.gif\";\n",
+    "      ANIMATION_IMG6 == \"images/sm_6.gif\";\n",
+    "      ANIMATION_IMG7 == \"images/sm_7.gif\";\n",
+    "      ANIMATION_IMG8 == \"images/sm_8.gif\";\n",
+    "      ANIMATION_IMG9 == \"images/sm_9.gif\"\n",
+    "CONSTANTS Board\n",
+    "PROPERTIES\n",
+    "  Board : DOM --> (DOM --> DOM)\n",
+    "  ∧\n",
+    "  /*@label \"Horizontal and vertical lines\" */\n",
+    "  ∀y.(y:DOM ⇒ ∀(x1,x2).(x1∈D1 ∧ x1<x2 ∧ x2∈D2  ⇒ (Board(x1)(y) ≠ Board(x2)(y) ∧\n",
+    "                                                    Board(y)(x1) ≠ Board(y)(x2))))\n",
+    "     /*@desc \"within a vertical or horizontal line all numbers must be different\" */\n",
+    "  ∧\n",
+    "  \n",
+    "  /*@label \"Squares\" */\n",
+    "  ∀(s1,s2).(s1:SUBSQ ∧ s2:SUBSQ ⇒\n",
+    "             ∀(x1,y1,x2,y2).( (x1∈s1 ∧ x2∈s1 ∧ \n",
+    "                               x1>=x2 ∧ (x1=x2 ⇒ y1>y2) ∧ // lexicographical ordering\n",
+    "                               y1∈s2 ∧ y2∈s2 ∧ (x1,y1) ≠ (x2,y2))\n",
+    "                              ⇒\n",
+    "                              Board(x1)(y1) ≠ Board(x2)(y2)\n",
+    "                            ))\n",
+    "     /*@desc \"within a sub-square all numbers must be different\" */\n",
+    "    ∧\n",
+    " /* PUZZLE CONSTRAINTS : */\n",
+    "   Board(5)(3)=1 ∧ Board(6)(7)=2\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 17,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 17,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 18,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 18,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 20,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "<table style=\"font-family:monospace\"><tbody>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 20,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Now we found a classical Sudoku solution.\n",
+    "\n",
+    "We now also add the following constraints:\n",
+    "* Any two cells separated by a knight's or king's move (in chess) cannot contain the same digit\n",
+    "* Any two orthogonally adjacent cells cannot contain consecutive digits.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 21,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: Sudoku_Horizontal_Vertical"
+      ]
+     },
+     "execution_count": 21,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE Sudoku_Horizontal_Vertical\n",
+    "DEFINITIONS DOM == 1..9; D1 == 1..8; D2 == 2..9;\n",
+    "      SUBSQ == { {1,2,3}, {4,5,6}, {7,8,9} };\n",
+    "      ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..9 & c:1..9 & i=0};\n",
+    "      ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:DOM &  i = Board(r)(c)} );\n",
+    "      ANIMATION_IMG0 == \"images/sm_empty_box.gif\";\n",
+    "      ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+    "      ANIMATION_IMG2 == \"images/sm_2.gif\";\n",
+    "      ANIMATION_IMG3 == \"images/sm_3.gif\";\n",
+    "      ANIMATION_IMG4 == \"images/sm_4.gif\";\n",
+    "      ANIMATION_IMG5 == \"images/sm_5.gif\";\n",
+    "      ANIMATION_IMG6 == \"images/sm_6.gif\";\n",
+    "      ANIMATION_IMG7 == \"images/sm_7.gif\";\n",
+    "      ANIMATION_IMG8 == \"images/sm_8.gif\";\n",
+    "      ANIMATION_IMG9 == \"images/sm_9.gif\"\n",
+    "CONSTANTS Board\n",
+    "PROPERTIES\n",
+    "  Board : DOM --> (DOM --> DOM)\n",
+    "  ∧\n",
+    "  /*@label \"Horizontal and vertical lines\" */\n",
+    "  ∀y.(y:DOM ⇒ ∀(x1,x2).(x1∈D1 ∧ x1<x2 ∧ x2∈D2  ⇒ (Board(x1)(y) ≠ Board(x2)(y) ∧\n",
+    "                                                    Board(y)(x1) ≠ Board(y)(x2))))\n",
+    "     /*@desc \"within a vertical or horizontal line all numbers must be different\" */\n",
+    "  ∧\n",
+    "  \n",
+    "  /*@label \"Squares\" */\n",
+    "  ∀(s1,s2).(s1:SUBSQ ∧ s2:SUBSQ ⇒\n",
+    "             ∀(x1,y1,x2,y2).( (x1∈s1 ∧ x2∈s1 ∧ \n",
+    "                               x1>=x2 ∧ (x1=x2 ⇒ y1>y2) ∧ // lexicographical ordering\n",
+    "                               y1∈s2 ∧ y2∈s2 ∧ (x1,y1) ≠ (x2,y2))\n",
+    "                              ⇒\n",
+    "                              Board(x1)(y1) ≠ Board(x2)(y2)\n",
+    "                            ))\n",
+    "     /*@desc \"within a sub-square all numbers must be different\" */\n",
+    "  ∧\n",
+    "    /*@label \"King Moves\" */\n",
+    "  ∀(x,y).(x∈D2 ∧ y∈D2  ⇒\n",
+    "                          (Board(x)(y)   ≠ Board(x-1)(y-1) ∧\n",
+    "                           Board(x)(y-1) ≠ Board(x-1)(y) )\n",
+    "    )\n",
+    "  ∧\n",
+    "  /*@label \"Orthogonals\" */\n",
+    "  ∀(x,y).(x∈D1 ∧ y∈DOM  ⇒\n",
+    "                          (  Board(x)(y) ≠ 1+Board(x+1)(y) ∧\n",
+    "                           1+Board(x)(y) ≠   Board(x+1)(y) ∧\n",
+    "                             Board(y)(x) ≠ 1+Board(y)(x+1) ∧\n",
+    "                           1+Board(y)(x) ≠   Board(y)(x+1) )\n",
+    "    )\n",
+    "     /*@desc \"any two orthogonally adjacent cells cannot contain consecutive digits\" */\n",
+    "  ∧\n",
+    "\n",
+    "  /*@label \"Knight Moves 1\" */\n",
+    "  ∀(x,y).(x∈D1 ∧ y∈DOM  ⇒\n",
+    "                          ( y+2∈DOM ⇒ Board(x)(y) ≠ Board(x+1)(y+2)  ) ∧\n",
+    "                          ( y-2∈DOM ⇒ Board(x)(y) ≠ Board(x+1)(y-2)  )\n",
+    "    ) \n",
+    "  ∧\n",
+    "  /*@label \"Knight Moves 2\" */\n",
+    "  ∀(x,y).(x∈1..7 ∧ y∈DOM  ⇒\n",
+    "                          ( y+1∈DOM ⇒ Board(x)(y) ≠ Board(x+2)(y+1)  ) ∧\n",
+    "                          ( y-1∈DOM ⇒ Board(x)(y) ≠ Board(x+2)(y-1)  )\n",
+    "    )\n",
+    "\n",
+    "   ∧\n",
+    " /* PUZZLE CONSTRAINTS : */\n",
+    "   Board(5)(3)=1 ∧ Board(6)(7)=2\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 22,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 22,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 23,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 1: $initialise_machine()"
+      ]
+     },
+     "execution_count": 23,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 24,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "<table style=\"font-family:monospace\"><tbody>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "</tr>\n",
+       "<tr>\n",
+       "<td style=\"padding:0px\"><img alt=\"9\" src=\"images/sm_9.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/sm_4.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"8\" src=\"images/sm_8.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_3.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"7\" src=\"images/sm_7.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_2.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_6.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/sm_5.gif\"/></td>\n",
+       "</tr>\n",
+       "</tbody></table>"
+      ],
+      "text/plain": [
+       "<Animation function visualisation>"
+      ]
+     },
+     "execution_count": 24,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "This corresponds to the solution in https://www.youtube.com/watch?v=yKf9aUIxdb4 \n",
+    "We can see that there is only one solution:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 26,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n",
+       " -->\n",
+       "<!-- Title: visited_states Pages: 1 -->\n",
+       "<svg width=\"1162pt\" height=\"394pt\"\n",
+       " viewBox=\"0.00 0.00 1162.00 394.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 390)\">\n",
+       "<title>visited_states</title>\n",
+       "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-390 1159,-390 1159,5 -4,5\"/>\n",
+       "<!-- root -->\n",
+       "<g id=\"node1\" class=\"node\"><title>root</title>\n",
+       "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"577,-340.7 622.195,-374.15 531.805,-374.15 577,-340.7\"/>\n",
+       "<text text-anchor=\"middle\" x=\"577\" y=\"-359.4\" font-family=\"Times,serif\" font-size=\"12.00\">root</text>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+       "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"1154.21,-217.7 -0.213017,-217.7 -0.213017,-166.3 1154.21,-166.3 1154.21,-217.7\"/>\n",
+       "<text text-anchor=\"middle\" x=\"577\" y=\"-202.8\" font-family=\"Times,serif\" font-size=\"12.00\">Board(1) = {(1|&#45;&gt;4),(2|&#45;&gt;8),(3|&#45;&gt;3),(4|&#45;&gt;7),(5|&#45;&gt;2),(6|&#45;&gt;6),(7|&#45;&gt;1),(8|&#45;&gt;5),(9|&#45;...,Board(2) = {(1|&#45;&gt;7),(2|&#45;&gt;2),(3|&#45;&gt;6),(4|&#45;&gt;1),(5|&#45;&gt;5),(6|&#45;&gt;9),(7|&#45;&gt;4),(8|&#45;&gt;8),(9|&#45;...,Board(3) = {(1|&#45;&gt;1),(2|&#45;&gt;5),(3|&#45;&gt;9),(4|&#45;&gt;4),(5|&#45;&gt;8),(6|&#45;&gt;3),(7|&#45;&gt;7),(8|&#45;&gt;2),(9|&#45;...,</text>\n",
+       "<text text-anchor=\"middle\" x=\"577\" y=\"-188.4\" font-family=\"Times,serif\" font-size=\"12.00\">Board(4) = {(1|&#45;&gt;8),(2|&#45;&gt;3),(3|&#45;&gt;7),(4|&#45;&gt;2),(5|&#45;&gt;6),(6|&#45;&gt;1),(7|&#45;&gt;5),(8|&#45;&gt;9),(9|&#45;...,Board(5) = {(1|&#45;&gt;2),(2|&#45;&gt;6),(3|&#45;&gt;1),(4|&#45;&gt;5),(5|&#45;&gt;9),(6|&#45;&gt;4),(7|&#45;&gt;8),(8|&#45;&gt;3),(9|&#45;...,Board(6) = {(1|&#45;&gt;5),(2|&#45;&gt;9),(3|&#45;&gt;4),(4|&#45;&gt;8),(5|&#45;&gt;3),(6|&#45;&gt;7),(7|&#45;&gt;2),(8|&#45;&gt;6),(9|&#45;...,</text>\n",
+       "<text text-anchor=\"middle\" x=\"577\" y=\"-174\" font-family=\"Times,serif\" font-size=\"12.00\">Board(7) = {(1|&#45;&gt;3),(2|&#45;&gt;7),(3|&#45;&gt;2),(4|&#45;&gt;6),(5|&#45;&gt;1),(6|&#45;&gt;5),(7|&#45;&gt;9),(8|&#45;&gt;4),(9|&#45;...,Board(8) = {(1|&#45;&gt;6),(2|&#45;&gt;1),(3|&#45;&gt;5),(4|&#45;&gt;9),(5|&#45;&gt;4),(6|&#45;&gt;8),(7|&#45;&gt;3),(8|&#45;&gt;7),(9|&#45;...,Board(9) = {(1|&#45;&gt;9),(2|&#45;&gt;4),(3|&#45;&gt;8),(4|&#45;&gt;3),(5|&#45;&gt;7),(6|&#45;&gt;2),(7|&#45;&gt;6),(8|&#45;&gt;1),(9|&#45;...</text>\n",
+       "</g>\n",
+       "<!-- root&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\"><title>root&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M577,-340.596C577,-312.305 577,-262.089 577,-228.179\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"580.5,-227.79 577,-217.79 573.5,-227.79 580.5,-227.79\"/>\n",
+       "<text text-anchor=\"middle\" x=\"633.662\" y=\"-275.4\" font-family=\"Times,serif\" font-size=\"12.00\">SETUP_CONSTANTS</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node5\" class=\"node\"><title>1</title>\n",
+       "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"604,-14.5442 604,-29.4558 588.184,-40 565.816,-40 550,-29.4558 550,-14.5442 565.816,-4 588.184,-4 604,-14.5442\"/>\n",
+       "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"608,-12.4034 608,-31.5966 589.395,-44 564.605,-44 546,-31.5966 546,-12.4034 564.605,-3.55271e-15 589.395,-0 608,-12.4034\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"#006391\" d=\"M577,-166.211C577,-136.526 577,-86.7671 577,-54.4156\"/>\n",
+       "<polygon fill=\"#006391\" stroke=\"#006391\" points=\"580.5,-54.1656 577,-44.1656 573.5,-54.1657 580.5,-54.1656\"/>\n",
+       "<text text-anchor=\"middle\" x=\"622.976\" y=\"-101.4\" font-family=\"Times,serif\" font-size=\"12.00\">INITIALISATION</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>"
+      ],
+      "text/plain": [
+       "<Dot visualization: state_space []>"
+      ]
+     },
+     "execution_count": 26,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":dot state_space"
+   ]
+  },
+  {
+   "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
+}