Creating and Verifying a ROS Node

Imandrabot

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:

Imandrabot

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.

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.

1. ROS message OCaml types

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.

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:

In [1]:
module Geometry_msgs = struct
  type vector3 =
    { vector3_x : int
    ; vector3_y : int
    ; vector3_z : int
    }
  type twist =
    { twist_linear  : vector3
    ; twist_angular : vector3
    }
end
Out[1]:
module Geometry_msgs :
  sig
    type vector3 = { vector3_x : int; vector3_y : int; vector3_z : int; }
    type twist = { twist_linear : vector3; twist_angular : vector3; }
  end

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).

Let's move on and declare the incoming messages:

  • LaserScan sensor input message from the sensor_msgs ROS package
  • and the Clock message from the Rosgraph_msg ROS package

We define the wrapping modules for both messages and declare their datatypes:

In [2]:
module Sensor_msgs = struct
  type laserScan =
    { laserScan_range_min : int
    ; laserScan_range_max : int
    ; laserScan_ranges : int list
    }
end
module Rosgraph_msgs = struct
  type time =
    { seconds     : int
    ; nanoseconds : int
    }
  type clock = { clock : time }
end
Out[2]:
module Sensor_msgs :
  sig
    type laserScan = {
      laserScan_range_min : int;
      laserScan_range_max : int;
      laserScan_ranges : int list;
    }
  end
module Rosgraph_msgs :
  sig
    type time = { seconds : int; nanoseconds : int; }
    type clock = { clock : time; }
  end

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.

2. Creating a simple ROS Node model

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.

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:

Imandrabot

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.

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.

2.1 State datatype

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.

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:

  • the current mode of the bot -- whether we are driving forward or turning in a preferred direction
  • the latest minimal value of the ranges that the laser sensor returns
  • the preferred side for the robot to turn -- either clockwise (CW) or counter-clockwise (CCW)

Finally, we want the node to be able to send geometry_msgs/Twist ROS message depending on the stored min_range data:

In [3]:
type incoming_msg =
  | Clock  of Rosgraph_msgs.clock
  | Sensor of Sensor_msgs.laserScan

type outgoing_msg =
  | Twist of Geometry_msgs.twist

type direction = CW | CCW

type mode = Driving | Turning

type state =
  { mode : mode
  ; min_range : int option
  ; direction : direction option
  ; incoming  : incoming_msg option
  ; outgoing  : outgoing_msg option
  }
Out[3]:
type incoming_msg =
    Clock of Rosgraph_msgs.clock
  | Sensor of Sensor_msgs.laserScan
type outgoing_msg = Twist of Geometry_msgs.twist
type direction = CW | CCW
type mode = Driving | Turning
type state = {
  mode : mode;
  min_range : int option;
  direction : direction option;
  incoming : incoming_msg option;
  outgoing : outgoing_msg option;
}

2.2 State transition one_step function

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:

In [4]:
let rec foldi ~base ?(i=0) f l =
  match l with
  | [] -> base
  | x :: tail -> f i x ( foldi f ~base ~i:(i+1) tail )
Out[4]:
val foldi : base:'a -> ?i:int -> (int -> 'b -> 'a -> 'a) -> 'b list -> 'a =
  <fun>
termination proof

Termination proof

call `foldi base (Some ((if Is_a(None, ( *opt* )) then 0 else Option.get ( *opt* )) + 1)) f_2 (List.tl l)` from `foldi base ( *opt* ) f_2 l`
originalfoldi base ( *opt* ) f_2 l
subfoldi base (Some ((if Is_a(None, ( *opt* )) then 0 else Option.get ( *opt* )) + 1)) f_2 (List.tl l)
original ordinalOrdinal.Int (_cnt l)
sub ordinalOrdinal.Int (_cnt (List.tl l))
path[not Is_a([], l)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
num checks7
arith-make-feasible7
arith-max-columns10
rlimit count1551
arith-cheap-eqs1
mk clause11
datatype occurs check12
mk bool var36
arith-lower4
datatype splits1
decisions4
propagations6
arith-max-rows2
conflicts3
datatype accessor ax7
datatype constructor ax5
num allocs1004639
final checks4
added eqs26
del clause9
arith eq adapter3
arith-upper5
memory6.420000
max memory6.420000
Expand
  • start[0.015s]
      let (_x_0 : int) = count.list (const 0) l in
      let (_x_1 : ty_1 list) = List.tl l in
      let (_x_2 : int) = count.list (const 0) _x_1 in
      not Is_a([], l) && _x_0 >= 0 && _x_2 >= 0
      ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into
    let (_x_0 : ty_1 list) = List.tl l in
    let (_x_1 : int) = count.list (const 0) _x_0 in
    let (_x_2 : int) = count.list (const 0) l in
    (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
    || not ((not Is_a([], l) && _x_2 >= 0) && _x_1 >= 0)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`count.list (const 0)[0]`_1766| l_1753)
        expansions
        • unroll
          expr
          (|`count.list (const 0)[0]`_1766| (|get.::.1_1742| l_1753))
          expansions
          • unroll
            expr
            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                (|`count.list (const 0)[0]`_1766| (|get.::.…
            expansions
            • Unsat

            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.

            In [5]:
            let get_min_range max lst =
              List.fold_right ~base:max
                (fun x a -> if x < a then x else a) lst
            
            Out[5]:
            val get_min_range : int -> int list -> int = <fun>
            

            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.

            In [6]:
            let make_twist_message v omega=
              let open Geometry_msgs in
              let mkvector x y z =  { vector3_x = x; vector3_y = y; vector3_z = z   } in
              Twist { twist_linear  = mkvector v 0 0 ; twist_angular = mkvector 0 0 omega }
            
            let process_clock_message state =
              match state.mode with
              | Driving -> { state with outgoing = Some (make_twist_message 10000 0) }
              | Turning -> begin
              match state.direction with
                | None
                | Some ( CW ) -> { state with outgoing = Some (make_twist_message 0   10000) }
                | Some (CCW ) -> { state with outgoing = Some (make_twist_message 0 (-10000))}
              end
            
            Out[6]:
            val make_twist_message : int -> int -> outgoing_msg = <fun>
            val process_clock_message : state -> state = <fun>
            

            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:

            In [7]:
            let get_min_and_direction msg =
              let max = msg.Sensor_msgs.laserScan_range_max in
              let lst = msg.Sensor_msgs.laserScan_ranges in
              let min_range = get_min_range max lst in
              let mini = foldi ~base:(max, 0)
                (fun i a b -> if a < fst b then (a,i) else b) in
              let _ , idx = mini lst in
              if idx < List.length lst / 2 then min_range, CW else min_range, CCW
            
            let process_sensor_message state min_range min_direction =
              let dirving_state =
                { state with mode = Driving; min_range = None; direction = None } in
              let turning_state =
                { state with
                  mode      = Turning
                ; direction = Some min_direction
                ; min_range = Some min_range
                } in
              match state.mode , state.min_range with
              | Driving , _    -> if min_range < 20000 then turning_state else dirving_state
              | Turning , None -> if min_range > 25000 then dirving_state else turning_state
              | Turning , Some old_range ->
                if min_range > 25000 then dirving_state
                else if min_range > old_range then state else turning_state
            
            Out[7]:
            val get_min_and_direction : Sensor_msgs.laserScan -> int * direction = <fun>
            val process_sensor_message : state -> int -> direction -> state = <fun>
            

            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.

            In [8]:
            let one_step state =
              match state.incoming with None -> state | Some in_msg ->
              let state = { state with incoming = None; outgoing = None } in
              match in_msg with
              | Sensor laserScan ->
                let min_range, min_direction = get_min_and_direction laserScan in
                process_sensor_message state min_range min_direction
              | Clock  _ -> process_clock_message state
            
            Out[8]:
            val one_step : state -> state = <fun>
            

            2.3 Running the model as a ROS node

            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:

            Imandrabot

            3. Verifying the ROS node model

            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.

            3.1 Verifying outgoing Twist message at Clock ticks

            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.

            We can formally write this statement down as:

            $$ \forall s. IsClock(IncomingMessage(s)) \,\Rightarrow\, IsTwist(OutgoingMessage(OneStep(s))) $$

            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.

            We can almost literally encode this formal expression as an Imandra theorem:

            In [9]:
            let is_clock msg = match msg with  Some ( Clock _ ) -> true | _ -> false ;;
            let is_twist msg = match msg with  Some ( Twist _ ) -> true | _ -> false ;;
            
            theorem clock_creates_outbound state =
              is_clock state.incoming ==> is_twist (one_step state).outgoing
            
            Out[9]:
            val is_clock : incoming_msg option -> bool = <fun>
            val is_twist : outgoing_msg option -> bool = <fun>
            val clock_creates_outbound : state -> bool = <fun>
            
            Proved
            proof
            ground_instances0
            definitions0
            inductions0
            search_time
            0.013s
            details
            Expand
            smt_stats
            num checks2
            arith-make-feasible1
            arith-max-columns6
            rlimit count1866
            mk clause10
            mk bool var129
            datatype splits17
            decisions13
            propagations21
            conflicts8
            datatype accessor ax38
            datatype constructor ax35
            num allocs4178627
            added eqs200
            del clause5
            memory8.360000
            max memory8.360000
            Expand
            • start[0.013s]
                let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                let (_x_1 : bool) = Is_a(Clock, Option.get _x_0) in
                (if Is_a(Some, _x_0) then _x_1 else false)
                ==> Is_a(Some,
                    (if Is_a(None, _x_0) then ( :var_0: ) else if _x_1 then … else …).outgoing)
            • simplify

              into
              let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
              let (_x_1 : bool) = Is_a(Clock, Option.get _x_0) in
              not (Is_a(Some, _x_0) && _x_1)
              || Is_a(Some,
                 (if Is_a(None, _x_0) then ( :var_0: ) else if _x_1 then … else …).outgoing)
              expansions
              []
              rewrite_steps
                forward_chaining
                • Unsat

                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.

                3.2 Verifying that we never drive backwards

                As another example, let us check that, no matter what, the node will never send out a message with negative linear velocity.

                In [10]:
                let no_moving_back msg =
                    let open Geometry_msgs in
                    match msg with None -> true
                    | Some (Twist data) -> data.twist_linear.vector3_x >= 0
                
                verify ( fun state -> no_moving_back (one_step state).outgoing  )
                
                Out[10]:
                val no_moving_back : outgoing_msg option -> bool = <fun>
                - : state -> bool = <fun>
                module CX : sig val state : state end
                
                Counterexample (after 3 steps, 0.017s):
                 let (state : state) =
                  {mode = Driving; min_range = None; direction = None; incoming = None;
                   outgoing =
                    (Some
                     (Twist
                        ({Geometry_msgs.twist_linear =
                           {Geometry_msgs.vector3_x = (-7720); Geometry_msgs.vector3_y = 7;
                            Geometry_msgs.vector3_z = 8};
                          Geometry_msgs.twist_angular =
                           {Geometry_msgs.vector3_x = 9; Geometry_msgs.vector3_y = 10;
                            Geometry_msgs.vector3_z = 11}})))}
                
                Refuted
                proof attempt
                ground_instances3
                definitions0
                inductions0
                search_time
                0.017s
                details
                Expand
                smt_stats
                num checks7
                arith-make-feasible9
                arith-max-columns25
                rlimit count6389
                arith-cheap-eqs2
                mk clause49
                datatype occurs check248
                mk bool var361
                arith-lower7
                datatype splits35
                decisions169
                propagations187
                arith-max-rows7
                conflicts10
                datatype accessor ax61
                arith-bound-propagations-lp1
                datatype constructor ax150
                num allocs8234289
                final checks8
                added eqs736
                del clause4
                arith eq adapter4
                arith-upper10
                memory9.040000
                max memory9.040000
                Expand
                • start[0.017s]
                    if Is_a(None,
                       (if Is_a(None, ( :var_0: ).incoming) then ( :var_0: )
                        else if Is_a(Clock, …) then … else …).outgoing)
                    then true
                    else
                      (Destruct(Twist, 0, …)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x
                      >= 0
                • simplify

                  into
                  let (_x_0 : outgoing_msg option)
                      = (if Is_a(None, ( :var_0: ).incoming) then ( :var_0: )
                         else if Is_a(Clock, …) then … else …).outgoing
                  in
                  Is_a(None, _x_0)
                  || (Destruct(Twist, 0, Option.get _x_0)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x
                     >= 0
                  expansions
                  []
                  rewrite_steps
                    forward_chaining
                    • unroll
                      expr
                      (let ((a!1 (|Sensor_msgs.laserScan_range_max_29|
                                   (|get.Sensor.0_2100| (|get.Some.0_2102…
                      expansions
                      • unroll
                        expr
                        (let ((a!1 (|Sensor_msgs.laserScan_range_max_29|
                                     (|get.Sensor.0_2100| (|get.Some.0_2102…
                        expansions
                        • unroll
                          expr
                          (let ((a!1 (|Sensor_msgs.laserScan_ranges_30|
                                       (|get.Sensor.0_2100| (|get.Some.0_2102| (…
                          expansions
                          • Sat (Some let (state : state) = {mode = Driving; min_range = None; direction = None; incoming = None; outgoing = (Some (Twist ({Geometry_msgs.twist_linear = {Geometry_msgs.vector3_x = (-7720); Geometry_msgs.vector3_y = 7; Geometry_msgs.vector3_z = 8}; Geometry_msgs.twist_angular = {Geometry_msgs.vector3_x = 9; Geometry_msgs.vector3_y = 10; Geometry_msgs.vector3_z = 11}})))} )

                          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:

                          In [11]:
                          CX.state
                          
                          Out[11]:
                          - : state =
                          {mode = Driving; min_range = None; direction = None; incoming = None;
                           outgoing =
                            Some
                             (Twist
                               {Geometry_msgs.twist_linear =
                                 {Geometry_msgs.vector3_x = -7720; vector3_y = 7; vector3_z = 8};
                                twist_angular =
                                 {Geometry_msgs.vector3_x = 9; vector3_y = 10; vector3_z = 11}})}
                          

                          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.

                          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:

                          In [12]:
                          theorem never_goes_back state =
                            state.incoming <> None
                            ==>
                            no_moving_back (one_step state).outgoing
                          
                          Out[12]:
                          val never_goes_back : state -> bool = <fun>
                          
                          Proved
                          proof
                          ground_instances0
                          definitions0
                          inductions0
                          search_time
                          0.012s
                          details
                          Expand
                          smt_stats
                          num checks2
                          arith-make-feasible5
                          arith-max-columns18
                          rlimit count3524
                          mk clause49
                          mk bool var324
                          arith-lower8
                          arith-diseq2
                          datatype splits30
                          decisions67
                          arith-propagations2
                          propagations183
                          arith-bound-propagations-cheap2
                          arith-max-rows4
                          conflicts30
                          datatype accessor ax72
                          minimized lits14
                          datatype constructor ax95
                          num allocs14125836
                          added eqs631
                          del clause18
                          arith eq adapter5
                          arith-upper3
                          time0.001000
                          memory9.620000
                          max memory9.620000
                          Expand
                          • start[0.012s]
                              let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                              not (_x_0 = None)
                              ==> (if Is_a(None,
                                      (if Is_a(None, _x_0) then ( :var_0: )
                                       else if Is_a(Clock, …) then … else …).outgoing)
                                   then true
                                   else
                                     (Destruct(Twist, 0, …)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x
                                     >= 0)
                          • simplify

                            into
                            let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                            let (_x_1 : outgoing_msg option)
                                = (if Is_a(None, _x_0) then ( :var_0: )
                                   else if Is_a(Clock, …) then … else …).outgoing
                            in
                            (_x_0 = None || Is_a(None, _x_1))
                            || (Destruct(Twist, 0, Option.get _x_1)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x
                               >= 0
                            expansions
                            []
                            rewrite_steps
                              forward_chaining
                              • Unsat

                              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:

                              In [13]:
                              theorem never_goes_back_alt state =
                                state.outgoing = None
                                ==>
                                no_moving_back (one_step state).outgoing
                              
                              Out[13]:
                              val never_goes_back_alt : state -> bool = <fun>
                              
                              Proved
                              proof
                              ground_instances0
                              definitions0
                              inductions0
                              search_time
                              0.013s
                              details
                              Expand
                              smt_stats
                              num checks2
                              arith-make-feasible5
                              arith-max-columns18
                              rlimit count3470
                              mk clause49
                              mk bool var319
                              arith-lower8
                              arith-diseq2
                              datatype splits30
                              decisions63
                              arith-propagations2
                              propagations182
                              arith-bound-propagations-cheap2
                              arith-max-rows4
                              conflicts29
                              datatype accessor ax72
                              minimized lits14
                              datatype constructor ax90
                              num allocs21131249
                              added eqs625
                              del clause18
                              arith eq adapter5
                              arith-upper3
                              time0.001000
                              memory10.060000
                              max memory10.060000
                              Expand
                              • start[0.013s]
                                  ( :var_0: ).outgoing = None
                                  ==> (if Is_a(None,
                                          (if Is_a(None, ( :var_0: ).incoming) then ( :var_0: )
                                           else if Is_a(Clock, …) then … else …).outgoing)
                                       then true
                                       else
                                         (Destruct(Twist, 0, …)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x
                                         >= 0)
                              • simplify

                                into
                                let (_x_0 : outgoing_msg option)
                                    = (if Is_a(None, ( :var_0: ).incoming) then ( :var_0: )
                                       else if Is_a(Clock, …) then … else …).outgoing
                                in
                                (Is_a(None, _x_0)
                                 || (Destruct(Twist, 0, Option.get _x_0)).Geometry_msgs.twist_linear.Geometry_msgs.vector3_x
                                    >= 0)
                                || not (( :var_0: ).outgoing = None)
                                expansions
                                []
                                rewrite_steps
                                  forward_chaining
                                  • Unsat

                                  4. Inductive proofs. Stopping near objects.

                                  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:

                                  In [14]:
                                  verify ( fun state ->
                                    let open Sensor_msgs in
                                    match state.incoming with None | Some (Clock _ ) -> true
                                    | Some ( Sensor data ) ->
                                    (  List.for_all (fun x -> x < 20000) data.laserScan_ranges
                                    ) ==> (one_step state).mode = Turning
                                  )
                                  
                                  Out[14]:
                                  - : state -> bool = <fun>
                                  module CX : sig val state : state end
                                  
                                  Counterexample (after 4 steps, 0.016s):
                                   let (state : state) =
                                    {mode = Driving; min_range = None; direction = None;
                                     incoming =
                                      (Some
                                       (Sensor
                                          ({Sensor_msgs.laserScan_range_min = 3;
                                            Sensor_msgs.laserScan_range_max = 20000;
                                            Sensor_msgs.laserScan_ranges = []})));
                                     outgoing = None}
                                  
                                  Refuted
                                  proof attempt
                                  ground_instances4
                                  definitions0
                                  inductions0
                                  search_time
                                  0.016s
                                  details
                                  Expand
                                  smt_stats
                                  num checks9
                                  arith-make-feasible22
                                  arith-max-columns22
                                  rlimit count6712
                                  arith-cheap-eqs2
                                  mk clause43
                                  datatype occurs check118
                                  mk bool var271
                                  arith-lower7
                                  datatype splits30
                                  decisions198
                                  propagations114
                                  arith-max-rows7
                                  conflicts11
                                  datatype accessor ax31
                                  arith-bound-propagations-lp1
                                  datatype constructor ax132
                                  num allocs29269330
                                  final checks10
                                  added eqs584
                                  del clause4
                                  arith eq adapter4
                                  arith-upper22
                                  memory10.400000
                                  max memory10.400000
                                  Expand
                                  • start[0.016s]
                                      let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                                      let (_x_1 : bool) = Is_a(None, _x_0) in
                                      if _x_1 then true
                                      else
                                      if Is_a(Clock, Option.get _x_0) then true
                                      else
                                        List.for_all (fun x -> x < 20000) ….Sensor_msgs.laserScan_ranges
                                        ==> (if _x_1 then ( :var_0: ) else …).mode = Turning
                                  • simplify

                                    into
                                    let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                                    let (_x_1 : bool) = Is_a(Clock, Option.get _x_0) in
                                    let (_x_2 : bool) = Is_a(None, _x_0) in
                                    let (_x_3 : bool) = Is_a(Driving, …) in
                                    ((_x_1 || _x_2)
                                     || (if _x_2 then ( :var_0: )
                                         else
                                         if _x_1 then if _x_3 then … else … else if _x_3 then … else …).mode
                                        = Turning)
                                    || not (List.for_all (fun x -> x < 20000) ….Sensor_msgs.laserScan_ranges)
                                    expansions
                                    []
                                    rewrite_steps
                                      forward_chaining
                                      • unroll
                                        expr
                                        (let ((a!1 (|Sensor_msgs.laserScan_ranges_30|
                                                     (|get.Sensor.0_2418| (|get.Some.0_2420| (…
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|Sensor_msgs.laserScan_range_max_29|
                                                       (|get.Sensor.0_2418| (|get.Some.0_2420…
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|Sensor_msgs.laserScan_range_max_29|
                                                         (|get.Sensor.0_2418| (|get.Some.0_2420…
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|Sensor_msgs.laserScan_ranges_30|
                                                           (|get.Sensor.0_2418| (|get.Some.0_2420| (…
                                              expansions
                                              • Sat (Some let (state : state) = {mode = Driving; min_range = None; direction = None; incoming = (Some (Sensor ({Sensor_msgs.laserScan_range_min = 3; Sensor_msgs.laserScan_range_max = 20000; Sensor_msgs.laserScan_ranges = []}))); outgoing = None} )

                                              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.

                                              In [15]:
                                              CX.state
                                              
                                              Out[15]:
                                              - : state =
                                              {mode = Driving; min_range = None; direction = None;
                                               incoming =
                                                Some
                                                 (Sensor
                                                   {Sensor_msgs.laserScan_range_min = 3; laserScan_range_max = 20000;
                                                    laserScan_ranges = []});
                                               outgoing = None}
                                              

                                              Adding the extra requirement that the list is not [], we successfully verify the statement:

                                              In [16]:
                                              theorem stopping_if_for_all state =
                                                let open Sensor_msgs in
                                                match state.incoming with None | Some (Clock _ ) -> true
                                                | Some ( Sensor data ) ->
                                                (  data.laserScan_ranges <> []
                                                && List.for_all (fun x -> x < 20000) data.laserScan_ranges
                                                ) ==> (one_step state).mode = Turning
                                              
                                              Out[16]:
                                              val stopping_if_for_all : state -> bool = <fun>
                                              
                                              Proved
                                              proof
                                              ground_instances2
                                              definitions0
                                              inductions0
                                              search_time
                                              0.016s
                                              details
                                              Expand
                                              smt_stats
                                              num checks6
                                              arith-make-feasible36
                                              arith-max-columns20
                                              arith-conflicts2
                                              rlimit count6264
                                              mk clause38
                                              datatype occurs check76
                                              mk bool var302
                                              arith-lower11
                                              arith-diseq4
                                              datatype splits31
                                              decisions195
                                              arith-propagations3
                                              propagations204
                                              arith-bound-propagations-cheap3
                                              arith-max-rows7
                                              conflicts28
                                              datatype accessor ax27
                                              minimized lits6
                                              datatype constructor ax157
                                              num allocs34847331
                                              final checks6
                                              added eqs780
                                              del clause24
                                              arith eq adapter8
                                              arith-upper31
                                              memory13.620000
                                              max memory13.620000
                                              Expand
                                              • start[0.016s]
                                                  let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                                                  let (_x_1 : incoming_msg) = Option.get _x_0 in
                                                  let (_x_2 : int list)
                                                      = (Destruct(Sensor, 0, _x_1)).Sensor_msgs.laserScan_ranges
                                                  in
                                                  let (_x_3 : bool) = Is_a(None, _x_0) in
                                                  if _x_3 then true
                                                  else
                                                  if Is_a(Clock, _x_1) then true
                                                  else
                                                    not (_x_2 = []) && List.for_all (fun x -> x < 20000) _x_2
                                                    ==> (if _x_3 then ( :var_0: ) else …).mode = Turning
                                              • simplify

                                                into
                                                let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                                                let (_x_1 : incoming_msg) = Option.get _x_0 in
                                                let (_x_2 : bool) = Is_a(Clock, _x_1) in
                                                let (_x_3 : bool) = Is_a(None, _x_0) in
                                                let (_x_4 : bool) = Is_a(Driving, …) in
                                                let (_x_5 : int list)
                                                    = (Destruct(Sensor, 0, _x_1)).Sensor_msgs.laserScan_ranges
                                                in
                                                ((_x_2 || _x_3)
                                                 || (if _x_3 then ( :var_0: )
                                                     else
                                                     if _x_2 then if _x_4 then … else … else if _x_4 then … else …).mode
                                                    = Turning)
                                                || not (not (_x_5 = []) && List.for_all (fun x -> x < 20000) _x_5)
                                                expansions
                                                []
                                                rewrite_steps
                                                  forward_chaining
                                                  • unroll
                                                    expr
                                                    (let ((a!1 (|Sensor_msgs.laserScan_ranges_30|
                                                                 (|get.Sensor.0_2576| (|get.Some.0_2578| (…
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (let ((a!1 (|Sensor_msgs.laserScan_range_max_29|
                                                                   (|get.Sensor.0_2576| (|get.Some.0_2578…
                                                      expansions
                                                      • Unsat

                                                      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.

                                                      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:

                                                      In [17]:
                                                      let under_threshold x = x < 20000
                                                      
                                                      lemma lemma1 state =
                                                        let open Sensor_msgs in
                                                        match state.incoming with None | Some (Clock _ ) -> true
                                                        | Some ( Sensor data ) ->
                                                        (  data.laserScan_ranges <> []
                                                        && under_threshold (get_min_range data.laserScan_range_max data.laserScan_ranges)
                                                        ) ==> (one_step state).mode = Turning
                                                      
                                                      Out[17]:
                                                      val under_threshold : int -> bool = <fun>
                                                      val lemma1 : state -> bool = <fun>
                                                      
                                                      Proved
                                                      proof
                                                      ground_instances0
                                                      definitions0
                                                      inductions0
                                                      search_time
                                                      0.013s
                                                      details
                                                      Expand
                                                      smt_stats
                                                      num checks2
                                                      arith-make-feasible13
                                                      arith-max-columns17
                                                      arith-conflicts1
                                                      rlimit count3326
                                                      mk clause30
                                                      mk bool var202
                                                      arith-lower10
                                                      arith-diseq1
                                                      datatype splits19
                                                      decisions85
                                                      arith-propagations1
                                                      propagations88
                                                      arith-bound-propagations-cheap1
                                                      arith-max-rows5
                                                      conflicts15
                                                      datatype accessor ax25
                                                      datatype constructor ax89
                                                      num allocs41404586
                                                      added eqs372
                                                      del clause18
                                                      arith eq adapter5
                                                      arith-upper10
                                                      memory16.950000
                                                      max memory16.950000
                                                      Expand
                                                      • start[0.013s]
                                                          let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                                                          let (_x_1 : incoming_msg) = Option.get _x_0 in
                                                          let (_x_2 : Sensor_msgs.laserScan) = Destruct(Sensor, 0, _x_1) in
                                                          let (_x_3 : int list) = _x_2.Sensor_msgs.laserScan_ranges in
                                                          let (_x_4 : bool) = Is_a(None, _x_0) in
                                                          if _x_4 then true
                                                          else
                                                          if Is_a(Clock, _x_1) then true
                                                          else
                                                            not (_x_3 = [])
                                                            && List.fold_right (fun x a -> if x < a then x else a)
                                                               _x_2.Sensor_msgs.laserScan_range_max _x_3 < 20000
                                                            ==> (if _x_4 then ( :var_0: ) else …).mode = Turning
                                                      • simplify

                                                        into
                                                        let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                                                        let (_x_1 : incoming_msg) = Option.get _x_0 in
                                                        let (_x_2 : bool) = Is_a(Clock, _x_1) in
                                                        let (_x_3 : bool) = Is_a(None, _x_0) in
                                                        let (_x_4 : bool) = Is_a(Driving, …) in
                                                        let (_x_5 : Sensor_msgs.laserScan) = Destruct(Sensor, 0, _x_1) in
                                                        let (_x_6 : int list) = _x_5.Sensor_msgs.laserScan_ranges in
                                                        ((_x_2 || _x_3)
                                                         || (if _x_3 then ( :var_0: )
                                                             else
                                                             if _x_2 then if _x_4 then … else … else if _x_4 then … else …).mode
                                                            = Turning)
                                                        || not
                                                           (not (_x_6 = [])
                                                            && not
                                                               (20000 <=
                                                                List.fold_right (fun x a -> if x < a then x else a)
                                                                _x_5.Sensor_msgs.laserScan_range_max _x_6))
                                                        expansions
                                                        []
                                                        rewrite_steps
                                                          forward_chaining
                                                          • Unsat

                                                          Next, we prove a "bridge" lemma that translates between the get_min_range concept and the List.exists concept for the under_threshold function.

                                                          In [18]:
                                                          lemma bridge max lst =
                                                            List.exists under_threshold lst ==> under_threshold (get_min_range max lst)
                                                            [@@induct]
                                                          
                                                          Out[18]:
                                                          val bridge : int -> int list -> bool = <fun>
                                                          Goal:
                                                          
                                                          List.exists under_threshold lst ==> under_threshold (get_min_range max lst).
                                                          
                                                          1 nontautological subgoal.
                                                          
                                                          Subgoal 1:
                                                          
                                                           H0. List.exists under_threshold lst
                                                           H1. 20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst
                                                          |---------------------------------------------------------------------------
                                                           false
                                                          
                                                          
                                                          Must try induction.
                                                          
                                                          The recursive terms in the conjecture suggest 2 inductions.
                                                          Subsumption and merging reduces this to 1.
                                                          
                                                          We shall induct according to a scheme derived from List.fold_right.
                                                          
                                                          Induction scheme:
                                                          
                                                           (not
                                                            (List.hd lst <
                                                             List.fold_right (fun x a -> if x < a then x else a) max (List.tl lst)
                                                             && not Is_a([], lst))
                                                            && not
                                                               (not
                                                                (List.hd lst <
                                                                 List.fold_right (fun x a -> if x < a then x else a) max (List.tl lst))
                                                                && not Is_a([], lst))
                                                            ==> φ lst max)
                                                           && (not Is_a([], lst)
                                                               && not
                                                                  (List.hd lst <
                                                                   List.fold_right (fun x a -> if x < a then x else a) max
                                                                   (List.tl lst))
                                                                  && φ (List.tl lst) max && φ (List.tl lst) max
                                                               ==> φ lst max)
                                                              && (not Is_a([], lst)
                                                                  && List.hd lst <
                                                                     List.fold_right (fun x a -> if x < a then x else a) max
                                                                     (List.tl lst) && φ (List.tl lst) max
                                                                  ==> φ lst max).
                                                          
                                                          3 nontautological subgoals.
                                                          
                                                          Subgoal 1.3:
                                                          
                                                           H0. List.exists under_threshold lst
                                                           H1. 20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst
                                                           H2. not
                                                               (not
                                                                (List.fold_right (fun x a -> if x < a then x else a) max (List.tl lst)
                                                                 <= List.hd lst)
                                                                && not Is_a([], lst))
                                                           H3. not
                                                               (List.fold_right (fun x a -> if x < a then x else a) max (List.tl lst)
                                                                <= List.hd lst && not Is_a([], lst))
                                                          |---------------------------------------------------------------------------
                                                           false
                                                          
                                                          But simplification reduces this to true, using the definitions of List.exists
                                                          and List.fold_right.
                                                          
                                                          Subgoal 1.2:
                                                          
                                                           H0. List.exists under_threshold lst
                                                           H1. 20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst
                                                           H2. not Is_a([], lst)
                                                           H3. List.fold_right (fun x a -> if x < a then x else a) max (List.tl lst) <=
                                                               List.hd lst
                                                           H4. not (List.exists under_threshold (List.tl lst))
                                                               || not
                                                                  (20000 <=
                                                                   List.fold_right (fun x a -> if x < a then x else a) max
                                                                   (List.tl lst))
                                                          |---------------------------------------------------------------------------
                                                           false
                                                          
                                                          But simplification reduces this to true, using the definitions of List.exists
                                                          and List.fold_right.
                                                          
                                                          Subgoal 1.1:
                                                          
                                                           H0. List.exists under_threshold lst
                                                           H1. 20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst
                                                           H2. not Is_a([], lst)
                                                           H3. not
                                                               (List.fold_right (fun x a -> if x < a then x else a) max (List.tl lst)
                                                                <= List.hd lst)
                                                           H4. not (List.exists under_threshold (List.tl lst))
                                                               || not
                                                                  (20000 <=
                                                                   List.fold_right (fun x a -> if x < a then x else a) max
                                                                   (List.tl lst))
                                                          |---------------------------------------------------------------------------
                                                           false
                                                          
                                                          But simplification reduces this to true, using the definitions of List.exists
                                                          and List.fold_right.
                                                          
                                                           Rules:
                                                              (:def List.exists)
                                                              (:def List.fold_right)
                                                              (:induct List.fold_right)
                                                          
                                                          
                                                          Proved
                                                          proof
                                                          ground_instances0
                                                          definitions10
                                                          inductions1
                                                          search_time
                                                          0.349s
                                                          Expand
                                                          • start[0.349s, "Goal"]
                                                              List.exists under_threshold ( :var_0: )
                                                              ==> List.fold_right (fun x a -> if x < a then x else a) ( :var_1: )
                                                                  ( :var_0: ) < 20000
                                                          • subproof

                                                            not (List.exists under_threshold lst) || not (20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst)
                                                            • start[0.349s, "1"]
                                                                not (List.exists under_threshold lst)
                                                                || not
                                                                   (20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst)
                                                            • induction on (functional )
                                                              :scheme (not
                                                                       (List.hd lst <
                                                                        List.fold_right (fun x a -> if x < a then x else a) max
                                                                        (List.tl lst) && not Is_a([], lst))
                                                                       && not
                                                                          (not
                                                                           (List.hd lst <
                                                                            List.fold_right (fun x a -> if x < a then x else a) max
                                                                            (List.tl lst))
                                                                           && not Is_a([], lst))
                                                                       ==> φ lst max)
                                                                      && (not Is_a([], lst)
                                                                          && not
                                                                             (List.hd lst <
                                                                              List.fold_right (fun x a -> if x < a then x else a) max
                                                                              (List.tl lst))
                                                                             && φ (List.tl lst) max && φ (List.tl lst) max
                                                                          ==> φ lst max)
                                                                         && (not Is_a([], lst)
                                                                             && List.hd lst <
                                                                                List.fold_right (fun x a -> if x < a then x else a) max
                                                                                (List.tl lst) && φ (List.tl lst) max
                                                                             ==> φ lst max)
                                                            • Split (let (_x_0 : bool)
                                                                         = not (List.exists under_threshold lst)
                                                                           || not
                                                                              (20000 <=
                                                                               List.fold_right (fun x a -> if x < a then x else a) max lst)
                                                                     in
                                                                     let (_x_1 : int list) = List.tl lst in
                                                                     let (_x_2 : int)
                                                                         = List.fold_right (fun x a -> if x < a then x else a) max _x_1
                                                                     in
                                                                     let (_x_3 : bool) = _x_2 <= List.hd lst in
                                                                     let (_x_4 : bool) = not _x_3 in
                                                                     let (_x_5 : bool) = not Is_a([], lst) in
                                                                     let (_x_6 : bool)
                                                                         = not (List.exists under_threshold _x_1) || not (20000 <= _x_2)
                                                                     in
                                                                     ((_x_0 || not (not (_x_4 && _x_5) && not (_x_3 && _x_5)))
                                                                      && (_x_0 || not ((_x_5 && _x_3) && _x_6)))
                                                                     && (_x_0 || not ((_x_5 && _x_4) && _x_6))
                                                                     :cases [let (_x_0 : bool)
                                                                                 = List.fold_right (fun x a -> if x < a then x else a) max
                                                                                   (List.tl lst) <= List.hd lst
                                                                             in
                                                                             let (_x_1 : bool) = not Is_a([], lst) in
                                                                             ((not (List.exists under_threshold lst)
                                                                               || not
                                                                                  (20000 <=
                                                                                   List.fold_right (fun x a -> if x < a then x else a) max
                                                                                   lst))
                                                                              || not _x_0 && _x_1)
                                                                             || _x_0 && _x_1;
                                                                             let (_x_0 : int list) = List.tl lst in
                                                                             let (_x_1 : int)
                                                                                 = List.fold_right (fun x a -> if x < a then x else a) max
                                                                                   _x_0
                                                                             in
                                                                             (((not (List.exists under_threshold lst)
                                                                                || not
                                                                                   (20000 <=
                                                                                    List.fold_right (fun x a -> if x < a then x else a) max
                                                                                    lst))
                                                                               || Is_a([], lst))
                                                                              || not (_x_1 <= List.hd lst))
                                                                             || not
                                                                                (not (List.exists under_threshold _x_0)
                                                                                 || not (20000 <= _x_1));
                                                                             let (_x_0 : int list) = List.tl lst in
                                                                             let (_x_1 : int)
                                                                                 = List.fold_right (fun x a -> if x < a then x else a) max
                                                                                   _x_0
                                                                             in
                                                                             (((not (List.exists under_threshold lst)
                                                                                || not
                                                                                   (20000 <=
                                                                                    List.fold_right (fun x a -> if x < a then x else a) max
                                                                                    lst))
                                                                               || Is_a([], lst))
                                                                              || _x_1 <= List.hd lst)
                                                                             || not
                                                                                (not (List.exists under_threshold _x_0)
                                                                                 || not (20000 <= _x_1))])
                                                              • subproof
                                                                let (_x_0 : int list) = List.tl lst in let (_x_1 : int) = List.fold_right (fun x a -> if x < a then x else a) max _x_0 in (((not (List.exists under_threshold lst) || not (20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst)) || Is_a([], lst)) || _x_1 <= List.hd lst) || not (not (List.exists under_threshold _x_0) || not (20000 <= _x_1))
                                                                • start[0.282s, "1.1"]
                                                                    let (_x_0 : int list) = List.tl lst in
                                                                    let (_x_1 : int)
                                                                        = List.fold_right (fun x a -> if x < a then x else a) max _x_0
                                                                    in
                                                                    (((not (List.exists under_threshold lst)
                                                                       || not
                                                                          (20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst))
                                                                      || Is_a([], lst))
                                                                     || _x_1 <= List.hd lst)
                                                                    || not (not (List.exists under_threshold _x_0) || not (20000 <= _x_1))
                                                                • simplify
                                                                  into
                                                                  true
                                                                  expansions
                                                                  [List.exists, List.fold_right, List.fold_right]
                                                                  rewrite_steps
                                                                    forward_chaining
                                                                  • subproof
                                                                    let (_x_0 : int list) = List.tl lst in let (_x_1 : int) = List.fold_right (fun x a -> if x < a then x else a) max _x_0 in (((not (List.exists under_threshold lst) || not (20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst)) || Is_a([], lst)) || not (_x_1 <= List.hd lst)) || not (not (List.exists under_threshold _x_0) || not (20000 <= _x_1))
                                                                    • start[0.282s, "1.2"]
                                                                        let (_x_0 : int list) = List.tl lst in
                                                                        let (_x_1 : int)
                                                                            = List.fold_right (fun x a -> if x < a then x else a) max _x_0
                                                                        in
                                                                        (((not (List.exists under_threshold lst)
                                                                           || not
                                                                              (20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst))
                                                                          || Is_a([], lst))
                                                                         || not (_x_1 <= List.hd lst))
                                                                        || not (not (List.exists under_threshold _x_0) || not (20000 <= _x_1))
                                                                    • simplify
                                                                      into
                                                                      true
                                                                      expansions
                                                                      [List.exists, List.fold_right, List.fold_right]
                                                                      rewrite_steps
                                                                        forward_chaining
                                                                      • subproof
                                                                        let (_x_0 : bool) = List.fold_right (fun x a -> if x < a then x else a) max (List.tl lst) <= List.hd lst in let (_x_1 : bool) = not Is_a([], lst) in ((not (List.exists under_threshold lst) || not (20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst)) || not _x_0 && _x_1) || _x_0 && _x_1
                                                                        • start[0.282s, "1.3"]
                                                                            let (_x_0 : bool)
                                                                                = List.fold_right (fun x a -> if x < a then x else a) max (List.tl lst)
                                                                                  <= List.hd lst
                                                                            in
                                                                            let (_x_1 : bool) = not Is_a([], lst) in
                                                                            ((not (List.exists under_threshold lst)
                                                                              || not
                                                                                 (20000 <= List.fold_right (fun x a -> if x < a then x else a) max lst))
                                                                             || not _x_0 && _x_1)
                                                                            || _x_0 && _x_1
                                                                        • simplify
                                                                          into
                                                                          true
                                                                          expansions
                                                                          [List.exists, List.fold_right, List.exists, List.fold_right]
                                                                          rewrite_steps
                                                                            forward_chaining

                                                                      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:

                                                                      In [19]:
                                                                      theorem stopping_if_exists state =
                                                                        let open Sensor_msgs in
                                                                        match state.incoming with None | Some (Clock _ ) -> true
                                                                        | Some ( Sensor data ) ->
                                                                        (  data.laserScan_ranges <> []
                                                                        && List.exists under_threshold data.laserScan_ranges
                                                                        ) ==> (one_step state).mode = Turning
                                                                      [@@apply lemma1 state]
                                                                      [@@apply bridge
                                                                          (match state.incoming with Some (Sensor data) -> data.laserScan_range_max | _ -> 0)
                                                                          (match state.incoming with Some (Sensor data) -> data.laserScan_ranges | _ -> []) ]
                                                                      [@@induct]
                                                                      
                                                                      Out[19]:
                                                                      val stopping_if_exists : state -> bool = <fun>
                                                                      Goal:
                                                                      
                                                                      begin match (state.incoming : incoming_msg option) with
                                                                        | None -> true
                                                                        | Some (_pat_105 : incoming_msg) ->
                                                                          begin match (_pat_105 : incoming_msg) with
                                                                            | Clock (_pat_106 : Rosgraph_msgs.clock) -> true
                                                                            | Sensor (data : Sensor_msgs.laserScan) ->
                                                                              data.Sensor_msgs.laserScan_ranges <> []
                                                                              && List.exists under_threshold data.Sensor_msgs.laserScan_ranges
                                                                              ==> (one_step state).mode = Turning
                                                                          end
                                                                      end.
                                                                      
                                                                      A hint has been given, resulting in the following augmented conjecture:
                                                                      
                                                                      Goal':
                                                                      
                                                                      (if Is_a(None, state.incoming) then true
                                                                       else
                                                                       if Is_a(Clock, Option.get state.incoming) then true
                                                                       else
                                                                         not
                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                          = [])
                                                                         && List.fold_right (fun x a -> if x < a then x else a)
                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                            < 20000
                                                                         ==> (if Is_a(None, state.incoming) then state
                                                                              else
                                                                              if Is_a(Clock, Option.get state.incoming)
                                                                              then
                                                                                if Is_a(Driving, state.mode)
                                                                                then
                                                                                  {mode = state.mode; min_range = state.min_range;
                                                                                   direction = state.direction; incoming = None;
                                                                                   outgoing =
                                                                                   Some
                                                                                   (Twist
                                                                                    {Geometry_msgs.twist_linear =
                                                                                     {Geometry_msgs.vector3_x = 10000; Geometry_msgs.vector3_y = 0;
                                                                                      Geometry_msgs.vector3_z = 0};
                                                                                     Geometry_msgs.twist_angular =
                                                                                     {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                      Geometry_msgs.vector3_z = 0}})}
                                                                                else
                                                                                if Is_a(None, state.direction)
                                                                                then
                                                                                  {mode = state.mode; min_range = state.min_range;
                                                                                   direction = state.direction; incoming = None;
                                                                                   outgoing =
                                                                                   Some
                                                                                   (Twist
                                                                                    {Geometry_msgs.twist_linear =
                                                                                     {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                      Geometry_msgs.vector3_z = 0};
                                                                                     Geometry_msgs.twist_angular =
                                                                                     {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                      Geometry_msgs.vector3_z = 10000}})}
                                                                                else
                                                                                if Is_a(CW, Option.get state.direction)
                                                                                then
                                                                                  {mode = state.mode; min_range = state.min_range;
                                                                                   direction = state.direction; incoming = None;
                                                                                   outgoing =
                                                                                   Some
                                                                                   (Twist
                                                                                    {Geometry_msgs.twist_linear =
                                                                                     {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                      Geometry_msgs.vector3_z = 0};
                                                                                     Geometry_msgs.twist_angular =
                                                                                     {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                      Geometry_msgs.vector3_z = 10000}})}
                                                                                else
                                                                                  {mode = state.mode; min_range = state.min_range;
                                                                                   direction = state.direction; incoming = None;
                                                                                   outgoing =
                                                                                   Some
                                                                                   (Twist
                                                                                    {Geometry_msgs.twist_linear =
                                                                                     {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                      Geometry_msgs.vector3_z = 0};
                                                                                     Geometry_msgs.twist_angular =
                                                                                     {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                      Geometry_msgs.vector3_z = -10000}})}
                                                                              else
                                                                              if Is_a(Driving, state.mode)
                                                                              then
                                                                                if (if (foldi
                                                                                        ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                         0)
                                                                                        None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                       <
                                                                                       (List.length
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                        / 2)
                                                                                    then
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CW)
                                                                                    else
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CCW)).0
                                                                                   < 20000
                                                                                then
                                                                                  {mode = Turning;
                                                                                   min_range =
                                                                                   Some
                                                                                   (if (foldi
                                                                                        ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                         0)
                                                                                        None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                       <
                                                                                       (List.length
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                        / 2)
                                                                                    then
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CW)
                                                                                    else
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CCW)).0;
                                                                                   direction =
                                                                                   Some
                                                                                   (if (foldi
                                                                                        ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                         0)
                                                                                        None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                       <
                                                                                       (List.length
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                        / 2)
                                                                                    then
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CW)
                                                                                    else
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CCW)).1;
                                                                                   incoming = None; outgoing = None}
                                                                                else
                                                                                  {mode = Driving; min_range = None; direction = None;
                                                                                   incoming = None; outgoing = None}
                                                                              else
                                                                              if Is_a(None, state.min_range)
                                                                              then
                                                                                if (if (foldi
                                                                                        ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                         0)
                                                                                        None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                       <
                                                                                       (List.length
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                        / 2)
                                                                                    then
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CW)
                                                                                    else
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CCW)).0
                                                                                   > 25000
                                                                                then
                                                                                  {mode = Driving; min_range = None; direction = None;
                                                                                   incoming = None; outgoing = None}
                                                                                else
                                                                                  {mode = Turning;
                                                                                   min_range =
                                                                                   Some
                                                                                   (if (foldi
                                                                                        ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                         0)
                                                                                        None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                       <
                                                                                       (List.length
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                        / 2)
                                                                                    then
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CW)
                                                                                    else
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CCW)).0;
                                                                                   direction =
                                                                                   Some
                                                                                   (if (foldi
                                                                                        ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                         0)
                                                                                        None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                       <
                                                                                       (List.length
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                        / 2)
                                                                                    then
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CW)
                                                                                    else
                                                                                      (List.fold_right (fun x a -> if x < a then x else a)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                       CCW)).1;
                                                                                   incoming = None; outgoing = None}
                                                                              else
                                                                              if (if (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     <
                                                                                     (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)).0
                                                                                 > 25000
                                                                              then
                                                                                {mode = Driving; min_range = None; direction = None;
                                                                                 incoming = None; outgoing = None}
                                                                              else
                                                                              if (if (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     <
                                                                                     (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)).0
                                                                                 > Option.get state.min_range
                                                                              then
                                                                                {mode = state.mode; min_range = state.min_range;
                                                                                 direction = state.direction; incoming = None; outgoing = None}
                                                                              else
                                                                                {mode = Turning;
                                                                                 min_range =
                                                                                 Some
                                                                                 (if (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     <
                                                                                     (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)).0;
                                                                                 direction =
                                                                                 Some
                                                                                 (if (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     <
                                                                                     (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)).1;
                                                                                 incoming = None; outgoing = None}).mode
                                                                             = Turning)
                                                                      && (List.exists under_threshold
                                                                          (if Is_a(Some, state.incoming)
                                                                           then
                                                                             if Is_a(Sensor, Option.get state.incoming)
                                                                             then
                                                                               (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                             else []
                                                                           else [])
                                                                          ==> List.fold_right (fun x a -> if x < a then x else a)
                                                                              (if Is_a(Some, state.incoming)
                                                                               then
                                                                                 if Is_a(Sensor, Option.get state.incoming)
                                                                                 then
                                                                                   (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                 else 0
                                                                               else 0)
                                                                              (if Is_a(Some, state.incoming)
                                                                               then
                                                                                 if Is_a(Sensor, Option.get state.incoming)
                                                                                 then
                                                                                   (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                 else []
                                                                               else [])
                                                                              < 20000)
                                                                      ==> (if Is_a(None, state.incoming) then true
                                                                           else
                                                                           if Is_a(Clock, Option.get state.incoming) then true
                                                                           else
                                                                             not
                                                                             ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                              = [])
                                                                             && List.exists under_threshold
                                                                                (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                             ==> (if Is_a(None, state.incoming) then state
                                                                                  else
                                                                                  if Is_a(Clock, Option.get state.incoming)
                                                                                  then
                                                                                    if Is_a(Driving, state.mode)
                                                                                    then
                                                                                      {mode = state.mode; min_range = state.min_range;
                                                                                       direction = state.direction; incoming = None;
                                                                                       outgoing =
                                                                                       Some
                                                                                       (Twist
                                                                                        {Geometry_msgs.twist_linear =
                                                                                         {Geometry_msgs.vector3_x = 10000;
                                                                                          Geometry_msgs.vector3_y = 0; Geometry_msgs.vector3_z = 0};
                                                                                         Geometry_msgs.twist_angular =
                                                                                         {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                          Geometry_msgs.vector3_z = 0}})}
                                                                                    else
                                                                                    if Is_a(None, state.direction)
                                                                                    then
                                                                                      {mode = state.mode; min_range = state.min_range;
                                                                                       direction = state.direction; incoming = None;
                                                                                       outgoing =
                                                                                       Some
                                                                                       (Twist
                                                                                        {Geometry_msgs.twist_linear =
                                                                                         {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                          Geometry_msgs.vector3_z = 0};
                                                                                         Geometry_msgs.twist_angular =
                                                                                         {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                          Geometry_msgs.vector3_z = 10000}})}
                                                                                    else
                                                                                    if Is_a(CW, Option.get state.direction)
                                                                                    then
                                                                                      {mode = state.mode; min_range = state.min_range;
                                                                                       direction = state.direction; incoming = None;
                                                                                       outgoing =
                                                                                       Some
                                                                                       (Twist
                                                                                        {Geometry_msgs.twist_linear =
                                                                                         {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                          Geometry_msgs.vector3_z = 0};
                                                                                         Geometry_msgs.twist_angular =
                                                                                         {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                          Geometry_msgs.vector3_z = 10000}})}
                                                                                    else
                                                                                      {mode = state.mode; min_range = state.min_range;
                                                                                       direction = state.direction; incoming = None;
                                                                                       outgoing =
                                                                                       Some
                                                                                       (Twist
                                                                                        {Geometry_msgs.twist_linear =
                                                                                         {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                          Geometry_msgs.vector3_z = 0};
                                                                                         Geometry_msgs.twist_angular =
                                                                                         {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                          Geometry_msgs.vector3_z = -10000}})}
                                                                                  else
                                                                                  if Is_a(Driving, state.mode)
                                                                                  then
                                                                                    if (if (foldi
                                                                                            ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                             0)
                                                                                            None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                           <
                                                                                           (List.length
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                            / 2)
                                                                                        then
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CW)
                                                                                        else
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CCW)).0
                                                                                       < 20000
                                                                                    then
                                                                                      {mode = Turning;
                                                                                       min_range =
                                                                                       Some
                                                                                       (if (foldi
                                                                                            ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                             0)
                                                                                            None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                           <
                                                                                           (List.length
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                            / 2)
                                                                                        then
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CW)
                                                                                        else
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CCW)).0;
                                                                                       direction =
                                                                                       Some
                                                                                       (if (foldi
                                                                                            ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                             0)
                                                                                            None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                           <
                                                                                           (List.length
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                            / 2)
                                                                                        then
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CW)
                                                                                        else
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CCW)).1;
                                                                                       incoming = None; outgoing = None}
                                                                                    else
                                                                                      {mode = Driving; min_range = None; direction = None;
                                                                                       incoming = None; outgoing = None}
                                                                                  else
                                                                                  if Is_a(None, state.min_range)
                                                                                  then
                                                                                    if (if (foldi
                                                                                            ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                             0)
                                                                                            None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                           <
                                                                                           (List.length
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                            / 2)
                                                                                        then
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CW)
                                                                                        else
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CCW)).0
                                                                                       > 25000
                                                                                    then
                                                                                      {mode = Driving; min_range = None; direction = None;
                                                                                       incoming = None; outgoing = None}
                                                                                    else
                                                                                      {mode = Turning;
                                                                                       min_range =
                                                                                       Some
                                                                                       (if (foldi
                                                                                            ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                             0)
                                                                                            None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                           <
                                                                                           (List.length
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                            / 2)
                                                                                        then
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CW)
                                                                                        else
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CCW)).0;
                                                                                       direction =
                                                                                       Some
                                                                                       (if (foldi
                                                                                            ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                             0)
                                                                                            None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                           <
                                                                                           (List.length
                                                                                            (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                            / 2)
                                                                                        then
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CW)
                                                                                        else
                                                                                          (List.fold_right (fun x a -> if x < a then x else a)
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                           CCW)).1;
                                                                                       incoming = None; outgoing = None}
                                                                                  else
                                                                                  if (if (foldi
                                                                                          ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                           0)
                                                                                          None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                         <
                                                                                         (List.length
                                                                                          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                          / 2)
                                                                                      then
                                                                                        (List.fold_right (fun x a -> if x < a then x else a)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                         CW)
                                                                                      else
                                                                                        (List.fold_right (fun x a -> if x < a then x else a)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                         CCW)).0
                                                                                     > 25000
                                                                                  then
                                                                                    {mode = Driving; min_range = None; direction = None;
                                                                                     incoming = None; outgoing = None}
                                                                                  else
                                                                                  if (if (foldi
                                                                                          ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                           0)
                                                                                          None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                         <
                                                                                         (List.length
                                                                                          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                          / 2)
                                                                                      then
                                                                                        (List.fold_right (fun x a -> if x < a then x else a)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                         CW)
                                                                                      else
                                                                                        (List.fold_right (fun x a -> if x < a then x else a)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                         CCW)).0
                                                                                     > Option.get state.min_range
                                                                                  then
                                                                                    {mode = state.mode; min_range = state.min_range;
                                                                                     direction = state.direction; incoming = None; outgoing = None}
                                                                                  else
                                                                                    {mode = Turning;
                                                                                     min_range =
                                                                                     Some
                                                                                     (if (foldi
                                                                                          ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                           0)
                                                                                          None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                         <
                                                                                         (List.length
                                                                                          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                          / 2)
                                                                                      then
                                                                                        (List.fold_right (fun x a -> if x < a then x else a)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                         CW)
                                                                                      else
                                                                                        (List.fold_right (fun x a -> if x < a then x else a)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                         CCW)).0;
                                                                                     direction =
                                                                                     Some
                                                                                     (if (foldi
                                                                                          ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                           0)
                                                                                          None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                         <
                                                                                         (List.length
                                                                                          (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                          / 2)
                                                                                      then
                                                                                        (List.fold_right (fun x a -> if x < a then x else a)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                         CW)
                                                                                      else
                                                                                        (List.fold_right (fun x a -> if x < a then x else a)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                         CCW)).1;
                                                                                     incoming = None; outgoing = None}).mode
                                                                                 = Turning).
                                                                      
                                                                      1 nontautological subgoal.
                                                                      
                                                                      Subgoal 1:
                                                                      
                                                                       H0. ((Is_a(None, state.incoming) || Is_a(Clock, Option.get state.incoming))
                                                                            || not
                                                                               (not
                                                                                ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                 = [])
                                                                                && not
                                                                                   (20000 <=
                                                                                    List.fold_right (fun x a -> if x < a then x else a)
                                                                                    (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                    (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges)))
                                                                           || (if Is_a(None, state.incoming) then state
                                                                               else
                                                                               if Is_a(Clock, Option.get state.incoming)
                                                                               then
                                                                                 if Is_a(Driving, state.mode)
                                                                                 then
                                                                                   {mode = state.mode; min_range = state.min_range;
                                                                                    direction = state.direction; incoming = None;
                                                                                    outgoing =
                                                                                    Some
                                                                                    (Twist
                                                                                     {Geometry_msgs.twist_linear =
                                                                                      {Geometry_msgs.vector3_x = 10000;
                                                                                       Geometry_msgs.vector3_y = 0; Geometry_msgs.vector3_z = 0};
                                                                                      Geometry_msgs.twist_angular =
                                                                                      {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                       Geometry_msgs.vector3_z = 0}})}
                                                                                 else
                                                                                 if Is_a(None, state.direction)
                                                                                    || Is_a(CW, Option.get state.direction)
                                                                                 then
                                                                                   {mode = state.mode; min_range = state.min_range;
                                                                                    direction = state.direction; incoming = None;
                                                                                    outgoing =
                                                                                    Some
                                                                                    (Twist
                                                                                     {Geometry_msgs.twist_linear =
                                                                                      {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                       Geometry_msgs.vector3_z = 0};
                                                                                      Geometry_msgs.twist_angular =
                                                                                      {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                       Geometry_msgs.vector3_z = 10000}})}
                                                                                 else
                                                                                   {mode = state.mode; min_range = state.min_range;
                                                                                    direction = state.direction; incoming = None;
                                                                                    outgoing =
                                                                                    Some
                                                                                    (Twist
                                                                                     {Geometry_msgs.twist_linear =
                                                                                      {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                       Geometry_msgs.vector3_z = 0};
                                                                                      Geometry_msgs.twist_angular =
                                                                                      {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                       Geometry_msgs.vector3_z = -10000}})}
                                                                               else
                                                                               if Is_a(Driving, state.mode)
                                                                               then
                                                                                 if 20000 <=
                                                                                    (if (List.length
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                         / 2)
                                                                                        <=
                                                                                        (foldi
                                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                          0)
                                                                                         None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     then
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CCW)
                                                                                     else
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CW)).0
                                                                                 then
                                                                                   {mode = Driving; min_range = None; direction = None;
                                                                                    incoming = None; outgoing = None}
                                                                                 else
                                                                                   {mode = Turning;
                                                                                    min_range =
                                                                                    Some
                                                                                    (if (List.length
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                         / 2)
                                                                                        <=
                                                                                        (foldi
                                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                          0)
                                                                                         None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     then
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CCW)
                                                                                     else
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CW)).0;
                                                                                    direction =
                                                                                    Some
                                                                                    (if (List.length
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                         / 2)
                                                                                        <=
                                                                                        (foldi
                                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                          0)
                                                                                         None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     then
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CCW)
                                                                                     else
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CW)).1;
                                                                                    incoming = None; outgoing = None}
                                                                               else
                                                                               if Is_a(None, state.min_range)
                                                                               then
                                                                                 if (if (List.length
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                         / 2)
                                                                                        <=
                                                                                        (foldi
                                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                          0)
                                                                                         None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     then
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CCW)
                                                                                     else
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CW)).0
                                                                                    <= 25000
                                                                                 then
                                                                                   {mode = Turning;
                                                                                    min_range =
                                                                                    Some
                                                                                    (if (List.length
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                         / 2)
                                                                                        <=
                                                                                        (foldi
                                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                          0)
                                                                                         None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     then
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CCW)
                                                                                     else
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CW)).0;
                                                                                    direction =
                                                                                    Some
                                                                                    (if (List.length
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                         / 2)
                                                                                        <=
                                                                                        (foldi
                                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                          0)
                                                                                         None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     then
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CCW)
                                                                                     else
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CW)).1;
                                                                                    incoming = None; outgoing = None}
                                                                                 else
                                                                                   {mode = Driving; min_range = None; direction = None;
                                                                                    incoming = None; outgoing = None}
                                                                               else
                                                                               if (if (List.length
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                       / 2)
                                                                                      <=
                                                                                      (foldi
                                                                                       ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                        0)
                                                                                       None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                       (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                   then
                                                                                     (List.fold_right (fun x a -> if x < a then x else a)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                      CCW)
                                                                                   else
                                                                                     (List.fold_right (fun x a -> if x < a then x else a)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                      CW)).0
                                                                                  <= 25000
                                                                               then
                                                                                 if (if (List.length
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                         / 2)
                                                                                        <=
                                                                                        (foldi
                                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                          0)
                                                                                         None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     then
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CCW)
                                                                                     else
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CW)).0
                                                                                    <= Option.get state.min_range
                                                                                 then
                                                                                   {mode = Turning;
                                                                                    min_range =
                                                                                    Some
                                                                                    (if (List.length
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                         / 2)
                                                                                        <=
                                                                                        (foldi
                                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                          0)
                                                                                         None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     then
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CCW)
                                                                                     else
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CW)).0;
                                                                                    direction =
                                                                                    Some
                                                                                    (if (List.length
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                         / 2)
                                                                                        <=
                                                                                        (foldi
                                                                                         ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                          0)
                                                                                         None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                         (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                     then
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CCW)
                                                                                     else
                                                                                       (List.fold_right (fun x a -> if x < a then x else a)
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                        (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                        CW)).1;
                                                                                    incoming = None; outgoing = None}
                                                                                 else
                                                                                   {mode = state.mode; min_range = state.min_range;
                                                                                    direction = state.direction; incoming = None; outgoing = None}
                                                                               else
                                                                                 {mode = Driving; min_range = None; direction = None;
                                                                                  incoming = None; outgoing = None}).mode
                                                                              = Turning
                                                                       H1. not
                                                                           (List.exists under_threshold
                                                                            (if Is_a(Some, state.incoming)
                                                                             then
                                                                               if Is_a(Sensor, Option.get state.incoming)
                                                                               then
                                                                                 (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                               else []
                                                                             else []))
                                                                           || not
                                                                              (20000 <=
                                                                               List.fold_right (fun x a -> if x < a then x else a)
                                                                               (if Is_a(Some, state.incoming)
                                                                                then
                                                                                  if Is_a(Sensor, Option.get state.incoming)
                                                                                  then
                                                                                    (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                  else 0
                                                                                else 0)
                                                                               (if Is_a(Some, state.incoming)
                                                                                then
                                                                                  if Is_a(Sensor, Option.get state.incoming)
                                                                                  then
                                                                                    (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                  else []
                                                                                else []))
                                                                       H2. not
                                                                           ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                            = [])
                                                                       H3. List.exists under_threshold
                                                                           (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                      |---------------------------------------------------------------------------
                                                                       C0. Is_a(None, state.incoming)
                                                                       C1. Is_a(Clock, Option.get state.incoming)
                                                                       C2. (if Is_a(None, state.incoming) then state
                                                                            else
                                                                            if Is_a(Clock, Option.get state.incoming)
                                                                            then
                                                                              if Is_a(Driving, state.mode)
                                                                              then
                                                                                {mode = state.mode; min_range = state.min_range;
                                                                                 direction = state.direction; incoming = None;
                                                                                 outgoing =
                                                                                 Some
                                                                                 (Twist
                                                                                  {Geometry_msgs.twist_linear =
                                                                                   {Geometry_msgs.vector3_x = 10000; Geometry_msgs.vector3_y = 0;
                                                                                    Geometry_msgs.vector3_z = 0};
                                                                                   Geometry_msgs.twist_angular =
                                                                                   {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                    Geometry_msgs.vector3_z = 0}})}
                                                                              else
                                                                              if Is_a(None, state.direction)
                                                                                 || Is_a(CW, Option.get state.direction)
                                                                              then
                                                                                {mode = state.mode; min_range = state.min_range;
                                                                                 direction = state.direction; incoming = None;
                                                                                 outgoing =
                                                                                 Some
                                                                                 (Twist
                                                                                  {Geometry_msgs.twist_linear =
                                                                                   {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                    Geometry_msgs.vector3_z = 0};
                                                                                   Geometry_msgs.twist_angular =
                                                                                   {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                    Geometry_msgs.vector3_z = 10000}})}
                                                                              else
                                                                                {mode = state.mode; min_range = state.min_range;
                                                                                 direction = state.direction; incoming = None;
                                                                                 outgoing =
                                                                                 Some
                                                                                 (Twist
                                                                                  {Geometry_msgs.twist_linear =
                                                                                   {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                    Geometry_msgs.vector3_z = 0};
                                                                                   Geometry_msgs.twist_angular =
                                                                                   {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                    Geometry_msgs.vector3_z = -10000}})}
                                                                            else
                                                                            if Is_a(Driving, state.mode)
                                                                            then
                                                                              if 20000 <=
                                                                                 (if (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                     <=
                                                                                     (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)).0
                                                                              then
                                                                                {mode = Driving; min_range = None; direction = None;
                                                                                 incoming = None; outgoing = None}
                                                                              else
                                                                                {mode = Turning;
                                                                                 min_range =
                                                                                 Some
                                                                                 (if (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                     <=
                                                                                     (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)).0;
                                                                                 direction =
                                                                                 Some
                                                                                 (if (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                     <=
                                                                                     (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)).1;
                                                                                 incoming = None; outgoing = None}
                                                                            else
                                                                            if Is_a(None, state.min_range)
                                                                            then
                                                                              if (if (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                     <=
                                                                                     (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)).0
                                                                                 <= 25000
                                                                              then
                                                                                {mode = Turning;
                                                                                 min_range =
                                                                                 Some
                                                                                 (if (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                     <=
                                                                                     (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)).0;
                                                                                 direction =
                                                                                 Some
                                                                                 (if (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                     <=
                                                                                     (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)).1;
                                                                                 incoming = None; outgoing = None}
                                                                              else
                                                                                {mode = Driving; min_range = None; direction = None;
                                                                                 incoming = None; outgoing = None}
                                                                            else
                                                                            if (if (List.length
                                                                                    (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                    / 2)
                                                                                   <=
                                                                                   (foldi
                                                                                    ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                     0)
                                                                                    None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                    (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                then
                                                                                  (List.fold_right (fun x a -> if x < a then x else a)
                                                                                   (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                   (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                   CCW)
                                                                                else
                                                                                  (List.fold_right (fun x a -> if x < a then x else a)
                                                                                   (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                   (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                   CW)).0
                                                                               <= 25000
                                                                            then
                                                                              if (if (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                     <=
                                                                                     (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)).0
                                                                                 <= Option.get state.min_range
                                                                              then
                                                                                {mode = Turning;
                                                                                 min_range =
                                                                                 Some
                                                                                 (if (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                     <=
                                                                                     (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)).0;
                                                                                 direction =
                                                                                 Some
                                                                                 (if (List.length
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
                                                                                      / 2)
                                                                                     <=
                                                                                     (foldi
                                                                                      ((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
                                                                                       0)
                                                                                      None (fun i a b -> if a < fst b then (a, i) else b)
                                                                                      (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
                                                                                  then
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CCW)
                                                                                  else
                                                                                    (List.fold_right (fun x a -> if x < a then x else a)
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
                                                                                     (Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
                                                                                     CW)).1;
                                                                                 incoming = None; outgoing = None}
                                                                              else
                                                                                {mode = state.mode; min_range = state.min_range;
                                                                                 direction = state.direction; incoming = None; outgoing = None}
                                                                            else
                                                                              {mode = Driving; min_range = None; direction = None; incoming = None;
                                                                               outgoing = None}).mode
                                                                           = Turning
                                                                      
                                                                      But simplification reduces this to true, using the forward-chaining rule
                                                                      List.len_nonnegative.
                                                                      
                                                                       Rules:
                                                                          (:fc List.len_nonnegative)
                                                                          (:app apply_hint.stopping_if_exists.0)
                                                                          (:app apply_hint.stopping_if_exists.1)
                                                                      
                                                                      
                                                                      Proved
                                                                      proof
                                                                      ground_instances0
                                                                      definitions0
                                                                      inductions0
                                                                      search_time
                                                                      0.248s
                                                                      Expand
                                                                      • start[0.248s, "Goal"]
                                                                          let (_x_0 : incoming_msg option) = ( :var_0: ).incoming in
                                                                          let (_x_1 : incoming_msg) = Option.get _x_0 in
                                                                          let (_x_2 : Sensor_msgs.laserScan) = Destruct(Sensor, 0, _x_1) in
                                                                          let (_x_3 : int list) = _x_2.Sensor_msgs.laserScan_ranges in
                                                                          let (_x_4 : bool) = not (_x_3 = []) in
                                                                          let (_x_5 : int) = _x_2.Sensor_msgs.laserScan_range_max in
                                                                          let (_x_6 : bool) = Is_a(None, _x_0) in
                                                                          let (_x_7 : bool) = (if _x_6 then ( :var_0: ) else …).mode = Turning in
                                                                          let (_x_8 : bool) = Is_a(Clock, _x_1) in
                                                                          let (_x_9 : bool) = Is_a(Sensor, _x_1) in
                                                                          let (_x_10 : bool) = Is_a(Some, _x_0) in
                                                                          let (_x_11 : int list) = if _x_10 then if _x_9 then _x_3 else [] else [] in
                                                                          (if _x_6 then true
                                                                           else
                                                                           if _x_8 then true
                                                                           else
                                                                             _x_4
                                                                             && List.fold_right (fun x a -> if x < a then x else a) _x_5 _x_3 < 20000
                                                                             ==> _x_7)
                                                                          && (List.exists under_threshold _x_11
                                                                              ==> List.fold_right (fun x a -> if x < a then x else a)
                                                                                  (if _x_10 then if _x_9 then _x_5 else 0 else 0) _x_11 < 20000)
                                                                          ==> (if _x_6 then true
                                                                               else
                                                                               if _x_8 then true
                                                                               else _x_4 && List.exists under_threshold _x_3 ==> _x_7)
                                                                      • subproof

                                                                        let (_x_0 : incoming_msg option) = state.incoming in let (_x_1 : bool) = Is_a(None, _x_0) in let (_x_2 : incoming_msg) = Option.get _x_0 in let (_x_3 : bool) = Is_a(Clock, _x_2) in let (_x_4 : Sensor_msgs.laserScan) = Destruct(Sensor, 0, _x_2) in let (_x_5 : int list) = _x_4.Sensor_msgs.laserScan_ranges in let (_x_6 : int) = _x_4.Sensor_msgs.laserScan_range_max in let (_x_7 : int) = List.fold_right (fun x a -> if x < a then x else a) _x_6 _x_5 in let (_x_8 : state) = {mode = Driving; min_range = None; direction = None; incoming = None; outgoing = None} in let (_x_9 : mode) = state.mode in let (_x_10 : int option) = state.min_range in let (_x_11 : direction option) = state.direction in let (_x_12 : (int * direction)) = if (List.length _x_5 / 2) <= (foldi (_x_6, 0) None (fun i a b -> if a < fst b then (a, i) else b) _x_5).1 then (_x_7, CCW) else (_x_7, CW) in let (_x_13 : int) = _x_12.0 in let (_x_14 : state) = {mode = Turning; min_range = Some _x_13; direction = Some _x_12.1; incoming = None; outgoing = None} in let (_x_15 : bool) = _x_13 <= 25000 in let (_x_16 : bool) = Is_a(Driving, _x_9) in let (_x_17 : Geometry_msgs.vector3) = {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0; Geometry_msgs.vector3_z = 0} in let (_x_18 : bool) = (if _x_1 then state else if _x_3 then if _x_16 then {mode = _x_9; min_range = _x_10; direction = _x_11; incoming = None; outgoing = Some (Twist {Geometry_msgs.twist_linear = {Geometry_msgs.vector3_x = 10000; Geometry_msgs.vector3_y = 0; Geometry_msgs.vector3_z = 0}; Geometry_msgs.twist_angular = _x_17})} else if Is_a(None, _x_11) || Is_a(CW, Option.get _x_11) then {mode = _x_9; min_range = _x_10; direction = _x_11; incoming = None; outgoing = Some (Twist {Geometry_msgs.twist_linear = _x_17; Geometry_msgs.twist_angular = {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0; Geometry_msgs.vector3_z = 10000}})} else {mode = _x_9; min_range = _x_10; direction = _x_11; incoming = None; outgoing = Some (Twist {Geometry_msgs.twist_linear = _x_17; Geometry_msgs.twist_angular = {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0; Geometry_msgs.vector3_z = -10000}})} else if _x_16 then if 20000 <= _x_13 then _x_8 else _x_14 else if Is_a(None, _x_10) then if _x_15 then _x_14 else _x_8 else if _x_15 then if _x_13 <= Option.get _x_10 then _x_14 else {mode = _x_9; min_range = _x_10; direction = _x_11; incoming = None; outgoing = None} else _x_8).mode = Turning in let (_x_19 : bool) = Is_a(Sensor, _x_2) in let (_x_20 : bool) = Is_a(Some, _x_0) in let (_x_21 : int list) = if _x_20 then if _x_19 then _x_5 else [] else [] in (((((not (((_x_1 || _x_3) || not (not (_x_5 = []) && not (20000 <= _x_7))) || _x_18) || not (not (List.exists under_threshold _x_21) || not (20000 <= List.fold_right (fun x a -> if x < a then x else a) (if _x_20 then if _x_19 then _x_6 else 0 else 0) _x_21))) || (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges = []) || not (List.exists under_threshold _x_5)) || _x_1) || _x_3) || _x_18
                                                                        • start[0.246s, "1"]
                                                                            let (_x_0 : incoming_msg option) = state.incoming in
                                                                            let (_x_1 : bool) = Is_a(None, _x_0) in
                                                                            let (_x_2 : incoming_msg) = Option.get _x_0 in
                                                                            let (_x_3 : bool) = Is_a(Clock, _x_2) in
                                                                            let (_x_4 : Sensor_msgs.laserScan) = Destruct(Sensor, 0, _x_2) in
                                                                            let (_x_5 : int list) = _x_4.Sensor_msgs.laserScan_ranges in
                                                                            let (_x_6 : int) = _x_4.Sensor_msgs.laserScan_range_max in
                                                                            let (_x_7 : int)
                                                                                = List.fold_right (fun x a -> if x < a then x else a) _x_6 _x_5
                                                                            in
                                                                            let (_x_8 : state)
                                                                                = {mode = Driving; min_range = None; direction = None; incoming = None;
                                                                                   outgoing = None}
                                                                            in
                                                                            let (_x_9 : mode) = state.mode in
                                                                            let (_x_10 : int option) = state.min_range in
                                                                            let (_x_11 : direction option) = state.direction in
                                                                            let (_x_12 : (int * direction))
                                                                                = if (List.length _x_5 / 2) <=
                                                                                     (foldi (_x_6, 0) None
                                                                                      (fun i a b -> if a < fst b then (a, i) else b) _x_5).1
                                                                                  then (_x_7, CCW) else (_x_7, CW)
                                                                            in
                                                                            let (_x_13 : int) = _x_12.0 in
                                                                            let (_x_14 : state)
                                                                                = {mode = Turning; min_range = Some _x_13; direction = Some _x_12.1;
                                                                                   incoming = None; outgoing = None}
                                                                            in
                                                                            let (_x_15 : bool) = _x_13 <= 25000 in
                                                                            let (_x_16 : bool) = Is_a(Driving, _x_9) in
                                                                            let (_x_17 : Geometry_msgs.vector3)
                                                                                = {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                   Geometry_msgs.vector3_z = 0}
                                                                            in
                                                                            let (_x_18 : bool)
                                                                                = (if _x_1 then state
                                                                                   else
                                                                                   if _x_3
                                                                                   then
                                                                                     if _x_16
                                                                                     then
                                                                                       {mode = _x_9; min_range = _x_10; direction = _x_11;
                                                                                        incoming = None;
                                                                                        outgoing =
                                                                                        Some
                                                                                        (Twist
                                                                                         {Geometry_msgs.twist_linear =
                                                                                          {Geometry_msgs.vector3_x = 10000;
                                                                                           Geometry_msgs.vector3_y = 0; Geometry_msgs.vector3_z = 0};
                                                                                          Geometry_msgs.twist_angular = _x_17})}
                                                                                     else
                                                                                     if Is_a(None, _x_11) || Is_a(CW, Option.get _x_11)
                                                                                     then
                                                                                       {mode = _x_9; min_range = _x_10; direction = _x_11;
                                                                                        incoming = None;
                                                                                        outgoing =
                                                                                        Some
                                                                                        (Twist
                                                                                         {Geometry_msgs.twist_linear = _x_17;
                                                                                          Geometry_msgs.twist_angular =
                                                                                          {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                           Geometry_msgs.vector3_z = 10000}})}
                                                                                     else
                                                                                       {mode = _x_9; min_range = _x_10; direction = _x_11;
                                                                                        incoming = None;
                                                                                        outgoing =
                                                                                        Some
                                                                                        (Twist
                                                                                         {Geometry_msgs.twist_linear = _x_17;
                                                                                          Geometry_msgs.twist_angular =
                                                                                          {Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
                                                                                           Geometry_msgs.vector3_z = -10000}})}
                                                                                   else
                                                                                   if _x_16 then if 20000 <= _x_13 then _x_8 else _x_14
                                                                                   else
                                                                                   if Is_a(None, _x_10) then if _x_15 then _x_14 else _x_8
                                                                                   else
                                                                                   if _x_15
                                                                                   then
                                                                                     if _x_13 <= Option.get _x_10 then _x_14
                                                                                     else
                                                                                       {mode = _x_9; min_range = _x_10; direction = _x_11;
                                                                                        incoming = None; outgoing = None}
                                                                                   else _x_8).mode
                                                                                  = Turning
                                                                            in
                                                                            let (_x_19 : bool) = Is_a(Sensor, _x_2) in
                                                                            let (_x_20 : bool) = Is_a(Some, _x_0) in
                                                                            let (_x_21 : int list) = if _x_20 then if _x_19 then _x_5 else [] else []
                                                                            in
                                                                            (((((not
                                                                                 (((_x_1 || _x_3) || not (not (_x_5 = []) && not (20000 <= _x_7)))
                                                                                  || _x_18)
                                                                                 || not
                                                                                    (not (List.exists under_threshold _x_21)
                                                                                     || not
                                                                                        (20000 <=
                                                                                         List.fold_right (fun x a -> if x < a then x else a)
                                                                                         (if _x_20 then if _x_19 then _x_6 else 0 else 0) _x_21)))
                                                                                || (Destruct(Sensor, 0, Option.get ….incoming)).Sensor_msgs.laserScan_ranges
                                                                                   = [])
                                                                               || not (List.exists under_threshold _x_5))
                                                                              || _x_1)
                                                                             || _x_3)
                                                                            || _x_18
                                                                        • simplify
                                                                          into
                                                                          true
                                                                          expansions
                                                                          []
                                                                          rewrite_steps
                                                                            forward_chaining
                                                                            List.len_nonnegative