open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Bool

open Jmeq

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Russell

open Util

open List

open Lists

open Nat

open Positive

open Types

open Identifiers

open CostLabel

open Sets

open Listb

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

open IOMonad

open IO

open Hide

type status_class =
| Cl_return
| Cl_jump
| Cl_call
| Cl_tailcall
| Cl_other

val status_class_rect_Type4 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1

val status_class_rect_Type5 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1

val status_class_rect_Type3 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1

val status_class_rect_Type2 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1

val status_class_rect_Type1 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1

val status_class_rect_Type0 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1

val status_class_inv_rect_Type4 :
  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val status_class_inv_rect_Type3 :
  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val status_class_inv_rect_Type2 :
  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val status_class_inv_rect_Type1 :
  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val status_class_inv_rect_Type0 :
  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
  (__ -> 'a1) -> 'a1

val status_class_discr : status_class -> status_class -> __

val status_class_jmdiscr : status_class -> status_class -> __

type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
                         as_classify : (__ -> status_class);
                         as_label_of_pc : (__ -> CostLabel.costlabel
                                          Types.option);
                         as_result : (__ -> Integers.int Types.option);
                         as_call_ident : (__ Types.sig0 -> AST.ident);
                         as_tailcall_ident : (__ Types.sig0 -> AST.ident) }

val abstract_status_rect_Type4 :
  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
  AST.ident) -> 'a1) -> abstract_status -> 'a1

val abstract_status_rect_Type5 :
  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
  AST.ident) -> 'a1) -> abstract_status -> 'a1

val abstract_status_rect_Type3 :
  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
  AST.ident) -> 'a1) -> abstract_status -> 'a1

val abstract_status_rect_Type2 :
  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
  AST.ident) -> 'a1) -> abstract_status -> 'a1

val abstract_status_rect_Type1 :
  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
  AST.ident) -> 'a1) -> abstract_status -> 'a1

val abstract_status_rect_Type0 :
  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
  AST.ident) -> 'a1) -> abstract_status -> 'a1

type as_status 

val as_pc : abstract_status -> Deqsets.deqSet

val as_pc_of : abstract_status -> __ -> __

val as_classify : abstract_status -> __ -> status_class

val as_label_of_pc :
  abstract_status -> __ -> CostLabel.costlabel Types.option

val as_result : abstract_status -> __ -> Integers.int Types.option

val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident

val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident

val abstract_status_inv_rect_Type4 :
  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1

val abstract_status_inv_rect_Type3 :
  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1

val abstract_status_inv_rect_Type2 :
  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1

val abstract_status_inv_rect_Type1 :
  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1

val abstract_status_inv_rect_Type0 :
  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1

val abstract_status_jmdiscr : abstract_status -> abstract_status -> __

val as_label : abstract_status -> __ -> CostLabel.costlabel Types.option

val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum

type as_cost_label = CostLabel.costlabel Types.sig0

type as_cost_labels = as_cost_label List.list

val as_cost_get_label :
  abstract_status -> as_cost_label -> CostLabel.costlabel

type as_cost_map = as_cost_label -> Nat.nat

val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label

val lift_sigma_map_id :
  'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
  Types.sig0 -> 'a2

val lift_cost_map_id :
  abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
  Types.sum) -> as_cost_map -> as_cost_map

type trace_ends_with_ret =
| Ends_with_ret
| Doesnt_end_with_ret

val trace_ends_with_ret_rect_Type4 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1

val trace_ends_with_ret_rect_Type5 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1

val trace_ends_with_ret_rect_Type3 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1

val trace_ends_with_ret_rect_Type2 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1

val trace_ends_with_ret_rect_Type1 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1

val trace_ends_with_ret_rect_Type0 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1

