diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index 7fa9ce80026596831cac1f57aee9965e5c772990..494f1567092de90ab5ac3176d564c1fa2bcc569b 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -258,19 +258,10 @@
    "outputs": [
     {
      "ename": "IllegalArgumentException",
-     "evalue": "Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS with additional predicate",
+     "evalue": "Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS in state root with additional predicate",
      "output_type": "error",
      "traceback": [
-      "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS with additional predicate\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ConstantsCommand.run(ConstantsCommand.java:48)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m"
+      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS in state root with additional predicate\u001b[0m"
      ]
     }
    ],
@@ -572,16 +563,7 @@
      "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS",
      "output_type": "error",
      "traceback": [
-      "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ConstantsCommand.run(ConstantsCommand.java:48)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m"
+      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS\u001b[0m"
      ]
     }
    ],
@@ -599,16 +581,7 @@
      "evalue": "Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION",
      "output_type": "error",
      "traceback": [
-      "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.InitialiseCommand.run(InitialiseCommand.java:48)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m"
+      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION\u001b[0m"
      ]
     }
    ],
@@ -626,16 +599,7 @@
      "evalue": "Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope",
      "output_type": "error",
      "traceback": [
-      "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:53)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m"
+      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope\u001b[0m"
      ]
     }
    ],
@@ -650,19 +614,10 @@
    "outputs": [
     {
      "ename": "IllegalArgumentException",
-     "evalue": "Executing operation add with predicate 1=0 produced errors: Could not execute operation add with additional predicate",
+     "evalue": "Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)",
      "output_type": "error",
      "traceback": [
-      "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add with additional predicate\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:53)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m"
+      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)\u001b[0m"
      ]
     }
    ],
@@ -702,19 +657,10 @@
    "outputs": [
     {
      "ename": "IllegalArgumentException",
-     "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS",
+     "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root",
      "output_type": "error",
      "traceback": [
-      "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ConstantsCommand.run(ConstantsCommand.java:48)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:228)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:251)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
-      "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m"
+      "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root\u001b[0m"
      ]
     }
    ],
@@ -861,6 +807,221 @@
    "source": [
     "y"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Local variables can be used in operation predicates."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 35,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: Counter"
+      ]
+     },
+     "execution_count": 35,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE Counter\n",
+    "CONSTANTS min_value, max_value\n",
+    "PROPERTIES min_value : MININT..0 & max_value : 0..MAXINT & min_value <= max_value\n",
+    "VARIABLES value\n",
+    "INVARIANT value : min_value..max_value\n",
+    "INITIALISATION value :: min_value..max_value\n",
+    "OPERATIONS\n",
+    "    add(diff) = SELECT\n",
+    "        value+diff : min_value..max_value\n",
+    "    THEN\n",
+    "        value := value+diff\n",
+    "    END\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 36,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$1$"
+      ],
+      "text/plain": [
+       "1"
+      ]
+     },
+     "execution_count": 36,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let one 1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 37,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$2$"
+      ],
+      "text/plain": [
+       "2"
+      ]
+     },
+     "execution_count": 37,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let two 2"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 38,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 38,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants min_value=-one & max_value=two"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 39,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{-1,0,1,2\\}$"
+      ],
+      "text/plain": [
+       "{−1,0,1,2}"
+      ]
+     },
+     "execution_count": 39,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "min_value..max_value"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 40,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine initialised using operation 3: $initialise_machine()"
+      ]
+     },
+     "execution_count": 40,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":init value=one"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 41,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$1$"
+      ],
+      "text/plain": [
+       "1"
+      ]
+     },
+     "execution_count": 41,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "value"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 42,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: add(-1)"
+      ]
+     },
+     "execution_count": 42,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec add diff=-one"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 43,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$0$"
+      ],
+      "text/plain": [
+       "0"
+      ]
+     },
+     "execution_count": 43,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "value"
+   ]
   }
  ],
  "metadata": {
diff --git a/notebooks/tests/assert.ipynb b/notebooks/tests/assert.ipynb
index c7b71024b992a4c7f513f12351a9fcee261480d7..f2476511aa3c1cc46562ee1ea73aeab5e23de414 100644
--- a/notebooks/tests/assert.ipynb
+++ b/notebooks/tests/assert.ipynb
@@ -229,6 +229,100 @@
    "source": [
     ":assert 123 + {}"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Local variables can be used in assertions."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let trü TRUE"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let flasche FALSE"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":assert trü"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "ename": "CommandExecutionException",
+     "evalue": ":assert: Assertion is not true: FALSE",
+     "output_type": "error",
+     "traceback": [
+      "\u001b[1m\u001b[31m:assert: Assertion is not true: FALSE\u001b[0m"
+     ]
+    }
+   ],
+   "source": [
+    ":assert flasche"
+   ]
   }
  ],
  "metadata": {
diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb
index 459e2fa2296c2a8b11c31f31ed3127281de011f3..66c0b525c54d0885820e8f2f26c841f89870dc21 100644
--- a/notebooks/tests/dot.ipynb
+++ b/notebooks/tests/dot.ipynb
@@ -20,23 +20,26 @@
        "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)\n",
        "* `state_space` - State Space: Show state space\n",
        "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n",
+       "* `current_state` - Current State in State Space: Show current state and successors in state space\n",
+       "* `history` - Path to Current State: Show a path leading to current state\n",
        "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n",
        "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n",
-       "* `state_as_graph` - State Graph: Show values in current state as a graph\n",
-       "* `custom_graph` - Customized State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n",
+       "* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
+       "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
+       "* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
+       "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n",
+       "* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
+       "* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
        "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
        "* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
        "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
        "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
-       "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n",
-       "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n",
-       "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
+       "* `goal` - Goal Formula Tree: Show GOAL as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models with a GOAL DEFINITION)\n",
        "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
+       "* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
        "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
-       "* `expr_as_graph` - Expression Graph: Show expression value as a graph\n",
-       "* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree\n",
-       "* `transition_diagram` - Transition Diagram Projection: Project state space onto expression values\n",
-       "* `predicate_dependency` - Predicate Dependency Graph: Show dependence graph of conjuncts of a predicate\n"
+       "* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
+       "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n"
       ],
       "text/plain": [
        ":dot COMMAND [FORMULA]\n",
@@ -48,23 +51,26 @@
        "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)\n",
        "* `state_space` - State Space: Show state space\n",
        "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n",
+       "* `current_state` - Current State in State Space: Show current state and successors in state space\n",
+       "* `history` - Path to Current State: Show a path leading to current state\n",
        "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n",
        "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n",
-       "* `state_as_graph` - State Graph: Show values in current state as a graph\n",
-       "* `custom_graph` - Customized State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n",
+       "* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
+       "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
+       "* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
+       "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n",
+       "* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
+       "* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
        "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
        "* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
        "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
        "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
-       "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n",
-       "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n",
-       "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
+       "* `goal` - Goal Formula Tree: Show GOAL as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models with a GOAL DEFINITION)\n",
        "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
+       "* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
        "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
-       "* `expr_as_graph` - Expression Graph: Show expression value as a graph\n",
-       "* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree\n",
-       "* `transition_diagram` - Transition Diagram Projection: Project state space onto expression values\n",
-       "* `predicate_dependency` - Predicate Dependency Graph: Show dependence graph of conjuncts of a predicate\n"
+       "* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
+       "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n"
       ]
      },
      "execution_count": 1,
