open Preamble

open Deqsets_extra

open CostSpec

open Sets

open Listb

open StructuredTraces

open BitVectorTrie

open Graphs

open Order

open Registers

open FrontEndOps

open RTLabs_syntax

open SmallstepExec

open CostLabel

open Events

open IOMonad

open IO

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open Globalenvs

open ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Errors

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open RTLabs_semantics

open RTLabs_abstract

open CostMisc

open Executions

open Listb_extra

type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
and ('o, 'i) __flat_trace =
| Ft_stop of RTLabs_semantics.state
| Ft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
   * ('o, 'i) flat_trace

val flat_trace_inv_rect_Type4 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3

val flat_trace_inv_rect_Type3 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3

val flat_trace_inv_rect_Type2 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3

val flat_trace_inv_rect_Type1 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3

val flat_trace_inv_rect_Type0 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3

val flat_trace_discr :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
  ('a1, 'a2) flat_trace -> __

val flat_trace_jmdiscr :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
  ('a1, 'a2) flat_trace -> __

val make_flat_trace :
  __ -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace

val make_whole_flat_trace : __ -> __ -> (IO.io_out, IO.io_in) flat_trace

type will_return =
| Wr_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
| Wr_call of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
| Wr_ret of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
| Wr_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
   * (IO.io_out, IO.io_in) flat_trace

val will_return_rect_Type4 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
  flat_trace -> will_return -> 'a1

val will_return_rect_Type3 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
  flat_trace -> will_return -> 'a1

val will_return_rect_Type2 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
  flat_trace -> will_return -> 'a1

val will_return_rect_Type1 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
  flat_trace -> will_return -> 'a1

val will_return_rect_Type0 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
  flat_trace -> will_return -> 'a1

val will_return_inv_rect_Type4 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  __ -> __ -> __ -> __ -> 'a1) -> 'a1

val will_return_inv_rect_Type3 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  __ -> __ -> __ -> __ -> 'a1) -> 'a1

val will_return_inv_rect_Type2 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  __ -> __ -> __ -> __ -> 'a1) -> 'a1

val will_return_inv_rect_Type1 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  __ -> __ -> __ -> __ -> 'a1) -> 'a1

val will_return_inv_rect_Type0 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
  __ -> __ -> __ -> __ -> 'a1) -> 'a1

val will_return_jmdiscr :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> will_return -> __

val will_return_length :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> Nat.nat

val will_return_end :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state, (IO.io_out,
  IO.io_in) flat_trace) Types.dPair

val will_return_call :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> will_return Types.sig0

val will_return_return :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> __

val will_return_notfn :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> (__, __)
  Types.sum -> will_return -> will_return Types.sig0

val will_return_prepend :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> Nat.nat -> RTLabs_semantics.state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return

val nat_jmdiscr : Nat.nat -> Nat.nat -> __

val will_return_remove_call :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return ->
  RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return

val will_return_lower :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
  IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return

val list_jmdiscr : 'a1 List.list -> 'a1 List.list -> __

type 't trace_result = { new_state : RTLabs_abstract.rTLabs_ext_state;
                         remainder : (IO.io_out, IO.io_in) flat_trace;
                         new_trace : 't; terminates : __ }

val trace_result_rect_Type4 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
  -> 'a2

val trace_result_rect_Type5 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
  -> 'a2

val trace_result_rect_Type3 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
  -> 'a2

val trace_result_rect_Type2 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
  -> 'a2

val trace_result_rect_Type1 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
  -> 'a2

val trace_result_rect_Type0 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
  -> 'a2

val new_state :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result ->
  RTLabs_abstract.rTLabs_ext_state

val remainder :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result -> (IO.io_out, IO.io_in)
  flat_trace

val new_trace :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result -> 'a1

val terminates :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result -> __