val trace_ends_with_ret_inv_rect_Type4 :
  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val trace_ends_with_ret_inv_rect_Type3 :
  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val trace_ends_with_ret_inv_rect_Type2 :
  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val trace_ends_with_ret_inv_rect_Type1 :
  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val trace_ends_with_ret_inv_rect_Type0 :
  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val trace_ends_with_ret_discr :
  trace_ends_with_ret -> trace_ends_with_ret -> __

val trace_ends_with_ret_jmdiscr :
  trace_ends_with_ret -> trace_ends_with_ret -> __

type trace_label_return =
| Tlr_base of __ * __ * trace_label_label
| Tlr_step of __ * __ * __ * trace_label_label * trace_label_return
and trace_label_label =
| Tll_base of trace_ends_with_ret * __ * __ * trace_any_label
and trace_any_label =
| Tal_base_not_return of __ * __
| Tal_base_return of __ * __
| Tal_base_call of __ * __ * __ * trace_label_return
| Tal_base_tailcall of __ * __ * __ * trace_label_return
| Tal_step_call of trace_ends_with_ret * __ * __ * __ * __
   * trace_label_return * trace_any_label
| Tal_step_default of trace_ends_with_ret * __ * __ * __ * trace_any_label

val trace_label_return_inv_rect_Type4 :
  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_return_inv_rect_Type3 :
  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_return_inv_rect_Type2 :
  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_return_inv_rect_Type1 :
  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_return_inv_rect_Type0 :
  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_label_inv_rect_Type4 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_label_label_inv_rect_Type3 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_label_label_inv_rect_Type2 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_label_label_inv_rect_Type1 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_label_label_inv_rect_Type0 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_any_label_inv_rect_Type4 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_label_inv_rect_Type3 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_label_inv_rect_Type2 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_label_inv_rect_Type1 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_label_inv_rect_Type0 :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_return_discr :
  abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
  __

val trace_label_label_discr :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  trace_label_label -> __

val trace_label_return_jmdiscr :
  abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
  __

val trace_label_label_jmdiscr :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  trace_label_label -> __

val trace_any_label_jmdiscr :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
  trace_any_label -> __

val tal_pc_list :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> __
  List.list

val as_trace_any_label_length' :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
  Nat.nat

val tll_hd_label :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  CostLabel.costlabel

val tlr_hd_label :
  abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel

type trace_any_call =
| Tac_base of __
| Tac_step_call of __ * __ * __ * __ * trace_label_return * trace_any_call
| Tac_step_default of __ * __ * __ * trace_any_call

val trace_any_call_rect_Type4 :
  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
  -> trace_any_call -> 'a1

val trace_any_call_rect_Type3 :
  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
  -> trace_any_call -> 'a1

val trace_any_call_rect_Type2 :
  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
  -> trace_any_call -> 'a1

val trace_any_call_rect_Type1 :
  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
  -> trace_any_call -> 'a1

val trace_any_call_rect_Type0 :
  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
  -> trace_any_call -> 'a1

val trace_any_call_inv_rect_Type4 :
  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_call_inv_rect_Type3 :
  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_call_inv_rect_Type2 :
  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_call_inv_rect_Type1 :
  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_call_inv_rect_Type0 :
  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_call_jmdiscr :
  abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __

type trace_label_call =
| Tlc_base of __ * __ * trace_any_call

val trace_label_call_rect_Type4 :
  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
  trace_label_call -> 'a1

val trace_label_call_rect_Type5 :
  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
  trace_label_call -> 'a1

val trace_label_call_rect_Type3 :
  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
  trace_label_call -> 'a1

val trace_label_call_rect_Type2 :
  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
  trace_label_call -> 'a1

val trace_label_call_rect_Type1 :
  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
  trace_label_call -> 'a1

val trace_label_call_rect_Type0 :
  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
  trace_label_call -> 'a1

val trace_label_call_inv_rect_Type4 :
  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_call_inv_rect_Type3 :
  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_call_inv_rect_Type2 :
  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_call_inv_rect_Type1 :
  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_call_inv_rect_Type0 :
  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_label_call_discr :
  abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __

val trace_label_call_jmdiscr :
  abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __

val tlc_hd_label :
  abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel

type trace_label_diverges = __trace_label_diverges Lazy.t
and __trace_label_diverges =
| Tld_step of __ * __ * trace_label_label * trace_label_diverges
| Tld_base of __ * __ * __ * trace_label_call * trace_label_diverges

val trace_label_diverges_inv_rect_Type4 :
  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
  -> 'a1) -> 'a1

val trace_label_diverges_inv_rect_Type3 :
  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
  -> 'a1) -> 'a1

val trace_label_diverges_inv_rect_Type2 :
  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
  -> 'a1) -> 'a1

val trace_label_diverges_inv_rect_Type1 :
  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
  -> 'a1) -> 'a1

val trace_label_diverges_inv_rect_Type0 :
  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
  -> 'a1) -> 'a1

val trace_label_diverges_jmdiscr :
  abstract_status -> __ -> trace_label_diverges -> trace_label_diverges -> __

val tld_hd_label :
  abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel

type trace_whole_program =
| Twp_terminating of __ * __ * __ * trace_label_return
| Twp_diverges of __ * __ * trace_label_diverges

val trace_whole_program_rect_Type4 :
  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
  trace_whole_program -> 'a1

val trace_whole_program_rect_Type5 :
  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
  trace_whole_program -> 'a1

val trace_whole_program_rect_Type3 :
  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
  trace_whole_program -> 'a1

val trace_whole_program_rect_Type2 :
  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
  trace_whole_program -> 'a1

val trace_whole_program_rect_Type1 :
  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
  trace_whole_program -> 'a1

val trace_whole_program_rect_Type0 :
  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
  trace_whole_program -> 'a1

val trace_whole_program_inv_rect_Type4 :
  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1

val trace_whole_program_inv_rect_Type3 :
  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1

val trace_whole_program_inv_rect_Type2 :
  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1

val trace_whole_program_inv_rect_Type1 :
  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1

val trace_whole_program_inv_rect_Type0 :
  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1

val trace_whole_program_jmdiscr :
  abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __

val tal_tl_label :
  abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel

val tll_tl_label :
  abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel

type trace_any_any =
| Taa_base of __
| Taa_step of __ * __ * __ * trace_any_any

val trace_any_any_rect_Type4 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1

val trace_any_any_rect_Type3 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1

val trace_any_any_rect_Type2 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1

val trace_any_any_rect_Type1 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1

val trace_any_any_rect_Type0 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1

val trace_any_any_inv_rect_Type4 :
  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_any_inv_rect_Type3 :
  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_any_inv_rect_Type2 :
  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_any_inv_rect_Type1 :
  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_any_inv_rect_Type0 :
  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1

val trace_any_any_jmdiscr :
  abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __

val taa_non_empty : abstract_status -> __ -> __ -> trace_any_any -> Bool.bool

val dpi1__o__taa_to_bool__o__inject :
  abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
  Bool.bool Types.sig0

val dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject :
  abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> __
  Types.sig0

val eject__o__taa_to_bool__o__inject :
  abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
  Types.sig0

val eject__o__taa_to_bool__o__bool_to_Prop__o__inject :
  abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> __ Types.sig0

val taa_to_bool__o__bool_to_Prop__o__inject :
  abstract_status -> __ -> __ -> trace_any_any -> __ Types.sig0

val taa_to_bool__o__inject :
  abstract_status -> __ -> __ -> trace_any_any -> Bool.bool Types.sig0

val dpi1__o__taa_to_bool :
  abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
  Bool.bool

val eject__o__taa_to_bool :
  abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool

val taa_append_tal :
  abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
  -> trace_any_label -> trace_any_label

type intensional_event =
| IEVcost of CostLabel.costlabel
| IEVcall of AST.ident
| IEVtailcall of AST.ident * AST.ident
| IEVret of AST.ident