@@ -207,17 +213,17 @@
        "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
        " -->\n",
        "<!-- Title: g Pages: 1 -->\n",
-       "<svg width=\"155pt\" height=\"62pt\"\n",
-       " viewBox=\"0.00 0.00 155.08 61.74\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 57.7401)\">\n",
+       "<svg width=\"62pt\" height=\"46pt\"\n",
+       " viewBox=\"0.00 0.00 62.00 46.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 42)\">\n",
        "<title>g</title>\n",
-       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-57.7401 151.0782,-57.7401 151.0782,4 -4,4\"/>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-42 58,-42 58,4 -4,4\"/>\n",
        "<!-- Noderoot -->\n",
        "<g id=\"node1\" class=\"node\">\n",
        "<title>Noderoot</title>\n",
-       "<ellipse fill=\"#b3ee3a\" stroke=\"#000000\" cx=\"73.5391\" cy=\"-26.8701\" rx=\"73.5782\" ry=\"26.7407\"/>\n",
-       "<text text-anchor=\"middle\" x=\"73.5391\" y=\"-30.6701\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">(TRUE:BOOL)</text>\n",
-       "<text text-anchor=\"middle\" x=\"73.5391\" y=\"-15.6701\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\"> true</text>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M42,-38C42,-38 12,-38 12,-38 6,-38 0,-32 0,-26 0,-26 0,-12 0,-12 0,-6 6,0 12,0 12,0 42,0 42,0 48,0 54,-6 54,-12 54,-12 54,-26 54,-26 54,-32 48,-38 42,-38\"/>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-22.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">⊤</text>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-7.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>"
@@ -249,16 +255,16 @@
        "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
        " -->\n",
        "<!-- Title: state Pages: 1 -->\n",
-       "<svg width=\"128pt\" height=\"218pt\"\n",
-       " viewBox=\"0.00 0.00 128.00 218.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<svg width=\"326pt\" height=\"218pt\"\n",
+       " viewBox=\"0.00 0.00 326.00 218.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 214)\">\n",
        "<title>state</title>\n",
-       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-214 124,-214 124,4 -4,4\"/>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-214 322,-214 322,4 -4,4\"/>\n",
        "<!-- 3 -->\n",
        "<g id=\"node1\" class=\"node\">\n",
        "<title>3</title>\n",
-       "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"90,-210 36,-210 36,-174 90,-174 90,-210\"/>\n",
-       "<text text-anchor=\"middle\" x=\"63\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
+       "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"130,-210 76,-210 76,-174 130,-174 130,-210\"/>\n",
+       "<text text-anchor=\"middle\" x=\"103\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
@@ -269,29 +275,29 @@
        "<!-- 3&#45;&gt;1 -->\n",
        "<g id=\"edge1\" class=\"edge\">\n",
        "<title>3&#45;&gt;1</title>\n",
-       "<path fill=\"none\" stroke=\"#b22222\" d=\"M48.2776,-173.7725C44.455,-168.3152 40.6674,-162.1419 38,-156 34.9241,-148.9173 32.677,-140.8962 31.0477,-133.3471\"/>\n",
-       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"34.4794,-132.6574 29.1892,-123.4779 27.6003,-133.9529 34.4794,-132.6574\"/>\n",
-       "<text text-anchor=\"middle\" x=\"57\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">[2,3,1]</text>\n",
+       "<path fill=\"none\" stroke=\"#b22222\" d=\"M75.6408,-186.4668C58.8257,-181.5148 38.5455,-172.4004 28,-156 23.7372,-149.3705 22.3175,-141.1865 22.2793,-133.3301\"/>\n",
+       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"25.7725,-133.5476 22.9019,-123.3491 18.786,-133.1117 25.7725,-133.5476\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(1|&#45;&gt;2),(2|&#45;&gt;3),(3|&#45;&gt;1)}</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node3\" class=\"node\">\n",
        "<title>2</title>\n",
-       "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"85,-36 31,-36 31,0 85,0 85,-36\"/>\n",
-       "<text text-anchor=\"middle\" x=\"58\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+       "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"130,-36 76,-36 76,0 130,0 130,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"103\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge3\" class=\"edge\">\n",
        "<title>1&#45;&gt;2</title>\n",
