diff --git a/notebooks/tests/SatSolverTests.ipynb b/notebooks/tests/SatSolverTests.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..0d58deeb439c87fb5907aef67afd2f1f13ec45d0
--- /dev/null
+++ b/notebooks/tests/SatSolverTests.ipynb
@@ -0,0 +1,668 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "a4a213e8",
+ "metadata": {},
+ "source": [
+ "## SAT Solver Tests"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "01e215d3",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "```\n",
+ ":solve SOLVER PREDICATE\n",
+ "```\n",
+ "\n",
+ "Solve a predicate with the specified solver.\n",
+ "\n",
+ "The following solvers are currently available:\n",
+ "\n",
+ "* `cdclt`\n",
+ "* `cvc4`\n",
+ "* `kodkod`\n",
+ "* `prob`\n",
+ "* `sat`\n",
+ "* `smt_supported_interpreter`\n",
+ "* `z3`\n",
+ "* `z3axm`\n",
+ "* `z3cns`\n"
+ ],
+ "text/plain": [
+ ":solve SOLVER PREDICATE\n",
+ "Solve a predicate with the specified solver.\n",
+ "\n",
+ "The following solvers are currently available:\n",
+ "\n",
+ "* `cdclt`\n",
+ "* `cvc4`\n",
+ "* `kodkod`\n",
+ "* `prob`\n",
+ "* `sat`\n",
+ "* `smt_supported_interpreter`\n",
+ "* `z3`\n",
+ "* `z3axm`\n",
+ "* `z3cns`\n"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help solve"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "02a2dbf2",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = \\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = FALSE"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve sat x=TRUE or x=FALSE"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "c8f648d6",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = \\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = TRUE"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve sat x=TRUE"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "id": "4cc4a611",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: test"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE test\n",
+ "CONSTANTS m,f,y\n",
+ "PROPERTIES\n",
+ " m=4 & f:1..m --> BOOL & y=f(1)\n",
+ " END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "421cc45b",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants were not set up yet. Automatically set up constants using arbitrary transition: SETUP_CONSTANTS()\n",
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "7e6378c2",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = \\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = TRUE"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve sat x=TRUE"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "dc2a70bd",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "y"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "846f3a21",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{f} = \\{(1\\mapsto\\mathit{TRUE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE})\\}$\n",
+ "* $\\mathit{x} = \\mathit{TRUE}$\n",
+ "* $\\mathit{y} = \\mathit{TRUE}$\n",
+ "* $\\mathit{n} = 4$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tf = {(1↦TRUE),(2↦FALSE),(3↦FALSE),(4↦FALSE)}\n",
+ "\tx = TRUE\n",
+ "\ty = TRUE\n",
+ "\tn = 4"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve sat x=y"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "a8ebb357",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{f} = \\{(1\\mapsto\\mathit{TRUE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE})\\}$\n",
+ "* $\\mathit{x} = \\mathit{FALSE}$\n",
+ "* $\\mathit{y} = \\mathit{TRUE}$\n",
+ "* $\\mathit{n} = 4$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tf = {(1↦TRUE),(2↦FALSE),(3↦FALSE),(4↦FALSE)}\n",
+ "\tx = FALSE\n",
+ "\ty = TRUE\n",
+ "\tn = 4"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve sat x/=y"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "id": "596333cd",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{ff} = \\{(1\\mapsto\\mathit{TRUE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{TRUE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{TRUE}),(10\\mapsto\\mathit{FALSE}),(11\\mapsto\\mathit{FALSE}),(12\\mapsto\\mathit{FALSE}),(13\\mapsto\\mathit{FALSE}),(14\\mapsto\\mathit{FALSE}),(15\\mapsto\\mathit{FALSE}),(16\\mapsto\\mathit{FALSE}),(17\\mapsto\\mathit{FALSE}),(18\\mapsto\\mathit{FALSE}),(19\\mapsto\\mathit{FALSE}),(20\\mapsto\\mathit{TRUE}),(21\\mapsto\\mathit{FALSE}),(22\\mapsto\\mathit{FALSE}),(23\\mapsto\\mathit{FALSE}),(24\\mapsto\\mathit{FALSE}),(25\\mapsto\\mathit{FALSE}),(26\\mapsto\\mathit{FALSE}),(27\\mapsto\\mathit{FALSE}),(28\\mapsto\\mathit{FALSE}),(29\\mapsto\\mathit{FALSE}),(30\\mapsto\\mathit{FALSE}),(31\\mapsto\\mathit{FALSE}),(32\\mapsto\\mathit{FALSE}),(33\\mapsto\\mathit{FALSE}),(34\\mapsto\\mathit{FALSE}),(35\\mapsto\\mathit{FALSE}),(36\\mapsto\\mathit{FALSE}),(37\\mapsto\\mathit{FALSE}),(38\\mapsto\\mathit{FALSE}),(39\\mapsto\\mathit{FALSE}),(40\\mapsto\\mathit{TRUE}),(41\\mapsto\\mathit{FALSE}),(42\\mapsto\\mathit{FALSE}),(43\\mapsto\\mathit{FALSE}),(44\\mapsto\\mathit{FALSE}),(45\\mapsto\\mathit{FALSE}),(46\\mapsto\\mathit{FALSE}),(47\\mapsto\\mathit{FALSE}),(48\\mapsto\\mathit{FALSE}),(49\\mapsto\\mathit{FALSE}),(50\\mapsto\\mathit{TRUE}),(51\\mapsto\\mathit{FALSE}),(52\\mapsto\\mathit{FALSE}),(53\\mapsto\\mathit{FALSE}),(54\\mapsto\\mathit{FALSE}),(55\\mapsto\\mathit{FALSE}),(56\\mapsto\\mathit{FALSE}),(57\\mapsto\\mathit{FALSE}),(58\\mapsto\\mathit{FALSE}),(59\\mapsto\\mathit{FALSE}),(60\\mapsto\\mathit{TRUE}),(61\\mapsto\\mathit{FALSE}),(62\\mapsto\\mathit{FALSE}),(63\\mapsto\\mathit{FALSE}),(64\\mapsto\\mathit{FALSE}),(65\\mapsto\\mathit{FALSE}),(66\\mapsto\\mathit{FALSE}),(67\\mapsto\\mathit{FALSE}),(68\\mapsto\\mathit{FALSE}),(69\\mapsto\\mathit{FALSE}),(70\\mapsto\\mathit{TRUE}),(71\\mapsto\\mathit{FALSE}),(72\\mapsto\\mathit{FALSE}),(73\\mapsto\\mathit{FALSE}),(74\\mapsto\\mathit{FALSE}),(75\\mapsto\\mathit{FALSE}),(76\\mapsto\\mathit{FALSE}),(77\\mapsto\\mathit{FALSE}),(78\\mapsto\\mathit{FALSE}),(79\\mapsto\\mathit{FALSE}),(80\\mapsto\\mathit{TRUE}),(81\\mapsto\\mathit{FALSE}),(82\\mapsto\\mathit{FALSE}),(83\\mapsto\\mathit{FALSE}),(84\\mapsto\\mathit{FALSE}),(85\\mapsto\\mathit{FALSE}),(86\\mapsto\\mathit{FALSE}),(87\\mapsto\\mathit{FALSE}),(88\\mapsto\\mathit{FALSE}),(89\\mapsto\\mathit{FALSE}),(90\\mapsto\\mathit{FALSE}),(91\\mapsto\\mathit{FALSE}),(92\\mapsto\\mathit{FALSE}),(93\\mapsto\\mathit{FALSE}),(94\\mapsto\\mathit{FALSE}),(95\\mapsto\\mathit{FALSE}),(96\\mapsto\\mathit{FALSE}),(97\\mapsto\\mathit{FALSE}),(98\\mapsto\\mathit{FALSE}),(99\\mapsto\\mathit{FALSE}),(100\\mapsto\\mathit{TRUE})\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tff = {(1↦TRUE),(2↦FALSE),(3↦TRUE),(4↦FALSE),(5↦FALSE),(6↦FALSE),(7↦FALSE),(8↦FALSE),(9↦TRUE),(10↦FALSE),(11↦FALSE),(12↦FALSE),(13↦FALSE),(14↦FALSE),(15↦FALSE),(16↦FALSE),(17↦FALSE),(18↦FALSE),(19↦FALSE),(20↦TRUE),(21↦FALSE),(22↦FALSE),(23↦FALSE),(24↦FALSE),(25↦FALSE),(26↦FALSE),(27↦FALSE),(28↦FALSE),(29↦FALSE),(30↦FALSE),(31↦FALSE),(32↦FALSE),(33↦FALSE),(34↦FALSE),(35↦FALSE),(36↦FALSE),(37↦FALSE),(38↦FALSE),(39↦FALSE),(40↦TRUE),(41↦FALSE),(42↦FALSE),(43↦FALSE),(44↦FALSE),(45↦FALSE),(46↦FALSE),(47↦FALSE),(48↦FALSE),(49↦FALSE),(50↦TRUE),(51↦FALSE),(52↦FALSE),(53↦FALSE),(54↦FALSE),(55↦FALSE),(56↦FALSE),(57↦FALSE),(58↦FALSE),(59↦FALSE),(60↦TRUE),(61↦FALSE),(62↦FALSE),(63↦FALSE),(64↦FALSE),(65↦FALSE),(66↦FALSE),(67↦FALSE),(68↦FALSE),(69↦FALSE),(70↦TRUE),(71↦FALSE),(72↦FALSE),(73↦FALSE),(74↦FALSE),(75↦FALSE),(76↦FALSE),(77↦FALSE),(78↦FALSE),(79↦FALSE),(80↦TRUE),(81↦FALSE),(82↦FALSE),(83↦FALSE),(84↦FALSE),(85↦FALSE),(86↦FALSE),(87↦FALSE),(88↦FALSE),(89↦FALSE),(90↦FALSE),(91↦FALSE),(92↦FALSE),(93↦FALSE),(94↦FALSE),(95↦FALSE),(96↦FALSE),(97↦FALSE),(98↦FALSE),(99↦FALSE),(100↦TRUE)}"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve sat ff:1..100-->BOOL & \n",
+ " card({y|y:1..100 & ff(y)=TRUE}) <=10 &\n",
+ " ff(1)=TRUE & ff(3)=TRUE & \n",
+ " !i.(i:1..10 => (ff(i)=FALSE => ff(i*10)=TRUE))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "7d045d11",
+ "metadata": {},
+ "source": [
+ "## Dominating Sets\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "id": "717c9961",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\def\\upto{\\mathbin{.\\mkern1mu.}}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{NODES} = (1 \\upto 24)$\n",
+ "* $\\mathit{edge} = \\{(1\\mapsto 2),(1\\mapsto 4),(2\\mapsto 3),(3\\mapsto 4),(3\\mapsto 5),(3\\mapsto 7),(4\\mapsto 7),(5\\mapsto 6),(5\\mapsto 9),(6\\mapsto 7),(6\\mapsto 8),(7\\mapsto 8),(8\\mapsto 10),(8\\mapsto 13),(9\\mapsto 10),(9\\mapsto 11),(9\\mapsto 12),(11\\mapsto 12),(11\\mapsto 14),(12\\mapsto 13),(13\\mapsto 16),(14\\mapsto 15),(14\\mapsto 17),(15\\mapsto 16),(15\\mapsto 17),(15\\mapsto 18),(15\\mapsto 21),(16\\mapsto 18),(16\\mapsto 19),(17\\mapsto 19),(18\\mapsto 19),(18\\mapsto 20),(18\\mapsto 21),(19\\mapsto 20),(19\\mapsto 21),(20\\mapsto 21),(20\\mapsto 22),(21\\mapsto 22),(21\\mapsto 23),(21\\mapsto 24),(22\\mapsto 23),(23\\mapsto 24)\\}$\n",
+ "* $\\mathit{ice} = \\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{TRUE}),(4\\mapsto\\mathit{TRUE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{TRUE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{FALSE}),(11\\mapsto\\mathit{TRUE}),(12\\mapsto\\mathit{FALSE}),(13\\mapsto\\mathit{FALSE}),(14\\mapsto\\mathit{FALSE}),(15\\mapsto\\mathit{FALSE}),(16\\mapsto\\mathit{FALSE}),(17\\mapsto\\mathit{FALSE}),(18\\mapsto\\mathit{FALSE}),(19\\mapsto\\mathit{TRUE}),(20\\mapsto\\mathit{FALSE}),(21\\mapsto\\mathit{TRUE}),(22\\mapsto\\mathit{FALSE}),(23\\mapsto\\mathit{FALSE}),(24\\mapsto\\mathit{FALSE})\\}$\n",
+ "* $\\mathit{neighbours} = \\{(1\\mapsto\\{2,4\\}),(2\\mapsto\\{1,3\\}),(3\\mapsto\\{2,4,5,7\\}),(4\\mapsto\\{1,3,7\\}),(5\\mapsto\\{3,6,9\\}),(6\\mapsto\\{5,7,8\\}),(7\\mapsto\\{3,4,6,8\\}),(8\\mapsto\\{6,7,10,13\\}),(9\\mapsto\\{5,10,11,12\\}),(10\\mapsto\\{8,9\\}),(11\\mapsto\\{9,12,14\\}),(12\\mapsto\\{9,11,13\\}),(13\\mapsto\\{8,12,16\\}),(14\\mapsto\\{11,15,17\\}),(15\\mapsto\\{14,16,17,18,21\\}),(16\\mapsto\\{13,15,18,19\\}),(17\\mapsto\\{14,15,19\\}),(18\\mapsto\\{15,16,19,20,21\\}),(19\\mapsto\\{16,17,18,20,21\\}),(20\\mapsto\\{18,19,21,22\\}),(21\\mapsto\\{15,18,19,20,22,23,24\\}),(22\\mapsto\\{20,21,23\\}),(23\\mapsto\\{21,22,24\\}),(24\\mapsto\\{21,23\\})\\}$\n",
+ "* $\\mathit{bi\\_edge} = \\{(1\\mapsto 2),(1\\mapsto 4),(2\\mapsto 1),(2\\mapsto 3),(3\\mapsto 2),(3\\mapsto 4),(3\\mapsto 5),(3\\mapsto 7),(4\\mapsto 1),(4\\mapsto 3),(4\\mapsto 7),(5\\mapsto 3),(5\\mapsto 6),(5\\mapsto 9),(6\\mapsto 5),(6\\mapsto 7),(6\\mapsto 8),(7\\mapsto 3),(7\\mapsto 4),(7\\mapsto 6),(7\\mapsto 8),(8\\mapsto 6),(8\\mapsto 7),(8\\mapsto 10),(8\\mapsto 13),(9\\mapsto 5),(9\\mapsto 10),(9\\mapsto 11),(9\\mapsto 12),(10\\mapsto 8),(10\\mapsto 9),(11\\mapsto 9),(11\\mapsto 12),(11\\mapsto 14),(12\\mapsto 9),(12\\mapsto 11),(12\\mapsto 13),(13\\mapsto 8),(13\\mapsto 12),(13\\mapsto 16),(14\\mapsto 11),(14\\mapsto 15),(14\\mapsto 17),(15\\mapsto 14),(15\\mapsto 16),(15\\mapsto 17),(15\\mapsto 18),(15\\mapsto 21),(16\\mapsto 13),(16\\mapsto 15),(16\\mapsto 18),(16\\mapsto 19),(17\\mapsto 14),(17\\mapsto 15),(17\\mapsto 19),(18\\mapsto 15),(18\\mapsto 16),(18\\mapsto 19),(18\\mapsto 20),(18\\mapsto 21),(19\\mapsto 16),(19\\mapsto 17),(19\\mapsto 18),(19\\mapsto 20),(19\\mapsto 21),(20\\mapsto 18),(20\\mapsto 19),(20\\mapsto 21),(20\\mapsto 22),(21\\mapsto 15),(21\\mapsto 18),(21\\mapsto 19),(21\\mapsto 20),(21\\mapsto 22),(21\\mapsto 23),(21\\mapsto 24),(22\\mapsto 20),(22\\mapsto 21),(22\\mapsto 23),(23\\mapsto 21),(23\\mapsto 22),(23\\mapsto 24),(24\\mapsto 21),(24\\mapsto 23)\\}$\n",
+ "* $\\mathit{N} = 24$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tNODES = (1 ‥ 24)\n",
+ "\tedge = {(1↦2),(1↦4),(2↦3),(3↦4),(3↦5),(3↦7),(4↦7),(5↦6),(5↦9),(6↦7),(6↦8),(7↦8),(8↦10),(8↦13),(9↦10),(9↦11),(9↦12),(11↦12),(11↦14),(12↦13),(13↦16),(14↦15),(14↦17),(15↦16),(15↦17),(15↦18),(15↦21),(16↦18),(16↦19),(17↦19),(18↦19),(18↦20),(18↦21),(19↦20),(19↦21),(20↦21),(20↦22),(21↦22),(21↦23),(21↦24),(22↦23),(23↦24)}\n",
+ "\tice = {(1↦FALSE),(2↦FALSE),(3↦TRUE),(4↦TRUE),(5↦FALSE),(6↦FALSE),(7↦FALSE),(8↦TRUE),(9↦FALSE),(10↦FALSE),(11↦TRUE),(12↦FALSE),(13↦FALSE),(14↦FALSE),(15↦FALSE),(16↦FALSE),(17↦FALSE),(18↦FALSE),(19↦TRUE),(20↦FALSE),(21↦TRUE),(22↦FALSE),(23↦FALSE),(24↦FALSE)}\n",
+ "\tneighbours = {(1↦{2,4}),(2↦{1,3}),(3↦{2,4,5,7}),(4↦{1,3,7}),(5↦{3,6,9}),(6↦{5,7,8}),(7↦{3,4,6,8}),(8↦{6,7,10,13}),(9↦{5,10,11,12}),(10↦{8,9}),(11↦{9,12,14}),(12↦{9,11,13}),(13↦{8,12,16}),(14↦{11,15,17}),(15↦{14,16,17,18,21}),(16↦{13,15,18,19}),(17↦{14,15,19}),(18↦{15,16,19,20,21}),(19↦{16,17,18,20,21}),(20↦{18,19,21,22}),(21↦{15,18,19,20,22,23,24}),(22↦{20,21,23}),(23↦{21,22,24}),(24↦{21,23})}\n",
+ "\tbi_edge = {(1↦2),(1↦4),(2↦1),(2↦3),(3↦2),(3↦4),(3↦5),(3↦7),(4↦1),(4↦3),(4↦7),(5↦3),(5↦6),(5↦9),(6↦5),(6↦7),(6↦8),(7↦3),(7↦4),(7↦6),(7↦8),(8↦6),(8↦7),(8↦10),(8↦13),(9↦5),(9↦10),(9↦11),(9↦12),(10↦8),(10↦9),(11↦9),(11↦12),(11↦14),(12↦9),(12↦11),(12↦13),(13↦8),(13↦12),(13↦16),(14↦11),(14↦15),(14↦17),(15↦14),(15↦16),(15↦17),(15↦18),(15↦21),(16↦13),(16↦15),(16↦18),(16↦19),(17↦14),(17↦15),(17↦19),(18↦15),(18↦16),(18↦19),(18↦20),(18↦21),(19↦16),(19↦17),(19↦18),(19↦20),(19↦21),(20↦18),(20↦19),(20↦21),(20↦22),(21↦15),(21↦18),(21↦19),(21↦20),(21↦22),(21↦23),(21↦24),(22↦20),(22↦21),(22↦23),(23↦21),(23↦22),(23↦24),(24↦21),(24↦23)}\n",
+ "\tN = 24"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve sat N = 24\n",
+ " &\n",
+ " NODES = 1..N\n",
+ " &\n",
+ " edge: NODES <-> NODES\n",
+ " &\n",
+ " edge = { 1|->2, 1|->4,\n",
+ " 2|->3,\n",
+ " 3|->4, 3|->5, 3|->7,\n",
+ " 4|->7,\n",
+ " 5|->6, 5|->9,\n",
+ " 6|->7, 6|->8,\n",
+ " 7|->8,\n",
+ " 8|->10, 8|->13,\n",
+ " 9|->10, 9|->11, 9|->12,\n",
+ " 11|->12, 11|->14,\n",
+ " 12|->13,\n",
+ " 13|->16,\n",
+ " 14|->15, 14|->17,\n",
+ " 15|->16, 15|->17, 15|->18, 15|->21,\n",
+ " 16|->18, 16|->19,\n",
+ " 17|->19,\n",
+ " 18|->19, 18|->20, 18|->21,\n",
+ " 19|->20, 19|->21,\n",
+ " 20|->21, 20|->22,\n",
+ " 21|->22, 21|->23, 21|->24,\n",
+ " 22|->23, 21|->24,\n",
+ " 23|->24} &\n",
+ " bi_edge = (edge \\/ edge~) &\n",
+ " ice : NODES--> BOOL &\n",
+ " neighbours = %x.(x:NODES|bi_edge[{x}]) &\n",
+ " !x.(x:NODES =>\n",
+ " (ice(x)=TRUE\n",
+ " or\n",
+ " #neighbour.(neighbour: neighbours(x) & ice(neighbour)=TRUE)\n",
+ " )\n",
+ " )\n",
+ "\n",
+ "// & vans = card(ice~[{TRUE}])\n",
+ "// & vans <7 /* minimal solution requires 6 vans */\n",
+ " \n",
+ " & card({n|n:NODES & ice(n)=TRUE}) < 7"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "55688278",
+ "metadata": {},
+ "source": [
+ "## N-Queens"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "id": "316f98aa",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\def\\upto{\\mathbin{.\\mkern1mu.}}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{DOM} = (1 \\upto 10)$\n",
+ "* $\\mathit{board} = \\{(1\\mapsto\\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{TRUE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{FALSE})\\}),(2\\mapsto\\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{TRUE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{FALSE})\\}),(3\\mapsto\\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{TRUE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{FALSE})\\}),(4\\mapsto\\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{TRUE}),(10\\mapsto\\mathit{FALSE})\\}),(5\\mapsto\\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{TRUE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{FALSE})\\}),(6\\mapsto\\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{TRUE})\\}),(7\\mapsto\\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{TRUE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{FALSE})\\}),(8\\mapsto\\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{TRUE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{FALSE})\\}),(9\\mapsto\\{(1\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{TRUE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{FALSE})\\}),(10\\mapsto\\{(1\\mapsto\\mathit{TRUE}),(2\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{FALSE})\\})\\}$\n",
+ "* $\\mathit{n} = 10$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tDOM = (1 ‥ 10)\n",
+ "\tboard = {(1↦{(1↦FALSE),(2↦FALSE),(3↦FALSE),(4↦FALSE),(5↦FALSE),(6↦FALSE),(7↦TRUE),(8↦FALSE),(9↦FALSE),(10↦FALSE)}),(2↦{(1↦FALSE),(2↦FALSE),(3↦FALSE),(4↦TRUE),(5↦FALSE),(6↦FALSE),(7↦FALSE),(8↦FALSE),(9↦FALSE),(10↦FALSE)}),(3↦{(1↦FALSE),(2↦TRUE),(3↦FALSE),(4↦FALSE),(5↦FALSE),(6↦FALSE),(7↦FALSE),(8↦FALSE),(9↦FALSE),(10↦FALSE)}),(4↦{(1↦FALSE),(2↦FALSE),(3↦FALSE),(4↦FALSE),(5↦FALSE),(6↦FALSE),(7↦FALSE),(8↦FALSE),(9↦TRUE),(10↦FALSE)}),(5↦{(1↦FALSE),(2↦FALSE),(3↦FALSE),(4↦FALSE),(5↦TRUE),(6↦FALSE),(7↦FALSE),(8↦FALSE),(9↦FALSE),(10↦FALSE)}),(6↦{(1↦FALSE),(2↦FALSE),(3↦FALSE),(4↦FALSE),(5↦FALSE),(6↦FALSE),(7↦FALSE),(8↦FALSE),(9↦FALSE),(10↦TRUE)}),(7↦{(1↦FALSE),(2↦FALSE),(3↦FALSE),(4↦FALSE),(5↦FALSE),(6↦FALSE),(7↦FALSE),(8↦TRUE),(9↦FALSE),(10↦FALSE)}),(8↦{(1↦FALSE),(2↦FALSE),(3↦FALSE),(4↦FALSE),(5↦FALSE),(6↦TRUE),(7↦FALSE),(8↦FALSE),(9↦FALSE),(10↦FALSE)}),(9↦{(1↦FALSE),(2↦FALSE),(3↦TRUE),(4↦FALSE),(5↦FALSE),(6↦FALSE),(7↦FALSE),(8↦FALSE),(9↦FALSE),(10↦FALSE)}),(10↦{(1↦TRUE),(2↦FALSE),(3↦FALSE),(4↦FALSE),(5↦FALSE),(6↦FALSE),(7↦FALSE),(8↦FALSE),(9↦FALSE),(10↦FALSE)})}\n",
+ "\tn = 10"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve sat\n",
+ " n = 10 & DOM = 1..n &\n",
+ " board : (1..n) --> ( (1..n) --> BOOL ) /* board contains coordinates of all queens */\n",
+ " &\n",
+ " !i.(i:1..n =>\n",
+ " card({j|j:(1..n) & board(i)(j)=TRUE}) = 1)\n",
+ " /*@desc \"One queen per row\" */\n",
+ " &\n",
+ " // version v2: we rewrite and inline boardfalse by hand below\n",
+ " !(p).(p:DOM =>\n",
+ " !q.(q:DOM =>\n",
+ " ( board(p)(q)=TRUE\n",
+ " => !i.((i /= 0 & i:-n..n) =>\n",
+ " (p+i:DOM => board(p+i)(q)=FALSE) &\n",
+ " (q+i:DOM => board(p)(q+i)=FALSE) &\n",
+ " (p+i:DOM & q+i:DOM => board(p+i)(q+i)=FALSE) &\n",
+ " (p+i:DOM & q-i:DOM => board(p+i)(q-i)=FALSE)\n",
+ " )\n",
+ " )\n",
+ " )\n",
+ " )"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "e1efb425",
+ "metadata": {},
+ "source": [
+ "## Bounded Model Checking aka Cook's Theorem"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 41,
+ "id": "037efa10",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: TuringMachine_Cook_SAT_SATSOLVER"
+ ]
+ },
+ "execution_count": 41,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE TuringMachine_Cook_SAT_SATSOLVER\n",
+ "// v2: rewritten quantifiers for Z3; v3: assume det. delta\n",
+ "// SATSOLVER: uses SATSOLVER external function\n",
+ "/* B model of a 1-band Turing machine */\n",
+ "/* and a translation of the SAT encoding of Cook's theorem */\n",
+ "/* by Michael Leuschel, 2023 */\n",
+ "/* The turing machine implements the +1 function on binary numbers */\n",
+ "/* See Slide 2 from folien-kapitel-7.pdf (Info 4) */\n",
+ "SETS\n",
+ " Alphabet={O,I,`BLANK`};\n",
+ " States = {z0,z1,z2,ze};\n",
+ " Direction = {L,R,N}\n",
+ "DEFINITIONS\n",
+ " pn == 12; // we simulate Turing machine from time 0 to time pn\n",
+ " last_time == pn+3; //\n",
+ " TIME == 0..last_time;\n",
+ " TIME1 == 0..(last_time-1);\n",
+ " POS == -pn .. pn;\n",
+ " offset == {L↦-1, R↦1, N↦0}\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 42,
+ "id": "effd2f47",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{head} = \\{(0\\mapsto-12\\mapsto\\mathit{FALSE}),(0\\mapsto-11\\mapsto\\mathit{FALSE}),(0\\mapsto-10\\mapsto\\mathit{FALSE}),(0\\mapsto-9\\mapsto\\mathit{FALSE}),(0\\mapsto-8\\mapsto\\mathit{FALSE}),(0\\mapsto-7\\mapsto\\mathit{FALSE}),(0\\mapsto-6\\mapsto\\mathit{FALSE}),(0\\mapsto-5\\mapsto\\mathit{FALSE}),(0\\mapsto-4\\mapsto\\mathit{FALSE}),(0\\mapsto-3\\mapsto\\mathit{FALSE}),(0\\mapsto-2\\mapsto\\mathit{FALSE}),(0\\mapsto-1\\mapsto\\mathit{FALSE}),(0\\mapsto 0\\mapsto\\mathit{TRUE}),(0\\mapsto 1\\mapsto\\mathit{FALSE}),(0\\mapsto 2\\mapsto\\mathit{FALSE}),(0\\mapsto 3\\mapsto\\mathit{FALSE}),(0\\mapsto 4\\mapsto\\mathit{FALSE}),(0\\mapsto 5\\mapsto\\mathit{FALSE}),(0\\mapsto 6\\mapsto\\mathit{FALSE}),(0\\mapsto 7\\mapsto\\mathit{FALSE}),(0\\mapsto 8\\mapsto\\mathit{FALSE}),(0\\mapsto 9\\mapsto\\mathit{FALSE}),(0\\mapsto 10\\mapsto\\mathit{FALSE}),(0\\mapsto 11\\mapsto\\mathit{FALSE}),(0\\mapsto 12\\mapsto\\mathit{FALSE}),(1\\mapsto-12\\mapsto\\mathit{FALSE}),(1\\mapsto-11\\mapsto\\mathit{FALSE}),(1\\mapsto-10\\mapsto\\mathit{FALSE}),(1\\mapsto-9\\mapsto\\mathit{FALSE}),(1\\mapsto-8\\mapsto\\mathit{FALSE}),(1\\mapsto-7\\mapsto\\mathit{FALSE}),(1\\mapsto-6\\mapsto\\mathit{FALSE}),(1\\mapsto-5\\mapsto\\mathit{FALSE}),(1\\mapsto-4\\mapsto\\mathit{FALSE}),(1\\mapsto-3\\mapsto\\mathit{FALSE}),(1\\mapsto-2\\mapsto\\mathit{FALSE}),(1\\mapsto-1\\mapsto\\mathit{FALSE}),(1\\mapsto 0\\mapsto\\mathit{FALSE}),(1\\mapsto 1\\mapsto\\mathit{TRUE}),(1\\mapsto 2\\mapsto\\mathit{FALSE}),(1\\mapsto 3\\mapsto\\mathit{FALSE}),(1\\mapsto 4\\mapsto\\mathit{FALSE}),(1\\mapsto 5\\mapsto\\mathit{FALSE}),(1\\mapsto 6\\mapsto\\mathit{FALSE}),(1\\mapsto 7\\mapsto\\mathit{FALSE}),(1\\mapsto 8\\mapsto\\mathit{FALSE}),(1\\mapsto 9\\mapsto\\mathit{FALSE}),(1\\mapsto 10\\mapsto\\mathit{FALSE}),(1\\mapsto 11\\mapsto\\mathit{FALSE}),(1\\mapsto 12\\mapsto\\mathit{FALSE}),(2\\mapsto-12\\mapsto\\mathit{FALSE}),(2\\mapsto-11\\mapsto\\mathit{FALSE}),(2\\mapsto-10\\mapsto\\mathit{FALSE}),(2\\mapsto-9\\mapsto\\mathit{FALSE}),(2\\mapsto-8\\mapsto\\mathit{FALSE}),(2\\mapsto-7\\mapsto\\mathit{FALSE}),(2\\mapsto-6\\mapsto\\mathit{FALSE}),(2\\mapsto-5\\mapsto\\mathit{FALSE}),(2\\mapsto-4\\mapsto\\mathit{FALSE}),(2\\mapsto-3\\mapsto\\mathit{FALSE}),(2\\mapsto-2\\mapsto\\mathit{FALSE}),(2\\mapsto-1\\mapsto\\mathit{FALSE}),(2\\mapsto 0\\mapsto\\mathit{FALSE}),(2\\mapsto 1\\mapsto\\mathit{FALSE}),(2\\mapsto 2\\mapsto\\mathit{TRUE}),(2\\mapsto 3\\mapsto\\mathit{FALSE}),(2\\mapsto 4\\mapsto\\mathit{FALSE}),(2\\mapsto 5\\mapsto\\mathit{FALSE}),(2\\mapsto 6\\mapsto\\mathit{FALSE}),(2\\mapsto 7\\mapsto\\mathit{FALSE}),(2\\mapsto 8\\mapsto\\mathit{FALSE}),(2\\mapsto 9\\mapsto\\mathit{FALSE}),(2\\mapsto 10\\mapsto\\mathit{FALSE}),(2\\mapsto 11\\mapsto\\mathit{FALSE}),(2\\mapsto 12\\mapsto\\mathit{FALSE}),(3\\mapsto-12\\mapsto\\mathit{FALSE}),(3\\mapsto-11\\mapsto\\mathit{FALSE}),(3\\mapsto-10\\mapsto\\mathit{FALSE}),(3\\mapsto-9\\mapsto\\mathit{FALSE}),(3\\mapsto-8\\mapsto\\mathit{FALSE}),(3\\mapsto-7\\mapsto\\mathit{FALSE}),(3\\mapsto-6\\mapsto\\mathit{FALSE}),(3\\mapsto-5\\mapsto\\mathit{FALSE}),(3\\mapsto-4\\mapsto\\mathit{FALSE}),(3\\mapsto-3\\mapsto\\mathit{FALSE}),(3\\mapsto-2\\mapsto\\mathit{FALSE}),(3\\mapsto-1\\mapsto\\mathit{FALSE}),(3\\mapsto 0\\mapsto\\mathit{FALSE}),(3\\mapsto 1\\mapsto\\mathit{FALSE}),(3\\mapsto 2\\mapsto\\mathit{FALSE}),(3\\mapsto 3\\mapsto\\mathit{TRUE}),(3\\mapsto 4\\mapsto\\mathit{FALSE}),(3\\mapsto 5\\mapsto\\mathit{FALSE}),(3\\mapsto 6\\mapsto\\mathit{FALSE}),(3\\mapsto 7\\mapsto\\mathit{FALSE}),(3\\mapsto 8\\mapsto\\mathit{FALSE}),(3\\mapsto 9\\mapsto\\mathit{FALSE}),(3\\mapsto 10\\mapsto\\mathit{FALSE}),(3\\mapsto 11\\mapsto\\mathit{FALSE}),(3\\mapsto 12\\mapsto\\mathit{FALSE}),\\ldots\\}$\n",
+ "* $\\mathit{tape} = \\{(0\\mapsto-12\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-12\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-12\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-11\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-11\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-11\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-10\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-10\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-10\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-9\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-9\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-9\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-8\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-8\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-8\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-7\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-7\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-7\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-6\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-6\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-6\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-5\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-5\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-5\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-4\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-4\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-4\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-3\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-3\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-3\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-2\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-2\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-2\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto-1\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto-1\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto-1\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 0\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 0\\mapsto\\mathit{I}\\mapsto\\mathit{TRUE}),(0\\mapsto 0\\mapsto\\mathit{BLANK}\\mapsto\\mathit{FALSE}),(0\\mapsto 1\\mapsto\\mathit{O}\\mapsto\\mathit{TRUE}),(0\\mapsto 1\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 1\\mapsto\\mathit{BLANK}\\mapsto\\mathit{FALSE}),(0\\mapsto 2\\mapsto\\mathit{O}\\mapsto\\mathit{TRUE}),(0\\mapsto 2\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 2\\mapsto\\mathit{BLANK}\\mapsto\\mathit{FALSE}),(0\\mapsto 3\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 3\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 3\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 4\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 4\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 4\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 5\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 5\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 5\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 6\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 6\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 6\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 7\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 7\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 7\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 8\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 8\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 8\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 9\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 9\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 9\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 10\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 10\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 10\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 11\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 11\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 11\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(0\\mapsto 12\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(0\\mapsto 12\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(0\\mapsto 12\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(1\\mapsto-12\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(1\\mapsto-12\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(1\\mapsto-12\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(1\\mapsto-11\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(1\\mapsto-11\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(1\\mapsto-11\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(1\\mapsto-10\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(1\\mapsto-10\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(1\\mapsto-10\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(1\\mapsto-9\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(1\\mapsto-9\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(1\\mapsto-9\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(1\\mapsto-8\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(1\\mapsto-8\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(1\\mapsto-8\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(1\\mapsto-7\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(1\\mapsto-7\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(1\\mapsto-7\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(1\\mapsto-6\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(1\\mapsto-6\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(1\\mapsto-6\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(1\\mapsto-5\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),(1\\mapsto-5\\mapsto\\mathit{I}\\mapsto\\mathit{FALSE}),(1\\mapsto-5\\mapsto\\mathit{BLANK}\\mapsto\\mathit{TRUE}),(1\\mapsto-4\\mapsto\\mathit{O}\\mapsto\\mathit{FALSE}),\\ldots\\}$\n",
+ "* $\\mathit{δ} = \\{(\\mathit{z0}\\mapsto\\mathit{O}\\mapsto(\\mathit{z0}\\mapsto\\mathit{O}\\mapsto\\mathit{R})),(\\mathit{z0}\\mapsto\\mathit{I}\\mapsto(\\mathit{z0}\\mapsto\\mathit{I}\\mapsto\\mathit{R})),(\\mathit{z0}\\mapsto\\mathit{BLANK}\\mapsto(\\mathit{z1}\\mapsto\\mathit{BLANK}\\mapsto\\mathit{L})),(\\mathit{z1}\\mapsto\\mathit{O}\\mapsto(\\mathit{z2}\\mapsto\\mathit{I}\\mapsto\\mathit{L})),(\\mathit{z1}\\mapsto\\mathit{I}\\mapsto(\\mathit{z1}\\mapsto\\mathit{O}\\mapsto\\mathit{L})),(\\mathit{z1}\\mapsto\\mathit{BLANK}\\mapsto(\\mathit{ze}\\mapsto\\mathit{I}\\mapsto\\mathit{N})),(\\mathit{z2}\\mapsto\\mathit{O}\\mapsto(\\mathit{z2}\\mapsto\\mathit{O}\\mapsto\\mathit{L})),(\\mathit{z2}\\mapsto\\mathit{I}\\mapsto(\\mathit{z2}\\mapsto\\mathit{I}\\mapsto\\mathit{L})),(\\mathit{z2}\\mapsto\\mathit{BLANK}\\mapsto(\\mathit{ze}\\mapsto\\mathit{BLANK}\\mapsto\\mathit{R})),(\\mathit{ze}\\mapsto\\mathit{O}\\mapsto(\\mathit{ze}\\mapsto\\mathit{O}\\mapsto\\mathit{N})),(\\mathit{ze}\\mapsto\\mathit{I}\\mapsto(\\mathit{ze}\\mapsto\\mathit{I}\\mapsto\\mathit{N})),(\\mathit{ze}\\mapsto\\mathit{BLANK}\\mapsto(\\mathit{ze}\\mapsto\\mathit{BLANK}\\mapsto\\mathit{N}))\\}$\n",
+ "* $\\mathit{state} = \\{(0\\mapsto\\mathit{z0}\\mapsto\\mathit{TRUE}),(0\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(0\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(0\\mapsto\\mathit{ze}\\mapsto\\mathit{FALSE}),(1\\mapsto\\mathit{z0}\\mapsto\\mathit{TRUE}),(1\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(1\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(1\\mapsto\\mathit{ze}\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{z0}\\mapsto\\mathit{TRUE}),(2\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(2\\mapsto\\mathit{ze}\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{z0}\\mapsto\\mathit{TRUE}),(3\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(3\\mapsto\\mathit{ze}\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{z1}\\mapsto\\mathit{TRUE}),(4\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(4\\mapsto\\mathit{ze}\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(5\\mapsto\\mathit{z2}\\mapsto\\mathit{TRUE}),(5\\mapsto\\mathit{ze}\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(6\\mapsto\\mathit{z2}\\mapsto\\mathit{TRUE}),(6\\mapsto\\mathit{ze}\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(7\\mapsto\\mathit{z2}\\mapsto\\mathit{TRUE}),(7\\mapsto\\mathit{ze}\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(8\\mapsto\\mathit{ze}\\mapsto\\mathit{TRUE}),(9\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(9\\mapsto\\mathit{ze}\\mapsto\\mathit{TRUE}),(10\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(10\\mapsto\\mathit{ze}\\mapsto\\mathit{TRUE}),(11\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(11\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(11\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(11\\mapsto\\mathit{ze}\\mapsto\\mathit{TRUE}),(12\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(12\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(12\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(12\\mapsto\\mathit{ze}\\mapsto\\mathit{TRUE}),(13\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(13\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(13\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(13\\mapsto\\mathit{ze}\\mapsto\\mathit{TRUE}),(14\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(14\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(14\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(14\\mapsto\\mathit{ze}\\mapsto\\mathit{TRUE}),(15\\mapsto\\mathit{z0}\\mapsto\\mathit{FALSE}),(15\\mapsto\\mathit{z1}\\mapsto\\mathit{FALSE}),(15\\mapsto\\mathit{z2}\\mapsto\\mathit{FALSE}),(15\\mapsto\\mathit{ze}\\mapsto\\mathit{TRUE})\\}$\n",
+ "* $\\mathit{Final} = \\{\\mathit{ze}\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\thead = {(0↦−12↦FALSE),(0↦−11↦FALSE),(0↦−10↦FALSE),(0↦−9↦FALSE),(0↦−8↦FALSE),(0↦−7↦FALSE),(0↦−6↦FALSE),(0↦−5↦FALSE),(0↦−4↦FALSE),(0↦−3↦FALSE),(0↦−2↦FALSE),(0↦−1↦FALSE),(0↦0↦TRUE),(0↦1↦FALSE),(0↦2↦FALSE),(0↦3↦FALSE),(0↦4↦FALSE),(0↦5↦FALSE),(0↦6↦FALSE),(0↦7↦FALSE),(0↦8↦FALSE),(0↦9↦FALSE),(0↦10↦FALSE),(0↦11↦FALSE),(0↦12↦FALSE),(1↦−12↦FALSE),(1↦−11↦FALSE),(1↦−10↦FALSE),(1↦−9↦FALSE),(1↦−8↦FALSE),(1↦−7↦FALSE),(1↦−6↦FALSE),(1↦−5↦FALSE),(1↦−4↦FALSE),(1↦−3↦FALSE),(1↦−2↦FALSE),(1↦−1↦FALSE),(1↦0↦FALSE),(1↦1↦TRUE),(1↦2↦FALSE),(1↦3↦FALSE),(1↦4↦FALSE),(1↦5↦FALSE),(1↦6↦FALSE),(1↦7↦FALSE),(1↦8↦FALSE),(1↦9↦FALSE),(1↦10↦FALSE),(1↦11↦FALSE),(1↦12↦FALSE),(2↦−12↦FALSE),(2↦−11↦FALSE),(2↦−10↦FALSE),(2↦−9↦FALSE),(2↦−8↦FALSE),(2↦−7↦FALSE),(2↦−6↦FALSE),(2↦−5↦FALSE),(2↦−4↦FALSE),(2↦−3↦FALSE),(2↦−2↦FALSE),(2↦−1↦FALSE),(2↦0↦FALSE),(2↦1↦FALSE),(2↦2↦TRUE),(2↦3↦FALSE),(2↦4↦FALSE),(2↦5↦FALSE),(2↦6↦FALSE),(2↦7↦FALSE),(2↦8↦FALSE),(2↦9↦FALSE),(2↦10↦FALSE),(2↦11↦FALSE),(2↦12↦FALSE),(3↦−12↦FALSE),(3↦−11↦FALSE),(3↦−10↦FALSE),(3↦−9↦FALSE),(3↦−8↦FALSE),(3↦−7↦FALSE),(3↦−6↦FALSE),(3↦−5↦FALSE),(3↦−4↦FALSE),(3↦−3↦FALSE),(3↦−2↦FALSE),(3↦−1↦FALSE),(3↦0↦FALSE),(3↦1↦FALSE),(3↦2↦FALSE),(3↦3↦TRUE),(3↦4↦FALSE),(3↦5↦FALSE),(3↦6↦FALSE),(3↦7↦FALSE),(3↦8↦FALSE),(3↦9↦FALSE),(3↦10↦FALSE),(3↦11↦FALSE),(3↦12↦FALSE),…}\n",
+ "\ttape = {(0↦−12↦O↦FALSE),(0↦−12↦I↦FALSE),(0↦−12↦BLANK↦TRUE),(0↦−11↦O↦FALSE),(0↦−11↦I↦FALSE),(0↦−11↦BLANK↦TRUE),(0↦−10↦O↦FALSE),(0↦−10↦I↦FALSE),(0↦−10↦BLANK↦TRUE),(0↦−9↦O↦FALSE),(0↦−9↦I↦FALSE),(0↦−9↦BLANK↦TRUE),(0↦−8↦O↦FALSE),(0↦−8↦I↦FALSE),(0↦−8↦BLANK↦TRUE),(0↦−7↦O↦FALSE),(0↦−7↦I↦FALSE),(0↦−7↦BLANK↦TRUE),(0↦−6↦O↦FALSE),(0↦−6↦I↦FALSE),(0↦−6↦BLANK↦TRUE),(0↦−5↦O↦FALSE),(0↦−5↦I↦FALSE),(0↦−5↦BLANK↦TRUE),(0↦−4↦O↦FALSE),(0↦−4↦I↦FALSE),(0↦−4↦BLANK↦TRUE),(0↦−3↦O↦FALSE),(0↦−3↦I↦FALSE),(0↦−3↦BLANK↦TRUE),(0↦−2↦O↦FALSE),(0↦−2↦I↦FALSE),(0↦−2↦BLANK↦TRUE),(0↦−1↦O↦FALSE),(0↦−1↦I↦FALSE),(0↦−1↦BLANK↦TRUE),(0↦0↦O↦FALSE),(0↦0↦I↦TRUE),(0↦0↦BLANK↦FALSE),(0↦1↦O↦TRUE),(0↦1↦I↦FALSE),(0↦1↦BLANK↦FALSE),(0↦2↦O↦TRUE),(0↦2↦I↦FALSE),(0↦2↦BLANK↦FALSE),(0↦3↦O↦FALSE),(0↦3↦I↦FALSE),(0↦3↦BLANK↦TRUE),(0↦4↦O↦FALSE),(0↦4↦I↦FALSE),(0↦4↦BLANK↦TRUE),(0↦5↦O↦FALSE),(0↦5↦I↦FALSE),(0↦5↦BLANK↦TRUE),(0↦6↦O↦FALSE),(0↦6↦I↦FALSE),(0↦6↦BLANK↦TRUE),(0↦7↦O↦FALSE),(0↦7↦I↦FALSE),(0↦7↦BLANK↦TRUE),(0↦8↦O↦FALSE),(0↦8↦I↦FALSE),(0↦8↦BLANK↦TRUE),(0↦9↦O↦FALSE),(0↦9↦I↦FALSE),(0↦9↦BLANK↦TRUE),(0↦10↦O↦FALSE),(0↦10↦I↦FALSE),(0↦10↦BLANK↦TRUE),(0↦11↦O↦FALSE),(0↦11↦I↦FALSE),(0↦11↦BLANK↦TRUE),(0↦12↦O↦FALSE),(0↦12↦I↦FALSE),(0↦12↦BLANK↦TRUE),(1↦−12↦O↦FALSE),(1↦−12↦I↦FALSE),(1↦−12↦BLANK↦TRUE),(1↦−11↦O↦FALSE),(1↦−11↦I↦FALSE),(1↦−11↦BLANK↦TRUE),(1↦−10↦O↦FALSE),(1↦−10↦I↦FALSE),(1↦−10↦BLANK↦TRUE),(1↦−9↦O↦FALSE),(1↦−9↦I↦FALSE),(1↦−9↦BLANK↦TRUE),(1↦−8↦O↦FALSE),(1↦−8↦I↦FALSE),(1↦−8↦BLANK↦TRUE),(1↦−7↦O↦FALSE),(1↦−7↦I↦FALSE),(1↦−7↦BLANK↦TRUE),(1↦−6↦O↦FALSE),(1↦−6↦I↦FALSE),(1↦−6↦BLANK↦TRUE),(1↦−5↦O↦FALSE),(1↦−5↦I↦FALSE),(1↦−5↦BLANK↦TRUE),(1↦−4↦O↦FALSE),…}\n",
+ "\tδ = {(z0↦O↦(z0↦O↦R)),(z0↦I↦(z0↦I↦R)),(z0↦BLANK↦(z1↦BLANK↦L)),(z1↦O↦(z2↦I↦L)),(z1↦I↦(z1↦O↦L)),(z1↦BLANK↦(ze↦I↦N)),(z2↦O↦(z2↦O↦L)),(z2↦I↦(z2↦I↦L)),(z2↦BLANK↦(ze↦BLANK↦R)),(ze↦O↦(ze↦O↦N)),(ze↦I↦(ze↦I↦N)),(ze↦BLANK↦(ze↦BLANK↦N))}\n",
+ "\tstate = {(0↦z0↦TRUE),(0↦z1↦FALSE),(0↦z2↦FALSE),(0↦ze↦FALSE),(1↦z0↦TRUE),(1↦z1↦FALSE),(1↦z2↦FALSE),(1↦ze↦FALSE),(2↦z0↦TRUE),(2↦z1↦FALSE),(2↦z2↦FALSE),(2↦ze↦FALSE),(3↦z0↦TRUE),(3↦z1↦FALSE),(3↦z2↦FALSE),(3↦ze↦FALSE),(4↦z0↦FALSE),(4↦z1↦TRUE),(4↦z2↦FALSE),(4↦ze↦FALSE),(5↦z0↦FALSE),(5↦z1↦FALSE),(5↦z2↦TRUE),(5↦ze↦FALSE),(6↦z0↦FALSE),(6↦z1↦FALSE),(6↦z2↦TRUE),(6↦ze↦FALSE),(7↦z0↦FALSE),(7↦z1↦FALSE),(7↦z2↦TRUE),(7↦ze↦FALSE),(8↦z0↦FALSE),(8↦z1↦FALSE),(8↦z2↦FALSE),(8↦ze↦TRUE),(9↦z0↦FALSE),(9↦z1↦FALSE),(9↦z2↦FALSE),(9↦ze↦TRUE),(10↦z0↦FALSE),(10↦z1↦FALSE),(10↦z2↦FALSE),(10↦ze↦TRUE),(11↦z0↦FALSE),(11↦z1↦FALSE),(11↦z2↦FALSE),(11↦ze↦TRUE),(12↦z0↦FALSE),(12↦z1↦FALSE),(12↦z2↦FALSE),(12↦ze↦TRUE),(13↦z0↦FALSE),(13↦z1↦FALSE),(13↦z2↦FALSE),(13↦ze↦TRUE),(14↦z0↦FALSE),(14↦z1↦FALSE),(14↦z2↦FALSE),(14↦ze↦TRUE),(15↦z0↦FALSE),(15↦z1↦FALSE),(15↦z2↦FALSE),(15↦ze↦TRUE)}\n",
+ "\tFinal = {ze}"
+ ]
+ },
+ "execution_count": 42,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve sat\n",
+ " Final ⊆ States ∧\n",
+ " δ ∈ (States * Alphabet) ↔ (States * Alphabet * Direction) ∧\n",
+ "\n",
+ " δ = { (z0,O) ↦ (z0,O,R), (z0,I) ↦ (z0,I,R), (z0,`BLANK`) ↦ (z1,`BLANK`,L),\n",
+ " (z1,O) ↦ (z2,I,L), (z1,I) ↦ (z1,O,L), (z1,`BLANK`) ↦ (ze,I,N),\n",
+ " (z2,O) ↦ (z2,O,L), (z2,I) ↦ (z2,I,L), (z2,`BLANK`) ↦ (ze,`BLANK`,R),\n",
+ " (ze,O) ↦ (ze,O,N), (ze,I) ↦ (ze,I,N), (ze,`BLANK`) ↦ (ze,`BLANK`,N) } ∧\n",
+ " Final = {ze} ∧\n",
+ "\n",
+ " // die logischen Aussagen:\n",
+ " state ∈ TIME * States → BOOL ∧\n",
+ " head ∈ TIME * POS → BOOL ∧\n",
+ " tape ∈ TIME * POS * Alphabet → BOOL ∧\n",
+ " \n",
+ " // Teilformel K\n",
+ " ∀t.(t∈TIME ⇒ card({s|state(t,s)=TRUE})=1) ∧\n",
+ " ∀t.(t∈TIME ⇒ card({p|p∈POS ∧ head(t,p)=TRUE})=1) ∧\n",
+ " ∀(t,p).(t∈TIME ∧ p∈POS ⇒ card({s|tape(t,p,s)=TRUE})=1)\n",
+ " \n",
+ " &\n",
+ " \n",
+ " // Teilformel S\n",
+ " \n",
+ " state(0,z0) = TRUE ∧\n",
+ " head(0,0) = TRUE ∧\n",
+ " tape(0,0,I) = TRUE ∧ // Anfangswort auf dem Band\n",
+ " tape(0,1,O) = TRUE ∧\n",
+ " tape(0,2,O) = TRUE ∧\n",
+ " ∀i.(i∈-pn..-1 ⇒ tape(0,i,`BLANK`)=TRUE) ∧\n",
+ " ∀i.(i∈3..pn ⇒ tape(0,i,`BLANK`)=TRUE)\n",
+ " \n",
+ " &\n",
+ " \n",
+ " // TeilFormel_U1: Übergangsrelation 1: delta\n",
+ " ∀(t,s).( (t,s) ∈ (TIME1 * {z0,z1,z2,ze}) // TIME1: diese Bedingung ist neu gegenüber dem Skript\n",
+ " =>\n",
+ " !(i,a) .(\n",
+ " (i,a) ∈ (POS * {O,I,`BLANK`}) &\n",
+ " i+offset(prj2(δ(s,a))) : POS // Needed for WD\n",
+ " ⇒\n",
+ " ((state(t,s)=TRUE ∧ head(t,i)=TRUE ∧ tape(t,i,a)=TRUE)\n",
+ " ⇒\n",
+ " (\n",
+ " //∃(s2,a2,y).( δ(s,a)=(s2,a2,y)∈δ ∧\n",
+ " state(t+1,prj1(prj1(δ(s,a))))=TRUE ∧\n",
+ " head(t+1,i+offset(prj2(δ(s,a))))=TRUE ∧\n",
+ " tape(t+1,i,prj2(prj1(δ(s,a))))=TRUE)\n",
+ " ) \n",
+ " )\n",
+ " )\n",
+ " \n",
+ " &\n",
+ " \n",
+ " // TeilFormel_U2: Übergangsrelation 2: Frame Axiom: unbeschriebene Bandinhalte bleiben gleich\n",
+ " ∀(t).(t:TIME1 =>\n",
+ " !(i,a).( (i,a)∈(POS*{O,I,`BLANK`})\n",
+ " ⇒\n",
+ " ( (head(t,i) = FALSE ∧ tape(t,i,a)=TRUE)\n",
+ " ⇒ tape(t+1,i,a)=TRUE\n",
+ " ) \n",
+ " )\n",
+ " ) \n",
+ " \n",
+ " &\n",
+ " \n",
+ " // Teilformel E\n",
+ " state(last_time,ze)=TRUE"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "dee392b1",
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "d982916e",
+ "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": 5
+}