val intensional_event_rect_Type4 :
  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1

val intensional_event_rect_Type5 :
  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1

val intensional_event_rect_Type3 :
  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1

val intensional_event_rect_Type2 :
  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1

val intensional_event_rect_Type1 :
  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1

val intensional_event_rect_Type0 :
  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1

val intensional_event_inv_rect_Type4 :
  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
  'a1) -> 'a1

val intensional_event_inv_rect_Type3 :
  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
  'a1) -> 'a1

val intensional_event_inv_rect_Type2 :
  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
  'a1) -> 'a1

val intensional_event_inv_rect_Type1 :
  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
  'a1) -> 'a1

val intensional_event_inv_rect_Type0 :
  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
  'a1) -> 'a1

val intensional_event_discr : intensional_event -> intensional_event -> __

val intensional_event_jmdiscr : intensional_event -> intensional_event -> __

type as_trace = intensional_event List.list Types.sig0

val cons_safe :
  'a1 Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0

val append_safe :
  'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list
  Types.sig0

val nil_safe : 'a1 List.list Types.sig0

val emittable_cost :
  abstract_status -> as_cost_label -> intensional_event Types.sig0

val observables_trace_label_return :
  abstract_status -> __ -> __ -> trace_label_return -> AST.ident -> as_trace

val observables_trace_any_label :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
  AST.ident -> as_trace

val observables_trace_label_label :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  AST.ident -> as_trace

val filter_map : ('a1 -> 'a2 Types.option) -> 'a1 List.list -> 'a2 List.list

val list_distribute_sig_aux : 'a1 List.list -> 'a1 Types.sig0 List.list

val list_distribute_sig :
  'a1 List.list Types.sig0 -> 'a1 Types.sig0 List.list

val list_factor_sig : 'a1 Types.sig0 List.list -> 'a1 List.list Types.sig0

val costlabels_of_observables :
  abstract_status -> as_trace -> as_cost_label List.list

val flatten_trace_label_return :
  abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
  List.list

val flatten_trace_label_label :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
  as_cost_label List.list

val flatten_trace_any_label :
  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
  as_cost_label List.list

type trace_any_any_free =
| Taaf_base of __
| Taaf_step of __ * __ * __ * trace_any_any
| Taaf_step_jump of __ * __ * __ * trace_any_any

val trace_any_any_free_rect_Type4 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
  __ -> __ -> trace_any_any_free -> 'a1

val trace_any_any_free_rect_Type5 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
  __ -> __ -> trace_any_any_free -> 'a1

val trace_any_any_free_rect_Type3 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
  __ -> __ -> trace_any_any_free -> 'a1

val trace_any_any_free_rect_Type2 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
  __ -> __ -> trace_any_any_free -> 'a1

val trace_any_any_free_rect_Type1 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
  __ -> __ -> trace_any_any_free -> 'a1

val trace_any_any_free_rect_Type0 :
  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
  __ -> __ -> trace_any_any_free -> 'a1

val trace_any_any_free_inv_rect_Type4 :
  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_any_any_free_inv_rect_Type3 :
  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_any_any_free_inv_rect_Type2 :
  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_any_any_free_inv_rect_Type1 :
  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_any_any_free_inv_rect_Type0 :
  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
  -> __ -> 'a1) -> 'a1

val trace_any_any_free_jmdiscr :
  abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free ->
  __

val taaf_non_empty :
  abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool

val taa_append_taa :
  abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any ->
  trace_any_any

val taaf_to_taa :
  abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any

val taaf_append_tal :
  abstract_status -> __ -> trace_ends_with_ret -> __ -> __ ->
  trace_any_any_free -> trace_any_label -> trace_any_label

val taaf_append_taa :
  abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any ->
  trace_any_any

val taaf_cons :
  abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
  trace_any_any_free

val taaf_append_taaf :
  abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
  trace_any_any_free -> trace_any_any_free