-       "<path fill=\"none\" stroke=\"#b22222\" d=\"M29.6039,-86.69C31.3415,-76.8067 34.0458,-64.5126 38,-54 39.0973,-51.0827 40.4008,-48.115 41.8086,-45.1988\"/>\n",
-       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"44.9918,-46.6647 46.5353,-36.1829 38.7922,-43.4144 44.9918,-46.6647\"/>\n",
-       "<text text-anchor=\"middle\" x=\"57\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">[2,3,1]</text>\n",
+       "<path fill=\"none\" stroke=\"#b22222\" d=\"M22.9019,-86.6509C21.6193,-76.2846 21.8693,-63.5346 28,-54 36.5682,-40.6747 51.5628,-32.1592 65.9039,-26.7783\"/>\n",
+       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"67.2605,-30.0155 75.6408,-23.5332 65.0472,-23.3746 67.2605,-30.0155\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(1|&#45;&gt;2),(2|&#45;&gt;3),(3|&#45;&gt;1)}</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge2\" class=\"edge\">\n",
        "<title>2&#45;&gt;3</title>\n",
-       "<path fill=\"none\" stroke=\"#b22222\" d=\"M69.0675,-36.0594C71.9014,-41.6127 74.5551,-47.8793 76,-54 86.4155,-98.1206 83.8156,-111.3455 76,-156 75.5328,-158.6693 74.8845,-161.4018 74.1248,-164.1095\"/>\n",
-       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"70.7862,-163.0583 71.0089,-173.6508 77.4404,-165.2314 70.7862,-163.0583\"/>\n",
-       "<text text-anchor=\"middle\" x=\"101\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">[2,3,1]</text>\n",
+       "<path fill=\"none\" stroke=\"#b22222\" d=\"M130.2715,-26.586C143.2238,-32.1915 157.4858,-40.9478 165,-54 187.6182,-93.2878 187.6182,-116.7122 165,-156 159.2469,-165.9931 149.5384,-173.468 139.4907,-178.9387\"/>\n",
+       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"137.7391,-175.8983 130.2715,-183.414 140.796,-182.1956 137.7391,-175.8983\"/>\n",
+       "<text text-anchor=\"middle\" x=\"249.5\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(1|&#45;&gt;2),(2|&#45;&gt;3),(3|&#45;&gt;1)}</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>"
@@ -661,54 +667,55 @@
        "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
        " -->\n",
        "<!-- Title: g Pages: 1 -->\n",
-       "<svg width=\"247pt\" height=\"100pt\"\n",
-       " viewBox=\"0.00 0.00 247.40 100.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 96)\">\n",
+       "<svg width=\"242pt\" height=\"110pt\"\n",
+       " viewBox=\"0.00 0.00 242.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\">\n",
        "<title>g</title>\n",
-       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-96 243.397,-96 243.397,4 -4,4\"/>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
        "<!-- Noderoot -->\n",
        "<g id=\"node1\" class=\"node\">\n",
        "<title>Noderoot</title>\n",
-       "<ellipse fill=\"#b3ee3a\" stroke=\"#000000\" cx=\"29.6985\" cy=\"-46\" rx=\"29.8983\" ry=\"26.7407\"/>\n",
-       "<text text-anchor=\"middle\" x=\"29.6985\" y=\"-49.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">=</text>\n",
-       "<text text-anchor=\"middle\" x=\"29.6985\" y=\"-34.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\"> true</text>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M42,-72.5C42,-72.5 12,-72.5 12,-72.5 6,-72.5 0,-66.5 0,-60.5 0,-60.5 0,-46.5 0,-46.5 0,-40.5 6,-34.5 12,-34.5 12,-34.5 42,-34.5 42,-34.5 48,-34.5 54,-40.5 54,-46.5 54,-46.5 54,-60.5 54,-60.5 54,-66.5 48,-72.5 42,-72.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-57.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">=</text>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-42.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
        "</g>\n",
        "<!-- Node1 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
        "<title>Node1</title>\n",
-       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"149.397,-92 95.397,-92 95.397,-56 149.397,-56 149.397,-92\"/>\n",
-       "<text text-anchor=\"middle\" x=\"122.397\" y=\"-70.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-65.5 90,-101.5 144,-101.5 144,-65.5 90,-65.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"117\" y=\"-79.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
        "</g>\n",
        "<!-- Node1&#45;&gt;Noderoot -->\n",
        "<g id=\"edge1\" class=\"edge\">\n",
        "<title>Node1&#45;&gt;Noderoot</title>\n",
-       "<path fill=\"none\" stroke=\"#000000\" d=\"M95.0857,-65.7505C86.5358,-63.168 76.9398,-60.2694 67.7877,-57.505\"/>\n",
-       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"68.6865,-54.1204 58.1016,-54.5793 66.6624,-60.8214 68.6865,-54.1204\"/>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-74.499C81.796,-71.7653 72.6401,-68.7134 63.905,-65.8017\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"64.8886,-62.4403 54.295,-62.5983 62.675,-69.0811 64.8886,-62.4403\"/>\n",
        "</g>\n",
        "<!-- Node2 -->\n",
        "<g id=\"node3\" class=\"node\">\n",
        "<title>Node2</title>\n",
-       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"149.397,-38 95.397,-38 95.397,0 149.397,0 149.397,-38\"/>\n",
-       "<text text-anchor=\"middle\" x=\"122.397\" y=\"-22.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">card</text>\n",
-       "<text text-anchor=\"middle\" x=\"122.397\" y=\"-7.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\"> 2</text>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-.5 90,-46.5 144,-46.5 144,-.5 90,-.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">card</text>\n",
+       "<polyline fill=\"none\" stroke=\"#000000\" points=\"90,-23.5 144,-23.5 \"/>\n",
+       "<text text-anchor=\"middle\" x=\"117\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
        "</g>\n",
        "<!-- Node2&#45;&gt;Noderoot -->\n",
        "<g id=\"edge2\" class=\"edge\">\n",
        "<title>Node2&#45;&gt;Noderoot</title>\n",
-       "<path fill=\"none\" stroke=\"#000000\" d=\"M95.0857,-26.9549C86.5358,-29.4452 76.9398,-32.2402 67.7877,-34.9059\"/>\n",
-       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.7238,-31.5702 58.1016,-37.7271 68.6814,-38.2909 66.7238,-31.5702\"/>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-32.501C81.796,-35.2347 72.6401,-38.2866 63.905,-41.1983\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.675,-37.9189 54.295,-44.4017 64.8886,-44.5597 62.675,-37.9189\"/>\n",
        "</g>\n",
        "<!-- Node3 -->\n",
        "<g id=\"node4\" class=\"node\">\n",
        "<title>Node3</title>\n",
-       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"239.397,-37 185.397,-37 185.397,-1 239.397,-1 239.397,-37\"/>\n",
-       "<text text-anchor=\"middle\" x=\"212.397\" y=\"-15.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{1,2}</text>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"180,-5.5 180,-41.5 234,-41.5 234,-5.5 180,-5.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"207\" y=\"-19.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{1,2}</text>\n",
        "</g>\n",
        "<!-- Node3&#45;&gt;Node2 -->\n",
        "<g id=\"edge3\" class=\"edge\">\n",
        "<title>Node3&#45;&gt;Node2</title>\n",
-       "<path fill=\"none\" stroke=\"#000000\" d=\"M185.394,-19C177.3693,-19 168.4304,-19 159.8661,-19\"/>\n",
-       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"159.692,-15.5001 149.6919,-19 159.6919,-22.5001 159.692,-15.5001\"/>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M179.997,-23.5C171.9723,-23.5 163.0335,-23.5 154.4691,-23.5\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.295,-20.0001 144.295,-23.5 154.2949,-27.0001 154.295,-20.0001\"/>\n",
        "</g>\n",
        "</g>\n",
        "</svg>"
