examples/notebooks/example-01-ws1s-formulae.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "b2e4fbf1",
   "metadata": {},
   "source": [
    "# Example 01: WS1S Logic\n",
    "In this example, we will demonstrate the capabilities of the `libmata` library on usage for deciding WS1S logic. WS1S is a weak monadic second order logic with one sucessor, which means it can quantify over sets and structure with one successor, making it suitable for modelling and reasoning about linear structures.\n",
    "\n",
    "In particular, we will exploit the correspondence between the formulae of the WS1S logic and finite automata. For given formula we will show we can construct an automaton, whose language we can further analyse to decide whether the formula is: (1) satisfiable, i.e., for some words true, for some false; (2) unsatisfiable, i.e., always false; or (3) valid, i.e., always true.\n",
    "\n",
    "In this example, we will limit ourselves to first order variables, such as `x` or `y`. We will encode them as strings, of `0` and `1`, such that the index of the first `1` will correspond to the numerical value of the variable. E.g. the word `0 0 1` corresponds to `2`. For each variable we will have one such column in the string. E.g. we will encode that `x = 3` and `y = 1` as word `00 01 00 10`: the first column corresponds to variable `x` and the second to variable `y`.\n",
    "\n",
    "#### Example formula\n",
    "In this example, we will analyze the decidability of the following formula: $(x = y + 1 \\wedge y = z + 1) \\rightarrow x = z + 2$.\n",
    "\n",
    "The semantics of the binary operator `+` is as expected."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "71098389",
   "metadata": {},
   "outputs": [],
   "source": [
    "import libmata.nfa.nfa as mata_nfa\n",
    "import libmata.alphabets as alphabets\n",
    "from libmata.plotting import plot\n",
    "config = mata_nfa.store()\n",
    "config['alphabet'] = alphabets.OnTheFlyAlphabet()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0ee94caa",
   "metadata": {},
   "source": [
    "#### Atomic formulae\n",
    "First, we will construct automata corresponding to atomic formulae. Since, we have three variables, in each symbol we have three values. Note, that since, we do not use the variable `z` in the first automaton, we \"don't care\" about its value, and hence we add two transitions, one for `z = 0` and one for `z = 1`. In decision procedures this is usually implemented in much more efficient way."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "e03a2033",
   "metadata": {},
   "outputs": [],
   "source": [
    "x_is_y_plus_one = mata_nfa.Nfa(3, label=\"x = y + 1\")\n",
    "x_is_y_plus_one.make_initial_state(0)\n",
    "x_is_y_plus_one.add_transition(0, \"000\", 0)\n",
    "x_is_y_plus_one.add_transition(0, \"001\", 0)\n",
    "x_is_y_plus_one.add_transition(0, \"010\", 1)\n",
    "x_is_y_plus_one.add_transition(0, \"011\", 1)\n",
    "x_is_y_plus_one.add_transition(1, \"100\", 2)\n",
    "x_is_y_plus_one.add_transition(1, \"101\", 2)\n",
    "x_is_y_plus_one.add_transition(2, \"000\", 2)\n",
    "x_is_y_plus_one.add_transition(2, \"001\", 2)\n",
    "x_is_y_plus_one.make_final_state(2)\n",
    "\n",
    "y_is_z_plus_one = mata_nfa.Nfa(3, label=\"y = z + 1\")\n",
    "y_is_z_plus_one.make_initial_state(0)\n",
    "y_is_z_plus_one.add_transition(0, \"000\", 0)\n",
    "y_is_z_plus_one.add_transition(0, \"100\", 0)\n",
    "y_is_z_plus_one.add_transition(0, \"001\", 1)\n",
    "y_is_z_plus_one.add_transition(0, \"101\", 1)\n",
    "y_is_z_plus_one.add_transition(1, \"010\", 2)\n",
    "y_is_z_plus_one.add_transition(1, \"110\", 2)\n",
    "y_is_z_plus_one.add_transition(2, \"000\", 2)\n",
    "y_is_z_plus_one.add_transition(2, \"100\", 2)\n",
    "y_is_z_plus_one.make_final_state(2)\n",
    "\n",
    "x_is_z_plus_two = mata_nfa.Nfa(4, label=\"x = z + 2\")\n",
    "x_is_z_plus_two.make_initial_state(0)\n",
    "x_is_z_plus_two.add_transition(0, \"000\", 0)\n",
    "x_is_z_plus_two.add_transition(0, \"010\", 0)\n",
    "x_is_z_plus_two.add_transition(0, \"001\", 1)\n",
    "x_is_z_plus_two.add_transition(0, \"011\", 1)\n",
    "x_is_z_plus_two.add_transition(1, \"000\", 2)\n",
    "x_is_z_plus_two.add_transition(1, \"010\", 2)\n",
    "x_is_z_plus_two.add_transition(2, \"100\", 3)\n",
    "x_is_z_plus_two.add_transition(2, \"110\", 3)\n",
    "x_is_z_plus_two.add_transition(3, \"000\", 3)\n",
    "x_is_z_plus_two.add_transition(3, \"010\", 3)\n",
    "x_is_z_plus_two.make_final_state(3)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c7b6963c",
   "metadata": {},
   "source": [
    "We will plot all of the resulting automata using the `mata.plot` function"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "10274176",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div style='vertical-align:text-top;display:inline-block;'><?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.43.0 (0)\n",
       " -->\n",
       "<!-- Title: dot Pages: 1 -->\n",
       "<svg width=\"136pt\" height=\"280pt\"\n",
       " viewBox=\"0.00 0.00 136.00 280.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 276)\">\n",
       "<title>dot</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-276 132,-276 132,4 -4,4\"/>\n",
       "<text text-anchor=\"middle\" x=\"64\" y=\"-256.8\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">x = y + 1</text>\n",
       "<!-- q0 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>q0</title>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-165\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-161.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
       "</g>\n",
       "<!-- q0&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>q0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-212.85C27,-204.71 27,-194.93 27,-186.42\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-186.2 27,-176.2 23.5,-186.2 30.5,-186.2\"/>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M37.41,-169.38C46.44,-171.38 56,-169.92 56,-165 56,-162 52.45,-160.29 47.63,-159.86\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"47.12,-156.39 37.41,-160.62 47.64,-163.37 47.12,-156.39\"/>\n",
       "<text text-anchor=\"start\" x=\"56\" y=\"-161.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 001</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-92\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-88.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-153.83C27,-143.28 27,-126.52 27,-113.26\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-113.15 27,-103.15 23.5,-113.15 30.5,-113.15\"/>\n",
       "<text text-anchor=\"start\" x=\"27\" y=\"-124.8\" font-family=\"Times,serif\" font-size=\"14.00\">010 | 011</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-15\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-15\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-11.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;2 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-80.89C27,-70.54 27,-54.07 27,-40.32\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-40.04 27,-30.04 23.5,-40.04 30.5,-40.04\"/>\n",
       "<text text-anchor=\"start\" x=\"27\" y=\"-51.8\" font-family=\"Times,serif\" font-size=\"14.00\">100 | 101</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>2&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M40.56,-21.69C50.3,-23.87 60,-21.64 60,-15 60,-10.75 56.02,-8.3 50.6,-7.67\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"50.32,-4.18 40.56,-8.31 50.76,-11.16 50.32,-4.18\"/>\n",
       "<text text-anchor=\"start\" x=\"60\" y=\"-11.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 001</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n",
       "</div><div style='vertical-align:text-top;display:inline-block;'><?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.43.0 (0)\n",
       " -->\n",
       "<!-- Title: dot Pages: 1 -->\n",
       "<svg width=\"136pt\" height=\"280pt\"\n",
       " viewBox=\"0.00 0.00 136.00 280.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 276)\">\n",
       "<title>dot</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-276 132,-276 132,4 -4,4\"/>\n",
       "<text text-anchor=\"middle\" x=\"64\" y=\"-256.8\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">y = z + 1</text>\n",
       "<!-- q0 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>q0</title>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-165\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-161.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
       "</g>\n",
       "<!-- q0&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>q0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-212.85C27,-204.71 27,-194.93 27,-186.42\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-186.2 27,-176.2 23.5,-186.2 30.5,-186.2\"/>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M37.41,-169.38C46.44,-171.38 56,-169.92 56,-165 56,-162 52.45,-160.29 47.63,-159.86\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"47.12,-156.39 37.41,-160.62 47.64,-163.37 47.12,-156.39\"/>\n",
       "<text text-anchor=\"start\" x=\"56\" y=\"-161.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 100</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-92\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-88.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-153.83C27,-143.28 27,-126.52 27,-113.26\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-113.15 27,-103.15 23.5,-113.15 30.5,-113.15\"/>\n",
       "<text text-anchor=\"start\" x=\"27\" y=\"-124.8\" font-family=\"Times,serif\" font-size=\"14.00\">001 | 101</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-15\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-15\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-11.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;2 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-80.89C27,-70.54 27,-54.07 27,-40.32\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-40.04 27,-30.04 23.5,-40.04 30.5,-40.04\"/>\n",
       "<text text-anchor=\"start\" x=\"27\" y=\"-51.8\" font-family=\"Times,serif\" font-size=\"14.00\">010 | 110</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>2&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M40.56,-21.69C50.3,-23.87 60,-21.64 60,-15 60,-10.75 56.02,-8.3 50.6,-7.67\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"50.32,-4.18 40.56,-8.31 50.76,-11.16 50.32,-4.18\"/>\n",
       "<text text-anchor=\"start\" x=\"60\" y=\"-11.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 100</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n",
       "</div><div style='vertical-align:text-top;display:inline-block;'><?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.43.0 (0)\n",
       " -->\n",
       "<!-- Title: dot Pages: 1 -->\n",
       "<svg width=\"136pt\" height=\"353pt\"\n",
       " viewBox=\"0.00 0.00 136.00 353.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 349)\">\n",
       "<title>dot</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-349 132,-349 132,4 -4,4\"/>\n",
       "<text text-anchor=\"middle\" x=\"64\" y=\"-329.8\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">x = z + 2</text>\n",
       "<!-- q0 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>q0</title>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-238\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-234.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
       "</g>\n",
       "<!-- q0&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>q0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-285.85C27,-277.71 27,-267.93 27,-259.42\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-259.2 27,-249.2 23.5,-259.2 30.5,-259.2\"/>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M37.41,-242.38C46.44,-244.38 56,-242.92 56,-238 56,-235 52.45,-233.29 47.63,-232.86\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"47.12,-229.39 37.41,-233.62 47.64,-236.37 47.12,-229.39\"/>\n",
       "<text text-anchor=\"start\" x=\"56\" y=\"-234.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 010</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-165\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-161.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-226.83C27,-216.28 27,-199.52 27,-186.26\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-186.15 27,-176.15 23.5,-186.15 30.5,-186.15\"/>\n",
       "<text text-anchor=\"start\" x=\"27\" y=\"-197.8\" font-family=\"Times,serif\" font-size=\"14.00\">001 | 011</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-92\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-88.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;2 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-153.83C27,-143.28 27,-126.52 27,-113.26\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-113.15 27,-103.15 23.5,-113.15 30.5,-113.15\"/>\n",
       "<text text-anchor=\"start\" x=\"27\" y=\"-124.8\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 010</text>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-15\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-15\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-11.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-80.89C27,-70.54 27,-54.07 27,-40.32\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-40.04 27,-30.04 23.5,-40.04 30.5,-40.04\"/>\n",
       "<text text-anchor=\"start\" x=\"27\" y=\"-51.8\" font-family=\"Times,serif\" font-size=\"14.00\">100 | 110</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;3 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>3&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M40.56,-21.69C50.3,-23.87 60,-21.64 60,-15 60,-10.75 56.02,-8.3 50.6,-7.67\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"50.32,-4.18 40.56,-8.31 50.76,-11.16 50.32,-4.18\"/>\n",
       "<text text-anchor=\"start\" x=\"60\" y=\"-11.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 010</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n",
       "</div>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "plot(x_is_y_plus_one, y_is_z_plus_one, x_is_z_plus_two)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fd36703f",
   "metadata": {},
   "source": [
    "#### Logical connectives\n",
    "\n",
    "By induction on the structure of the formulae we construct the more complex automata. First, we will construct the automaton corresponding to the premise of the implication. The logical `and` corresponds to the intersection of the automata."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "b633e7e5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div style='vertical-align:text-top;display:inline-block;'><?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.43.0 (0)\n",
       " -->\n",
       "<!-- Title: dot Pages: 1 -->\n",
       "<svg width=\"178pt\" height=\"353pt\"\n",
       " viewBox=\"0.00 0.00 178.00 353.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 349)\">\n",
       "<title>dot</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-349 174,-349 174,4 -4,4\"/>\n",
       "<text text-anchor=\"middle\" x=\"85\" y=\"-329.8\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">x = y + 1 ∧ y = z + 1</text>\n",
       "<!-- q0 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>q0</title>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"68\" cy=\"-238\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"68\" y=\"-234.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
       "</g>\n",
       "<!-- q0&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>q0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M68,-285.85C68,-277.71 68,-267.93 68,-259.42\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"71.5,-259.2 68,-249.2 64.5,-259.2 71.5,-259.2\"/>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M78.41,-242.38C87.44,-244.38 97,-242.92 97,-238 97,-235 93.45,-233.29 88.63,-232.86\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"88.12,-229.39 78.41,-233.62 88.64,-236.37 88.12,-229.39\"/>\n",
       "<text text-anchor=\"start\" x=\"97\" y=\"-234.3\" font-family=\"Times,serif\" font-size=\"14.00\">000</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"68\" cy=\"-165\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"68\" y=\"-161.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M68,-226.83C68,-216.28 68,-199.52 68,-186.26\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"71.5,-186.15 68,-176.15 64.5,-186.15 71.5,-186.15\"/>\n",
       "<text text-anchor=\"start\" x=\"68\" y=\"-197.8\" font-family=\"Times,serif\" font-size=\"14.00\">001</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"68\" cy=\"-92\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"68\" y=\"-88.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;2 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M68,-153.83C68,-143.28 68,-126.52 68,-113.26\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"71.5,-113.15 68,-103.15 64.5,-113.15 71.5,-113.15\"/>\n",
       "<text text-anchor=\"start\" x=\"68\" y=\"-124.8\" font-family=\"Times,serif\" font-size=\"14.00\">010</text>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"68\" cy=\"-15\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"68\" cy=\"-15\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"68\" y=\"-11.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M68,-80.89C68,-70.54 68,-54.07 68,-40.32\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"71.5,-40.04 68,-30.04 64.5,-40.04 71.5,-40.04\"/>\n",
       "<text text-anchor=\"start\" x=\"68\" y=\"-51.8\" font-family=\"Times,serif\" font-size=\"14.00\">100</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;3 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>3&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M81.56,-21.69C91.3,-23.87 101,-21.64 101,-15 101,-10.75 97.02,-8.3 91.6,-7.67\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"91.32,-4.18 81.56,-8.31 91.76,-11.16 91.32,-4.18\"/>\n",
       "<text text-anchor=\"start\" x=\"101\" y=\"-11.3\" font-family=\"Times,serif\" font-size=\"14.00\">000</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n",
       "</div>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "premise = mata_nfa.intersection(x_is_y_plus_one, y_is_z_plus_one)\n",
    "premise.label = \"x = y + 1 ∧ y = z + 1\"\n",
    "plot(premise)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6a74876c",
   "metadata": {},
   "source": [
    "Since, there is no corresponding operation for an logical implication, we use one of the laws to simplify the implication $A \\rightarrow B$ to $\\neg A \\vee B$\n",
    "\n",
    "Hence, we next complement the premise automaton. Note, that we need to supply the alphabet to perform the complementation. Since, we have not set any alphabet for this example, a default alphabet is used, that maps the seen strings to unique identifications."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "b9b1721f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div style='vertical-align:text-top;display:inline-block;'><?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.43.0 (0)\n",
       " -->\n",
       "<!-- Title: dot Pages: 1 -->\n",
       "<svg width=\"950pt\" height=\"450pt\"\n",
       " viewBox=\"0.00 0.00 949.51 450.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 446)\">\n",
       "<title>dot</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-446 945.51,-446 945.51,4 -4,4\"/>\n",
       "<text text-anchor=\"middle\" x=\"470.75\" y=\"-426.8\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">¬(x = y + 1 ∧ y = z + 1)</text>\n",
       "<!-- q0 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>q0</title>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"628.51\" cy=\"-331\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"628.51\" cy=\"-331\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"628.51\" y=\"-327.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
       "</g>\n",
       "<!-- q0&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>q0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M628.51,-382.84C628.51,-374.78 628.51,-365.04 628.51,-356.25\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"632.01,-356.17 628.51,-346.17 625.01,-356.17 632.01,-356.17\"/>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M642.75,-336.47C652.26,-338.01 661.51,-336.19 661.51,-331 661.51,-327.76 657.89,-325.83 652.86,-325.22\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"652.64,-321.72 642.75,-325.53 652.86,-328.72 652.64,-321.72\"/>\n",
       "<text text-anchor=\"start\" x=\"661.51\" y=\"-327.3\" font-family=\"Times,serif\" font-size=\"14.00\">000</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"506.51\" cy=\"-250\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"506.51\" cy=\"-250\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"506.51\" y=\"-246.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M616.36,-322.14C595.64,-308.72 553.22,-281.25 527.58,-264.65\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"529.26,-261.56 518.97,-259.07 525.46,-267.44 529.26,-261.56\"/>\n",
       "<text text-anchor=\"start\" x=\"577.51\" y=\"-286.8\" font-family=\"Times,serif\" font-size=\"14.00\">001</text>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"377.51\" cy=\"-15\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"377.51\" cy=\"-15\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"377.51\" y=\"-11.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">4</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;4 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M643.59,-327.6C676.44,-321.42 751.51,-301.76 751.51,-251 751.51,-251 751.51,-251 751.51,-91 751.51,-19.7 486.9,-15.28 402.82,-15.68\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"402.61,-12.18 392.63,-15.76 402.66,-19.18 402.61,-12.18\"/>\n",
       "<text text-anchor=\"start\" x=\"751.51\" y=\"-165.3\" font-family=\"Times,serif\" font-size=\"14.00\">010 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"248.51\" cy=\"-169\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"248.51\" cy=\"-169\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"248.51\" y=\"-165.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;2 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>1&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M492.27,-244.64C450.07,-231.72 325.33,-193.52 272.54,-177.36\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"273.29,-173.93 262.7,-174.35 271.24,-180.62 273.29,-173.93\"/>\n",
       "<text text-anchor=\"start\" x=\"400.51\" y=\"-205.8\" font-family=\"Times,serif\" font-size=\"14.00\">010</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;4 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>1&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M506.98,-234.92C507.93,-199.25 508.73,-106.32 492.51,-81 471.87,-48.78 429.28,-30.95 402.12,-22.44\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"402.79,-18.98 392.21,-19.53 400.82,-25.7 402.79,-18.98\"/>\n",
       "<text text-anchor=\"start\" x=\"504.51\" y=\"-124.8\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 001 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"79.51\" cy=\"-92\" rx=\"11\" ry=\"11\"/>\n",
       "<text text-anchor=\"middle\" x=\"79.51\" y=\"-88.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M234.96,-161.99C205.01,-148.7 133.07,-116.77 98.58,-101.46\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"99.73,-98.14 89.17,-97.29 96.89,-104.54 99.73,-98.14\"/>\n",
       "<text text-anchor=\"start\" x=\"174.51\" y=\"-124.8\" font-family=\"Times,serif\" font-size=\"14.00\">100</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>2&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M247.23,-153.98C246.29,-135.56 247.22,-102.98 262.51,-81 284.36,-49.59 326.58,-31.51 353.34,-22.73\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"354.57,-26.01 363.09,-19.72 352.5,-19.33 354.57,-26.01\"/>\n",
       "<text text-anchor=\"start\" x=\"262.51\" y=\"-88.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 001 | 010 | 011 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;3 -->\n",
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>3&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M89.31,-97.46C98.52,-100.29 108.51,-98.47 108.51,-92 108.51,-87.96 104.61,-85.73 99.43,-85.32\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"98.82,-81.87 89.31,-86.54 99.66,-88.82 98.82,-81.87\"/>\n",
       "<text text-anchor=\"start\" x=\"108.51\" y=\"-88.3\" font-family=\"Times,serif\" font-size=\"14.00\">000</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;4 -->\n",
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>3&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M68.55,-89.12C43.14,-84.33 -16.09,-70.45 4.51,-48 27.96,-22.45 271.64,-17.26 351.98,-16.24\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"352.23,-19.74 362.19,-16.12 352.15,-12.74 352.23,-19.74\"/>\n",
       "<text text-anchor=\"start\" x=\"4.51\" y=\"-51.8\" font-family=\"Times,serif\" font-size=\"14.00\">001 | 010 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;4 -->\n",
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>4&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M391.07,-21.69C400.81,-23.87 410.51,-21.64 410.51,-15 410.51,-10.75 406.53,-8.3 401.1,-7.67\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"400.82,-4.18 391.07,-8.31 401.27,-11.16 400.82,-4.18\"/>\n",
       "<text text-anchor=\"start\" x=\"410.51\" y=\"-11.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 001 | 010 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n",
       "</div>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "not_premise = mata_nfa.complement(premise, alphabet=config['alphabet'])\n",
    "not_premise.label = \"¬(x = y + 1 ∧ y = z + 1)\"\n",
    "plot(not_premise)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "970137fd",
   "metadata": {},
   "source": [
    "Finally, we do the union of the complemented premise with the last atomic automaton. We further determinize the result to obtain complete and deterministic automaton."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "21b2a1e6",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div style='vertical-align:text-top;display:inline-block;'><?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.43.0 (0)\n",
       " -->\n",
       "<!-- Title: dot Pages: 1 -->\n",
       "<svg width=\"1243pt\" height=\"539pt\"\n",
       " viewBox=\"0.00 0.00 1243.00 539.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 535)\">\n",
       "<title>dot</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-535 1239,-535 1239,4 -4,4\"/>\n",
       "<text text-anchor=\"middle\" x=\"617.5\" y=\"-515.8\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">¬(x = y + 1 ∧ y = z + 1) ∨ x = z + 2</text>\n",
       "<!-- q0 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>q0</title>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"216\" cy=\"-420\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"216\" cy=\"-420\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"216\" y=\"-416.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
       "</g>\n",
       "<!-- q0&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>q0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M216,-471.84C216,-463.78 216,-454.04 216,-445.25\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"219.5,-445.17 216,-435.17 212.5,-445.17 219.5,-445.17\"/>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M230.25,-425.47C239.75,-427.01 249,-425.19 249,-420 249,-416.76 245.39,-414.83 240.36,-414.22\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"240.13,-410.72 230.25,-414.53 240.35,-417.72 240.13,-410.72\"/>\n",
       "<text text-anchor=\"start\" x=\"249\" y=\"-416.3\" font-family=\"Times,serif\" font-size=\"14.00\">000</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"418\" cy=\"-339\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"418\" cy=\"-339\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"418\" y=\"-335.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M229.88,-413.57C264.06,-400.21 352.53,-365.6 394.82,-349.06\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"396.25,-352.27 404.29,-345.36 393.7,-345.75 396.25,-352.27\"/>\n",
       "<text text-anchor=\"start\" x=\"335\" y=\"-375.8\" font-family=\"Times,serif\" font-size=\"14.00\">001</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"124\" cy=\"-339\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"124\" cy=\"-339\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"124\" y=\"-335.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">2</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M205.09,-409.63C189.66,-396.38 161.28,-372.01 142.52,-355.91\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"144.77,-353.22 134.9,-349.36 140.21,-358.53 144.77,-353.22\"/>\n",
       "<text text-anchor=\"start\" x=\"178\" y=\"-375.8\" font-family=\"Times,serif\" font-size=\"14.00\">010</text>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>3</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"261\" cy=\"-258\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"261\" cy=\"-258\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"261\" y=\"-254.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">3</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;3 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>0&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M219.84,-405.36C227.51,-378.08 244.82,-316.53 254.37,-282.58\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"257.83,-283.18 257.17,-272.61 251.1,-281.29 257.83,-283.18\"/>\n",
       "<text text-anchor=\"start\" x=\"242\" y=\"-335.3\" font-family=\"Times,serif\" font-size=\"14.00\">011</text>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"375\" cy=\"-15\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"375\" cy=\"-15\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"375\" y=\"-11.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">4</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;4 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>0&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M201.15,-416.87C152.35,-409.47 0,-382.92 0,-340 0,-340 0,-340 0,-95 0,-23.37 265.32,-16.35 349.62,-15.92\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"349.84,-19.42 359.84,-15.9 349.83,-12.42 349.84,-19.42\"/>\n",
       "<text text-anchor=\"start\" x=\"0\" y=\"-213.8\" font-family=\"Times,serif\" font-size=\"14.00\">100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;4 -->\n",
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>1&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M433.19,-337.73C528.94,-335.84 1045,-322.7 1045,-259 1045,-259 1045,-259 1045,-95 1045,-28.84 523.08,-17.93 400.53,-16.28\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"400.3,-12.77 390.25,-16.15 400.21,-19.77 400.3,-12.77\"/>\n",
       "<text text-anchor=\"start\" x=\"1045\" y=\"-173.3\" font-family=\"Times,serif\" font-size=\"14.00\">001 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 5 -->\n",
       "<g id=\"node7\" class=\"node\">\n",
       "<title>5</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"393\" cy=\"-177\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"393\" cy=\"-177\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"393\" y=\"-173.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">5</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;5 -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>1&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M415.83,-324.08C411.56,-296.78 402.05,-235.9 396.75,-201.99\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"400.19,-201.34 395.19,-192 393.27,-202.42 400.19,-201.34\"/>\n",
       "<text text-anchor=\"start\" x=\"407\" y=\"-254.3\" font-family=\"Times,serif\" font-size=\"14.00\">000</text>\n",
       "</g>\n",
       "<!-- 7 -->\n",
       "<g id=\"node9\" class=\"node\">\n",
       "<title>7</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"676\" cy=\"-258\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"676\" cy=\"-258\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"676\" y=\"-254.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">7</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;7 -->\n",
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>1&#45;&gt;7</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M432.24,-333.64C474.44,-320.72 599.18,-282.52 651.97,-266.36\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"653.27,-269.62 661.81,-263.35 651.22,-262.93 653.27,-269.62\"/>\n",
       "<text text-anchor=\"start\" x=\"570\" y=\"-294.8\" font-family=\"Times,serif\" font-size=\"14.00\">010</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;2 -->\n",
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>2&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M137.56,-345.69C147.3,-347.87 157,-345.64 157,-339 157,-334.75 153.02,-332.3 147.6,-331.67\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"147.32,-328.18 137.56,-332.31 147.76,-335.16 147.32,-328.18\"/>\n",
       "<text text-anchor=\"start\" x=\"157\" y=\"-335.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 010</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M134.13,-327.48C144.58,-317.1 161.76,-301.33 179,-291 197.35,-280.01 220.14,-271.47 237.04,-265.99\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"238.2,-269.3 246.7,-262.98 236.11,-262.61 238.2,-269.3\"/>\n",
       "<text text-anchor=\"start\" x=\"179\" y=\"-294.8\" font-family=\"Times,serif\" font-size=\"14.00\">001 | 011</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;4 -->\n",
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>2&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M124,-323.73C124,-307.91 124,-281.63 124,-259 124,-259 124,-259 124,-95 124,-47.93 286.65,-25.45 350.09,-18.47\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"350.48,-21.95 360.05,-17.41 349.74,-14.99 350.48,-21.95\"/>\n",
       "<text text-anchor=\"start\" x=\"124\" y=\"-173.3\" font-family=\"Times,serif\" font-size=\"14.00\">100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;4 -->\n",
       "<g id=\"edge14\" class=\"edge\">\n",
       "<title>3&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M261.65,-242.91C261.79,-222.21 258.83,-183.71 237,-162 213.3,-138.44 184.61,-170.31 164,-144 159.89,-138.75 160.88,-134.89 164,-129 201.59,-57.95 302.84,-29.76 350.09,-20.22\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"350.92,-23.62 360.09,-18.32 349.61,-16.75 350.92,-23.62\"/>\n",
       "<text text-anchor=\"start\" x=\"164\" y=\"-132.8\" font-family=\"Times,serif\" font-size=\"14.00\">001 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;5 -->\n",
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>3&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M271.68,-247.08C283.03,-236.87 301.84,-220.96 320,-210 335.79,-200.47 354.92,-192.2 369.63,-186.45\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"370.91,-189.7 379.02,-182.89 368.43,-183.16 370.91,-189.7\"/>\n",
       "<text text-anchor=\"start\" x=\"320\" y=\"-213.8\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 010</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;4 -->\n",
       "<g id=\"edge15\" class=\"edge\">\n",
       "<title>4&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M388.56,-21.69C398.3,-23.87 408,-21.64 408,-15 408,-10.75 404.02,-8.3 398.6,-7.67\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"398.32,-4.18 388.56,-8.31 398.76,-11.16 398.32,-4.18\"/>\n",
       "<text text-anchor=\"start\" x=\"408\" y=\"-11.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 001 | 010 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;4 -->\n",
       "<g id=\"edge16\" class=\"edge\">\n",
       "<title>5&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M386.8,-163.19C380.89,-152.39 370.99,-137.39 358,-129 326.66,-108.76 299.38,-140.07 276,-111 248.03,-76.22 314.04,-41.46 351.45,-25.32\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"353.25,-28.36 361.13,-21.28 350.56,-21.9 353.25,-28.36\"/>\n",
       "<text text-anchor=\"start\" x=\"276\" y=\"-92.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 001 | 010 | 011 | 101</text>\n",
       "</g>\n",
       "<!-- 6 -->\n",
       "<g id=\"node8\" class=\"node\">\n",
       "<title>6</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"711\" cy=\"-96\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"711\" cy=\"-96\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"711\" y=\"-92.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">6</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;6 -->\n",
       "<g id=\"edge17\" class=\"edge\">\n",
       "<title>5&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M407.47,-171.99C438.76,-163.39 515.18,-142.85 580,-129 625.02,-119.38 638.19,-125.14 682,-111 684.33,-110.25 686.72,-109.34 689.07,-108.36\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"690.73,-111.45 698.32,-104.06 687.78,-105.1 690.73,-111.45\"/>\n",
       "<text text-anchor=\"start\" x=\"580\" y=\"-132.8\" font-family=\"Times,serif\" font-size=\"14.00\">100 | 110</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;4 -->\n",
       "<g id=\"edge19\" class=\"edge\">\n",
       "<title>6&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M698,-87.9C693.1,-85.44 687.4,-82.84 682,-81 580.44,-46.3 453.4,-26.52 400.23,-19.24\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"400.42,-15.73 390.04,-17.87 399.49,-22.67 400.42,-15.73\"/>\n",
       "<text text-anchor=\"start\" x=\"616\" y=\"-51.8\" font-family=\"Times,serif\" font-size=\"14.00\">001 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;6 -->\n",
       "<g id=\"edge18\" class=\"edge\">\n",
       "<title>6&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M724.56,-102.69C734.3,-104.87 744,-102.64 744,-96 744,-91.75 740.02,-89.3 734.6,-88.67\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"734.32,-85.18 724.56,-89.31 734.76,-92.16 734.32,-85.18\"/>\n",
       "<text text-anchor=\"start\" x=\"744\" y=\"-92.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 010</text>\n",
       "</g>\n",
       "<!-- 7&#45;&gt;4 -->\n",
       "<g id=\"edge20\" class=\"edge\">\n",
       "<title>7&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M688.26,-248.8C733.47,-217.71 884.5,-105.97 810,-48 777.62,-22.8 488.28,-17.33 400.28,-16.25\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"400.17,-12.75 390.13,-16.13 400.09,-19.75 400.17,-12.75\"/>\n",
       "<text text-anchor=\"start\" x=\"815\" y=\"-132.8\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 001 | 010 | 011 | 101</text>\n",
       "</g>\n",
       "<!-- 7&#45;&gt;6 -->\n",
       "<g id=\"edge22\" class=\"edge\">\n",
       "<title>7&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M679.04,-243.08C685.02,-215.78 698.33,-154.9 705.75,-120.99\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"709.22,-121.52 707.94,-111 702.38,-120.02 709.22,-121.52\"/>\n",
       "<text text-anchor=\"start\" x=\"696\" y=\"-173.3\" font-family=\"Times,serif\" font-size=\"14.00\">110</text>\n",
       "</g>\n",
       "<!-- 8 -->\n",
       "<g id=\"node10\" class=\"node\">\n",
       "<title>8</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"614\" cy=\"-177\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"614\" cy=\"-177\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"614\" y=\"-173.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">8</text>\n",
       "</g>\n",
       "<!-- 7&#45;&gt;8 -->\n",
       "<g id=\"edge21\" class=\"edge\">\n",
       "<title>7&#45;&gt;8</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M667.12,-245.68C657.26,-233.13 641.19,-212.65 629.3,-197.5\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"631.79,-195 622.87,-189.3 626.29,-199.33 631.79,-195\"/>\n",
       "<text text-anchor=\"start\" x=\"650\" y=\"-213.8\" font-family=\"Times,serif\" font-size=\"14.00\">100</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;4 -->\n",
       "<g id=\"edge24\" class=\"edge\">\n",
       "<title>8&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M600.69,-170.02C578.24,-159.63 531.9,-136.88 497,-111 481.6,-99.58 480.73,-93.27 466,-81 442.93,-61.78 414.51,-42.05 395.63,-29.45\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"397.47,-26.47 387.2,-23.87 393.61,-32.31 397.47,-26.47\"/>\n",
       "<text text-anchor=\"start\" x=\"497\" y=\"-92.3\" font-family=\"Times,serif\" font-size=\"14.00\">001 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;6 -->\n",
       "<g id=\"edge25\" class=\"edge\">\n",
       "<title>8&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M624.81,-166.45C635.79,-156.83 653.36,-141.62 669,-129 676.02,-123.33 683.85,-117.29 690.83,-112\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"693.21,-114.6 699.1,-105.79 689,-109 693.21,-114.6\"/>\n",
       "<text text-anchor=\"start\" x=\"669\" y=\"-132.8\" font-family=\"Times,serif\" font-size=\"14.00\">010</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;8 -->\n",
       "<g id=\"edge23\" class=\"edge\">\n",
       "<title>8&#45;&gt;8</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M627.56,-183.69C637.3,-185.87 647,-183.64 647,-177 647,-172.75 643.02,-170.3 637.6,-169.67\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"637.32,-166.18 627.56,-170.31 637.76,-173.16 637.32,-166.18\"/>\n",
       "<text text-anchor=\"start\" x=\"647\" y=\"-173.3\" font-family=\"Times,serif\" font-size=\"14.00\">000</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n",
       "</div>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "formula = mata_nfa.determinize(mata_nfa.union(not_premise, x_is_z_plus_two))\n",
    "formula.label = \"¬(x = y + 1 ∧ y = z + 1) ∨ x = z + 2\"\n",
    "plot(formula)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a9d3cbf1",
   "metadata": {},
   "source": [
    "#### Minimization of the result\n",
    "However, the resulting automaton is too complex. Hence, we try to minimize the results to merge equivalent (from the language perspective) states."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "5ffdd34e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div style='vertical-align:text-top;display:inline-block;'><?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.43.0 (0)\n",
       " -->\n",
       "<!-- Title: dot Pages: 1 -->\n",
       "<svg width=\"339pt\" height=\"134pt\"\n",
       " viewBox=\"0.00 0.00 339.00 134.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 130)\">\n",
       "<title>dot</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-130 335,-130 335,4 -4,4\"/>\n",
       "<text text-anchor=\"middle\" x=\"165.5\" y=\"-110.8\" font-family=\"Helvetica,sans-Serif\" font-size=\"14.00\">¬(x = y + 1 ∧ y = z + 1) ∨ x = z + 2</text>\n",
       "<!-- q0 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>q0</title>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"lightsteelblue\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-15\" rx=\"11\" ry=\"11\"/>\n",
       "<ellipse fill=\"none\" stroke=\"darkblue\" stroke-width=\"1.5\" cx=\"27\" cy=\"-15\" rx=\"15\" ry=\"15\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-11.9\" font-family=\"Courier,monospace\" font-weight=\"bold\" font-size=\"12.00\">0</text>\n",
       "</g>\n",
       "<!-- q0&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>q0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M27,-66.84C27,-58.78 27,-49.04 27,-40.25\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"30.5,-40.17 27,-30.17 23.5,-40.17 30.5,-40.17\"/>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"midnightblue\" stroke-width=\"1.5\" d=\"M41.25,-20.47C50.75,-22.01 60,-20.19 60,-15 60,-11.76 56.39,-9.83 51.36,-9.22\"/>\n",
       "<polygon fill=\"midnightblue\" stroke=\"midnightblue\" stroke-width=\"1.5\" points=\"51.13,-5.72 41.25,-9.53 51.35,-12.72 51.13,-5.72\"/>\n",
       "<text text-anchor=\"start\" x=\"60\" y=\"-11.3\" font-family=\"Times,serif\" font-size=\"14.00\">000 | 001 | 010 | 011 | 100 | 101 | 110</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n",
       "</div>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "minimized_formula = mata_nfa.minimize(formula)\n",
    "minimized_formula.label = \"¬(x = y + 1 ∧ y = z + 1) ∨ x = z + 2\"\n",
    "plot(minimized_formula)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3a92199f",
   "metadata": {},
   "source": [
    "#### The final result\n",
    "One can see that the resulting automaton is universal. I.e., it accepts everyting. This means, that the original formula $(x = y + 1 \\wedge y = z + 1) \\rightarrow x = z + 2$ is tautology.\n",
    "\n",
    "We can verify our observation using the `is_universal` test implemented in the `libmata`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "157032f9",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "minimized_formula.is_universal(config['alphabet'])"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}