docs/notebooks/Creating and verifying a ROS node in Imandra.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "![Imandrabot](../images/kostya_ros_medium_1.png)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*At AI, we've been working on an IML (Imandra Modelling Language) interface to ROS, allowing one to develop ROS nodes and use Imandra to verify their properties. In this notebook, we will go through creation and verification of a Robotic Operating System (ROS) node in Imandra. We will make a robot control node that controls the motion of a simple 2-wheeler bot:*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "![Imandrabot](../images/Imandrabot.png)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We'll create a controller that uses the laser scanner to avoid obstacles and drive around the scene. The Imandra ML code can be compiled in OCaml and plugged into the ROS system - the behaviour of the bot can be observed in the Gazebo simulator.\n",
    "\n",
    "Then we'll illustrate how to use Imandra to formally verify various statements about the model and how to find bugs and corner cases by exploring the Imandra-generated counterexamples for false conjectures."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 1. ROS message OCaml types"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For our Imandra-ROS project we’ve processed all the standard ROS messages with our code generation tool creating a collection of strongly-typed IML/OCaml bindings for them. But, in order to keep this notebook self-contained we'll define the necessary messaging modules here.  \n",
    "\n",
    "First, we'll need to declare the message type that will control our robot. This is typically done with a `Twist` message from the `geometry_msgs` standard ROS package. We want to mimic ROS messaging nomenclauture as close as possible, so we'll create an OCaml/Imadra `module` with the same name as the package and will place the necessary type/message declaraions inside:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "module Geometry_msgs :\n",
       "  sig\n",
       "    type vector3 = { vector3_x : int; vector3_y : int; vector3_z : int; }\n",
       "    type twist = { twist_linear : vector3; twist_angular : vector3; }\n",
       "  end\n"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "module Geometry_msgs = struct\n",
    "  type vector3 = \n",
    "    { vector3_x : int\n",
    "    ; vector3_y : int\n",
    "    ; vector3_z : int\n",
    "    }\n",
    "  type twist = \n",
    "    { twist_linear  : vector3\n",
    "    ; twist_angular : vector3\n",
    "    }    \n",
    "end"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "You might have noticed that we've replaced floating point values for vector coordinates with integers. In this context, it is more straight-forward for Imandra to reason about integers, so we assume that there is a common factor of 100,000 multiplying all the incoming floating point values and divides all the outgoing integers. (That effectively makes our unit of measurement of length to be 10 micrometres).\n",
    "\n",
    "Let's move on and declare the incoming messages: \n",
    " - `LaserScan` sensor input message from the `sensor_msgs` ROS package\n",
    " - and the `Clock` message from the `Rosgraph_msg` ROS package  \n",
    " \n",
    "We define the wrapping modules for both messages and declare their datatypes:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "module Sensor_msgs :\n",
       "  sig\n",
       "    type laserScan = {\n",
       "      laserScan_range_min : int;\n",
       "      laserScan_range_max : int;\n",
       "      laserScan_ranges : int list;\n",
       "    }\n",
       "  end\n",
       "module Rosgraph_msgs :\n",
       "  sig\n",
       "    type time = { seconds : int; nanoseconds : int; }\n",
       "    type clock = { clock : time; }\n",
       "  end\n"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "module Sensor_msgs = struct\n",
    "  type laserScan = \n",
    "    { laserScan_range_min : int \n",
    "    ; laserScan_range_max : int \n",
    "    ; laserScan_ranges : int list \n",
    "    }\n",
    "end\n",
    "module Rosgraph_msgs = struct\n",
    "  type time = \n",
    "    { seconds     : int\n",
    "    ; nanoseconds : int\n",
    "    }\n",
    "  type clock = { clock : time }\n",
    "end"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Robotics OS middleware will communicate with our node via messages of these three types. The code that we'll write for of our node will represent the formal mathematical model of the controller algorithm - we can use Imandra to reason and verify various statements about the code. Since IML is valid OCaml, we'll leverage its compiler to create an executable from the verified IML code."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 2. Creating a simple ROS Node model"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We want to create some simple but non-trivial robot controller that makes our bot drive around avoiding the obstacles. The bot is going to drive forward until one of the laser scanner ranges becomes too low, meaning that we've gotten too close to some obstacle - in that case, we want the bot to stop and turn until the scanner tells us that the road ahead is clear. To make the model a bit more complicated, we'd like to implement the ability to choose the turning direction depending on the laser scanner ranges.\n",
    "\n",
    "One might try to make a \"naive\" controller that doesn't have any memory about its previous states and observations - such a bot reacts to the currently observed scanner values and decides its actions based solely on that information. Such an approach will quickly lead to the bot being \"stuck\" in infinite oscillatory loops. E.g. here is a bot that decides which side to turn depending on the first value in the `ranges` array:"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "![Imandrabot](../images/Stuck.gif)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To avoid this kind of oscillations we need the model to have some memory of its previous states. The idea is to introduce two modes of model's operation: driving forward and turning in one place. The bot is in the \"driving\" mode by default, but it can transition to the turning mode if it gets dangerously close to surrounding objects.\n",
    "\n",
    "The turning direction is calculated using the direction of the minimum of the distances that the scanner returns. While the robot is turning in one place, it stores the minimal range that the scanner has detected at that location. If at some point the scanner detects a range that is lower than the stored one - the turning direction gets recalculated, and the minimal range gets updated."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 2.1 State datatype"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Working with Imandra we’ve adopted a standard way to construct formal models of message-driven systems. At the top of the model we have a single OCaml datatype that holds all the data needed to describe the system at a given moment, including incoming and outgoing messages. We call this record type `state`. Together with this `state` type we define a `one_step` transition `state -> state` function, which performs a single logically isolated step of the simulation and returns the new `state` after the transition."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As an example, consider an IML/OCaml type declaration for a simple ROS node that is able to accept `rosgraph_msgs/Clock` and `sensor_msgs/LaserScan` standard ROS messages. We also want the state to store three values: \n",
    " - the current mode of the bot -- whether we are driving forward or turning in a preferred direction\n",
    " - the latest minimal value of the ranges that the laser sensor returns\n",
    " - the preferred side for the robot to turn -- either clockwise (`CW`) or counter-clockwise (`CCW`) \n",
    " \n",
    "Finally, we want the node to be able to send `geometry_msgs/Twist` ROS message depending on the stored `min_range` data:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "type incoming_msg =\n",
       "    Clock of Rosgraph_msgs.clock\n",
       "  | Sensor of Sensor_msgs.laserScan\n",
       "type outgoing_msg = Twist of Geometry_msgs.twist\n",
       "type direction = CW | CCW\n",
       "type mode = Driving | Turning\n",
       "type state = {\n",
       "  mode : mode;\n",
       "  min_range : int option;\n",
       "  direction : direction option;\n",
       "  incoming : incoming_msg option;\n",
       "  outgoing : outgoing_msg option;\n",
       "}\n"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "type incoming_msg = \n",
    "  | Clock  of Rosgraph_msgs.clock\n",
    "  | Sensor of Sensor_msgs.laserScan\n",
    "  \n",
    "type outgoing_msg =\n",
    "  | Twist of Geometry_msgs.twist\n",
    "\n",
    "type direction = CW | CCW \n",
    "\n",
    "type mode = Driving | Turning\n",
    "\n",
    "type state =\n",
    "  { mode : mode\n",
    "  ; min_range : int option\n",
    "  ; direction : direction option\n",
    "  ; incoming  : incoming_msg option\n",
    "  ; outgoing  : outgoing_msg option \n",
    "  }"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 2.2 State transition `one_step` function"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To implement our node, we'll need a function that scans through a list of values and returns the minimum value and its index. We'll make a generic function `foldi` that does an indexed version of the `List.fold_right`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val foldi : base:'a -> ?i:Z.t -> (Z.t -> 'b -> 'a -> 'a) -> 'b list -> 'a =\n",
       "  <fun>\n"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/html": [
       "<div><div class=\"imandra-fold panel panel-default\" id=\"fold-216e2fb4-e78c-46b9-b284-fcd02a6ffade\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>termination proof</span></div></div><div class=\"panel-body collapse\"><div><h3>Termination proof</h3><p></p><div class=\"imandra-fold panel panel-default\" id=\"fold-bf83a87e-c193-4fd1-8abc-7926e24d4578\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>call `foldi base (Some ((if Is_a(Some, *opt*) then Option.get *opt* else 0) + 1))\n",
       "f_2 (List.tl l)` from `foldi base *opt* f_2 l`</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-table\" id=\"table-e0bd668a-e916-499a-866e-ac84c41481d9\"><table><tr><td><b>original</b></td><td>foldi base *opt* f_2 l</td></tr><tr><td><b>sub</b></td><td>foldi base (Some ((if Is_a(Some, *opt*) then Option.get *opt* else 0) + 1))\n",
       "f_2 (List.tl l)</td></tr><tr><td><b>original ordinal</b></td><td>Ordinal.Int (Ordinal.count l)</td></tr><tr><td><b>sub ordinal</b></td><td>Ordinal.Int (Ordinal.count (List.tl l))</td></tr><tr><td><b>path</b></td><td>[not (l = [])]</td></tr><tr><td><b>proof</b></td><td><div class=\"imandra-fold panel panel-default\" id=\"fold-9f29f841-4f34-4f51-9e71-c764567a6575\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>detailed proof</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-proof\"><div class=\"imandra-alternatives\" id=\"alt-d188ac19-78fc-4c9c-a77b-8ad6263201af\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>summary</a></li><li class=\"\" data-toggle=\"tab\"><a>full</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-table\" id=\"table-a8b668c8-be10-4da1-bd44-e4ad36aa5394\"><table><tr><td><b>ground_instances</b></td><td>3</td></tr><tr><td><b>definitions</b></td><td>0</td></tr><tr><td><b>inductions</b></td><td>0</td></tr><tr><td><b>search_time</b></td><td><pre>0.010s</pre></td></tr><tr><td><b>details</b></td><td><div class=\"imandra-fold panel panel-default\" id=\"fold-dd241a12-6f3b-49c6-ab24-2ccb64fc5d0a\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-table\" id=\"table-82ef2dc1-6954-4fe6-a3a6-0d0b322a3005\"><table><tr><td><b>smt_stats</b></td><td><div class=\"imandra-table\" id=\"table-1a52fc83-b54b-4ad6-926a-209a1daee269\"><table><tr><td><b>num checks</b></td><td>7</td></tr><tr><td><b>arith assert lower</b></td><td>6</td></tr><tr><td><b>arith pivots</b></td><td>5</td></tr><tr><td><b>rlimit count</b></td><td>1908</td></tr><tr><td><b>mk clause</b></td><td>3</td></tr><tr><td><b>datatype occurs check</b></td><td>43</td></tr><tr><td><b>mk bool var</b></td><td>54</td></tr><tr><td><b>arith assert upper</b></td><td>6</td></tr><tr><td><b>datatype splits</b></td><td>3</td></tr><tr><td><b>decisions</b></td><td>7</td></tr><tr><td><b>arith add rows</b></td><td>15</td></tr><tr><td><b>propagations</b></td><td>2</td></tr><tr><td><b>conflicts</b></td><td>7</td></tr><tr><td><b>arith fixed eqs</b></td><td>5</td></tr><tr><td><b>datatype accessor ax</b></td><td>5</td></tr><tr><td><b>arith conflicts</b></td><td>1</td></tr><tr><td><b>datatype constructor ax</b></td><td>8</td></tr><tr><td><b>num allocs</b></td><td>562868257</td></tr><tr><td><b>final checks</b></td><td>6</td></tr><tr><td><b>added eqs</b></td><td>34</td></tr><tr><td><b>del clause</b></td><td>1</td></tr><tr><td><b>arith eq adapter</b></td><td>4</td></tr><tr><td><b>memory</b></td><td>11.290000</td></tr><tr><td><b>max memory</b></td><td>19.550000</td></tr></table></div></td></tr></table></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-dd241a12-6f3b-49c6-ab24-2ccb64fc5d0a';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></td></tr></table></div></div><div class=\"tab-pane\"><div class=\"imandra-fold panel panel-default\" id=\"fold-449ae23c-fde4-471b-b76e-9a02640c9ee9\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.010s]\n",
       "  not (l = []) &amp;&amp; Ordinal.count l &gt;= 0 &amp;&amp; Ordinal.count (List.tl l) &gt;= 0\n",
       "  ==&gt; List.tl l = []\n",
       "      || Ordinal.Int (Ordinal.count (List.tl l)) Ordinal.&lt;&lt;\n",
       "         Ordinal.Int (Ordinal.count l)</pre></li><li><div><h5>simplify</h5><div class=\"imandra-table\" id=\"table-1c3df60c-09ef-44bc-bae7-c82098cecbbd\"><table><tr><td><b>into</b></td><td><pre>(not\n",
       " ((not (l = []) &amp;&amp; Ordinal.count l &gt;= 0) &amp;&amp; Ordinal.count (List.tl l) &gt;= 0)\n",
       " || List.tl l = [])\n",
       "|| Ordinal.Int (Ordinal.count (List.tl l)) Ordinal.&lt;&lt;\n",
       "   Ordinal.Int (Ordinal.count l)</pre></td></tr><tr><td><b>expansions</b></td><td><pre>[]</pre></td></tr><tr><td><b>rewrite_steps</b></td><td><ul></ul></td></tr><tr><td><b>forward_chaining</b></td><td><ul></ul></td></tr></table></div></div></li><li><div>unroll<div class=\"imandra-table\" id=\"table-32227fd3-d8da-41c7-bb46-32135e1a8987\"><table><tr><td><b>expr</b></td><td><pre>(Ordinal.&lt;&lt;_131 (Ordinal.Int_122 (|count_`ty_1 list`_2255|\n",
       "                                   (|get.…</pre></td></tr><tr><td><b>expansions</b></td><td><ul></ul></td></tr></table></div></div></li><li><div>unroll<div class=\"imandra-table\" id=\"table-388eafb3-f405-4961-ab76-383a95e62509\"><table><tr><td><b>expr</b></td><td><pre>(|count_`ty_1 list`_2255| (|get.::.1_2233| l_2244))</pre></td></tr><tr><td><b>expansions</b></td><td><ul></ul></td></tr></table></div></div></li><li><div>unroll<div class=\"imandra-table\" id=\"table-04d89841-d7ba-4261-a2ee-50b0d17c0911\"><table><tr><td><b>expr</b></td><td><pre>(|count_`ty_1 list`_2255| l_2244)</pre></td></tr><tr><td><b>expansions</b></td><td><ul></ul></td></tr></table></div></div></li><li><div><h5>unsat</h5><pre>(let ((a!1 (ite (&gt;= (|count_`ty_1 list`_2255| (|get.::.1_2233| l_2244)) 0)\n",
       "                (|count_`…</pre></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-449ae23c-fde4-471b-b76e-9a02640c9ee9';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-d188ac19-78fc-4c9c-a77b-8ad6263201af';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-9f29f841-4f34-4f51-9e71-c764567a6575';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></td></tr></table></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-bf83a87e-c193-4fd1-8abc-7926e24d4578';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div><p></p></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-216e2fb4-e78c-46b9-b284-fcd02a6ffade';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "let rec foldi ~base ?(i=0) f l =\n",
    "  match l with\n",
    "  | [] -> base\n",
    "  | x :: tail -> f i x ( foldi f ~base ~i:(i+1) tail )"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "When accepting this function, Imandra constructs its \"termination proof\" - that means that Imandra managed to prove that recursive calls in this function will not end up in an infinite loop. Imandra proves such things using inductive reasoning and is able to prove further statements about other properties of such functions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val get_min_range : int -> int list -> int = <fun>\n"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let get_min_range max lst =\n",
    "  List.fold_right ~base:max\n",
    "    (fun x a -> if x < a then x else a) lst"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On an incoming `Clock` tick we are simply sending out a `Twist` message which tells the robot to either move forward or turn, depending on the mode that it is currently in. We encode it by introducing the `make_twist_message` helper function and the `process_clock_message : state -> state` function."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val make_twist_message : int -> int -> outgoing_msg = <fun>\n",
       "val process_clock_message : state -> state = <fun>\n"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let make_twist_message v omega=\n",
    "  let open Geometry_msgs in\n",
    "  let mkvector x y z =  { vector3_x = x; vector3_y = y; vector3_z = z   } in \n",
    "  Twist { twist_linear  = mkvector v 0 0 ; twist_angular = mkvector 0 0 omega }\n",
    "\n",
    "let process_clock_message state =\n",
    "  match state.mode with \n",
    "  | Driving -> { state with outgoing = Some (make_twist_message 10000 0) } \n",
    "  | Turning -> begin\n",
    "  match state.direction with \n",
    "    | None\n",
    "    | Some ( CW ) -> { state with outgoing = Some (make_twist_message 0   10000) } \n",
    "    | Some (CCW ) -> { state with outgoing = Some (make_twist_message 0 (-10000))} \n",
    "  end"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On incoming `Scan` message, we want to find the minimum of the received ranges and the index of that minimum in the list. Depending on the index, we decide in which direction to turn. To implement this, we create another helper function and the `process_sensor_message` one:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val get_min_and_direction : Sensor_msgs.laserScan -> int * direction = <fun>\n",
       "val process_sensor_message : state -> int -> direction -> state = <fun>\n"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let get_min_and_direction msg =\n",
    "  let max = msg.Sensor_msgs.laserScan_range_max in\n",
    "  let lst = msg.Sensor_msgs.laserScan_ranges in\n",
    "  let min_range = get_min_range max lst in\n",
    "  let mini = foldi ~base:(max, 0)\n",
    "    (fun i a b -> if a < fst b then (a,i) else b) in\n",
    "  let _ , idx = mini lst in\n",
    "  if idx < List.length lst / 2 then min_range, CW else min_range, CCW\n",
    "\n",
    "let process_sensor_message state min_range min_direction =\n",
    "  let dirving_state = \n",
    "    { state with mode = Driving; min_range = None; direction = None } in\n",
    "  let turning_state = \n",
    "    { state with \n",
    "      mode      = Turning\n",
    "    ; direction = Some min_direction\n",
    "    ; min_range = Some min_range \n",
    "    } in  \n",
    "  match state.mode , state.min_range with \n",
    "  | Driving , _    -> if min_range < 20000 then turning_state else dirving_state\n",
    "  | Turning , None -> if min_range > 25000 then dirving_state else turning_state\n",
    "  | Turning , Some old_range -> \n",
    "    if min_range > 25000 then dirving_state\n",
    "    else if min_range > old_range then state else turning_state"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "With the help of these functions, we can create our `one_step` transition function, which just dispatches the messages to the appropriate helper function above."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val one_step : state -> state = <fun>\n"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let one_step state =\n",
    "  match state.incoming with None -> state | Some in_msg ->\n",
    "  let state = { state with incoming = None; outgoing = None } in\n",
    "  match in_msg with \n",
    "  | Sensor laserScan -> \n",
    "    let min_range, min_direction = get_min_and_direction laserScan in\n",
    "    process_sensor_message state min_range min_direction\n",
    "  | Clock  _ -> process_clock_message state"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 2.3 Running the model as a ROS node"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now that we have an early model, let's compile it with our ROS node wrapper into an executable. Here is the model, controlling our \"imandrabot\" in the Gazebo simulation environment:"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "![Imandrabot](../images/Imandra_Demo.gif)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 3. Verifying the ROS node model"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Formal verification is the process of reasoning mathematically about the correctness of computer programs. We'll use Imandra to formally verify some properties of the ROS node model we've created."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 3.1 Verifying outgoing `Twist` message at `Clock` ticks "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Our model is designed in such a way that it updates its state parameters upon `LaserScan` messages and sends out `Twist` control messages in response to `Clock` messages. Let's verify a simple theorem that on every incoming `Clock` message, there is an outgoing `Twist` message. \n",
    "\n",
    "We can formally write this statement down as:\n",
    "\n",
    "$$ \\forall s. IsClock(IncomingMessage(s)) \\,\\Rightarrow\\, IsTwist(OutgoingMessage(OneStep(s))) $$\n",
    "\n",
    "eaning that for every state $s$, if the state contains an incoming message and this message is a `Clock` message, then the state's `outgoing` message is a `Twist` after we've called `one_step` on it.  \n",
    "\n",
    "We can almost literally encode this formal expression as an Imandra `theorem`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val is_clock : incoming_msg option -> bool = <fun>\n",
       "val is_twist : outgoing_msg option -> bool = <fun>\n",
       "val clock_creates_outbound : state -> bool = <fun>\n"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/html": [
       "<div><div>Proved<div class=\"imandra-alternatives\" id=\"alt-7218cbad-45e9-4d83-bffa-e20b8e3ed860\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>proof</a></li><li class=\"\" data-toggle=\"tab\"><a>call graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-proof-top\"><div class=\"imandra-fold panel panel-default\" id=\"fold-36698213-085a-47ad-8bcb-e25e16c4803e\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>proof</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-proof\"><div class=\"imandra-alternatives\" id=\"alt-ab5e6e85-0b15-4718-8ca1-9d4111caddf6\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>summary</a></li><li class=\"\" data-toggle=\"tab\"><a>full</a></li><li class=\"\" data-toggle=\"tab\"><a>graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-table\" id=\"table-0855c20b-9644-4871-a4cf-ce7769551ee1\"><table><tr><td><b>ground_instances</b></td><td>0</td></tr><tr><td><b>definitions</b></td><td>0</td></tr><tr><td><b>inductions</b></td><td>0</td></tr><tr><td><b>search_time</b></td><td><pre>0.008s</pre></td></tr><tr><td><b>details</b></td><td><div class=\"imandra-fold panel panel-default\" id=\"fold-10c1fa61-b925-450c-b15c-6530a3983568\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-table\" id=\"table-3071c750-01b3-4132-bfc2-4c76708ca110\"><table><tr><td><b>smt_stats</b></td><td><div class=\"imandra-table\" id=\"table-40dcf532-0e21-4fd6-8c6e-2b5b9f5ebfac\"><table><tr><td><b>num checks</b></td><td>2</td></tr><tr><td><b>arith assert lower</b></td><td>2</td></tr><tr><td><b>rlimit count</b></td><td>1799</td></tr><tr><td><b>mk clause</b></td><td>39</td></tr><tr><td><b>mk bool var</b></td><td>209</td></tr><tr><td><b>arith assert upper</b></td><td>2</td></tr><tr><td><b>datatype splits</b></td><td>26</td></tr><tr><td><b>decisions</b></td><td>17</td></tr><tr><td><b>propagations</b></td><td>35</td></tr><tr><td><b>conflicts</b></td><td>10</td></tr><tr><td><b>datatype accessor ax</b></td><td>47</td></tr><tr><td><b>datatype constructor ax</b></td><td>33</td></tr><tr><td><b>num allocs</b></td><td>642576992</td></tr><tr><td><b>added eqs</b></td><td>284</td></tr><tr><td><b>del clause</b></td><td>3</td></tr><tr><td><b>arith eq adapter</b></td><td>1</td></tr><tr><td><b>memory</b></td><td>12.700000</td></tr><tr><td><b>max memory</b></td><td>19.550000</td></tr></table></div></td></tr></table></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-10c1fa61-b925-450c-b15c-6530a3983568';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></td></tr></table></div></div><div class=\"tab-pane\"><div class=\"imandra-fold panel panel-default\" id=\"fold-b34396d1-f8b1-4beb-8157-8f0bf1864be5\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.008s]\n",
       "  (if Is_a(Clock, Option.get :var_0:.incoming)\n",
       "      &amp;&amp; Is_a(Some, :var_0:.incoming)\n",
       "   then true else false)\n",
       "  ==&gt; (if Is_a(Twist,\n",
       "          Option.get\n",
       "          (if :var_0:.incoming = None then :var_0: else …).outgoing)\n",
       "          &amp;&amp; Is_a(Some,\n",
       "             (if :var_0:.incoming = None then :var_0: else …).outgoing)\n",
       "       then true else false)</pre></li><li><div><h4>simplify</h4><div class=\"imandra-table\" id=\"table-dff5b908-5636-4a05-9834-e036f27bf3ab\"><table><tr><td><b>into</b></td><td><pre>not\n",
       "(Is_a(Clock, Option.get :var_0:.incoming) &amp;&amp; Is_a(Some, :var_0:.incoming))\n",
       "|| Is_a(Twist,\n",
       "   Option.get (if :var_0:.incoming = None then :var_0: else …).outgoing)\n",
       "   &amp;&amp; Is_a(Some, (if :var_0:.incoming = None then :var_0: else …).outgoing)</pre></td></tr><tr><td><b>expansions</b></td><td><pre>[]</pre></td></tr><tr><td><b>rewrite_steps</b></td><td><ul></ul></td></tr><tr><td><b>forward_chaining</b></td><td><ul></ul></td></tr></table></div></div></li><li><div><h4>unsat</h4><pre>(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_2438 (get.Some.0_2440 (inco…</pre></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-b34396d1-f8b1-4beb-8157-8f0bf1864be5';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-b0623ee1-530c-4d5c-8236-361fafd34e58\"><textarea style=\"display: none\">digraph &quot;proof&quot; {\n",
       "p_208 [label=&quot;Start ((if Is_a(Clock, Option.get :var_0:.incoming)\\l           &amp;&amp; Is_a(Some, :var_0:.incoming)\\l        then true else false)\\l       ==\\&gt; (if Is_a(Twist,\\l               Option.get\\l               (if :var_0:.incoming = None then :var_0: else …).outgoing)\\l               &amp;&amp; Is_a(Some,\\l                  (if :var_0:.incoming = None then :var_0: else …).outgoing)\\l            then true else false)\\l       :time 0.008s)&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_208 -&gt; p_207 [label=&quot;&quot;];\n",
       "p_207 [label=&quot;Simplify (not\\l          (Is_a(Clock, Option.get :var_0:.incoming)\\l           &amp;&amp; Is_a(Some, :var_0:.incoming))\\l          \\|\\| Is_a(Twist,\\l             Option.get\\l             (if :var_0:.incoming = None then :var_0: else …).outgoing)\\l             &amp;&amp; Is_a(Some,\\l                (if :var_0:.incoming = None then :var_0: else …).outgoing)\\l          :expansions [] :rw [] :fc [])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_207 -&gt; p_206 [label=&quot;&quot;];\n",
       "p_206 -&gt; p_z3_1031 [label=&quot;&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_z3_1031 [label=&quot;(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_2438 (get.Some.0_2440 (inco…&quot;,shape=box,fontname=&quot;courier&quot;,fontsize=14];p_206 [label=&quot;unsat&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-b0623ee1-530c-4d5c-8236-361fafd34e58';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-ab5e6e85-0b15-4718-8ca1-9d4111caddf6';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-36698213-085a-47ad-8bcb-e25e16c4803e';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-25b9e936-ae14-4626-8299-8ae517affaf9\"><textarea style=\"display: none\">digraph &quot;call graph&quot; {\n",
       "goal [label=&quot;not\\l(not (Is_a(Clock, Option.get state.incoming) &amp;&amp; Is_a(Some, state.incoming))\\l \\|\\| Is_a(Twist,\\l    Option.get (if state.incoming = None then state else …).outgoing)\\l    &amp;&amp; Is_a(Some, (if state.incoming = None then state else …).outgoing))&quot;,shape=box,style=filled,color=&quot;cyan&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "call_292 [label=&quot;foldi ((Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_range_max, 0) None\\lanon_fun.get_min_and_direction.0\\l(Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_292 [label=&quot;calls&quot;];\n",
       "call_295 [label=&quot;List.fold_right anon_fun.get_min_range.0\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_range_max\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_295 [label=&quot;calls&quot;];\n",
       "call_288 [label=&quot;List.length\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_288 [label=&quot;calls&quot;];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-25b9e936-ae14-4626-8299-8ae517affaf9';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-7218cbad-45e9-4d83-bffa-e20b8e3ed860';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "let is_clock msg = match msg with  Some ( Clock _ ) -> true | _ -> false ;;\n",
    "let is_twist msg = match msg with  Some ( Twist _ ) -> true | _ -> false ;;\n",
    "\n",
    "theorem clock_creates_outbound state =\n",
    "  is_clock state.incoming ==> is_twist (one_step state).outgoing"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One can see that Imandra says that it \"Proved\" the theorem, meaning that Imandra has formally checked that this property holds for all possible input states. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 3.2 Verifying that we never drive backwards "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As another example, let us check that, no matter what, the node will never send out a message with negative linear velocity."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val no_moving_back : outgoing_msg option -> bool = <fun>\n",
       "- : state -> bool = <fun>\n",
       "module CX : sig val state : state end\n"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let no_moving_back msg = \n",
    "    let open Geometry_msgs in\n",
    "    match msg with None -> true \n",
    "    | Some (Twist data) -> data.twist_linear.vector3_x >= 0\n",
    "  \n",
    "verify ( fun state -> no_moving_back (one_step state).outgoing  )"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We have failed to prove the statement and Imandra have created a counterexample `CX` module for us. This module  contains concrete values for the parameters of the verified statement, that violate the statement's condition. Let's examine the value of `CX.state`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : state =\n",
       "{mode = Turning; min_range = Some 2282; direction = None; incoming = None;\n",
       " outgoing =\n",
       "  Some\n",
       "   (Twist\n",
       "     {Geometry_msgs.twist_linear =\n",
       "       {Geometry_msgs.vector3_x = -1; vector3_y = 9; vector3_z = 10};\n",
       "      twist_angular =\n",
       "       {Geometry_msgs.vector3_x = 11; vector3_y = 12; vector3_z = 13}})}\n"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "CX.state"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The counterexample `state` produced by imandra has the `incoming` message set to `None` and the `outgoing` message set to a `Twist` message with negative `linear.x`. Our `one_step` function keeps the state unchanged if the incoming message is empty. \n",
    "\n",
    "We can either consider this behavior as a bug and change our `one_step` implementation; or we can consider this a normal behavior and amend our theorem, adding the non-empty incoming message as an extra premise of the theorem: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val never_goes_back : state -> bool = <fun>\n"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/html": [
       "<div><div>Proved<div class=\"imandra-alternatives\" id=\"alt-c61b3bad-e163-4887-853e-91c930b809d8\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>proof</a></li><li class=\"\" data-toggle=\"tab\"><a>call graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-proof-top\"><div class=\"imandra-fold panel panel-default\" id=\"fold-e59f8a3b-192d-475c-b15c-0d22bdb26670\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>proof</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-proof\"><div class=\"imandra-alternatives\" id=\"alt-e82ed48b-c4c0-4b04-b6e3-de40ae8b5a87\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>summary</a></li><li class=\"\" data-toggle=\"tab\"><a>full</a></li><li class=\"\" data-toggle=\"tab\"><a>graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-table\" id=\"table-688a329e-fd53-4fe2-82bc-588c72fdd4c8\"><table><tr><td><b>ground_instances</b></td><td>0</td></tr><tr><td><b>definitions</b></td><td>0</td></tr><tr><td><b>inductions</b></td><td>0</td></tr><tr><td><b>search_time</b></td><td><pre>0.010s</pre></td></tr><tr><td><b>details</b></td><td><div class=\"imandra-fold panel panel-default\" id=\"fold-294beae0-2a42-4f12-80cf-e52d37cbf0fb\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-table\" id=\"table-299e69f6-e11e-4a74-b143-e528d7a4817f\"><table><tr><td><b>smt_stats</b></td><td><div class=\"imandra-table\" id=\"table-29ffc197-5e90-45cc-b088-62bf6398c794\"><table><tr><td><b>num checks</b></td><td>2</td></tr><tr><td><b>arith assert lower</b></td><td>3</td></tr><tr><td><b>rlimit count</b></td><td>2372</td></tr><tr><td><b>mk clause</b></td><td>48</td></tr><tr><td><b>mk bool var</b></td><td>282</td></tr><tr><td><b>arith assert upper</b></td><td>14</td></tr><tr><td><b>datatype splits</b></td><td>28</td></tr><tr><td><b>decisions</b></td><td>56</td></tr><tr><td><b>propagations</b></td><td>162</td></tr><tr><td><b>conflicts</b></td><td>21</td></tr><tr><td><b>datatype accessor ax</b></td><td>57</td></tr><tr><td><b>minimized lits</b></td><td>7</td></tr><tr><td><b>arith assert diseq</b></td><td>2</td></tr><tr><td><b>datatype constructor ax</b></td><td>74</td></tr><tr><td><b>num allocs</b></td><td>814411800</td></tr><tr><td><b>added eqs</b></td><td>534</td></tr><tr><td><b>del clause</b></td><td>3</td></tr><tr><td><b>arith eq adapter</b></td><td>5</td></tr><tr><td><b>memory</b></td><td>26.710000</td></tr><tr><td><b>max memory</b></td><td>26.710000</td></tr></table></div></td></tr></table></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-294beae0-2a42-4f12-80cf-e52d37cbf0fb';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></td></tr></table></div></div><div class=\"tab-pane\"><div class=\"imandra-fold panel panel-default\" id=\"fold-b650f39a-14b2-4f96-84ad-7d6e44e8a177\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.010s]\n",
       "  not (:var_0:.incoming = None)\n",
       "  ==&gt; (if (if :var_0:.incoming = None then :var_0:\n",
       "           else\n",
       "           if Is_a(Sensor, Option.get :var_0:.incoming)\n",
       "           then if ….mode = Driving then … else …\n",
       "           else if ….mode = Driving then … else …).outgoing\n",
       "          = None\n",
       "       then true\n",
       "       else\n",
       "         (Destruct(Twist, 0, …)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\n",
       "         &gt;= 0)</pre></li><li><div><h4>simplify</h4><div class=\"imandra-table\" id=\"table-2645e366-d204-4840-863c-e5c2237ebba3\"><table><tr><td><b>into</b></td><td><pre>(:var_0:.incoming = None\n",
       " || (if :var_0:.incoming = None then :var_0:\n",
       "     else\n",
       "     if Is_a(Sensor, Option.get :var_0:.incoming)\n",
       "     then if :var_0:.mode = Driving then … else …\n",
       "     else if :var_0:.mode = Driving then … else …).outgoing\n",
       "    = None)\n",
       "|| (Destruct(Twist, 0,\n",
       "             Option.get\n",
       "             (if :var_0:.incoming = None then :var_0:\n",
       "              else\n",
       "              if Is_a(Sensor, Option.get :var_0:.incoming)\n",
       "              then if :var_0:.mode = Driving then … else …\n",
       "              else if :var_0:.mode = Driving then … else …).outgoing)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\n",
       "   &gt;= 0</pre></td></tr><tr><td><b>expansions</b></td><td><pre>[]</pre></td></tr><tr><td><b>rewrite_steps</b></td><td><ul></ul></td></tr><tr><td><b>forward_chaining</b></td><td><ul></ul></td></tr></table></div></div></li><li><div><h4>unsat</h4><pre>(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_2821 (get.Some.0_2823 (inco…</pre></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-b650f39a-14b2-4f96-84ad-7d6e44e8a177';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-21f6072a-987f-4710-8952-d01c19cd4cac\"><textarea style=\"display: none\">digraph &quot;proof&quot; {\n",
       "p_232 [label=&quot;Start (not (:var_0:.incoming = None)\\l       ==\\&gt; (if (if :var_0:.incoming = None then :var_0:\\l                else\\l                if Is_a(Sensor, Option.get :var_0:.incoming)\\l                then if ….mode = Driving then … else …\\l                else if ….mode = Driving then … else …).outgoing\\l               = None\\l            then true\\l            else\\l              (Destruct(Twist, 0, …)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\\l              \\&gt;= 0)\\l       :time 0.010s)&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_232 -&gt; p_231 [label=&quot;&quot;];\n",
       "p_231 [label=&quot;Simplify ((:var_0:.incoming = None\\l           \\|\\| (if :var_0:.incoming = None then :var_0:\\l               else\\l               if Is_a(Sensor, Option.get :var_0:.incoming)\\l               then if :var_0:.mode = Driving then … else …\\l               else if :var_0:.mode = Driving then … else …).outgoing\\l              = None)\\l          \\|\\| (Destruct(Twist, 0,\\l                       Option.get\\l                       (if :var_0:.incoming = None then :var_0:\\l                        else\\l                        if Is_a(Sensor, Option.get :var_0:.incoming)\\l                        then if :var_0:.mode = Driving then … else …\\l                        else if :var_0:.mode = Driving then … else …).outgoing)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\\l             \\&gt;= 0\\l          :expansions [] :rw [] :fc [])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_231 -&gt; p_230 [label=&quot;&quot;];\n",
       "p_230 -&gt; p_z3_1378 [label=&quot;&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_z3_1378 [label=&quot;(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_2821 (get.Some.0_2823 (inco…&quot;,shape=box,fontname=&quot;courier&quot;,fontsize=14];p_230 [label=&quot;unsat&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-21f6072a-987f-4710-8952-d01c19cd4cac';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-e82ed48b-c4c0-4b04-b6e3-de40ae8b5a87';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-e59f8a3b-192d-475c-b15c-0d22bdb26670';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-2a47906c-c5d7-47b5-8b56-97902352b858\"><textarea style=\"display: none\">digraph &quot;call graph&quot; {\n",
       "goal [label=&quot;not\\l((state.incoming = None\\l  \\|\\| (if state.incoming = None then state\\l      else\\l      if Is_a(Sensor, Option.get state.incoming)\\l      then if state.mode = Driving then … else …\\l      else if state.mode = Driving then … else …).outgoing\\l     = None)\\l \\|\\| (Destruct(Twist, 0,\\l              Option.get\\l              (if state.incoming = None then state\\l               else\\l               if Is_a(Sensor, Option.get state.incoming)\\l               then if state.mode = Driving then … else …\\l               else if state.mode = Driving then … else …).outgoing)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\\l    \\&gt;= 0)&quot;,shape=box,style=filled,color=&quot;cyan&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "call_284 [label=&quot;List.fold_right anon_fun.get_min_range.0\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_range_max\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_284 [label=&quot;calls&quot;];\n",
       "call_281 [label=&quot;foldi ((Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_range_max, 0) None\\lanon_fun.get_min_and_direction.0\\l(Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_281 [label=&quot;calls&quot;];\n",
       "call_200 [label=&quot;List.length\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_200 [label=&quot;calls&quot;];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-2a47906c-c5d7-47b5-8b56-97902352b858';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-c61b3bad-e163-4887-853e-91c930b809d8';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "theorem never_goes_back state = \n",
    "  state.incoming <> None\n",
    "  ==>\n",
    "  no_moving_back (one_step state).outgoing  "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We've proven that the model never creates negative linear speed in response to any incoming message - alternatively we can set `state.outgoing = None` as a premise, proving that an empty `outgoing` message is never filled with a `Twist` with negative velocity:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val never_goes_back_alt : state -> bool = <fun>\n"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/html": [
       "<div><div>Proved<div class=\"imandra-alternatives\" id=\"alt-d61f436e-904a-4dbe-afdb-be4c41c22501\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>proof</a></li><li class=\"\" data-toggle=\"tab\"><a>call graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-proof-top\"><div class=\"imandra-fold panel panel-default\" id=\"fold-d8c635f4-4bdd-4809-bd6d-2528d39b22ea\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>proof</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-proof\"><div class=\"imandra-alternatives\" id=\"alt-445dad3f-1e46-4dd3-a029-831a23f7462e\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>summary</a></li><li class=\"\" data-toggle=\"tab\"><a>full</a></li><li class=\"\" data-toggle=\"tab\"><a>graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-table\" id=\"table-dec05aa8-c023-42a6-b5c4-1b1fc327aca0\"><table><tr><td><b>ground_instances</b></td><td>0</td></tr><tr><td><b>definitions</b></td><td>0</td></tr><tr><td><b>inductions</b></td><td>0</td></tr><tr><td><b>search_time</b></td><td><pre>0.009s</pre></td></tr><tr><td><b>details</b></td><td><div class=\"imandra-fold panel panel-default\" id=\"fold-deb9897c-e27a-4a33-b542-4673c77baaff\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-table\" id=\"table-9d03b857-97a8-4684-8c0c-1407f886beb2\"><table><tr><td><b>smt_stats</b></td><td><div class=\"imandra-table\" id=\"table-e3a335ac-621b-4756-8988-648a29307d48\"><table><tr><td><b>num checks</b></td><td>2</td></tr><tr><td><b>arith assert lower</b></td><td>3</td></tr><tr><td><b>rlimit count</b></td><td>2521</td></tr><tr><td><b>mk clause</b></td><td>51</td></tr><tr><td><b>mk bool var</b></td><td>265</td></tr><tr><td><b>arith assert upper</b></td><td>10</td></tr><tr><td><b>datatype splits</b></td><td>27</td></tr><tr><td><b>decisions</b></td><td>53</td></tr><tr><td><b>propagations</b></td><td>178</td></tr><tr><td><b>conflicts</b></td><td>23</td></tr><tr><td><b>datatype accessor ax</b></td><td>58</td></tr><tr><td><b>minimized lits</b></td><td>5</td></tr><tr><td><b>arith assert diseq</b></td><td>2</td></tr><tr><td><b>datatype constructor ax</b></td><td>63</td></tr><tr><td><b>num allocs</b></td><td>933708233</td></tr><tr><td><b>added eqs</b></td><td>495</td></tr><tr><td><b>del clause</b></td><td>5</td></tr><tr><td><b>arith eq adapter</b></td><td>5</td></tr><tr><td><b>memory</b></td><td>32.130000</td></tr><tr><td><b>max memory</b></td><td>32.130000</td></tr></table></div></td></tr></table></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-deb9897c-e27a-4a33-b542-4673c77baaff';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></td></tr></table></div></div><div class=\"tab-pane\"><div class=\"imandra-fold panel panel-default\" id=\"fold-c190886c-fdf1-4c05-b789-d5c650852b85\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.009s]\n",
       "  :var_0:.outgoing = None\n",
       "  ==&gt; (if (if :var_0:.incoming = None then :var_0:\n",
       "           else\n",
       "           if Is_a(Sensor, Option.get :var_0:.incoming)\n",
       "           then if ….mode = Driving then … else …\n",
       "           else if ….mode = Driving then … else …).outgoing\n",
       "          = None\n",
       "       then true\n",
       "       else\n",
       "         (Destruct(Twist, 0, …)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\n",
       "         &gt;= 0)</pre></li><li><div><h4>simplify</h4><div class=\"imandra-table\" id=\"table-e6204332-8d34-4593-ae9b-fa3504e7950c\"><table><tr><td><b>into</b></td><td><pre>(not (:var_0:.outgoing = None)\n",
       " || (if :var_0:.incoming = None then :var_0:\n",
       "     else\n",
       "     if Is_a(Sensor, Option.get :var_0:.incoming)\n",
       "     then if :var_0:.mode = Driving then … else …\n",
       "     else if :var_0:.mode = Driving then … else …).outgoing\n",
       "    = None)\n",
       "|| (Destruct(Twist, 0,\n",
       "             Option.get\n",
       "             (if :var_0:.incoming = None then :var_0:\n",
       "              else\n",
       "              if Is_a(Sensor, Option.get :var_0:.incoming)\n",
       "              then if :var_0:.mode = Driving then … else …\n",
       "              else if :var_0:.mode = Driving then … else …).outgoing)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\n",
       "   &gt;= 0</pre></td></tr><tr><td><b>expansions</b></td><td><pre>[]</pre></td></tr><tr><td><b>rewrite_steps</b></td><td><ul></ul></td></tr><tr><td><b>forward_chaining</b></td><td><ul></ul></td></tr></table></div></div></li><li><div><h4>unsat</h4><pre>(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_2979 (get.Some.0_2981 (inco…</pre></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-c190886c-fdf1-4c05-b789-d5c650852b85';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-33ed7bdd-d253-4203-b71a-b0748dfb707c\"><textarea style=\"display: none\">digraph &quot;proof&quot; {\n",
       "p_238 [label=&quot;Start (:var_0:.outgoing = None\\l       ==\\&gt; (if (if :var_0:.incoming = None then :var_0:\\l                else\\l                if Is_a(Sensor, Option.get :var_0:.incoming)\\l                then if ….mode = Driving then … else …\\l                else if ….mode = Driving then … else …).outgoing\\l               = None\\l            then true\\l            else\\l              (Destruct(Twist, 0, …)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\\l              \\&gt;= 0)\\l       :time 0.009s)&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_238 -&gt; p_237 [label=&quot;&quot;];\n",
       "p_237 [label=&quot;Simplify ((not (:var_0:.outgoing = None)\\l           \\|\\| (if :var_0:.incoming = None then :var_0:\\l               else\\l               if Is_a(Sensor, Option.get :var_0:.incoming)\\l               then if :var_0:.mode = Driving then … else …\\l               else if :var_0:.mode = Driving then … else …).outgoing\\l              = None)\\l          \\|\\| (Destruct(Twist, 0,\\l                       Option.get\\l                       (if :var_0:.incoming = None then :var_0:\\l                        else\\l                        if Is_a(Sensor, Option.get :var_0:.incoming)\\l                        then if :var_0:.mode = Driving then … else …\\l                        else if :var_0:.mode = Driving then … else …).outgoing)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\\l             \\&gt;= 0\\l          :expansions [] :rw [] :fc [])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_237 -&gt; p_236 [label=&quot;&quot;];\n",
       "p_236 -&gt; p_z3_1396 [label=&quot;&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_z3_1396 [label=&quot;(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_2979 (get.Some.0_2981 (inco…&quot;,shape=box,fontname=&quot;courier&quot;,fontsize=14];p_236 [label=&quot;unsat&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-33ed7bdd-d253-4203-b71a-b0748dfb707c';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-445dad3f-1e46-4dd3-a029-831a23f7462e';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-d8c635f4-4bdd-4809-bd6d-2528d39b22ea';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-2b8f1e8c-453f-4250-b454-e1b751002cca\"><textarea style=\"display: none\">digraph &quot;call graph&quot; {\n",
       "goal [label=&quot;not\\l((not (state.outgoing = None)\\l  \\|\\| (if state.incoming = None then state\\l      else\\l      if Is_a(Sensor, Option.get state.incoming)\\l      then if state.mode = Driving then … else …\\l      else if state.mode = Driving then … else …).outgoing\\l     = None)\\l \\|\\| (Destruct(Twist, 0,\\l              Option.get\\l              (if state.incoming = None then state\\l               else\\l               if Is_a(Sensor, Option.get state.incoming)\\l               then if state.mode = Driving then … else …\\l               else if state.mode = Driving then … else …).outgoing)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x\\l    \\&gt;= 0)&quot;,shape=box,style=filled,color=&quot;cyan&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "call_229 [label=&quot;foldi ((Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_range_max, 0) None\\lanon_fun.get_min_and_direction.0\\l(Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_229 [label=&quot;calls&quot;];\n",
       "call_180 [label=&quot;List.length\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_180 [label=&quot;calls&quot;];\n",
       "call_232 [label=&quot;List.fold_right anon_fun.get_min_range.0\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_range_max\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_232 [label=&quot;calls&quot;];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-2b8f1e8c-453f-4250-b454-e1b751002cca';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-d61f436e-904a-4dbe-afdb-be4c41c22501';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "theorem never_goes_back_alt state = \n",
    "  state.outgoing = None\n",
    "  ==>\n",
    "  no_moving_back (one_step state).outgoing  "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 4. Inductive proofs. Stopping near objects."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As a final formal verification goal, we want to be able to prove that the robot stops and starts turning if one of the values in the scanner `ranges` is lower than 0.2 meters. In general, reasoning about variable-sized lists requires inductive proofs - and these might require proving some lemmas to guide Imandra to the proof. So, we will first try to prove a simpler version of the theorem - if all the ranges in the incoming laser scan message are less than 0.2 meters, then we definitely transition to the `Turning` state. We'll try to encode our theorem using `List.for_all` standard function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : state -> bool = <fun>\n",
       "module CX : sig val state : state end\n"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "verify ( fun state ->\n",
    "  let open Sensor_msgs in\n",
    "  match state.incoming with None | Some (Clock _ ) -> true \n",
    "  | Some ( Sensor data ) ->\n",
    "  (  List.for_all (fun x -> x < 20000) data.laserScan_ranges    \n",
    "  ) ==> (one_step state).mode = Turning\n",
    ")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We have failed to prove the statement and Imandra has created a counterexample `CX` module for us. Examining the counterexample state we notice that the incoming `laserScan_ranges list` is empty."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "- : state =\n",
       "{mode = Turning; min_range = Some 7719; direction = None;\n",
       " incoming =\n",
       "  Some\n",
       "   (Sensor\n",
       "     {Sensor_msgs.laserScan_range_min = 3; laserScan_range_max = 25001;\n",
       "      laserScan_ranges = []});\n",
       " outgoing = None}\n"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "CX.state"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Adding the extra requirement that the list is not `[]`, we successfully verify the statement:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val stopping_if_for_all : state -> bool = <fun>\n"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/html": [
       "<div><div>Proved<div class=\"imandra-alternatives\" id=\"alt-bf3c02f4-df44-479f-85f9-0d296fc9a376\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>proof</a></li><li class=\"\" data-toggle=\"tab\"><a>call graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-proof-top\"><div class=\"imandra-fold panel panel-default\" id=\"fold-f6464602-13dc-431c-b999-400d5845fe11\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>proof</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-proof\"><div class=\"imandra-alternatives\" id=\"alt-27b39f22-1765-4b56-ba2e-373f917368ed\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>summary</a></li><li class=\"\" data-toggle=\"tab\"><a>full</a></li><li class=\"\" data-toggle=\"tab\"><a>graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-table\" id=\"table-fd975efd-2444-429a-839e-e9f075c4a387\"><table><tr><td><b>ground_instances</b></td><td>4</td></tr><tr><td><b>definitions</b></td><td>0</td></tr><tr><td><b>inductions</b></td><td>0</td></tr><tr><td><b>search_time</b></td><td><pre>0.017s</pre></td></tr><tr><td><b>details</b></td><td><div class=\"imandra-fold panel panel-default\" id=\"fold-983aa86b-4e3a-41c6-82af-a873f64a88de\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-table\" id=\"table-b3d3091a-e8de-4ea4-83f1-f03eeb9fc5d2\"><table><tr><td><b>smt_stats</b></td><td><div class=\"imandra-table\" id=\"table-e48f4619-1739-40e1-9742-1dbc20e4adba\"><table><tr><td><b>arith offset eqs</b></td><td>5</td></tr><tr><td><b>num checks</b></td><td>10</td></tr><tr><td><b>arith assert lower</b></td><td>36</td></tr><tr><td><b>arith pivots</b></td><td>18</td></tr><tr><td><b>rlimit count</b></td><td>7652</td></tr><tr><td><b>mk clause</b></td><td>67</td></tr><tr><td><b>datatype occurs check</b></td><td>1584</td></tr><tr><td><b>mk bool var</b></td><td>571</td></tr><tr><td><b>arith assert upper</b></td><td>46</td></tr><tr><td><b>datatype splits</b></td><td>49</td></tr><tr><td><b>decisions</b></td><td>361</td></tr><tr><td><b>arith add rows</b></td><td>25</td></tr><tr><td><b>propagations</b></td><td>284</td></tr><tr><td><b>conflicts</b></td><td>27</td></tr><tr><td><b>arith fixed eqs</b></td><td>9</td></tr><tr><td><b>datatype accessor ax</b></td><td>56</td></tr><tr><td><b>minimized lits</b></td><td>2</td></tr><tr><td><b>arith conflicts</b></td><td>3</td></tr><tr><td><b>arith assert diseq</b></td><td>9</td></tr><tr><td><b>datatype constructor ax</b></td><td>301</td></tr><tr><td><b>num allocs</b></td><td>1031543182</td></tr><tr><td><b>final checks</b></td><td>12</td></tr><tr><td><b>added eqs</b></td><td>1385</td></tr><tr><td><b>del clause</b></td><td>35</td></tr><tr><td><b>arith eq adapter</b></td><td>18</td></tr><tr><td><b>memory</b></td><td>39.270000</td></tr><tr><td><b>max memory</b></td><td>39.270000</td></tr></table></div></td></tr></table></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-983aa86b-4e3a-41c6-82af-a873f64a88de';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></td></tr></table></div></div><div class=\"tab-pane\"><div class=\"imandra-fold panel panel-default\" id=\"fold-b549ba70-e051-44a3-95e0-467d1bcf9678\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.017s]\n",
       "  if :var_0:.incoming = None\n",
       "     || Is_a(Some, :var_0:.incoming)\n",
       "        &amp;&amp; Is_a(Clock, Option.get :var_0:.incoming)\n",
       "  then true\n",
       "  else\n",
       "    not\n",
       "    ((Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\n",
       "     = [])\n",
       "    &amp;&amp; List.for_all anon_fun.stopping_if_for_all.0\n",
       "       (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\n",
       "    ==&gt; (if :var_0:.incoming = None then :var_0:\n",
       "         else if Is_a(Sensor, Option.get :var_0:.incoming) then … else …).mode\n",
       "        = Turning</pre></li><li><div><h4>simplify</h4><div class=\"imandra-table\" id=\"table-a7c82a8f-7e8e-47d4-bc9a-28ca0ed2adbf\"><table><tr><td><b>into</b></td><td><pre>((:var_0:.incoming = None\n",
       "  || Is_a(Some, :var_0:.incoming) &amp;&amp; Is_a(Clock, Option.get :var_0:.incoming))\n",
       " || not\n",
       "    (not\n",
       "     ((Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\n",
       "      = [])\n",
       "     &amp;&amp; List.for_all anon_fun.stopping_if_for_all.0\n",
       "        (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges))\n",
       "|| (if :var_0:.incoming = None then :var_0:\n",
       "    else\n",
       "    if Is_a(Sensor, Option.get :var_0:.incoming)\n",
       "    then if :var_0:.mode = Driving then … else …\n",
       "    else if :var_0:.mode = Driving then … else …).mode\n",
       "   = Turning</pre></td></tr><tr><td><b>expansions</b></td><td><pre>[]</pre></td></tr><tr><td><b>rewrite_steps</b></td><td><ul></ul></td></tr><tr><td><b>forward_chaining</b></td><td><ul></ul></td></tr></table></div></div></li><li><div>unroll<div class=\"imandra-table\" id=\"table-7a173b0d-6057-4b60-9212-a8208b7f0e69\"><table><tr><td><b>expr</b></td><td><pre>(let ((a!1 (Sensor_msgs.laserScan_range_max_2143\n",
       "             (get.Sensor.0_3143 (get.Some.0_3145 (i…</pre></td></tr><tr><td><b>expansions</b></td><td><ul></ul></td></tr></table></div></div></li><li><div>unroll<div class=\"imandra-table\" id=\"table-dff765fa-071d-4107-b484-29dda36b9653\"><table><tr><td><b>expr</b></td><td><pre>(let ((a!1 (Sensor_msgs.laserScan_range_max_2143\n",
       "             (get.Sensor.0_3143 (get.Some.0_3145 (i…</pre></td></tr><tr><td><b>expansions</b></td><td><ul></ul></td></tr></table></div></div></li><li><div>unroll<div class=\"imandra-table\" id=\"table-181a9a7a-29bc-459a-bbe1-483d8d15563f\"><table><tr><td><b>expr</b></td><td><pre>(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_3143 (get.Some.0_3145 (inco…</pre></td></tr><tr><td><b>expansions</b></td><td><ul></ul></td></tr></table></div></div></li><li><div>unroll<div class=\"imandra-table\" id=\"table-b133db17-4da4-43f7-91f4-f59efe29b2e4\"><table><tr><td><b>expr</b></td><td><pre>(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_3143 (get.Some.0_3145 (inco…</pre></td></tr><tr><td><b>expansions</b></td><td><ul></ul></td></tr></table></div></div></li><li><div><h4>unsat</h4><pre>(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_3143 (get.Some.0_3145 (inco…</pre></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-b549ba70-e051-44a3-95e0-467d1bcf9678';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-90cecec0-5c96-4270-bd79-92a3388c722d\"><textarea style=\"display: none\">digraph &quot;proof&quot; {\n",
       "p_252 [label=&quot;Start (if :var_0:.incoming = None\\l          \\|\\| Is_a(Some, :var_0:.incoming)\\l             &amp;&amp; Is_a(Clock, Option.get :var_0:.incoming)\\l       then true\\l       else\\l         not\\l         ((Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\\l          = [])\\l         &amp;&amp; List.for_all anon_fun.stopping_if_for_all.0\\l            (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\\l         ==\\&gt; (if :var_0:.incoming = None then :var_0:\\l              else\\l              if Is_a(Sensor, Option.get :var_0:.incoming) then … else …).mode\\l             = Turning\\l       :time 0.017s)&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_252 -&gt; p_251 [label=&quot;&quot;];\n",
       "p_251 [label=&quot;Simplify (((:var_0:.incoming = None\\l            \\|\\| Is_a(Some, :var_0:.incoming)\\l               &amp;&amp; Is_a(Clock, Option.get :var_0:.incoming))\\l           \\|\\| not\\l              (not\\l               ((Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\\l                = [])\\l               &amp;&amp; List.for_all anon_fun.stopping_if_for_all.0\\l                  (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges))\\l          \\|\\| (if :var_0:.incoming = None then :var_0:\\l              else\\l              if Is_a(Sensor, Option.get :var_0:.incoming)\\l              then if :var_0:.mode = Driving then … else …\\l              else if :var_0:.mode = Driving then … else …).mode\\l             = Turning\\l          :expansions [] :rw [] :fc [])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_251 -&gt; p_250 [label=&quot;&quot;];\n",
       "p_250 [label=&quot;Unroll ([List.fold_right anon_fun.get_min_range.0\\l         (Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_range_max\\l         (Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges],\\l        [[]])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_250 -&gt; p_249 [label=&quot;&quot;];\n",
       "p_249 [label=&quot;Unroll ([foldi\\l         ((Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_range_max, 0) None\\l         anon_fun.get_min_and_direction.0\\l         (Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_ranges],\\l        [[]])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_249 -&gt; p_248 [label=&quot;&quot;];\n",
       "p_248 [label=&quot;Unroll ([List.length\\l         (Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges],\\l        [[]])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_248 -&gt; p_247 [label=&quot;&quot;];\n",
       "p_247 [label=&quot;Unroll ([List.for_all anon_fun.stopping_if_for_all.0\\l         (Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges],\\l        [[]])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_247 -&gt; p_246 [label=&quot;&quot;];\n",
       "p_246 -&gt; p_z3_1640 [label=&quot;&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_z3_1640 [label=&quot;(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_3143 (get.Some.0_3145 (inco…&quot;,shape=box,fontname=&quot;courier&quot;,fontsize=14];p_246 [label=&quot;unsat&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-90cecec0-5c96-4270-bd79-92a3388c722d';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-27b39f22-1765-4b56-ba2e-373f917368ed';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-f6464602-13dc-431c-b999-400d5845fe11';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-8f4f9393-2e74-4ff7-82a2-740f338cd445\"><textarea style=\"display: none\">digraph &quot;call graph&quot; {\n",
       "goal [label=&quot;not\\l(((state.incoming = None\\l   \\|\\| Is_a(Some, state.incoming) &amp;&amp; Is_a(Clock, Option.get state.incoming))\\l  \\|\\| not\\l     (not\\l      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\\l       = [])\\l      &amp;&amp; List.for_all anon_fun.stopping_if_for_all.0\\l         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges))\\l \\|\\| (if state.incoming = None then state\\l     else\\l     if Is_a(Sensor, Option.get state.incoming)\\l     then if state.mode = Driving then … else …\\l     else if state.mode = Driving then … else …).mode\\l    = Turning)&quot;,shape=box,style=filled,color=&quot;cyan&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "call_186 [label=&quot;List.fold_right anon_fun.get_min_range.0\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_range_max\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;green&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "call_186 -&gt; expr_1041 [label=&quot;=&quot;];\n",
       "expr_1041 [label=&quot;if (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges\\l   = []\\lthen\\l  (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_range_max\\lelse\\lif List.fold_right anon_fun.get_min_range.0\\l   (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_range_max\\l   (List.tl\\l    (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges)\\l   \\&lt;=\\l   List.hd\\l   (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges\\lthen\\l  List.fold_right anon_fun.get_min_range.0\\l  (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_range_max\\l  (List.tl\\l   (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges)\\lelse\\l  List.hd\\l  (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;grey&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_186 [label=&quot;calls&quot;];\n",
       "call_177 [label=&quot;List.length\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;green&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "call_177 -&gt; expr_1336 [label=&quot;=&quot;];\n",
       "expr_1336 [label=&quot;if (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges\\l   = []\\lthen 0\\lelse\\l  1\\l  + List.length\\l    (List.tl\\l     (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges)&quot;,shape=box,style=filled,color=&quot;grey&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_177 [label=&quot;calls&quot;];\n",
       "call_182 [label=&quot;foldi ((Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_range_max, 0) None\\lanon_fun.get_min_and_direction.0\\l(Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;green&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "call_182 -&gt; expr_1165 [label=&quot;=&quot;];\n",
       "expr_1165 [label=&quot;if (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges\\l   = []\\lthen\\l  ((Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_range_max,\\l   0)\\lelse\\lif (foldi\\l    ((Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_range_max,\\l     0)\\l    (Some …) anon_fun.get_min_and_direction.0\\l    (List.tl\\l     (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges)).0\\l   \\&lt;=\\l   List.hd\\l   (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges\\lthen\\l  foldi\\l  ((Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_range_max,\\l   0)\\l  (Some …) anon_fun.get_min_and_direction.0\\l  (List.tl\\l   (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges)\\lelse\\l  (List.hd\\l   (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges,\\l   if Is_a(Some, …) then … else 0)&quot;,shape=box,style=filled,color=&quot;grey&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_182 [label=&quot;calls&quot;];\n",
       "call_1334 [label=&quot;List.length\\l(List.tl (Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges)&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "expr_1336 -&gt; call_1334 [label=&quot;calls&quot;];\n",
       "call_1158 [label=&quot;foldi ((Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_range_max, 0)\\l(Some (1 + 0)) anon_fun.get_min_and_direction.0\\l(List.tl (Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_ranges)&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "expr_1165 -&gt; call_1158 [label=&quot;calls&quot;];\n",
       "expr_1165 -&gt; call_1158 [label=&quot;calls&quot;];\n",
       "call_170 [label=&quot;List.for_all anon_fun.stopping_if_for_all.0\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;green&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "call_170 -&gt; expr_1397 [label=&quot;=&quot;];\n",
       "expr_1397 [label=&quot;(Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges =\\l[]\\l\\|\\| not\\l   (20000 \\&lt;=\\l    List.hd\\l    (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges)\\l   &amp;&amp; List.for_all anon_fun.stopping_if_for_all.0\\l      (List.tl\\l       (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges)&quot;,shape=box,style=filled,color=&quot;grey&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_170 [label=&quot;calls&quot;];\n",
       "call_1038 [label=&quot;List.fold_right anon_fun.get_min_range.0\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_range_max\\l(List.tl (Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges)&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "expr_1041 -&gt; call_1038 [label=&quot;calls&quot;];\n",
       "expr_1041 -&gt; call_1038 [label=&quot;calls&quot;];\n",
       "call_1394 [label=&quot;List.for_all anon_fun.stopping_if_for_all.0\\l(List.tl (Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges)&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "expr_1397 -&gt; call_1394 [label=&quot;calls&quot;];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-8f4f9393-2e74-4ff7-82a2-740f338cd445';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-bf3c02f4-df44-479f-85f9-0d296fc9a376';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "theorem stopping_if_for_all state =\n",
    "  let open Sensor_msgs in\n",
    "  match state.incoming with None | Some (Clock _ ) -> true \n",
    "  | Some ( Sensor data ) ->\n",
    "  (  data.laserScan_ranges <> []\n",
    "  && List.for_all (fun x -> x < 20000) data.laserScan_ranges    \n",
    "  ) ==> (one_step state).mode = Turning"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Imandra successfully proves the `stopping_if_for_all` theorem, but our ultimate goal is to prove the theorem when **some** of the values in `laserScan_ranges` are less than the cutoff. If we simply try to replace the `List.for_all` with `List.exists`, Imandra will fail to either prove or disprove the theorem.  The inductive structure of this proof is too complex for Imandra to figure out automatically without any hints from the user. We need to help it with the overall logic of the proof. To do that we will break this final theorem into several smaller steps, making a rough \"sketch\" of the inductive proof we want and and ask Imandra to fill in the gaps."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As a first step, we extract the anonymous threshold function and prove a lemma that if the `get_min_range` function returns a value satisfying the threshold, then the conclusion about the `one_step` function holds:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val under_threshold : int -> bool = <fun>\n",
       "val lemma1 : state -> bool = <fun>\n"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/html": [
       "<div><div>Proved<div class=\"imandra-alternatives\" id=\"alt-395fa93a-9d2c-4594-be86-a1fed7e157d0\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>proof</a></li><li class=\"\" data-toggle=\"tab\"><a>call graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-proof-top\"><div class=\"imandra-fold panel panel-default\" id=\"fold-55aaf097-3842-4bfb-b133-d49cc6cf3e3c\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>proof</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-proof\"><div class=\"imandra-alternatives\" id=\"alt-bc82126f-3db8-4f1f-b7ee-44d8344b0c83\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>summary</a></li><li class=\"\" data-toggle=\"tab\"><a>full</a></li><li class=\"\" data-toggle=\"tab\"><a>graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-table\" id=\"table-09376e2a-c513-4c26-b751-beef21677cbd\"><table><tr><td><b>ground_instances</b></td><td>0</td></tr><tr><td><b>definitions</b></td><td>0</td></tr><tr><td><b>inductions</b></td><td>0</td></tr><tr><td><b>search_time</b></td><td><pre>0.009s</pre></td></tr><tr><td><b>details</b></td><td><div class=\"imandra-fold panel panel-default\" id=\"fold-73e36ce9-e503-4391-888d-bf7b6677d23d\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-table\" id=\"table-f9476c83-73b8-4a35-afb6-6b9d5c9946ff\"><table><tr><td><b>smt_stats</b></td><td><div class=\"imandra-table\" id=\"table-462ac18b-c437-496f-b17b-94b38832c375\"><table><tr><td><b>num checks</b></td><td>2</td></tr><tr><td><b>arith assert lower</b></td><td>6</td></tr><tr><td><b>arith pivots</b></td><td>3</td></tr><tr><td><b>rlimit count</b></td><td>2362</td></tr><tr><td><b>mk clause</b></td><td>45</td></tr><tr><td><b>mk bool var</b></td><td>244</td></tr><tr><td><b>arith assert upper</b></td><td>17</td></tr><tr><td><b>datatype splits</b></td><td>26</td></tr><tr><td><b>decisions</b></td><td>60</td></tr><tr><td><b>arith add rows</b></td><td>1</td></tr><tr><td><b>propagations</b></td><td>101</td></tr><tr><td><b>conflicts</b></td><td>16</td></tr><tr><td><b>arith fixed eqs</b></td><td>2</td></tr><tr><td><b>datatype accessor ax</b></td><td>49</td></tr><tr><td><b>minimized lits</b></td><td>1</td></tr><tr><td><b>arith conflicts</b></td><td>1</td></tr><tr><td><b>arith assert diseq</b></td><td>1</td></tr><tr><td><b>datatype constructor ax</b></td><td>57</td></tr><tr><td><b>num allocs</b></td><td>1084619250</td></tr><tr><td><b>added eqs</b></td><td>361</td></tr><tr><td><b>del clause</b></td><td>25</td></tr><tr><td><b>arith eq adapter</b></td><td>5</td></tr><tr><td><b>memory</b></td><td>42.980000</td></tr><tr><td><b>max memory</b></td><td>42.980000</td></tr></table></div></td></tr></table></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-73e36ce9-e503-4391-888d-bf7b6677d23d';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></td></tr></table></div></div><div class=\"tab-pane\"><div class=\"imandra-fold panel panel-default\" id=\"fold-1c7269d5-9ea4-4348-972e-640f199bc09b\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.009s]\n",
       "  if :var_0:.incoming = None\n",
       "     || Is_a(Some, :var_0:.incoming)\n",
       "        &amp;&amp; Is_a(Clock, Option.get :var_0:.incoming)\n",
       "  then true\n",
       "  else\n",
       "    not\n",
       "    ((Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\n",
       "     = [])\n",
       "    &amp;&amp; List.fold_right anon_fun.get_min_range.0\n",
       "       (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_range_max\n",
       "       (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\n",
       "       &lt; 20000\n",
       "    ==&gt; (if :var_0:.incoming = None then :var_0:\n",
       "         else if Is_a(Sensor, Option.get :var_0:.incoming) then … else …).mode\n",
       "        = Turning</pre></li><li><div><h4>simplify</h4><div class=\"imandra-table\" id=\"table-7f37ea7b-be1d-4d5b-9466-2d784499ab3d\"><table><tr><td><b>into</b></td><td><pre>((:var_0:.incoming = None\n",
       "  || Is_a(Some, :var_0:.incoming) &amp;&amp; Is_a(Clock, Option.get :var_0:.incoming))\n",
       " || not\n",
       "    (not\n",
       "     ((Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\n",
       "      = [])\n",
       "     &amp;&amp; not\n",
       "        (20000 &lt;=\n",
       "         List.fold_right anon_fun.get_min_range.0\n",
       "         (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_range_max\n",
       "         (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges)))\n",
       "|| (if :var_0:.incoming = None then :var_0:\n",
       "    else\n",
       "    if Is_a(Sensor, Option.get :var_0:.incoming)\n",
       "    then if :var_0:.mode = Driving then … else …\n",
       "    else if :var_0:.mode = Driving then … else …).mode\n",
       "   = Turning</pre></td></tr><tr><td><b>expansions</b></td><td><pre>[]</pre></td></tr><tr><td><b>rewrite_steps</b></td><td><ul></ul></td></tr><tr><td><b>forward_chaining</b></td><td><ul></ul></td></tr></table></div></div></li><li><div><h4>unsat</h4><pre>(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_3242 (get.Some.0_3244 (inco…</pre></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-1c7269d5-9ea4-4348-972e-640f199bc09b';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-90e987b2-30ca-4686-a1dd-c2ec1524e35e\"><textarea style=\"display: none\">digraph &quot;proof&quot; {\n",
       "p_255 [label=&quot;Start (if :var_0:.incoming = None\\l          \\|\\| Is_a(Some, :var_0:.incoming)\\l             &amp;&amp; Is_a(Clock, Option.get :var_0:.incoming)\\l       then true\\l       else\\l         not\\l         ((Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\\l          = [])\\l         &amp;&amp; List.fold_right anon_fun.get_min_range.0\\l            (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_range_max\\l            (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\\l            \\&lt; 20000\\l         ==\\&gt; (if :var_0:.incoming = None then :var_0:\\l              else\\l              if Is_a(Sensor, Option.get :var_0:.incoming) then … else …).mode\\l             = Turning\\l       :time 0.009s)&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_255 -&gt; p_254 [label=&quot;&quot;];\n",
       "p_254 [label=&quot;Simplify (((:var_0:.incoming = None\\l            \\|\\| Is_a(Some, :var_0:.incoming)\\l               &amp;&amp; Is_a(Clock, Option.get :var_0:.incoming))\\l           \\|\\| not\\l              (not\\l               ((Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges\\l                = [])\\l               &amp;&amp; not\\l                  (20000 \\&lt;=\\l                   List.fold_right anon_fun.get_min_range.0\\l                   (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_range_max\\l                   (Destruct(Sensor, 0, Option.get :var_0:.incoming)).Sensor_msgs.laserScan_ranges)))\\l          \\|\\| (if :var_0:.incoming = None then :var_0:\\l              else\\l              if Is_a(Sensor, Option.get :var_0:.incoming)\\l              then if :var_0:.mode = Driving then … else …\\l              else if :var_0:.mode = Driving then … else …).mode\\l             = Turning\\l          :expansions [] :rw [] :fc [])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_254 -&gt; p_253 [label=&quot;&quot;];\n",
       "p_253 -&gt; p_z3_1039 [label=&quot;&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_z3_1039 [label=&quot;(let ((a!1 (Sensor_msgs.laserScan_ranges_2144\n",
       "             (get.Sensor.0_3242 (get.Some.0_3244 (inco…&quot;,shape=box,fontname=&quot;courier&quot;,fontsize=14];p_253 [label=&quot;unsat&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-90e987b2-30ca-4686-a1dd-c2ec1524e35e';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-bc82126f-3db8-4f1f-b7ee-44d8344b0c83';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-55aaf097-3842-4bfb-b133-d49cc6cf3e3c';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-1c5b9c89-9f1c-4934-9e26-560afd4b1de3\"><textarea style=\"display: none\">digraph &quot;call graph&quot; {\n",
       "goal [label=&quot;not\\l(((state.incoming = None\\l   \\|\\| Is_a(Some, state.incoming) &amp;&amp; Is_a(Clock, Option.get state.incoming))\\l  \\|\\| not\\l     (not\\l      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\\l       = [])\\l      &amp;&amp; not\\l         (20000 \\&lt;=\\l          List.fold_right anon_fun.get_min_range.0\\l          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\\l          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges)))\\l \\|\\| (if state.incoming = None then state\\l     else\\l     if Is_a(Sensor, Option.get state.incoming)\\l     then if state.mode = Driving then … else …\\l     else if state.mode = Driving then … else …).mode\\l    = Turning)&quot;,shape=box,style=filled,color=&quot;cyan&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "call_190 [label=&quot;foldi ((Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_range_max, 0) None\\lanon_fun.get_min_and_direction.0\\l(Destruct(Sensor, 0, …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_190 [label=&quot;calls&quot;];\n",
       "call_186 [label=&quot;List.length\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_186 [label=&quot;calls&quot;];\n",
       "call_177 [label=&quot;List.fold_right anon_fun.get_min_range.0\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_range_max\\l(Destruct(Sensor, 0, Option.get …)).Sensor_msgs.laserScan_ranges&quot;,shape=box,style=filled,color=&quot;yellow&quot;,fontname=&quot;courier&quot;,fontsize=14];\n",
       "goal -&gt; call_177 [label=&quot;calls&quot;];\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-1c5b9c89-9f1c-4934-9e26-560afd4b1de3';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-395fa93a-9d2c-4594-be86-a1fed7e157d0';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "let under_threshold x = x < 20000\n",
    "\n",
    "lemma lemma1 state =\n",
    "  let open Sensor_msgs in\n",
    "  match state.incoming with None | Some (Clock _ ) -> true \n",
    "  | Some ( Sensor data ) ->\n",
    "  (  data.laserScan_ranges <> []\n",
    "  && under_threshold (get_min_range data.laserScan_range_max data.laserScan_ranges)\n",
    "  ) ==> (one_step state).mode = Turning"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next, we prove a \"bridge\" lemma that translates between the `get_min_range`\n",
    "concept and the `List.exists` concept for the `under_threshold` function. Then, we `[@@apply]` the two lemmas above to prove our final theorem with the `List.exists` condition: these proofs require induction - to tell Imandra to use induction one should add the `[@@induct]` attribute to the theorem declaration:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "val bridge : int -> int list -> bool = <fun>\n",
       "\u001b[37;1mGoal\u001b[0m:\n",
       "\n",
       "List.exists under_threshold lst ==> under_threshold (get_min_range max lst).\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "1 nontautological subgoal.\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "\u001b[37;1mSubgoal 1\u001b[0m:\n",
       "\n",
       " H0. List.exists under_threshold lst\n",
       " H1. 20000 <= List.fold_right anon_fun.get_min_range.0 max lst\n",
       "|---------------------------------------------------------------------------\n",
       " false\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "Verified up to bound 5 (after 0.011s).\n",
       "\r",
       "\u001b[2K\r\n",
       "\r",
       "\u001b[2K\r",
       "Must try induction.\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "\u001b[36;1mInduction scheme\u001b[0m:\n",
       "\n",
       " φ [] max && (lst <> [] && φ (List.tl lst) max ==> φ lst max).\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "2 nontautological subgoals.\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "\u001b[37;1mSubgoal 1.2\u001b[0m:\n",
       "\n",
       " H0. List.exists under_threshold []\n",
       " H1. 20000 <= List.fold_right anon_fun.get_min_range.0 max []\n",
       "|---------------------------------------------------------------------------\n",
       " false\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "But simplification reduces this to true, using the definition of \u001b[34;1mList.exists\u001b[0m.\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "\u001b[37;1mSubgoal 1.1\u001b[0m:\n",
       "\n",
       " H0. lst <> []\n",
       " H1. not (List.exists under_threshold (List.tl lst))\n",
       "     || not\n",
       "        (20000 <= List.fold_right anon_fun.get_min_range.0 max (List.tl lst))\n",
       " H2. List.exists under_threshold lst\n",
       " H3. 20000 <= List.fold_right anon_fun.get_min_range.0 max lst\n",
       "|---------------------------------------------------------------------------\n",
       " false\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "But simplification reduces this to true, using the definitions of \u001b[34;1mList.exists\n",
       "\u001b[0mand\u001b[34;1m List.fold_right\u001b[0m.\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "val stopping_if_exists : state -> bool = <fun>\n",
       "\u001b[37;1mGoal\u001b[0m:\n",
       "\n",
       "if state.incoming = None\n",
       "   || Is_a(Some, state.incoming) && Is_a(Clock, Option.get state.incoming)\n",
       "then true\n",
       "else\n",
       "  let (data : Sensor_msgs.laserScan)\n",
       "      = Destruct(Sensor, 0, Option.get state.incoming)\n",
       "  in\n",
       "  data.Sensor_msgs.laserScan_ranges <> []\n",
       "  && List.exists under_threshold data.Sensor_msgs.laserScan_ranges\n",
       "  ==> (one_step state).mode = Turning.\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "1 nontautological subgoal.\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "\u001b[37;1mSubgoal 1\u001b[0m:\n",
       "\n",
       " H0. not\n",
       "     ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "      = [])\n",
       " H1. List.exists under_threshold\n",
       "     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "|---------------------------------------------------------------------------\n",
       " C0. state.incoming = None\n",
       " C1. Is_a(Some, state.incoming) && Is_a(Clock, Option.get state.incoming)\n",
       " C2. (if state.incoming = None then state\n",
       "      else\n",
       "      if Is_a(Sensor, Option.get state.incoming)\n",
       "      then\n",
       "        if state.mode = Driving\n",
       "        then\n",
       "          if 20000 <=\n",
       "             (if (List.length\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                  / 2)\n",
       "                 <=\n",
       "                 (foldi\n",
       "                  ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                   0)\n",
       "                  None anon_fun.get_min_and_direction.0\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "              then\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CCW)\n",
       "              else\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CW)).0\n",
       "          then\n",
       "            {mode = Driving; min_range = None; direction = None;\n",
       "             incoming = None; outgoing = None}\n",
       "          else\n",
       "            {mode = Turning;\n",
       "             min_range =\n",
       "             Some\n",
       "             (if (List.length\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                  / 2)\n",
       "                 <=\n",
       "                 (foldi\n",
       "                  ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                   0)\n",
       "                  None anon_fun.get_min_and_direction.0\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "              then\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CCW)\n",
       "              else\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CW)).0;\n",
       "             direction =\n",
       "             Some\n",
       "             (if (List.length\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                  / 2)\n",
       "                 <=\n",
       "                 (foldi\n",
       "                  ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                   0)\n",
       "                  None anon_fun.get_min_and_direction.0\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "              then\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CCW)\n",
       "              else\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CW)).1;\n",
       "             incoming = None; outgoing = None}\n",
       "        else\n",
       "        if state.min_range = None && state.mode = Turning\n",
       "        then\n",
       "          if (if (List.length\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                  / 2)\n",
       "                 <=\n",
       "                 (foldi\n",
       "                  ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                   0)\n",
       "                  None anon_fun.get_min_and_direction.0\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "              then\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CCW)\n",
       "              else\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CW)).0\n",
       "             <= 25000\n",
       "          then\n",
       "            {mode = Turning;\n",
       "             min_range =\n",
       "             Some\n",
       "             (if (List.length\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                  / 2)\n",
       "                 <=\n",
       "                 (foldi\n",
       "                  ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                   0)\n",
       "                  None anon_fun.get_min_and_direction.0\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "              then\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CCW)\n",
       "              else\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CW)).0;\n",
       "             direction =\n",
       "             Some\n",
       "             (if (List.length\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                  / 2)\n",
       "                 <=\n",
       "                 (foldi\n",
       "                  ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                   0)\n",
       "                  None anon_fun.get_min_and_direction.0\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "              then\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CCW)\n",
       "              else\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CW)).1;\n",
       "             incoming = None; outgoing = None}\n",
       "          else\n",
       "            {mode = Driving; min_range = None; direction = None;\n",
       "             incoming = None; outgoing = None}\n",
       "        else\n",
       "        if (if (List.length\n",
       "                (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                / 2)\n",
       "               <=\n",
       "               (foldi\n",
       "                ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                 0)\n",
       "                None anon_fun.get_min_and_direction.0\n",
       "                (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "            then\n",
       "              (List.fold_right anon_fun.get_min_range.0\n",
       "               (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "               (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "               CCW)\n",
       "            else\n",
       "              (List.fold_right anon_fun.get_min_range.0\n",
       "               (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "               (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "               CW)).0\n",
       "           <= 25000\n",
       "        then\n",
       "          if (if (List.length\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                  / 2)\n",
       "                 <=\n",
       "                 (foldi\n",
       "                  ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                   0)\n",
       "                  None anon_fun.get_min_and_direction.0\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "              then\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CCW)\n",
       "              else\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CW)).0\n",
       "             <= Option.get state.min_range\n",
       "          then\n",
       "            {mode = Turning;\n",
       "             min_range =\n",
       "             Some\n",
       "             (if (List.length\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                  / 2)\n",
       "                 <=\n",
       "                 (foldi\n",
       "                  ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                   0)\n",
       "                  None anon_fun.get_min_and_direction.0\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "              then\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CCW)\n",
       "              else\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CW)).0;\n",
       "             direction =\n",
       "             Some\n",
       "             (if (List.length\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "                  / 2)\n",
       "                 <=\n",
       "                 (foldi\n",
       "                  ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "                   0)\n",
       "                  None anon_fun.get_min_and_direction.0\n",
       "                  (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       "              then\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CCW)\n",
       "              else\n",
       "                (List.fold_right anon_fun.get_min_range.0\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,\n",
       "                 CW)).1;\n",
       "             incoming = None; outgoing = None}\n",
       "          else\n",
       "            {mode = state.mode; min_range = state.min_range;\n",
       "             direction = state.direction; incoming = None; outgoing = None}\n",
       "        else\n",
       "          {mode = Driving; min_range = None; direction = None;\n",
       "           incoming = None; outgoing = None}\n",
       "      else\n",
       "      if state.mode = Driving\n",
       "      then\n",
       "        {mode = state.mode; min_range = state.min_range;\n",
       "         direction = state.direction; incoming = None;\n",
       "         outgoing =\n",
       "         Some\n",
       "         (Twist\n",
       "          {Geometry_msgs.twist_linear =\n",
       "           {Geometry_msgs.vector3_x = 10000; Geometry_msgs.vector3_y = 0;\n",
       "            Geometry_msgs.vector3_z = 0};\n",
       "           Geometry_msgs.twist_angular =\n",
       "           {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;\n",
       "            Geometry_msgs.vector3_z = 0}})}\n",
       "      else\n",
       "      if state.direction = None\n",
       "         || Is_a(Some, state.direction) && Option.get state.direction = CW\n",
       "      then\n",
       "        {mode = state.mode; min_range = state.min_range;\n",
       "         direction = state.direction; incoming = None;\n",
       "         outgoing =\n",
       "         Some\n",
       "         (Twist\n",
       "          {Geometry_msgs.twist_linear =\n",
       "           {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;\n",
       "            Geometry_msgs.vector3_z = 0};\n",
       "           Geometry_msgs.twist_angular =\n",
       "           {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;\n",
       "            Geometry_msgs.vector3_z = 10000}})}\n",
       "      else\n",
       "        {mode = state.mode; min_range = state.min_range;\n",
       "         direction = state.direction; incoming = None;\n",
       "         outgoing =\n",
       "         Some\n",
       "         (Twist\n",
       "          {Geometry_msgs.twist_linear =\n",
       "           {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;\n",
       "            Geometry_msgs.vector3_z = 0};\n",
       "           Geometry_msgs.twist_angular =\n",
       "           {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;\n",
       "            Geometry_msgs.vector3_z = -10000}})}).mode\n",
       "     = Turning\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "This simplifies, using the forward-chaining rule \u001b[33;1mList.len_nonnegative\u001b[0m to the\n",
       "following 8 subgoals:\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "\u001b[37;1mSubgoal 1.8\u001b[0m:\n",
       "\n",
       " H0. 20000 <=\n",
       "     List.fold_right anon_fun.get_min_range.0\n",
       "     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max\n",
       "     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       " H1. (List.length\n",
       "      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       "      / 2)\n",
       "     <=\n",
       "     (foldi\n",
       "      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,\n",
       "       0)\n",
       "      None anon_fun.get_min_and_direction.0\n",
       "      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1\n",
       " H2. state.mode = Driving\n",
       " H3. List.exists under_threshold\n",
       "     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges\n",
       " H4. (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges <> []\n",
       "|---------------------------------------------------------------------------\n",
       " C0. Is_a(Clock, Option.get state.incoming)\n",
       " C1. state.incoming = None\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "Verified up to bound 5 (after 0.010s).\n",
       "\r",
       "\u001b[2K\r\n",
       "\r",
       "\u001b[2K\r",
       "\u001b[32;1mNote:\u001b[0m We must proceed by induction, but our current subgoal is less\n",
       "appropriate for induction than our original conjecture. Thus, we prefer to\n",
       "abandon our work until now and return our focus to the original conjecture\n",
       "which we shall attempt to prove by induction directly.\n",
       "\n",
       "\r",
       "\u001b[2K\r",
       "\u001b[31;1mError\u001b[0m: No suitable induction variables for structural induction - perhaps try functional induction\n"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/html": [
       "<div><div>Proved<div class=\"imandra-alternatives\" id=\"alt-221cdda8-345e-4961-b706-59487e6c248d\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>proof</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-proof-top\"><div class=\"imandra-fold panel panel-default\" id=\"fold-579deeae-1506-4769-af93-dedd49c5afd5\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>proof</span></div></div><div class=\"panel-body collapse\"><div class=\"imandra-proof\"><div class=\"imandra-alternatives\" id=\"alt-67ba287a-7215-4d1f-8245-efd92de3da96\"><ul class=\"nav nav-tabs\"><li class=\"active\" data-toggle=\"tab\"><a>summary</a></li><li class=\"\" data-toggle=\"tab\"><a>full</a></li><li class=\"\" data-toggle=\"tab\"><a>graph</a></li></ul><div class=\"tab-content\"><div class=\"tab-pane active\"><div class=\"imandra-table\" id=\"table-926f806e-d2fc-41c0-9e65-98e78ef005f8\"><table><tr><td><b>ground_instances</b></td><td>0</td></tr><tr><td><b>definitions</b></td><td>5</td></tr><tr><td><b>inductions</b></td><td>1</td></tr><tr><td><b>search_time</b></td><td><pre>0.073s</pre></td></tr></table></div></div><div class=\"tab-pane\"><div class=\"imandra-fold panel panel-default\" id=\"fold-9d1f4636-cd03-4f4c-b7aa-99043c235acc\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>Expand</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.073s, &quot;Goal&quot;]\n",
       "  List.exists under_threshold :var_0:\n",
       "  ==&gt; List.fold_right anon_fun.get_min_range.0 :var_1: :var_0: &lt; 20000</pre></li><li><div><h4>subproof</h4><div class=\"imandra-fold panel panel-default\" id=\"fold-a89656c1-f4af-456f-aeb1-9e7862cfae84\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>not (List.exists under_threshold lst)\n",
       "|| not (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max lst)</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.073s, &quot;1&quot;]\n",
       "  not (List.exists under_threshold lst)\n",
       "  || not (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max lst)</pre></li><li><pre>induction on (structural+ lst)\n",
       ":scheme φ [] max &amp;&amp; (lst &lt;&gt; [] &amp;&amp; φ (List.tl lst) max ==&gt; φ lst max)</pre></li><li><div><pre>Split ((not (List.exists under_threshold [])\n",
       "        || not (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max []))\n",
       "       &amp;&amp; ((not\n",
       "            (lst &lt;&gt; []\n",
       "             &amp;&amp; (not (List.exists under_threshold (List.tl lst))\n",
       "                 || not\n",
       "                    (20000 &lt;=\n",
       "                     List.fold_right anon_fun.get_min_range.0 max\n",
       "                     (List.tl lst))))\n",
       "            || not (List.exists under_threshold lst))\n",
       "           || not (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max lst))\n",
       "       :cases [not (List.exists under_threshold [])\n",
       "               || not\n",
       "                  (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max []);\n",
       "               ((not (lst &lt;&gt; [])\n",
       "                 || not\n",
       "                    (not (List.exists under_threshold (List.tl lst))\n",
       "                     || not\n",
       "                        (20000 &lt;=\n",
       "                         List.fold_right anon_fun.get_min_range.0 max\n",
       "                         (List.tl lst))))\n",
       "                || not (List.exists under_threshold lst))\n",
       "               || not\n",
       "                  (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max lst)])</pre><ul><li><div><h5>subproof</h5><div class=\"imandra-fold panel panel-default\" id=\"fold-affa88de-e8b4-42e6-9689-4e7550b0acf9\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>((not (lst &lt;&gt; [])\n",
       "  || not\n",
       "     (not (List.exists under_threshold (List.tl lst))\n",
       "      || not\n",
       "         (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max (List.tl lst))))\n",
       " || not (List.exists under_threshold lst))\n",
       "|| not (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max lst)</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.044s, &quot;1.1&quot;]\n",
       "  ((not (lst &lt;&gt; [])\n",
       "    || not\n",
       "       (not (List.exists under_threshold (List.tl lst))\n",
       "        || not\n",
       "           (20000 &lt;=\n",
       "            List.fold_right anon_fun.get_min_range.0 max (List.tl lst))))\n",
       "   || not (List.exists under_threshold lst))\n",
       "  || not (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max lst)</pre></li><li><div><h6>simplify</h6><div class=\"imandra-table\" id=\"table-ca018a10-1ac3-47f2-b39b-c1930033e02f\"><table><tr><td><b>into</b></td><td><pre>true</pre></td></tr><tr><td><b>expansions</b></td><td><pre>[List.fold_right, List.exists, List.fold_right, List.exists]</pre></td></tr><tr><td><b>rewrite_steps</b></td><td><ul></ul></td></tr><tr><td><b>forward_chaining</b></td><td><ul></ul></td></tr></table></div></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-affa88de-e8b4-42e6-9689-4e7550b0acf9';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></li><li><div><h5>subproof</h5><div class=\"imandra-fold panel panel-default\" id=\"fold-236c03b7-e219-4a5b-8bd0-132682af38cb\"><div class=\"panel-heading\"><div><i class=\"fa fa-chevron-down hidden\"></i><i class=\"fa fa-chevron-right\"></i><span>not (List.exists under_threshold [])\n",
       "|| not (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max [])</span></div></div><div class=\"panel-body collapse\"><ul><li><pre>start[0.044s, &quot;1.2&quot;]\n",
       "  not (List.exists under_threshold [])\n",
       "  || not (20000 &lt;= List.fold_right anon_fun.get_min_range.0 max [])</pre></li><li><div><h6>simplify</h6><div class=\"imandra-table\" id=\"table-f7623acc-907d-4f54-b4d1-1e6be7abe750\"><table><tr><td><b>into</b></td><td><pre>true</pre></td></tr><tr><td><b>expansions</b></td><td><pre>List.exists</pre></td></tr><tr><td><b>rewrite_steps</b></td><td><ul></ul></td></tr><tr><td><b>forward_chaining</b></td><td><ul></ul></td></tr></table></div></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-236c03b7-e219-4a5b-8bd0-132682af38cb';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></li></ul></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-a89656c1-f4af-456f-aeb1-9e7862cfae84';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></li></ul></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-9d1f4636-cd03-4f4c-b7aa-99043c235acc';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div><div class=\"tab-pane\"><div class=\"imandra-graphviz\" id=\"graphviz-d5d36830-b97e-4f27-9ca6-d4821a192e8e\"><textarea style=\"display: none\">digraph &quot;proof&quot; {\n",
       "p_299 [label=&quot;Start (List.exists under_threshold :var_0:\\l       ==\\&gt; List.fold_right anon_fun.get_min_range.0 :var_1: :var_0: \\&lt; 20000\\l       :name \\&quot;Goal\\&quot; :time 0.073s)&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_299 -&gt; p_297 [label=&quot;&quot;];\n",
       "subgraph cluster_298 {\n",
       "  color=blue;\n",
       "p_297 [label=&quot;Start (not (List.exists under_threshold lst)\\l       \\|\\| not (20000 \\&lt;= List.fold_right anon_fun.get_min_range.0 max lst)\\l       :name \\&quot;1\\&quot; :time 0.073s)&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_297 -&gt; p_296 [label=&quot;&quot;];\n",
       "p_296 [label=&quot;Induct ((structural+ lst),\\l        :scheme φ [] max\\l                &amp;&amp; (lst \\&lt;\\&gt; [] &amp;&amp; φ (List.tl lst) max ==\\&gt; φ lst max))&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_296 -&gt; p_295 [label=&quot;&quot;];\n",
       "p_295 [label=&quot;Split ((not (List.exists under_threshold [])\\l        \\|\\| not (20000 \\&lt;= List.fold_right anon_fun.get_min_range.0 max []))\\l       &amp;&amp; ((not\\l            (lst \\&lt;\\&gt; []\\l             &amp;&amp; (not (List.exists under_threshold (List.tl lst))\\l                 \\|\\| not\\l                    (20000 \\&lt;=\\l                     List.fold_right anon_fun.get_min_range.0 max\\l                     (List.tl lst))))\\l            \\|\\| not (List.exists under_threshold lst))\\l           \\|\\| not (20000 \\&lt;= List.fold_right anon_fun.get_min_range.0 max lst))\\l       :cases [not (List.exists under_threshold [])\\l               \\|\\| not\\l                  (20000 \\&lt;= List.fold_right anon_fun.get_min_range.0 max []);\\l               ((not (lst \\&lt;\\&gt; [])\\l                 \\|\\| not\\l                    (not (List.exists under_threshold (List.tl lst))\\l                     \\|\\| not\\l                        (20000 \\&lt;=\\l                         List.fold_right anon_fun.get_min_range.0 max\\l                         (List.tl lst))))\\l                \\|\\| not (List.exists under_threshold lst))\\l               \\|\\| not\\l                  (20000 \\&lt;= List.fold_right anon_fun.get_min_range.0 max lst)])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_295 -&gt; p_290 [label=&quot;&quot;];\n",
       "subgraph cluster_291 {\n",
       "  color=blue;\n",
       "p_290 [label=&quot;Start (((not (lst \\&lt;\\&gt; [])\\l         \\|\\| not\\l            (not (List.exists under_threshold (List.tl lst))\\l             \\|\\| not\\l                (20000 \\&lt;=\\l                 List.fold_right anon_fun.get_min_range.0 max (List.tl lst))))\\l        \\|\\| not (List.exists under_threshold lst))\\l       \\|\\| not (20000 \\&lt;= List.fold_right anon_fun.get_min_range.0 max lst)\\l       :name \\&quot;1.1\\&quot; :time 0.044s)&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_290 -&gt; p_289 [label=&quot;&quot;];\n",
       "p_289 [label=&quot;Simplify (true\\l          :expansions [List.fold_right;\\l                       List.exists;\\l                       List.fold_right;\\l                       List.exists]\\l          :rw [] :fc [])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "}\n",
       "p_295 -&gt; p_293 [label=&quot;&quot;];\n",
       "subgraph cluster_294 {\n",
       "  color=blue;\n",
       "p_293 [label=&quot;Start (not (List.exists under_threshold [])\\l       \\|\\| not (20000 \\&lt;= List.fold_right anon_fun.get_min_range.0 max [])\\l       :name \\&quot;1.2\\&quot; :time 0.044s)&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "p_293 -&gt; p_292 [label=&quot;&quot;];\n",
       "p_292 [label=&quot;Simplify (true :expansions [List.exists] :rw [] :fc [])&quot;,shape=box,style=filled,fontname=&quot;courier&quot;,fontsize=14];\n",
       "}\n",
       "}\n",
       "}\n",
       "</textarea><button class=\"btn btn-primary\">Load graph</button><div class=\"imandra-graphviz-loading display-none\">Loading..</div><div class=\"imandra-graphviz-target\"></div><script>\n",
       "require(['nbextensions/nbimandra/graphviz'], function (graphviz) {\n",
       "  var target = '#graphviz-d5d36830-b97e-4f27-9ca6-d4821a192e8e';\n",
       "  graphviz.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-67ba287a-7215-4d1f-8245-efd92de3da96';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/fold'], function (fold) {\n",
       "  var target = '#fold-579deeae-1506-4769-af93-dedd49c5afd5';\n",
       "  fold.hydrate(target);\n",
       "});\n",
       "</script></div></div></div></div><script>\n",
       "require(['nbextensions/nbimandra/alternatives'], function (alternatives) {\n",
       "  var target = '#alt-221cdda8-345e-4961-b706-59487e6c248d';\n",
       "  alternatives.hydrate(target);\n",
       "});\n",
       "</script></div></div></div>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "lemma bridge max lst =\n",
    "  List.exists under_threshold lst ==> under_threshold (get_min_range max lst)\n",
    "  [@@induct]\n",
    "\n",
    "theorem stopping_if_exists state =\n",
    "  let open Sensor_msgs in\n",
    "  match state.incoming with None | Some (Clock _ ) -> true \n",
    "  | Some ( Sensor data ) ->\n",
    "  (  data.laserScan_ranges <> []\n",
    "  && List.exists under_threshold data.laserScan_ranges\n",
    "  ) ==> (one_step state).mode = Turning\n",
    "[@@apply lemma1 state]\n",
    "[@@apply bridge\n",
    "    (match state.incoming with Some (Sensor data) -> data.laserScan_range_max | _ -> 0)\n",
    "    (match state.incoming with Some (Sensor data) -> data.laserScan_ranges | _ -> []) ]\n",
    "[@@induct]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Imandra",
   "language": "",
   "name": "imandra"
  },
  "language_info": {
   "codemirror_mode": "mllike",
   "file_extension": ".ml",
   "mimetype": "text",
   "name": "ocaml",
   "version": "0.1.0"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}