diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index 72bd4c8785123654c95278d98863f48ba1282934..85b339ba32413ac4dbd463744c41f2d685be1c14 100644
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -18,8 +18,11 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$5070602400912917605986812821504$"
+ ],
"text/plain": [
- "1024"
+ "5070602400912917605986812821504"
]
},
"execution_count": 1,
@@ -28,7 +31,7 @@
}
],
"source": [
- "2**10"
+ "2**102"
]
},
{
@@ -45,6 +48,9 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$1267650600228229401496703205376$"
+ ],
"text/plain": [
"1267650600228229401496703205376"
]
@@ -73,6 +79,9 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$"
+ ],
"text/plain": [
"TRUE"
]
@@ -101,6 +110,12 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $x = -10$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -132,6 +147,9 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$\\{-10,10\\}$"
+ ],
"text/plain": [
"{−10,10}"
]
@@ -160,6 +178,19 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $R = 8$\n",
+ "* $S = 9$\n",
+ "* $D = 7$\n",
+ "* $E = 5$\n",
+ "* $Y = 2$\n",
+ "* $M = 1$\n",
+ "* $N = 6$\n",
+ "* $O = 0$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -202,6 +233,19 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $R = 0$\n",
+ "* $S = 9$\n",
+ "* $D = 0$\n",
+ "* $E = 0$\n",
+ "* $Y = 0$\n",
+ "* $M = 1$\n",
+ "* $N = 0$\n",
+ "* $O = 0$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -243,6 +287,9 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$\\{(((((((9\\mapsto 5)\\mapsto 6)\\mapsto 7)\\mapsto 1)\\mapsto 0)\\mapsto 8)\\mapsto 2)\\}$"
+ ],
"text/plain": [
"{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}"
]
@@ -276,6 +323,18 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $P = 4$\n",
+ "* $A = 1$\n",
+ "* $S = 3$\n",
+ "* $I = 0$\n",
+ "* $K = 2$\n",
+ "* $N = 9$\n",
+ "* $O = 8$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -317,6 +376,13 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $queens = \\{(1\\mapsto 1),(2\\mapsto 5),(3\\mapsto 8),(4\\mapsto 6),(5\\mapsto 3),(6\\mapsto 7),(7\\mapsto 2),(8\\mapsto 4)\\}$\n",
+ "* $n = 8$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -340,7 +406,7 @@
},
{
"cell_type": "code",
- "execution_count": 1,
+ "execution_count": 11,
"metadata": {},
"outputs": [
{
@@ -369,7 +435,7 @@
"8\t8\t4\n"
]
},
- "execution_count": 1,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -380,11 +446,18 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $queens = \\{(1\\mapsto 1),(2\\mapsto 3),(3\\mapsto 5),(4\\mapsto 13),(5\\mapsto 11),(6\\mapsto 4),(7\\mapsto 15),(8\\mapsto 7),(9\\mapsto 16),(10\\mapsto 14),(11\\mapsto 2),(12\\mapsto 8),(13\\mapsto 6),(14\\mapsto 9),(15\\mapsto 12),(16\\mapsto 10)\\}$\n",
+ "* $n = 16$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -393,7 +466,7 @@
"\tn = 16"
]
},
- "execution_count": 11,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -426,11 +499,19 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $A = TRUE$\n",
+ "* $B = TRUE$\n",
+ "* $C = FALSE$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -440,7 +521,7 @@
"\tC = FALSE"
]
},
- "execution_count": 12,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -460,16 +541,19 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$\\{((TRUE\\mapsto TRUE)\\mapsto FALSE)\\}$"
+ ],
"text/plain": [
"{((TRUE↦TRUE)↦FALSE)}"
]
},
- "execution_count": 13,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -480,6 +564,33 @@
" (B=TRUE <=> A=TRUE) }"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|Nr|A|B|C|\n",
+ "|---|---|---|---|\n",
+ "|1|TRUE|TRUE|FALSE|\n"
+ ],
+ "text/plain": [
+ "Nr\tA\tB\tC\n",
+ "1\tTRUE\tTRUE\tFALSE\n"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {A,B,C| (A=TRUE <=> (B=FALSE or C=FALSE)) &\n",
+ " (B=TRUE <=> A=TRUE) }"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -489,11 +600,19 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $DOM = (1 \\ldots 9)$\n",
+ "* $Board = \\{(1\\mapsto\\{(1\\mapsto 7),(2\\mapsto 8),(3\\mapsto 1),(4\\mapsto 6),(5\\mapsto 3),(6\\mapsto 2),(7\\mapsto 9),(8\\mapsto 4),(9\\mapsto 5)\\}),(2\\mapsto\\{(1\\mapsto 9),(2\\mapsto 5),(3\\mapsto 2),(4\\mapsto 7),(5\\mapsto 1),(6\\mapsto 4),(7\\mapsto 6),(8\\mapsto 3),(9\\mapsto 8)\\}),(3\\mapsto\\{(1\\mapsto 4),(2\\mapsto 3),(3\\mapsto 6),(4\\mapsto 8),(5\\mapsto 9),(6\\mapsto 5),(7\\mapsto 7),(8\\mapsto 1),(9\\mapsto 2)\\}),(4\\mapsto\\{(1\\mapsto 2),(2\\mapsto 4),(3\\mapsto 9),(4\\mapsto 3),(5\\mapsto 7),(6\\mapsto 6),(7\\mapsto 8),(8\\mapsto 5),(9\\mapsto 1)\\}),(5\\mapsto\\{(1\\mapsto 6),(2\\mapsto 7),(3\\mapsto 3),(4\\mapsto 5),(5\\mapsto 8),(6\\mapsto 1),(7\\mapsto 2),(8\\mapsto 9),(9\\mapsto 4)\\}),(6\\mapsto\\{(1\\mapsto 5),(2\\mapsto 1),(3\\mapsto 8),(4\\mapsto 4),(5\\mapsto 2),(6\\mapsto 9),(7\\mapsto 3),(8\\mapsto 6),(9\\mapsto 7)\\}),(7\\mapsto\\{(1\\mapsto 1),(2\\mapsto 9),(3\\mapsto 4),(4\\mapsto 2),(5\\mapsto 6),(6\\mapsto 7),(7\\mapsto 5),(8\\mapsto 8),(9\\mapsto 3)\\}),(8\\mapsto\\{(1\\mapsto 8),(2\\mapsto 6),(3\\mapsto 7),(4\\mapsto 1),(5\\mapsto 5),(6\\mapsto 3),(7\\mapsto 4),(8\\mapsto 2),(9\\mapsto 9)\\}),(9\\mapsto\\{(1\\mapsto 3),(2\\mapsto 2),(3\\mapsto 5),(4\\mapsto 9),(5\\mapsto 4),(6\\mapsto 8),(7\\mapsto 1),(8\\mapsto 7),(9\\mapsto 6)\\})\\}$\n",
+ "* $SUBSQ = \\{\\{1,2,3\\},\\{4,5,6\\},\\{7,8,9\\}\\}$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -503,7 +622,7 @@
"\tSUBSQ = {{1,2,3},{4,5,6},{7,8,9}}"
]
},
- "execution_count": 14,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -554,11 +673,18 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $stolen = \\{(16\\mapsto 2),(17\\mapsto 4),(23\\mapsto 0),(24\\mapsto 0),(39\\mapsto 0),(40\\mapsto 0)\\}$\n",
+ "* $coins = \\{16,17,23,24,39,40\\}$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -567,7 +693,7 @@
"\tcoins = {16,17,23,24,39,40}"
]
},
- "execution_count": 15,
+ "execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
@@ -587,11 +713,21 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 17,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $Persons = \\{\"Agatha\",\"Charles\",\"butler\"\\}$\n",
+ "* $richer = \\{(\"Agatha\"\\mapsto\"Charles\"),(\"butler\"\\mapsto\"Agatha\"),(\"butler\"\\mapsto\"Charles\")\\}$\n",
+ "* $victim = \"Agatha\"$\n",
+ "* $killer = \"Agatha\"$\n",
+ "* $hates = \\{(\"Agatha\"\\mapsto\"Agatha\"),(\"Agatha\"\\mapsto\"Charles\"),(\"Charles\"\\mapsto\"butler\"),(\"butler\"\\mapsto\"Agatha\"),(\"butler\"\\mapsto\"Charles\")\\}$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -603,7 +739,7 @@
"\thates = {(\"Agatha\"↦\"Agatha\"),(\"Agatha\"↦\"Charles\"),(\"Charles\"↦\"butler\"),(\"butler\"↦\"Agatha\"),(\"butler\"↦\"Charles\")}"
]
},
- "execution_count": 16,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
@@ -639,11 +775,19 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 18,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $a = \\{(1\\mapsto 0),(2\\mapsto 2),(3\\mapsto 6),(4\\mapsto 9),(5\\mapsto 14),(6\\mapsto 24),(7\\mapsto 25)\\}$\n",
+ "* $len = 25$\n",
+ "* $n = 7$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -653,7 +797,7 @@
"\tn = 7"
]
},
- "execution_count": 17,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
@@ -674,11 +818,27 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 19,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $n1 = \"a\"$\n",
+ "* $iso = \\{(1\\mapsto\"c\"),(2\\mapsto\"a\"),(3\\mapsto\"b\")\\}$\n",
+ "* $n2 = \"b\"$\n",
+ "* $n3 = \"c\"$\n",
+ "* $V = \\{1,2,3\\}$\n",
+ "* $g1 = \\{(1\\mapsto 2),(1\\mapsto 3),(2\\mapsto 3)\\}$\n",
+ "* $g2 = \\{(\"a\"\\mapsto\"b\"),(\"c\"\\mapsto\"a\"),(\"c\"\\mapsto\"b\")\\}$\n",
+ "* $v1 = 1$\n",
+ "* $v2 = 2$\n",
+ "* $v3 = 3$\n",
+ "* $N = \\{\"a\",\"b\",\"c\"\\}$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -696,7 +856,7 @@
"\tN = {\"a\",\"b\",\"c\"}"
]
},
- "execution_count": 18,
+ "execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
@@ -711,6 +871,36 @@
"iso: V >->> N & !v.(v:V => iso[g1[{v}]] = g2[iso[{v}]])\n",
"END"
]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\"abc\"$"
+ ],
+ "text/plain": [
+ "\"abc\""
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "\"abc\""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
}
],
"metadata": {
@@ -720,8 +910,9 @@
"name": "prob2"
},
"language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
"file_extension": ".prob",
- "mimetype": "text/x-prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
"name": "prob"
}
},