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

- : state =
{mode = Turning; min_range = Some 7719; direction = None;
 incoming =
  Some
   (Sensor
     { Sensor_msgs.laserScan_range_min = 3
     ; laserScan_range_max = 25001
     ; laserScan_ranges = []
     });
 outgoing = None}

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
)

theorem never_goes_back state = 
  state.incoming <> None
  ==>
  no_moving_back (one_step state).outgoing

- : state =
 { mode = Turning; min_range = Some 2282
 ; direction = None; incoming = None
 ; outgoing = Some (Twist
   { twist_linear  = {vector3_x = -1; vector3_y = 9; vector3_z = 10}
   ; twist_angular = {vector3_x = 11; vector3_y = 1; vector3_z = 13}
 })}

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  )

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

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]

lemma bridge max lst =
  List.exists under_threshold lst ==> under_threshold (get_min_range max lst)
  [@@induct]

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