val trace_result_inv_rect_Type4 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result ->
  (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
  -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2

val trace_result_inv_rect_Type3 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result ->
  (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
  -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2

val trace_result_inv_rect_Type2 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result ->
  (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
  -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2

val trace_result_inv_rect_Type1 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result ->
  (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
  -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2

val trace_result_inv_rect_Type0 :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result ->
  (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
  -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2

val trace_result_jmdiscr :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> Nat.nat -> 'a1 trace_result -> 'a1 trace_result -> __

type 't sub_trace_result = { ends : StructuredTraces.trace_ends_with_ret;
                             trace_res : 't trace_result }

val sub_trace_result_rect_Type4 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
  (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
  sub_trace_result -> 'a2

val sub_trace_result_rect_Type5 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
  (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
  sub_trace_result -> 'a2

val sub_trace_result_rect_Type3 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
  (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
  sub_trace_result -> 'a2

val sub_trace_result_rect_Type2 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
  (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
  sub_trace_result -> 'a2

val sub_trace_result_rect_Type1 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
  (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
  sub_trace_result -> 'a2

val sub_trace_result_rect_Type0 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
  (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
  sub_trace_result -> 'a2

val ends :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
  sub_trace_result -> StructuredTraces.trace_ends_with_ret

val trace_res :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
  sub_trace_result -> 'a1 trace_result

val sub_trace_result_inv_rect_Type4 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
  sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
  trace_result -> __ -> 'a2) -> 'a2

val sub_trace_result_inv_rect_Type3 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
  sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
  trace_result -> __ -> 'a2) -> 'a2

val sub_trace_result_inv_rect_Type2 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
  sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
  trace_result -> __ -> 'a2) -> 'a2

val sub_trace_result_inv_rect_Type1 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
  sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
  trace_result -> __ -> 'a2) -> 'a2

val sub_trace_result_inv_rect_Type0 :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
  sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
  trace_result -> __ -> 'a2) -> 'a2

val sub_trace_result_discr :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
  sub_trace_result -> 'a1 sub_trace_result -> __

val sub_trace_result_jmdiscr :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
  sub_trace_result -> 'a1 sub_trace_result -> __

val replace_trace :
  RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> (IO.io_out, IO.io_in) flat_trace ->
  will_return -> will_return -> Nat.nat -> Nat.nat -> 'a1 trace_result -> 'a2
  -> 'a2 trace_result

val replace_sub_trace :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> Nat.nat
  -> Nat.nat -> 'a1 sub_trace_result -> 'a2 -> 'a2 sub_trace_result

val make_any_label :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
  StructuredTraces.trace_any_label sub_trace_result

val make_label_label :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
  StructuredTraces.trace_label_label sub_trace_result

val make_label_return :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
  StructuredTraces.trace_label_return trace_result

val make_label_return' :
  RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
  (IO.io_out, IO.io_in) flat_trace -> will_return ->
  StructuredTraces.trace_label_return trace_result

val actual_successor : RTLabs_semantics.state -> Graphs.label Types.option

val steps_for_statement : RTLabs_syntax.statement -> Nat.nat

type remainder_ok =
| Mk_remainder_ok

val remainder_ok_rect_Type4 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
  'a1

val remainder_ok_rect_Type5 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
  'a1

val remainder_ok_rect_Type3 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
  'a1

val remainder_ok_rect_Type2 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
  'a1

val remainder_ok_rect_Type1 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
  'a1

val remainder_ok_rect_Type0 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
  'a1

val remainder_ok_inv_rect_Type4 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
  -> 'a1

val remainder_ok_inv_rect_Type3 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
  -> 'a1

val remainder_ok_inv_rect_Type2 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
  -> 'a1

val remainder_ok_inv_rect_Type1 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
  -> 'a1

val remainder_ok_inv_rect_Type0 :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
  -> 'a1

val remainder_ok_discr :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __

val remainder_ok_jmdiscr :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
  IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __

val init_state_is :
  RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state -> (Pointers.block,
  __) Types.dPair

val ras_state_initial :
  RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
  RTLabs_abstract.rTLabs_ext_state

val deprop_execute :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
  -> Events.trace Types.sig0

val deprop_as_execute :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
  RTLabs_abstract.rTLabs_ext_state -> Events.trace Types.sig0

type ('o, 'i) partial_flat_trace =
| Pft_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
| Pft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
   * RTLabs_semantics.state * ('o, 'i) partial_flat_trace

val partial_flat_trace_rect_Type4 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3

val partial_flat_trace_rect_Type3 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3

val partial_flat_trace_rect_Type2 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3

val partial_flat_trace_rect_Type1 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3

val partial_flat_trace_rect_Type0 :
  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3

val partial_flat_trace_inv_rect_Type4 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3

val partial_flat_trace_inv_rect_Type3 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3

val partial_flat_trace_inv_rect_Type2 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3

val partial_flat_trace_inv_rect_Type1 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3

val partial_flat_trace_inv_rect_Type0 :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3

val partial_flat_trace_jmdiscr :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
  -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __

val append_partial_flat_trace :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
  -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
  partial_flat_trace -> ('a1, 'a2) partial_flat_trace

val partial_to_flat_trace :
  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
  -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2)
  flat_trace

val flat_trace_of_any_label :
  RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
  StructuredTraces.trace_any_label -> (IO.io_out, IO.io_in)
  partial_flat_trace

val flat_trace_of_label_label :
  RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
  RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
  StructuredTraces.trace_label_label -> (IO.io_out, IO.io_in)
  partial_flat_trace

val flat_trace_of_label_return :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
  RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_return ->
  (IO.io_out, IO.io_in) partial_flat_trace

val flat_trace_of_any_call :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
  RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
  Events.trace -> StructuredTraces.trace_any_call -> (IO.io_out, IO.io_in)
  partial_flat_trace

val flat_trace_of_label_call :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
  RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
  Events.trace -> StructuredTraces.trace_label_call -> (IO.io_out, IO.io_in)
  partial_flat_trace

val add_partial_flat_trace :
  RTLabs_semantics.genv -> RTLabs_semantics.state ->
  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
  partial_flat_trace -> StructuredTraces.trace_label_diverges -> (IO.io_out,
  IO.io_in) flat_trace

val flat_trace_of_label_diverges :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
  StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace

val flat_trace_of_whole_program :
  RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
  StructuredTraces.trace_whole_program -> (IO.io_out, IO.io_in) flat_trace

val state_fn : RTLabs_semantics.genv -> __ -> Pointers.block Types.option

val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __