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 **) let rec status_class_rect_Type4 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function | Cl_return -> h_cl_return | Cl_jump -> h_cl_jump | Cl_call -> h_cl_call | Cl_tailcall -> h_cl_tailcall | Cl_other -> h_cl_other (** val status_class_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **) let rec status_class_rect_Type5 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function | Cl_return -> h_cl_return | Cl_jump -> h_cl_jump | Cl_call -> h_cl_call | Cl_tailcall -> h_cl_tailcall | Cl_other -> h_cl_other (** val status_class_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **) let rec status_class_rect_Type3 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function | Cl_return -> h_cl_return | Cl_jump -> h_cl_jump | Cl_call -> h_cl_call | Cl_tailcall -> h_cl_tailcall | Cl_other -> h_cl_other (** val status_class_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **) let rec status_class_rect_Type2 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function | Cl_return -> h_cl_return | Cl_jump -> h_cl_jump | Cl_call -> h_cl_call | Cl_tailcall -> h_cl_tailcall | Cl_other -> h_cl_other (** val status_class_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **) let rec status_class_rect_Type1 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function | Cl_return -> h_cl_return | Cl_jump -> h_cl_jump | Cl_call -> h_cl_call | Cl_tailcall -> h_cl_tailcall | Cl_other -> h_cl_other (** val status_class_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **) let rec status_class_rect_Type0 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function | Cl_return -> h_cl_return | Cl_jump -> h_cl_jump | Cl_call -> h_cl_call | Cl_tailcall -> h_cl_tailcall | Cl_other -> h_cl_other (** val status_class_inv_rect_Type4 : status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let status_class_inv_rect_Type4 hterm h1 h2 h3 h4 h5 = let hcut = status_class_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __ (** val status_class_inv_rect_Type3 : status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let status_class_inv_rect_Type3 hterm h1 h2 h3 h4 h5 = let hcut = status_class_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __ (** val status_class_inv_rect_Type2 : status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let status_class_inv_rect_Type2 hterm h1 h2 h3 h4 h5 = let hcut = status_class_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __ (** val status_class_inv_rect_Type1 : status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let status_class_inv_rect_Type1 hterm h1 h2 h3 h4 h5 = let hcut = status_class_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __ (** val status_class_inv_rect_Type0 : status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let status_class_inv_rect_Type0 hterm h1 h2 h3 h4 h5 = let hcut = status_class_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __ (** val status_class_discr : status_class -> status_class -> __ **) let status_class_discr x y = Logic.eq_rect_Type2 x (match x with | Cl_return -> Obj.magic (fun _ dH -> dH) | Cl_jump -> Obj.magic (fun _ dH -> dH) | Cl_call -> Obj.magic (fun _ dH -> dH) | Cl_tailcall -> Obj.magic (fun _ dH -> dH) | Cl_other -> Obj.magic (fun _ dH -> dH)) y (** val status_class_jmdiscr : status_class -> status_class -> __ **) let status_class_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | Cl_return -> Obj.magic (fun _ dH -> dH) | Cl_jump -> Obj.magic (fun _ dH -> dH) | Cl_call -> Obj.magic (fun _ dH -> dH) | Cl_tailcall -> Obj.magic (fun _ dH -> dH) | Cl_other -> Obj.magic (fun _ dH -> dH)) y 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 **) let rec abstract_status_rect_Type4 h_mk_abstract_status x_22380 = let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0; as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident = as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22380 in h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __ as_result0 as_call_ident0 as_tailcall_ident0 (** 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 **) let rec abstract_status_rect_Type5 h_mk_abstract_status x_22382 = let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0; as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident = as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22382 in h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __ as_result0 as_call_ident0 as_tailcall_ident0 (** 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 **) let rec abstract_status_rect_Type3 h_mk_abstract_status x_22384 = let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0; as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident = as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22384 in h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __ as_result0 as_call_ident0 as_tailcall_ident0 (** 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 **) let rec abstract_status_rect_Type2 h_mk_abstract_status x_22386 = let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0; as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident = as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22386 in h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __ as_result0 as_call_ident0 as_tailcall_ident0 (** 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 **) let rec abstract_status_rect_Type1 h_mk_abstract_status x_22388 = let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0; as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident = as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22388 in h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __ as_result0 as_call_ident0 as_tailcall_ident0 (** 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 **) let rec abstract_status_rect_Type0 h_mk_abstract_status x_22390 = let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0; as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident = as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22390 in h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __ as_result0 as_call_ident0 as_tailcall_ident0 type as_status = __ (** val as_pc : abstract_status -> Deqsets.deqSet **) let rec as_pc xxx = xxx.as_pc (** val as_pc_of : abstract_status -> __ -> __ **) let rec as_pc_of xxx = xxx.as_pc_of (** val as_classify : abstract_status -> __ -> status_class **) let rec as_classify xxx = xxx.as_classify (** val as_label_of_pc : abstract_status -> __ -> CostLabel.costlabel Types.option **) let rec as_label_of_pc xxx = xxx.as_label_of_pc (** val as_result : abstract_status -> __ -> Integers.int Types.option **) let rec as_result xxx = xxx.as_result (** val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident **) let rec as_call_ident xxx = xxx.as_call_ident (** val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident **) let rec as_tailcall_ident xxx = xxx.as_tailcall_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 **) let abstract_status_inv_rect_Type4 hterm h1 = let hcut = abstract_status_rect_Type4 h1 hterm in hcut __ (** 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 **) let abstract_status_inv_rect_Type3 hterm h1 = let hcut = abstract_status_rect_Type3 h1 hterm in hcut __ (** 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 **) let abstract_status_inv_rect_Type2 hterm h1 = let hcut = abstract_status_rect_Type2 h1 hterm in hcut __ (** 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 **) let abstract_status_inv_rect_Type1 hterm h1 = let hcut = abstract_status_rect_Type1 h1 hterm in hcut __ (** 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 **) let abstract_status_inv_rect_Type0 hterm h1 = let hcut = abstract_status_rect_Type0 h1 hterm in hcut __ (** val abstract_status_jmdiscr : abstract_status -> abstract_status -> __ **) let abstract_status_jmdiscr x y = Logic.eq_rect_Type2 x (let { as_pc = a2; as_pc_of = a3; as_classify = a4; as_label_of_pc = a5; as_result = a7; as_call_ident = a8; as_tailcall_ident = a9 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y (** val as_label : abstract_status -> __ -> CostLabel.costlabel Types.option **) let as_label s s0 = s.as_label_of_pc (s.as_pc_of s0) (** val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum **) let as_costed_exc s s0 = match as_label s s0 with | Types.None -> Types.Inr __ | Types.Some c -> Types.Inl __ 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 **) let as_cost_get_label s l_sig = Types.pi1 l_sig type as_cost_map = as_cost_label -> Nat.nat (** val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label **) let as_label_safe a_s st_sig = Option.opt_safe (as_label a_s (Types.pi1 st_sig)) (** val lift_sigma_map_id : 'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 Types.sig0 -> 'a2 **) let lift_sigma_map_id dflt dec m a_sig = match dec (Types.pi1 a_sig) with | Types.Inl _ -> m (Types.pi1 a_sig) | Types.Inr _ -> dflt (** val lift_cost_map_id : abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __) Types.sum) -> as_cost_map -> as_cost_map **) let lift_cost_map_id s_in s_out = lift_sigma_map_id Nat.O 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 **) let rec trace_ends_with_ret_rect_Type4 h_ends_with_ret h_doesnt_end_with_ret = function | Ends_with_ret -> h_ends_with_ret | Doesnt_end_with_ret -> h_doesnt_end_with_ret (** val trace_ends_with_ret_rect_Type5 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **) let rec trace_ends_with_ret_rect_Type5 h_ends_with_ret h_doesnt_end_with_ret = function | Ends_with_ret -> h_ends_with_ret | Doesnt_end_with_ret -> h_doesnt_end_with_ret (** val trace_ends_with_ret_rect_Type3 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **) let rec trace_ends_with_ret_rect_Type3 h_ends_with_ret h_doesnt_end_with_ret = function | Ends_with_ret -> h_ends_with_ret | Doesnt_end_with_ret -> h_doesnt_end_with_ret (** val trace_ends_with_ret_rect_Type2 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **) let rec trace_ends_with_ret_rect_Type2 h_ends_with_ret h_doesnt_end_with_ret = function | Ends_with_ret -> h_ends_with_ret | Doesnt_end_with_ret -> h_doesnt_end_with_ret (** val trace_ends_with_ret_rect_Type1 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **) let rec trace_ends_with_ret_rect_Type1 h_ends_with_ret h_doesnt_end_with_ret = function | Ends_with_ret -> h_ends_with_ret | Doesnt_end_with_ret -> h_doesnt_end_with_ret (** val trace_ends_with_ret_rect_Type0 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **) let rec trace_ends_with_ret_rect_Type0 h_ends_with_ret h_doesnt_end_with_ret = function | Ends_with_ret -> h_ends_with_ret | Doesnt_end_with_ret -> h_doesnt_end_with_ret (** val trace_ends_with_ret_inv_rect_Type4 : trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let trace_ends_with_ret_inv_rect_Type4 hterm h1 h2 = let hcut = trace_ends_with_ret_rect_Type4 h1 h2 hterm in hcut __ (** val trace_ends_with_ret_inv_rect_Type3 : trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let trace_ends_with_ret_inv_rect_Type3 hterm h1 h2 = let hcut = trace_ends_with_ret_rect_Type3 h1 h2 hterm in hcut __ (** val trace_ends_with_ret_inv_rect_Type2 : trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let trace_ends_with_ret_inv_rect_Type2 hterm h1 h2 = let hcut = trace_ends_with_ret_rect_Type2 h1 h2 hterm in hcut __ (** val trace_ends_with_ret_inv_rect_Type1 : trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let trace_ends_with_ret_inv_rect_Type1 hterm h1 h2 = let hcut = trace_ends_with_ret_rect_Type1 h1 h2 hterm in hcut __ (** val trace_ends_with_ret_inv_rect_Type0 : trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let trace_ends_with_ret_inv_rect_Type0 hterm h1 h2 = let hcut = trace_ends_with_ret_rect_Type0 h1 h2 hterm in hcut __ (** val trace_ends_with_ret_discr : trace_ends_with_ret -> trace_ends_with_ret -> __ **) let trace_ends_with_ret_discr x y = Logic.eq_rect_Type2 x (match x with | Ends_with_ret -> Obj.magic (fun _ dH -> dH) | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y (** val trace_ends_with_ret_jmdiscr : trace_ends_with_ret -> trace_ends_with_ret -> __ **) let trace_ends_with_ret_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | Ends_with_ret -> Obj.magic (fun _ dH -> dH) | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y 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 **) let trace_label_return_inv_rect_Type4 x1 x2 x3 hterm h1 h2 = let hcut = match hterm with | Tlr_base (x, x0, x4) -> h1 x x0 x4 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6 in hcut __ __ __ (** val trace_label_return_inv_rect_Type3 : abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ -> trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_label_return_inv_rect_Type3 x1 x2 x3 hterm h1 h2 = let hcut = match hterm with | Tlr_base (x, x0, x4) -> h1 x x0 x4 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6 in hcut __ __ __ (** val trace_label_return_inv_rect_Type2 : abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ -> trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_label_return_inv_rect_Type2 x1 x2 x3 hterm h1 h2 = let hcut = match hterm with | Tlr_base (x, x0, x4) -> h1 x x0 x4 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6 in hcut __ __ __ (** val trace_label_return_inv_rect_Type1 : abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ -> trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_label_return_inv_rect_Type1 x1 x2 x3 hterm h1 h2 = let hcut = match hterm with | Tlr_base (x, x0, x4) -> h1 x x0 x4 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6 in hcut __ __ __ (** val trace_label_return_inv_rect_Type0 : abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ -> trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_label_return_inv_rect_Type0 x1 x2 x3 hterm h1 h2 = let hcut = match hterm with | Tlr_base (x, x0, x4) -> h1 x x0 x4 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6 in hcut __ __ __ (** 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 **) let trace_label_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 = let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in hcut __ __ __ __ (** 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 **) let trace_label_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 = let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in hcut __ __ __ __ (** 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 **) let trace_label_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 = let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in hcut __ __ __ __ (** 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 **) let trace_label_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 = let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in hcut __ __ __ __ (** 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 **) let trace_label_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 = let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in hcut __ __ __ __ (** 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 **) let trace_any_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 = let hcut = match hterm with | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __ | Tal_base_return (x, x0) -> h2 x x0 __ __ | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __ | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) -> h5 x x0 x5 x6 x7 __ __ __ x8 __ x9 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __ in hcut __ __ __ __ (** 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 **) let trace_any_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 = let hcut = match hterm with | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __ | Tal_base_return (x, x0) -> h2 x x0 __ __ | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __ | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) -> h5 x x0 x5 x6 x7 __ __ __ x8 __ x9 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __ in hcut __ __ __ __ (** 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 **) let trace_any_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 = let hcut = match hterm with | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __ | Tal_base_return (x, x0) -> h2 x x0 __ __ | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __ | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) -> h5 x x0 x5 x6 x7 __ __ __ x8 __ x9 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __ in hcut __ __ __ __ (** 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 **) let trace_any_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 = let hcut = match hterm with | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __ | Tal_base_return (x, x0) -> h2 x x0 __ __ | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __ | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) -> h5 x x0 x5 x6 x7 __ __ __ x8 __ x9 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __ in hcut __ __ __ __ (** 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 **) let trace_any_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 = let hcut = match hterm with | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __ | Tal_base_return (x, x0) -> h2 x x0 __ __ | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __ | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) -> h5 x x0 x5 x6 x7 __ __ __ x8 __ x9 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __ in hcut __ __ __ __ (** val trace_label_return_discr : abstract_status -> __ -> __ -> trace_label_return -> trace_label_return -> __ **) let trace_label_return_discr a1 a2 a3 x y = Logic.eq_rect_Type2 x (match x with | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | Tlr_step (a0, a10, a20, a30, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val trace_label_label_discr : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label -> trace_label_label -> __ **) let trace_label_label_discr a1 a2 a3 a4 x y = Logic.eq_rect_Type2 x (let Tll_base (a0, a10, a20, a30) = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val trace_label_return_jmdiscr : abstract_status -> __ -> __ -> trace_label_return -> trace_label_return -> __ **) let trace_label_return_jmdiscr a1 a2 a3 x y = Logic.eq_rect_Type2 x (match x with | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | Tlr_step (a0, a10, a20, a30, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val trace_label_label_jmdiscr : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label -> trace_label_label -> __ **) let trace_label_label_jmdiscr a1 a2 a3 a4 x y = Logic.eq_rect_Type2 x (let Tll_base (a0, a10, a20, a30) = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val trace_any_label_jmdiscr : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> trace_any_label -> __ **) let trace_any_label_jmdiscr a1 a2 a3 a4 x y = Logic.eq_rect_Type2 x (match x with | Tal_base_not_return (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __ __ __) | Tal_base_return (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __ __) | Tal_base_call (a0, a10, a20, a6) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __) | Tal_base_tailcall (a0, a10, a20, a5) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __) | Tal_step_call (a0, a10, a20, a30, a40, a8, a100) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __) | Tal_step_default (a0, a10, a20, a30, a5) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y (** val tal_pc_list : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ List.list **) let rec tal_pc_list s fl st1 st2 = function | Tal_base_not_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil) | Tal_base_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil) | Tal_base_call (pre, x, x0, x4) -> List.Cons ((s.as_pc_of pre), List.Nil) | Tal_base_tailcall (pre, x, x0, x3) -> List.Cons ((s.as_pc_of pre), List.Nil) | Tal_step_call (fl', pre, x, st1', st2', x3, tl) -> List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl)) | Tal_step_default (fl', pre, st1', st2', tl) -> List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl)) (** val as_trace_any_label_length' : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> Nat.nat **) let as_trace_any_label_length' s trace_ends_flag start_status final_status the_trace = List.length (tal_pc_list s trace_ends_flag start_status final_status the_trace) (** val tll_hd_label : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label -> CostLabel.costlabel **) let tll_hd_label s fl st1 st2 tr = (let Tll_base (x, st1', x0, x1) = tr in (fun _ _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __ __ (** val tlr_hd_label : abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel **) let tlr_hd_label s st1 st2 = function | Tlr_base (st1', st2', tll) -> tll_hd_label s Ends_with_ret st1' st2' tll | Tlr_step (st1', st2', x, tll, x0) -> tll_hd_label s Doesnt_end_with_ret st1' st2' tll 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 **) let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_22468 x_22467 = function | Tac_base status -> h_tac_base status __ | Tac_step_call (status_pre_fun_call, status_after_fun_call, status_final, status_start_fun_call, x_22473, x_22471) -> h_tac_step_call status_pre_fun_call status_after_fun_call status_final status_start_fun_call __ __ __ x_22473 __ x_22471 (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default status_after_fun_call status_final x_22471) | Tac_step_default (status_pre, status_end, status_init, x_22478) -> h_tac_step_default status_pre status_end status_init __ x_22478 __ __ (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default status_init status_end x_22478) (** 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 **) let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_22500 x_22499 = function | Tac_base status -> h_tac_base status __ | Tac_step_call (status_pre_fun_call, status_after_fun_call, status_final, status_start_fun_call, x_22505, x_22503) -> h_tac_step_call status_pre_fun_call status_after_fun_call status_final status_start_fun_call __ __ __ x_22505 __ x_22503 (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default status_after_fun_call status_final x_22503) | Tac_step_default (status_pre, status_end, status_init, x_22510) -> h_tac_step_default status_pre status_end status_init __ x_22510 __ __ (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default status_init status_end x_22510) (** 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 **) let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_22516 x_22515 = function | Tac_base status -> h_tac_base status __ | Tac_step_call (status_pre_fun_call, status_after_fun_call, status_final, status_start_fun_call, x_22521, x_22519) -> h_tac_step_call status_pre_fun_call status_after_fun_call status_final status_start_fun_call __ __ __ x_22521 __ x_22519 (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default status_after_fun_call status_final x_22519) | Tac_step_default (status_pre, status_end, status_init, x_22526) -> h_tac_step_default status_pre status_end status_init __ x_22526 __ __ (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default status_init status_end x_22526) (** 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 **) let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_22532 x_22531 = function | Tac_base status -> h_tac_base status __ | Tac_step_call (status_pre_fun_call, status_after_fun_call, status_final, status_start_fun_call, x_22537, x_22535) -> h_tac_step_call status_pre_fun_call status_after_fun_call status_final status_start_fun_call __ __ __ x_22537 __ x_22535 (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default status_after_fun_call status_final x_22535) | Tac_step_default (status_pre, status_end, status_init, x_22542) -> h_tac_step_default status_pre status_end status_init __ x_22542 __ __ (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default status_init status_end x_22542) (** 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 **) let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_22548 x_22547 = function | Tac_base status -> h_tac_base status __ | Tac_step_call (status_pre_fun_call, status_after_fun_call, status_final, status_start_fun_call, x_22553, x_22551) -> h_tac_step_call status_pre_fun_call status_after_fun_call status_final status_start_fun_call __ __ __ x_22553 __ x_22551 (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default status_after_fun_call status_final x_22551) | Tac_step_default (status_pre, status_end, status_init, x_22558) -> h_tac_step_default status_pre status_end status_init __ x_22558 __ __ (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default status_init status_end x_22558) (** 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 **) let trace_any_call_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_call_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** 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 **) let trace_any_call_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_call_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** 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 **) let trace_any_call_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_call_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** 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 **) let trace_any_call_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_call_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** 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 **) let trace_any_call_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_call_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** val trace_any_call_jmdiscr : abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __ **) let trace_any_call_jmdiscr a1 a2 a3 x y = Logic.eq_rect_Type2 x (match x with | Tac_base a0 -> Obj.magic (fun _ dH -> dH __ __) | Tac_step_call (a0, a10, a20, a30, a7, a9) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __) | Tac_step_default (a0, a10, a20, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y 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 **) let rec trace_label_call_rect_Type4 s h_tlc_base x_22666 x_22665 = function | Tlc_base (start_status, end_status, x_22669) -> h_tlc_base start_status end_status x_22669 __ (** val trace_label_call_rect_Type5 : abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ -> trace_label_call -> 'a1 **) let rec trace_label_call_rect_Type5 s h_tlc_base x_22672 x_22671 = function | Tlc_base (start_status, end_status, x_22675) -> h_tlc_base start_status end_status x_22675 __ (** val trace_label_call_rect_Type3 : abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ -> trace_label_call -> 'a1 **) let rec trace_label_call_rect_Type3 s h_tlc_base x_22678 x_22677 = function | Tlc_base (start_status, end_status, x_22681) -> h_tlc_base start_status end_status x_22681 __ (** val trace_label_call_rect_Type2 : abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ -> trace_label_call -> 'a1 **) let rec trace_label_call_rect_Type2 s h_tlc_base x_22684 x_22683 = function | Tlc_base (start_status, end_status, x_22687) -> h_tlc_base start_status end_status x_22687 __ (** val trace_label_call_rect_Type1 : abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ -> trace_label_call -> 'a1 **) let rec trace_label_call_rect_Type1 s h_tlc_base x_22690 x_22689 = function | Tlc_base (start_status, end_status, x_22693) -> h_tlc_base start_status end_status x_22693 __ (** val trace_label_call_rect_Type0 : abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ -> trace_label_call -> 'a1 **) let rec trace_label_call_rect_Type0 s h_tlc_base x_22696 x_22695 = function | Tlc_base (start_status, end_status, x_22699) -> h_tlc_base start_status end_status x_22699 __ (** val trace_label_call_inv_rect_Type4 : abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ -> trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_label_call_inv_rect_Type4 x1 x2 x3 hterm h1 = let hcut = trace_label_call_rect_Type4 x1 h1 x2 x3 hterm in hcut __ __ __ (** val trace_label_call_inv_rect_Type3 : abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ -> trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_label_call_inv_rect_Type3 x1 x2 x3 hterm h1 = let hcut = trace_label_call_rect_Type3 x1 h1 x2 x3 hterm in hcut __ __ __ (** val trace_label_call_inv_rect_Type2 : abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ -> trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_label_call_inv_rect_Type2 x1 x2 x3 hterm h1 = let hcut = trace_label_call_rect_Type2 x1 h1 x2 x3 hterm in hcut __ __ __ (** val trace_label_call_inv_rect_Type1 : abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ -> trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_label_call_inv_rect_Type1 x1 x2 x3 hterm h1 = let hcut = trace_label_call_rect_Type1 x1 h1 x2 x3 hterm in hcut __ __ __ (** val trace_label_call_inv_rect_Type0 : abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ -> trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_label_call_inv_rect_Type0 x1 x2 x3 hterm h1 = let hcut = trace_label_call_rect_Type0 x1 h1 x2 x3 hterm in hcut __ __ __ (** val trace_label_call_discr : abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **) let trace_label_call_discr a1 a2 a3 x y = Logic.eq_rect_Type2 x (let Tlc_base (a0, a10, a20) = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val trace_label_call_jmdiscr : abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **) let trace_label_call_jmdiscr a1 a2 a3 x y = Logic.eq_rect_Type2 x (let Tlc_base (a0, a10, a20) = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val tlc_hd_label : abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel **) let tlc_hd_label s st1 st2 tr = (let Tlc_base (st1', x, x0) = tr in (fun _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __ 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 **) let trace_label_diverges_inv_rect_Type4 x1 x2 hterm h1 h2 = let hcut = match Lazy.force hterm with | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5 in hcut __ __ (** 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 **) let trace_label_diverges_inv_rect_Type3 x1 x2 hterm h1 h2 = let hcut = match Lazy.force hterm with | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5 in hcut __ __ (** 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 **) let trace_label_diverges_inv_rect_Type2 x1 x2 hterm h1 h2 = let hcut = match Lazy.force hterm with | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5 in hcut __ __ (** 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 **) let trace_label_diverges_inv_rect_Type1 x1 x2 hterm h1 h2 = let hcut = match Lazy.force hterm with | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5 in hcut __ __ (** 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 **) let trace_label_diverges_inv_rect_Type0 x1 x2 hterm h1 h2 = let hcut = match Lazy.force hterm with | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5 in hcut __ __ (** val trace_label_diverges_jmdiscr : abstract_status -> __ -> trace_label_diverges -> trace_label_diverges -> __ **) let trace_label_diverges_jmdiscr a1 a2 x y = Logic.eq_rect_Type2 x (match Lazy.force x with | Tld_step (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __) | Tld_base (a0, a10, a20, a3, a6) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y (** val tld_hd_label : abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel **) let tld_hd_label s st tr = match Lazy.force tr with | Tld_step (st', st'', tll, x) -> tll_hd_label s Doesnt_end_with_ret st' st'' tll | Tld_base (st', st'', x, tlc, x2) -> tlc_hd_label s st' st'' tlc 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 **) let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_22748 = function | Twp_terminating (status_initial, status_start_fun, status_final, x_22751) -> h_twp_terminating status_initial status_start_fun status_final __ __ x_22751 __ | Twp_diverges (status_initial, status_start_fun, x_22754) -> h_twp_diverges status_initial status_start_fun __ __ x_22754 (** val trace_whole_program_rect_Type5 : abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ -> trace_whole_program -> 'a1 **) let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_22759 = function | Twp_terminating (status_initial, status_start_fun, status_final, x_22762) -> h_twp_terminating status_initial status_start_fun status_final __ __ x_22762 __ | Twp_diverges (status_initial, status_start_fun, x_22765) -> h_twp_diverges status_initial status_start_fun __ __ x_22765 (** val trace_whole_program_rect_Type3 : abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ -> trace_whole_program -> 'a1 **) let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_22770 = function | Twp_terminating (status_initial, status_start_fun, status_final, x_22773) -> h_twp_terminating status_initial status_start_fun status_final __ __ x_22773 __ | Twp_diverges (status_initial, status_start_fun, x_22776) -> h_twp_diverges status_initial status_start_fun __ __ x_22776 (** val trace_whole_program_rect_Type2 : abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ -> trace_whole_program -> 'a1 **) let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_22781 = function | Twp_terminating (status_initial, status_start_fun, status_final, x_22784) -> h_twp_terminating status_initial status_start_fun status_final __ __ x_22784 __ | Twp_diverges (status_initial, status_start_fun, x_22787) -> h_twp_diverges status_initial status_start_fun __ __ x_22787 (** val trace_whole_program_rect_Type1 : abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ -> trace_whole_program -> 'a1 **) let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_22792 = function | Twp_terminating (status_initial, status_start_fun, status_final, x_22795) -> h_twp_terminating status_initial status_start_fun status_final __ __ x_22795 __ | Twp_diverges (status_initial, status_start_fun, x_22798) -> h_twp_diverges status_initial status_start_fun __ __ x_22798 (** val trace_whole_program_rect_Type0 : abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ -> trace_whole_program -> 'a1 **) let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_22803 = function | Twp_terminating (status_initial, status_start_fun, status_final, x_22806) -> h_twp_terminating status_initial status_start_fun status_final __ __ x_22806 __ | Twp_diverges (status_initial, status_start_fun, x_22809) -> h_twp_diverges status_initial status_start_fun __ __ x_22809 (** val trace_whole_program_inv_rect_Type4 : abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **) let trace_whole_program_inv_rect_Type4 x1 x2 hterm h1 h2 = let hcut = trace_whole_program_rect_Type4 x1 h1 h2 x2 hterm in hcut __ __ (** val trace_whole_program_inv_rect_Type3 : abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **) let trace_whole_program_inv_rect_Type3 x1 x2 hterm h1 h2 = let hcut = trace_whole_program_rect_Type3 x1 h1 h2 x2 hterm in hcut __ __ (** val trace_whole_program_inv_rect_Type2 : abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **) let trace_whole_program_inv_rect_Type2 x1 x2 hterm h1 h2 = let hcut = trace_whole_program_rect_Type2 x1 h1 h2 x2 hterm in hcut __ __ (** val trace_whole_program_inv_rect_Type1 : abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **) let trace_whole_program_inv_rect_Type1 x1 x2 hterm h1 h2 = let hcut = trace_whole_program_rect_Type1 x1 h1 h2 x2 hterm in hcut __ __ (** val trace_whole_program_inv_rect_Type0 : abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **) let trace_whole_program_inv_rect_Type0 x1 x2 hterm h1 h2 = let hcut = trace_whole_program_rect_Type0 x1 h1 h2 x2 hterm in hcut __ __ (** val trace_whole_program_jmdiscr : abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __ **) let trace_whole_program_jmdiscr a1 a2 x y = Logic.eq_rect_Type2 x (match x with | Twp_terminating (a0, a10, a20, a5) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __) | Twp_diverges (a0, a10, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val tal_tl_label : abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel **) let tal_tl_label s st1 st2 tr = Types.pi1 (as_label_safe s st2) (** val tll_tl_label : abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel **) let tll_tl_label s st1 st2 tr = Types.pi1 (as_label_safe s st2) 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 **) let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_23033 x_23032 = function | Taa_base st -> h_taa_base st | Taa_step (st1, st2, st3, x_23035) -> h_taa_step st1 st2 st3 __ __ __ x_23035 (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_23035) (** val trace_any_any_rect_Type3 : abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **) let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_23051 x_23050 = function | Taa_base st -> h_taa_base st | Taa_step (st1, st2, st3, x_23053) -> h_taa_step st1 st2 st3 __ __ __ x_23053 (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_23053) (** val trace_any_any_rect_Type2 : abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **) let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_23060 x_23059 = function | Taa_base st -> h_taa_base st | Taa_step (st1, st2, st3, x_23062) -> h_taa_step st1 st2 st3 __ __ __ x_23062 (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_23062) (** val trace_any_any_rect_Type1 : abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **) let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_23069 x_23068 = function | Taa_base st -> h_taa_base st | Taa_step (st1, st2, st3, x_23071) -> h_taa_step st1 st2 st3 __ __ __ x_23071 (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_23071) (** val trace_any_any_rect_Type0 : abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **) let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_23078 x_23077 = function | Taa_base st -> h_taa_base st | Taa_step (st1, st2, st3, x_23080) -> h_taa_step st1 st2 st3 __ __ __ x_23080 (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_23080) (** val trace_any_any_inv_rect_Type4 : abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_inv_rect_Type4 x1 x2 x3 hterm h1 h2 = let hcut = trace_any_any_rect_Type4 x1 h1 h2 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_inv_rect_Type3 : abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_inv_rect_Type3 x1 x2 x3 hterm h1 h2 = let hcut = trace_any_any_rect_Type3 x1 h1 h2 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_inv_rect_Type2 : abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_inv_rect_Type2 x1 x2 x3 hterm h1 h2 = let hcut = trace_any_any_rect_Type2 x1 h1 h2 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_inv_rect_Type1 : abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_inv_rect_Type1 x1 x2 x3 hterm h1 h2 = let hcut = trace_any_any_rect_Type1 x1 h1 h2 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_inv_rect_Type0 : abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_inv_rect_Type0 x1 x2 x3 hterm h1 h2 = let hcut = trace_any_any_rect_Type0 x1 h1 h2 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_jmdiscr : abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __ **) let trace_any_any_jmdiscr a1 a2 a3 x y = Logic.eq_rect_Type2 x (match x with | Taa_base a0 -> Obj.magic (fun _ dH -> dH __) | Taa_step (a0, a10, a20, a6) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y (** val taa_non_empty : abstract_status -> __ -> __ -> trace_any_any -> Bool.bool **) let taa_non_empty s st1 st2 = function | Taa_base x -> Bool.False | Taa_step (x, x0, x1, x5) -> Bool.True (** val dpi1__o__taa_to_bool__o__inject : abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> Bool.bool Types.sig0 **) let dpi1__o__taa_to_bool__o__inject x1 x2 x3 x5 = taa_non_empty x1 x2 x3 x5.Types.dpi1 (** val dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject : abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> __ Types.sig0 **) let dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x5 = Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 x5.Types.dpi1) (** val eject__o__taa_to_bool__o__inject : abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool Types.sig0 **) let eject__o__taa_to_bool__o__inject x1 x2 x3 x5 = taa_non_empty x1 x2 x3 (Types.pi1 x5) (** val eject__o__taa_to_bool__o__bool_to_Prop__o__inject : abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> __ Types.sig0 **) let eject__o__taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x5 = Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 (Types.pi1 x5)) (** val taa_to_bool__o__bool_to_Prop__o__inject : abstract_status -> __ -> __ -> trace_any_any -> __ Types.sig0 **) let taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x4 = Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 x4) (** val taa_to_bool__o__inject : abstract_status -> __ -> __ -> trace_any_any -> Bool.bool Types.sig0 **) let taa_to_bool__o__inject x1 x2 x3 x4 = taa_non_empty x1 x2 x3 x4 (** val dpi1__o__taa_to_bool : abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> Bool.bool **) let dpi1__o__taa_to_bool x0 x1 x2 x4 = taa_non_empty x0 x1 x2 x4.Types.dpi1 (** val eject__o__taa_to_bool : abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool **) let eject__o__taa_to_bool x0 x1 x2 x4 = taa_non_empty x0 x1 x2 (Types.pi1 x4) (** val taa_append_tal : abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any -> trace_any_label -> trace_any_label **) let rec taa_append_tal s st1 fl st2 st3 taa = (match taa with | Taa_base st1' -> (fun fl0 st30 tal2 -> tal2) | Taa_step (st1', st2', st3', tl) -> (fun fl0 st30 tal2 -> Tal_step_default (fl0, st1', st2', st30, (taa_append_tal s st2' fl0 st3' st30 tl tal2)))) fl st3 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 **) let rec intensional_event_rect_Type4 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function | IEVcost x_23151 -> h_IEVcost x_23151 | IEVcall x_23152 -> h_IEVcall x_23152 | IEVtailcall (x_23154, x_23153) -> h_IEVtailcall x_23154 x_23153 | IEVret x_23155 -> h_IEVret x_23155 (** val intensional_event_rect_Type5 : (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident -> AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **) let rec intensional_event_rect_Type5 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function | IEVcost x_23161 -> h_IEVcost x_23161 | IEVcall x_23162 -> h_IEVcall x_23162 | IEVtailcall (x_23164, x_23163) -> h_IEVtailcall x_23164 x_23163 | IEVret x_23165 -> h_IEVret x_23165 (** val intensional_event_rect_Type3 : (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident -> AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **) let rec intensional_event_rect_Type3 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function | IEVcost x_23171 -> h_IEVcost x_23171 | IEVcall x_23172 -> h_IEVcall x_23172 | IEVtailcall (x_23174, x_23173) -> h_IEVtailcall x_23174 x_23173 | IEVret x_23175 -> h_IEVret x_23175 (** val intensional_event_rect_Type2 : (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident -> AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **) let rec intensional_event_rect_Type2 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function | IEVcost x_23181 -> h_IEVcost x_23181 | IEVcall x_23182 -> h_IEVcall x_23182 | IEVtailcall (x_23184, x_23183) -> h_IEVtailcall x_23184 x_23183 | IEVret x_23185 -> h_IEVret x_23185 (** val intensional_event_rect_Type1 : (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident -> AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **) let rec intensional_event_rect_Type1 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function | IEVcost x_23191 -> h_IEVcost x_23191 | IEVcall x_23192 -> h_IEVcall x_23192 | IEVtailcall (x_23194, x_23193) -> h_IEVtailcall x_23194 x_23193 | IEVret x_23195 -> h_IEVret x_23195 (** val intensional_event_rect_Type0 : (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident -> AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **) let rec intensional_event_rect_Type0 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function | IEVcost x_23201 -> h_IEVcost x_23201 | IEVcall x_23202 -> h_IEVcall x_23202 | IEVtailcall (x_23204, x_23203) -> h_IEVtailcall x_23204 x_23203 | IEVret x_23205 -> h_IEVret x_23205 (** val intensional_event_inv_rect_Type4 : intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **) let intensional_event_inv_rect_Type4 hterm h1 h2 h3 h4 = let hcut = intensional_event_rect_Type4 h1 h2 h3 h4 hterm in hcut __ (** val intensional_event_inv_rect_Type3 : intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **) let intensional_event_inv_rect_Type3 hterm h1 h2 h3 h4 = let hcut = intensional_event_rect_Type3 h1 h2 h3 h4 hterm in hcut __ (** val intensional_event_inv_rect_Type2 : intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **) let intensional_event_inv_rect_Type2 hterm h1 h2 h3 h4 = let hcut = intensional_event_rect_Type2 h1 h2 h3 h4 hterm in hcut __ (** val intensional_event_inv_rect_Type1 : intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **) let intensional_event_inv_rect_Type1 hterm h1 h2 h3 h4 = let hcut = intensional_event_rect_Type1 h1 h2 h3 h4 hterm in hcut __ (** val intensional_event_inv_rect_Type0 : intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **) let intensional_event_inv_rect_Type0 hterm h1 h2 h3 h4 = let hcut = intensional_event_rect_Type0 h1 h2 h3 h4 hterm in hcut __ (** val intensional_event_discr : intensional_event -> intensional_event -> __ **) let intensional_event_discr x y = Logic.eq_rect_Type2 x (match x with | IEVcost a0 -> Obj.magic (fun _ dH -> dH __) | IEVcall a0 -> Obj.magic (fun _ dH -> dH __) | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __) | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y (** val intensional_event_jmdiscr : intensional_event -> intensional_event -> __ **) let intensional_event_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | IEVcost a0 -> Obj.magic (fun _ dH -> dH __) | IEVcall a0 -> Obj.magic (fun _ dH -> dH __) | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __) | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y 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 **) let cons_safe x l = List.Cons ((Types.pi1 x), (Types.pi1 l)) (** val append_safe : 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 **) let append_safe l1 l2 = List.append (Types.pi1 l1) (Types.pi1 l2) (** val nil_safe : 'a1 List.list Types.sig0 **) let nil_safe = List.Nil (** val emittable_cost : abstract_status -> as_cost_label -> intensional_event Types.sig0 **) let emittable_cost s l = IEVcost (Types.pi1 l) (** val observables_trace_label_label : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label -> AST.ident -> as_trace **) let rec observables_trace_label_label s trace_ends_flag start_status final_status the_trace curr = let Tll_base (ends_flag, initial, final, given_trace) = the_trace in let label = as_label_safe s initial in cons_safe (emittable_cost s label) (observables_trace_any_label s ends_flag initial final given_trace curr) (** val observables_trace_any_label : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> AST.ident -> as_trace **) and observables_trace_any_label s trace_ends_flag start_status final_status the_trace curr = match the_trace with | Tal_base_not_return (the_status, x) -> nil_safe | Tal_base_return (the_status, x) -> cons_safe (IEVret curr) nil_safe | Tal_base_call (pre_fun_call, start_fun_call, final, call_trace) -> let id = s.as_call_ident pre_fun_call in cons_safe (IEVcall id) (observables_trace_label_return s start_fun_call final call_trace id) | Tal_base_tailcall (pre_fun_call, start_fun_call, final, call_trace) -> let id = s.as_tailcall_ident pre_fun_call in cons_safe (IEVtailcall (curr, id)) (observables_trace_label_return s start_fun_call final call_trace id) | Tal_step_call (end_flag, pre_fun_call, start_fun_call, after_fun_call, final, call_trace, final_trace) -> let id = s.as_call_ident pre_fun_call in let call_cost_trace = observables_trace_label_return s start_fun_call after_fun_call call_trace id in let final_cost_trace = observables_trace_any_label s end_flag after_fun_call final final_trace curr in append_safe (cons_safe (IEVcall id) call_cost_trace) final_cost_trace | Tal_step_default (end_flag, status_pre, status_init, status_end, tail_trace) -> observables_trace_any_label s end_flag status_init status_end tail_trace curr (** val observables_trace_label_return : abstract_status -> __ -> __ -> trace_label_return -> AST.ident -> as_trace **) and observables_trace_label_return s start_status final_status the_trace curr = match the_trace with | Tlr_base (before, after, trace_to_lift) -> observables_trace_label_label s Ends_with_ret before after trace_to_lift curr | Tlr_step (initial, labelled, final, labelled_trace, ret_trace) -> let labelled_cost = observables_trace_label_label s Doesnt_end_with_ret initial labelled labelled_trace curr in let return_cost = observables_trace_label_return s labelled final ret_trace curr in append_safe labelled_cost return_cost (** val filter_map : ('a1 -> 'a2 Types.option) -> 'a1 List.list -> 'a2 List.list **) let rec filter_map f = function | List.Nil -> List.Nil | List.Cons (hd, tl) -> List.append (match f hd with | Types.None -> List.Nil | Types.Some y -> List.Cons (y, List.Nil)) (filter_map f tl) (** val list_distribute_sig_aux : 'a1 List.list -> 'a1 Types.sig0 List.list **) let rec list_distribute_sig_aux l = (match l with | List.Nil -> (fun _ -> List.Nil) | List.Cons (hd, tl) -> (fun _ -> List.Cons (hd, (list_distribute_sig_aux tl)))) __ (** val list_distribute_sig : 'a1 List.list Types.sig0 -> 'a1 Types.sig0 List.list **) let list_distribute_sig l = list_distribute_sig_aux (Types.pi1 l) (** val list_factor_sig : 'a1 Types.sig0 List.list -> 'a1 List.list Types.sig0 **) let rec list_factor_sig = function | List.Nil -> nil_safe | List.Cons (hd, tl) -> cons_safe hd (list_factor_sig tl) (** val costlabels_of_observables : abstract_status -> as_trace -> as_cost_label List.list **) let costlabels_of_observables s l = filter_map (fun ev -> (match Types.pi1 ev with | IEVcost c -> (fun _ -> Types.Some c) | IEVcall x -> (fun _ -> Types.None) | IEVtailcall (x, x0) -> (fun _ -> Types.None) | IEVret x -> (fun _ -> Types.None)) __) (list_distribute_sig l) (** val flatten_trace_label_return : abstract_status -> __ -> __ -> trace_label_return -> as_cost_label List.list **) let flatten_trace_label_return s st1 st2 tlr = let dummy = Positive.One in costlabels_of_observables s (observables_trace_label_return s st1 st2 tlr dummy) (** val flatten_trace_label_label : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label -> as_cost_label List.list **) let flatten_trace_label_label s flag st1 st2 tll = let dummy = Positive.One in costlabels_of_observables s (observables_trace_label_label s flag st1 st2 tll dummy) (** val flatten_trace_any_label : abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> as_cost_label List.list **) let flatten_trace_any_label s flag st1 st2 tll = let dummy = Positive.One in costlabels_of_observables s (observables_trace_any_label s flag st1 st2 tll dummy) 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 **) let rec trace_any_any_free_rect_Type4 s h_taaf_base h_taaf_step h_taaf_step_jump x_23284 x_23283 = function | Taaf_base s0 -> h_taaf_base s0 | Taaf_step (s1, s2, s3, x_23288) -> h_taaf_step s1 s2 s3 x_23288 __ __ | Taaf_step_jump (s1, s2, s3, x_23292) -> h_taaf_step_jump s1 s2 s3 x_23292 __ __ __ (** val trace_any_any_free_rect_Type5 : abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **) let rec trace_any_any_free_rect_Type5 s h_taaf_base h_taaf_step h_taaf_step_jump x_23297 x_23296 = function | Taaf_base s0 -> h_taaf_base s0 | Taaf_step (s1, s2, s3, x_23301) -> h_taaf_step s1 s2 s3 x_23301 __ __ | Taaf_step_jump (s1, s2, s3, x_23305) -> h_taaf_step_jump s1 s2 s3 x_23305 __ __ __ (** val trace_any_any_free_rect_Type3 : abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **) let rec trace_any_any_free_rect_Type3 s h_taaf_base h_taaf_step h_taaf_step_jump x_23310 x_23309 = function | Taaf_base s0 -> h_taaf_base s0 | Taaf_step (s1, s2, s3, x_23314) -> h_taaf_step s1 s2 s3 x_23314 __ __ | Taaf_step_jump (s1, s2, s3, x_23318) -> h_taaf_step_jump s1 s2 s3 x_23318 __ __ __ (** val trace_any_any_free_rect_Type2 : abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **) let rec trace_any_any_free_rect_Type2 s h_taaf_base h_taaf_step h_taaf_step_jump x_23323 x_23322 = function | Taaf_base s0 -> h_taaf_base s0 | Taaf_step (s1, s2, s3, x_23327) -> h_taaf_step s1 s2 s3 x_23327 __ __ | Taaf_step_jump (s1, s2, s3, x_23331) -> h_taaf_step_jump s1 s2 s3 x_23331 __ __ __ (** val trace_any_any_free_rect_Type1 : abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **) let rec trace_any_any_free_rect_Type1 s h_taaf_base h_taaf_step h_taaf_step_jump x_23336 x_23335 = function | Taaf_base s0 -> h_taaf_base s0 | Taaf_step (s1, s2, s3, x_23340) -> h_taaf_step s1 s2 s3 x_23340 __ __ | Taaf_step_jump (s1, s2, s3, x_23344) -> h_taaf_step_jump s1 s2 s3 x_23344 __ __ __ (** val trace_any_any_free_rect_Type0 : abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **) let rec trace_any_any_free_rect_Type0 s h_taaf_base h_taaf_step h_taaf_step_jump x_23349 x_23348 = function | Taaf_base s0 -> h_taaf_base s0 | Taaf_step (s1, s2, s3, x_23353) -> h_taaf_step s1 s2 s3 x_23353 __ __ | Taaf_step_jump (s1, s2, s3, x_23357) -> h_taaf_step_jump s1 s2 s3 x_23357 __ __ __ (** val trace_any_any_free_inv_rect_Type4 : abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_free_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_any_free_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_free_inv_rect_Type3 : abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_free_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_any_free_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_free_inv_rect_Type2 : abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_free_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_any_free_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_free_inv_rect_Type1 : abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_free_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_any_free_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_free_inv_rect_Type0 : abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let trace_any_any_free_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 = let hcut = trace_any_any_free_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in hcut __ __ __ (** val trace_any_any_free_jmdiscr : abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free -> __ **) let trace_any_any_free_jmdiscr a1 a2 a3 x y = Logic.eq_rect_Type2 x (match x with | Taaf_base a0 -> Obj.magic (fun _ dH -> dH __) | Taaf_step (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __) | Taaf_step_jump (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y (** val taaf_non_empty : abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool **) let taaf_non_empty s s1 s2 = function | Taaf_base x -> Bool.False | Taaf_step (x, x0, x1, x2) -> Bool.True | Taaf_step_jump (x, x0, x1, x2) -> Bool.True (** val taa_append_taa : abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any -> trace_any_any **) let rec taa_append_taa s st1 st2 st3 taa = (match taa with | Taa_base st1' -> (fun st30 taa2 -> taa2) | Taa_step (st1', st2', st3', tl) -> (fun st30 taa2 -> Taa_step (st1', st2', st30, (taa_append_taa s st2' st3' st30 tl taa2)))) st3 (** val taaf_to_taa : abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any **) let taaf_to_taa s s1 s2 taaf = (match taaf with | Taaf_base s0 -> (fun _ -> Taa_base s0) | Taaf_step (s10, s20, s3, taa) -> (fun _ -> taa_append_taa s s10 s20 s3 taa (Taa_step (s20, s3, s3, (Taa_base s3)))) | Taaf_step_jump (s10, s20, s3, taa) -> (fun _ -> assert false (* absurd case *))) __ (** val taaf_append_tal : abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any_free -> trace_any_label -> trace_any_label **) let taaf_append_tal s st1 fl st2 st3 taaf = taa_append_tal s st1 fl st2 st3 (taaf_to_taa s st1 st2 taaf) (** val taaf_append_taa : abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any -> trace_any_any **) let taaf_append_taa s st1 st2 st3 taaf = taa_append_taa s st1 st2 st3 (taaf_to_taa s st1 st2 taaf) (** val taaf_cons : abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any_free **) let taaf_cons s s1 s2 s3 tl = (match tl with | Taaf_base s20 -> (fun _ _ -> Taaf_step (s1, s1, s20, (Taa_base s1))) | Taaf_step (s20, s30, s4, taa) -> (fun _ _ -> Taaf_step (s1, s30, s4, (Taa_step (s1, s20, s30, taa)))) | Taaf_step_jump (s20, s30, s4, taa) -> (fun _ _ -> Taaf_step_jump (s1, s30, s4, (Taa_step (s1, s20, s30, taa))))) __ __ (** val taaf_append_taaf : abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any_free -> trace_any_any_free **) let taaf_append_taaf s st1 st2 st3 taaf1 taaf2 = (match taaf2 with | Taaf_base s1 -> (fun taaf10 _ -> taaf10) | Taaf_step (s1, s2, s3, taa) -> (fun taaf10 _ -> Taaf_step (st1, s2, s3, (taaf_append_taa s st1 s1 s2 taaf10 taa))) | Taaf_step_jump (s2, s3, s4, taa) -> (fun taaf10 _ -> Taaf_step_jump (st1, s3, s4, (taaf_append_taa s st1 s2 s3 taaf10 taa)))) taaf1 __