@@ -725,6 +732,116 @@
    "source": [
     ":dot formula_tree 1*2 + 3/4 = card({1, 2})"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Local variables can be used in dot visualisation parameters."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$2$"
+      ],
+      "text/plain": [
+       "2"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let thing 1*2 + 3/4"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "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.40.1 (20161225.0304)\n",
+       " -->\n",
+       "<!-- Title: g Pages: 1 -->\n",
+       "<svg width=\"242pt\" height=\"110pt\"\n",
+       " viewBox=\"0.00 0.00 242.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\">\n",
+       "<title>g</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
+       "<!-- Noderoot -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>Noderoot</title>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M42,-72.5C42,-72.5 12,-72.5 12,-72.5 6,-72.5 0,-66.5 0,-60.5 0,-60.5 0,-46.5 0,-46.5 0,-40.5 6,-34.5 12,-34.5 12,-34.5 42,-34.5 42,-34.5 48,-34.5 54,-40.5 54,-46.5 54,-46.5 54,-60.5 54,-60.5 54,-66.5 48,-72.5 42,-72.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-57.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">=</text>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-42.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
+       "</g>\n",
+       "<!-- Node1 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>Node1</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-65.5 90,-101.5 144,-101.5 144,-65.5 90,-65.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"117\" y=\"-79.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+       "</g>\n",
+       "<!-- Node1&#45;&gt;Noderoot -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>Node1&#45;&gt;Noderoot</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-74.499C81.796,-71.7653 72.6401,-68.7134 63.905,-65.8017\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"64.8886,-62.4403 54.295,-62.5983 62.675,-69.0811 64.8886,-62.4403\"/>\n",
+       "</g>\n",
+       "<!-- Node2 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>Node2</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-.5 90,-46.5 144,-46.5 144,-.5 90,-.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">card</text>\n",
+       "<polyline fill=\"none\" stroke=\"#000000\" points=\"90,-23.5 144,-23.5 \"/>\n",
+       "<text text-anchor=\"middle\" x=\"117\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+       "</g>\n",
+       "<!-- Node2&#45;&gt;Noderoot -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>Node2&#45;&gt;Noderoot</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-32.501C81.796,-35.2347 72.6401,-38.2866 63.905,-41.1983\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.675,-37.9189 54.295,-44.4017 64.8886,-44.5597 62.675,-37.9189\"/>\n",
+       "</g>\n",
+       "<!-- Node3 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>Node3</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"180,-5.5 180,-41.5 234,-41.5 234,-5.5 180,-5.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"207\" y=\"-19.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{1,2}</text>\n",
+       "</g>\n",
+       "<!-- Node3&#45;&gt;Node2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>Node3&#45;&gt;Node2</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M179.997,-23.5C171.9723,-23.5 163.0335,-23.5 154.4691,-23.5\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.295,-20.0001 144.295,-23.5 154.2949,-27.0001 154.295,-20.0001\"/>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>"
+      ],
+      "text/plain": [
+       "<Dot visualization: formula_tree [thingthing=2thing=card({1,2})]>"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":dot formula_tree thing = card({1, 2})"
+   ]
   }
  ],
  "metadata": {
diff --git a/notebooks/tests/let.ipynb b/notebooks/tests/let.ipynb
index 6cb9bace87f2d92b89d9ab07686997e0a0822c2e..0896dfd942c6cc5184283da00bdbbad69e7c5f91 100644
--- a/notebooks/tests/let.ipynb
+++ b/notebooks/tests/let.ipynb
@@ -205,6 +205,105 @@
    "source": [
     "n"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Local variables can be used when setting a local variable."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$1$"
+      ],
+      "text/plain": [
+       "1"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let n 1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$2$"
+      ],
+      "text/plain": [
+       "2"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let m n + 1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$3$"
+      ],
+      "text/plain": [
+       "3"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let m m + 1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$3$"
+      ],
+      "text/plain": [
+       "3"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "m"
+   ]
   }
  ],
  "metadata": {
diff --git a/notebooks/tests/solve.ipynb b/notebooks/tests/solve.ipynb
index 6a78c898679a57d244a87e5380391f17838e8ce6..63f2940bd0802830cb536e25ca3be381c8ddc744 100644
--- a/notebooks/tests/solve.ipynb
+++ b/notebooks/tests/solve.ipynb
@@ -120,10 +120,10 @@
    "outputs": [
     {
      "ename": "ProBError",
-     "evalue": "(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4531520732),0,procedure,:(z3interface,/(pop_frame,0)),0)))",
+     "evalue": "(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4401885196),0,procedure,:(z3interface,/(pop_frame,0)),0)))",
      "output_type": "error",
      "traceback": [
-      "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31m(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4531520732),0,procedure,:(z3interface,/(pop_frame,0)),0)))\u001b[0m"
+      "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31m(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4401885196),0,procedure,:(z3interface,/(pop_frame,0)),0)))\u001b[0m"
      ]
     }
    ],
@@ -296,6 +296,98 @@
    "source": [
     ":solve prob z /= 2"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Local variables can be used in `:solve` predicates."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$5$"
+      ],
+      "text/plain": [
+       "5"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let five 5"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{xx} = 3$\n",
+       "* $\\mathit{yy} = 4$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\txx = 3\n",
+       "\tyy = 4"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":solve prob xx > 2 & yy < five & xx < yy"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{xx} = 3$\n",
+       "* $\\mathit{yy} = 4$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\txx = 3\n",
+       "\tyy = 4"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":solve kodkod xx > 2 & yy < five & xx < yy"
+   ]
   }
  ],
  "metadata": {
diff --git a/notebooks/tests/table.ipynb b/notebooks/tests/table.ipynb
index 37f853ecad9f7f1bcd6555f2b34fb7e3c7d31e6e..5ad6688fa5310ec59caa9f3d86faf2dfe4d54b50 100644
--- a/notebooks/tests/table.ipynb
+++ b/notebooks/tests/table.ipynb
@@ -199,6 +199,66 @@
    "source": [
     ":table {({1|->2, 3|->4}, {5|->6, 7|->8}), ({2|->1, 4|->3}, {6|->5, 8|->7})}"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Local variables can be used in expressions visualised as table."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(1\\mapsto 2\\mapsto 3),(4\\mapsto 5\\mapsto 6),(7\\mapsto 8\\mapsto 9)\\}$"
+      ],
+      "text/plain": [
+       "{(1↦2↦3),(4↦5↦6),(7↦8↦9)}"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let thing {(1, 2, 3), (4, 5, 6), (7, 8, 9)}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|prj11|prj12|prj2|\n",
+       "|---|---|---|\n",
+       "|$1$|$2$|$3$|\n",
+       "|$4$|$5$|$6$|\n",
+       "|$7$|$8$|$9$|\n"
+      ],
+      "text/plain": [
+       "prj11\tprj12\tprj2\n",
+       "1\t2\t3\n",
+       "4\t5\t6\n",
+       "7\t8\t9\n"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":table thing"
+   ]
   }
  ],
  "metadata": {
diff --git a/notebooks/tests/type.ipynb b/notebooks/tests/type.ipynb
index 32a7041af45d258ca05fa0c6658ab3b5540268c4..a1f692032035f91239ffa14488e927c76270766b 100644
--- a/notebooks/tests/type.ipynb
+++ b/notebooks/tests/type.ipynb
@@ -47,7 +47,7 @@
     {
      "data": {
       "text/plain": [
-       "integer"
+       "INTEGER"
       ]
      },
      "execution_count": 2,
@@ -67,7 +67,7 @@
     {
      "data": {
       "text/plain": [
-       "set(any)"
+       "POW(?)"
       ]
      },
      "execution_count": 3,
@@ -87,7 +87,7 @@
     {
      "data": {
       "text/plain": [
-       "set(integer)"
+       "POW(INTEGER)"
       ]
      },
      "execution_count": 4,
@@ -107,7 +107,7 @@
     {
      "data": {
       "text/plain": [
-       "set(integer)"
+       "POW(INTEGER)"
       ]
      },
      "execution_count": 5,
@@ -127,7 +127,7 @@
     {
      "data": {
       "text/plain": [
-       "seq(integer)"
+       "seq(INTEGER)"
       ]
      },
      "execution_count": 6,
@@ -147,7 +147,7 @@
     {
      "data": {
       "text/plain": [
-       "set(set(couple(couple(integer,integer),integer)))"
+       "POW(((INTEGER*INTEGER)<->INTEGER))"
       ]
      },
      "execution_count": 7,
@@ -174,7 +174,7 @@
     {
      "data": {
       "text/plain": [
-       "pred"
+       "predicate"
       ]
      },
      "execution_count": 8,
@@ -194,7 +194,7 @@
     {
      "data": {
       "text/plain": [
-       "pred"
+       "predicate"
       ]
      },
      "execution_count": 9,
@@ -220,14 +220,14 @@
    "outputs": [
     {
      "ename": "ProBError",
-     "evalue": "Type errors in formula\nProB returned error messages:\nError: Type mismatch: Expected INTEGER, but was BOOL in 'TRUE' (:1:4 to 1:8)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (:1:10 to 1:16)\nError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:20 to 1:22)",
+     "evalue": "Type errors in formula\nProB returned error messages:\nError: Type mismatch: Expected INTEGER, but was BOOL in 'TRUE' (:1:4 to 1:8)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (:1:10 to 1:18)\nError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:20 to 1:22)",
      "output_type": "error",
      "traceback": [
       "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mType errors in formula\u001b[0m",
       "\u001b[1m\u001b[30m3 errors:\u001b[0m",
       "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was BOOL in 'TRUE' (:1:4 to 1:8)\u001b[0m",
       "\u001b[1m\u001b[30m// Source code not known\u001b[0m",
-      "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (:1:10 to 1:16)\u001b[0m",
+      "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (:1:10 to 1:18)\u001b[0m",
       "\u001b[1m\u001b[30m// Source code not known\u001b[0m",
       "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:20 to 1:22)\u001b[0m",
       "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
@@ -257,6 +257,76 @@
    "source": [
     ":type 1 + {}"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Local variables can be passed to `:type`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{\\{(1\\mapsto 2\\mapsto 3),(4\\mapsto 5\\mapsto 6)\\},\\{(7\\mapsto 8\\mapsto 9)\\}\\}$"
+      ],
+      "text/plain": [
+       "{{(1↦2↦3),(4↦5↦6)},{(7↦8↦9)}}"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let thing {{(1, 2, 3), (4, 5, 6)}, {(7, 8, 9)}}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "POW(((INTEGER*INTEGER)<->INTEGER))"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":type thing"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "POW(((INTEGER*INTEGER)<->INTEGER))*INTEGER"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":type thing, 123"
+   ]
   }
  ],
  "metadata": {
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index a1505361b3e41c7999e3e9b94383b7057ed4a749..86b60b554dfcc8a0e71a63b6c2167eef797b1281 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -495,4 +495,8 @@ public final class ProBKernel extends BaseKernel {
 			throw e2;
 		}
 	}
+	
+	public @NotNull String insertLetVariables(final @NotNull String code) {
+		return CommandUtils.insertLetVariables(code, this.getVariables());
+	}
 }
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 68a7588b1915b8e5421e35a0712748616797ce96..ba2d64814fee7139e029dc166532e6197e4cbc24 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -1,12 +1,13 @@
 package de.prob2.jupyter.commands;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.animator.domainobjects.AbstractEvalResult;
 import de.prob.animator.domainobjects.EvalResult;
 import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.statespace.AnimationSelector;
-
+import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -17,12 +18,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class AssertCommand implements Command {
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private AssertCommand(final @NotNull AnimationSelector animationSelector) {
+	private AssertCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -44,7 +47,8 @@ public final class AssertCommand implements Command {
 	
 	@Override
 	public @NotNull DisplayData run(final @NotNull String argString) {
-		final AbstractEvalResult result = CommandUtils.withSourceCode(argString, () -> this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.TRUNCATE));
+		final String code = this.kernelProvider.get().insertLetVariables(argString);
+		final AbstractEvalResult result = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(code, FormulaExpand.TRUNCATE));
 		if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
 			// Use EvalResult.TRUE instead of the real result so that solution variables are not displayed.
 			return CommandUtils.displayDataForEvalResult(EvalResult.TRUE);
diff --git a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
index 929873d45b5e49a812d0bf6f1a728f69b99535c7..a29be680bba75b93097709be64a266484139aed5 100644
--- a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
@@ -8,6 +8,7 @@ import java.util.List;
 import java.util.Map;
 import java.util.NoSuchElementException;
 import java.util.Set;
+import java.util.StringJoiner;
 import java.util.function.Supplier;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
@@ -128,6 +129,20 @@ public final class CommandUtils {
 		});
 	}
 	
+	public static @NotNull String insertLetVariables(final @NotNull String code, final @NotNull Map<@NotNull String, @NotNull String> variables) {
+		if (variables.isEmpty()) {
+			return code;
+		} else {
+			final StringJoiner varNames = new StringJoiner(",");
+			final StringJoiner varAssignments = new StringJoiner("&");
+			variables.forEach((name, value) -> {
+				varNames.add(name);
+				varAssignments.add(name + "=(" + value + ')');
+			});
+			return String.format("LET %s BE %s IN(%s)END", varNames, varAssignments, code);
+		}
+	}
+	
 	public static @NotNull DisplayData displayDataForEvalResult(final @NotNull AbstractEvalResult aer) {
 		final StringBuilder sb = new StringBuilder();
 		final StringBuilder sbMarkdown = new StringBuilder();
diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
index 9532f6443f4560f02051fb8c1747259f55e9fcee..85e7b395e0f01165fdf08f352d6184f4be3b437b 100644
--- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
@@ -4,11 +4,13 @@ import java.util.Collections;
 import java.util.List;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 import de.prob.statespace.Transition;
+import de.prob2.jupyter.ProBKernel;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -17,12 +19,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class ConstantsCommand implements Command {
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private ConstantsCommand(final @NotNull AnimationSelector animationSelector) {
+	private ConstantsCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -44,7 +48,12 @@ public final class ConstantsCommand implements Command {
 	@Override
 	public @NotNull DisplayData run(final @NotNull String argString) {
 		final Trace trace = this.animationSelector.getCurrentTrace();
-		final String predicate = argString.isEmpty() ? "1=1" : argString;
+		final String predicate;
+		if (argString.isEmpty()) {
+			predicate = "1=1";
+		} else {
+			predicate = this.kernelProvider.get().insertLetVariables(argString);
+		}
 		final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$setup_constants", predicate, 1);
 		assert !ops.isEmpty();
 		final Transition op = ops.get(0);
diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
index 989ccf9522b5e900db0b5b497037fd2ccaf7e7a9..a287991aa069bb32ca815cfaef17ad58ee493ed1 100644
--- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
@@ -10,6 +10,7 @@ import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.animator.command.GetAllDotCommands;
 import de.prob.animator.command.GetSvgForVisualizationCommand;
@@ -18,7 +19,7 @@ import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.animator.domainobjects.IEvalElement;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
-
+import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -28,12 +29,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class DotCommand implements Command {
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private DotCommand(final @NotNull AnimationSelector animationSelector) {
+	private DotCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -76,11 +79,13 @@ public final class DotCommand implements Command {
 		assert !split.isEmpty();
 		final String command = split.get(0);
 		final List<IEvalElement> args;
+		final String code;
 		if (split.size() > 1) {
-			final String code = split.get(1);
+			code = this.kernelProvider.get().insertLetVariables(split.get(1));
 			final IEvalElement formula = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().getModel().parseFormula(code, FormulaExpand.EXPAND));
 			args = Collections.singletonList(formula);
 		} else {
+			code = null;
 			args = Collections.emptyList();
 		}
 		
@@ -101,8 +106,8 @@ public final class DotCommand implements Command {
 		final GetSvgForVisualizationCommand cmd2 = new GetSvgForVisualizationCommand(trace.getCurrentState(), item, outPath.toFile(), args);
 		// Provide source code (if any) to error highlighter
 		final Runnable execute = () -> trace.getStateSpace().execute(cmd2);
-		if (split.size() > 1) {
-			CommandUtils.withSourceCode(split.get(1), execute);
+		if (code != null) {
+			CommandUtils.withSourceCode(code, execute);
 		} else {
 			execute.run();
 		}
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index f142a9119f29891a9d60487c8a08e93a78a7beb7..7999d76d702df77b2ba4373159e95739a6dcca2c 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -1,14 +1,10 @@
 package de.prob2.jupyter.commands;
 
-import java.util.Map;
-import java.util.StringJoiner;
-
 import com.google.inject.Inject;
 import com.google.inject.Injector;
 
 import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.statespace.AnimationSelector;
-
 import de.prob2.jupyter.ProBKernel;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -47,19 +43,7 @@ public final class EvalCommand implements Command {
 	
 	@Override
 	public @NotNull DisplayData run(final @NotNull String argString) {
-		final Map<String, String> variables = this.injector.getInstance(ProBKernel.class).getVariables();
-		final String code;
-		if (variables.isEmpty()) {
-			code = argString;
-		} else {
-			final StringJoiner varNames = new StringJoiner(",");
-			final StringJoiner varAssignments = new StringJoiner("&");
-			variables.forEach((name, value) -> {
-				varNames.add(name);
-				varAssignments.add(name + "=(" + value + ')');
-			});
-			code = String.format("LET %s BE %s IN(%s)END", varNames, varAssignments, argString);
-		}
+		final String code = this.injector.getInstance(ProBKernel.class).insertLetVariables(argString);
 		return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(code, FormulaExpand.EXPAND)));
 	}
 	
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index 9ebd093da728f00624e6fb7a73dafb9222a3613d..941383095dba2fffdb7417f70e95d6f118c8a526 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -5,11 +5,13 @@ import java.util.List;
 import java.util.stream.Collectors;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 import de.prob.statespace.Transition;
+import de.prob2.jupyter.ProBKernel;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -18,12 +20,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class ExecCommand implements Command {
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private ExecCommand(final @NotNull AnimationSelector animationSelector) {
+	private ExecCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -49,7 +53,12 @@ public final class ExecCommand implements Command {
 		
 		final Trace trace = this.animationSelector.getCurrentTrace();
 		final String translatedOpName = CommandUtils.unprettyOperationName(split.get(0));
-		final String predicate = split.size() < 2 ? "1=1" : split.get(1);
+		final String predicate;
+		if (split.size() < 2) {
+			predicate = "1=1";
+		} else {
+			predicate = this.kernelProvider.get().insertLetVariables(split.get(1));
+		}
 		final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, predicate, 1);
 		assert !ops.isEmpty();
 		final Transition op = ops.get(0);
diff --git a/src/main/java/de/prob2/jupyter/commands/FindCommand.java b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
index 09e0bb8a4d72d1b379a19a93d74360ff8a84969a..c85a972e86280726d85e652846b0f921743762e6 100644
--- a/src/main/java/de/prob2/jupyter/commands/FindCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
@@ -1,11 +1,13 @@
 package de.prob2.jupyter.commands;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.animator.domainobjects.IEvalElement;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
+import de.prob2.jupyter.ProBKernel;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -14,12 +16,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class FindCommand implements Command {
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private FindCommand(final @NotNull AnimationSelector animationSelector) {
+	private FindCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -41,8 +45,9 @@ public final class FindCommand implements Command {
 	@Override
 	public @NotNull DisplayData run(final @NotNull String argString) {
 		final Trace trace = this.animationSelector.getCurrentTrace();
-		final Trace newTrace = CommandUtils.withSourceCode(argString, () -> {
-			final IEvalElement pred = trace.getModel().parseFormula(argString, FormulaExpand.EXPAND);
+		final String code = this.kernelProvider.get().insertLetVariables(argString);
+		final Trace newTrace = CommandUtils.withSourceCode(code, () -> {
+			final IEvalElement pred = trace.getModel().parseFormula(code, FormulaExpand.EXPAND);
 			return trace.getStateSpace().getTraceToState(pred);
 		});
 		this.animationSelector.changeCurrentAnimation(newTrace);
diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
index 3ec63d9c39bb0cf42d31406823859db82f615af6..3e91bb6446347eac4e20f9d0acc9c739cddb8082 100644
--- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
@@ -4,11 +4,13 @@ import java.util.Collections;
 import java.util.List;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 import de.prob.statespace.Transition;
+import de.prob2.jupyter.ProBKernel;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -17,12 +19,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class InitialiseCommand implements Command {
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private InitialiseCommand(final @NotNull AnimationSelector animationSelector) {
+	private InitialiseCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -44,7 +48,12 @@ public final class InitialiseCommand implements Command {
 	@Override
 	public @NotNull DisplayData run(final @NotNull String argString) {
 		final Trace trace = this.animationSelector.getCurrentTrace();
-		final String predicate = argString.isEmpty() ? "1=1" : argString;
+		final String predicate;
+		if (argString.isEmpty()) {
+			predicate = "1=1";
+		} else {
+			predicate = this.kernelProvider.get().insertLetVariables(argString);
+		}
 		final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$initialise_machine", predicate, 1);
 		assert !ops.isEmpty();
 		final Transition op = ops.get(0);
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
index 876a91dcfda3bd46e06e40b34d785fbc6532377e..f71d3bc66dca90de3761e4c3aa1ca638b0ec0927 100644
--- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -3,7 +3,7 @@ package de.prob2.jupyter.commands;
 import java.util.List;
 
 import com.google.inject.Inject;
-import com.google.inject.Injector;
+import com.google.inject.Provider;
 
 import de.prob.animator.domainobjects.AbstractEvalResult;
 import de.prob.animator.domainobjects.EvalResult;
@@ -19,14 +19,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class LetCommand implements Command {
-	private final @NotNull Injector injector;
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	public LetCommand(final @NotNull Injector injector, final @NotNull AnimationSelector animationSelector) {
+	public LetCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
-		this.injector = injector;
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -52,10 +52,10 @@ public final class LetCommand implements Command {
 			throw new UserErrorException("Expected 2 arguments, not " + split.size());
 		}
 		final String name = split.get(0);
-		final String expr = split.get(1);
+		final String expr = this.kernelProvider.get().insertLetVariables(split.get(1));
 		final AbstractEvalResult evaluated = CommandUtils.withSourceCode(expr, () -> this.animationSelector.getCurrentTrace().evalCurrent(expr, FormulaExpand.EXPAND));
 		if (evaluated instanceof EvalResult) {
-			this.injector.getInstance(ProBKernel.class).getVariables().put(name, evaluated.toString());
+			this.kernelProvider.get().getVariables().put(name, evaluated.toString());
 		}
 		return CommandUtils.displayDataForEvalResult(evaluated);
 	}
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index b12b289e3695daca70fd0c656b8ebaae9c2a1b4e..1e6887d51c20d76e32c2eb71dc61a13ae856132a 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -6,6 +6,7 @@ import java.util.Map;
 import java.util.stream.Collectors;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.animator.command.CbcSolveCommand;
 import de.prob.animator.domainobjects.FormulaExpand;
@@ -13,6 +14,7 @@ import de.prob.animator.domainobjects.IEvalElement;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 
+import de.prob2.jupyter.ProBKernel;
 import de.prob2.jupyter.UserErrorException;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -25,12 +27,14 @@ public final class SolveCommand implements Command {
 	private static final @NotNull Map<@NotNull String, CbcSolveCommand.@NotNull Solvers> SOLVERS = Arrays.stream(CbcSolveCommand.Solvers.values())
 		.collect(Collectors.toMap(s -> s.name().toLowerCase(), s -> s));
 	
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private SolveCommand(final @NotNull AnimationSelector animationSelector) {
+	private SolveCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -67,7 +71,7 @@ public final class SolveCommand implements Command {
 		if (solver == null) {
 			throw new UserErrorException("Unknown solver: " + split.get(0));
 		}
-		final String code = split.get(1);
+		final String code = this.kernelProvider.get().insertLetVariables(split.get(1));
 		final IEvalElement predicate = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
 		
 		final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver, this.animationSelector.getCurrentTrace().getCurrentState());
diff --git a/src/main/java/de/prob2/jupyter/commands/TableCommand.java b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
index 1043cf3d1c780f98549501f6fe82bbf605f35598..0e335fbbe198c5a593eb3c5ea55f541d083a6533 100644
--- a/src/main/java/de/prob2/jupyter/commands/TableCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
@@ -5,6 +5,7 @@ import java.util.List;
 import java.util.stream.Collectors;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.animator.command.GetAllTableCommands;
 import de.prob.animator.command.GetTableForVisualizationCommand;
@@ -15,6 +16,7 @@ import de.prob.animator.domainobjects.TableData;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
 import de.prob.unicode.UnicodeTranslator;
+import de.prob2.jupyter.ProBKernel;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -23,12 +25,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class TableCommand implements Command {
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private TableCommand(final @NotNull AnimationSelector animationSelector) {
+	private TableCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -50,7 +54,8 @@ public final class TableCommand implements Command {
 	@Override
 	public @NotNull DisplayData run(final @NotNull String argString) {
 		final Trace trace = this.animationSelector.getCurrentTrace();
-		final IEvalElement formula = CommandUtils.withSourceCode(argString, () -> trace.getModel().parseFormula(argString, FormulaExpand.EXPAND));
+		final String code = this.kernelProvider.get().insertLetVariables(argString);
+		final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
 		
 		final GetAllTableCommands cmd1 = new GetAllTableCommands(trace.getCurrentState());
 		trace.getStateSpace().execute(cmd1);
diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
index 6474646c49311f72e0c49fa6fff915a1851c58cb..c90318988850f5ce8f8ff2665f630ea47891d1fd 100644
--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
@@ -1,6 +1,7 @@
 package de.prob2.jupyter.commands;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 
 import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.animator.domainobjects.IEvalElement;
@@ -8,6 +9,7 @@ import de.prob.animator.domainobjects.TypeCheckResult;
 import de.prob.exception.ProBError;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.Trace;
+import de.prob2.jupyter.ProBKernel;
 
 import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
 import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -16,12 +18,14 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class TypeCommand implements Command {
+	private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
 	private final @NotNull AnimationSelector animationSelector;
 	
 	@Inject
-	private TypeCommand(final @NotNull AnimationSelector animationSelector) {
+	private TypeCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
 		super();
 		
+		this.kernelProvider = kernelProvider;
 		this.animationSelector = animationSelector;
 	}
 	
@@ -43,7 +47,8 @@ public final class TypeCommand implements Command {
 	@Override
 	public @NotNull DisplayData run(final @NotNull String argString) {
 		final Trace trace = this.animationSelector.getCurrentTrace();
-		final IEvalElement formula = CommandUtils.withSourceCode(argString, () -> trace.getModel().parseFormula(argString, FormulaExpand.EXPAND));
+		final String code = this.kernelProvider.get().insertLetVariables(argString);
+		final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
 		final TypeCheckResult result = trace.getStateSpace().typeCheck(formula);
 		if (result.isOk()) {
 			return new DisplayData(result.getType());