open Preamble open Hints_declaration open Core_notation open Pts open Logic open Proper open PositiveMap open Deqsets open ErrorMessages open PreIdentifiers open Errors open Extralib open Lists open Positive open Identifiers open Exp open Arithmetic open Vector open Div_and_mod open Util open FoldStuff open BitVector open Jmeq open Russell open List open Setoids open Monad open Option open Extranat open Bool open Relations open Nat open Integers open Types open AST open CostLabel open FrontEndVal open Hide open ByteValues open GenMem open FrontEndMem open Division open Z open BitVectorZ open Pointers open Coqlib open Values open FrontEndOps open Order open Registers open BitVectorTrie open Graphs type statement = | St_skip of Graphs.label | St_cost of CostLabel.costlabel * Graphs.label | St_const of AST.typ * Registers.register * FrontEndOps.constant * Graphs.label | St_op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * Registers.register * Registers.register * Graphs.label | St_op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation * Registers.register * Registers.register * Registers.register * Graphs.label | St_load of AST.typ * Registers.register * Registers.register * Graphs.label | St_store of AST.typ * Registers.register * Registers.register * Graphs.label | St_call_id of AST.ident * Registers.register List.list * Registers.register Types.option * Graphs.label | St_call_ptr of Registers.register * Registers.register List.list * Registers.register Types.option * Graphs.label | St_cond of Registers.register * Graphs.label * Graphs.label | St_return (** val statement_rect_Type4 : (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **) let rec statement_rect_Type4 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function | St_skip x_14903 -> h_St_skip x_14903 | St_cost (x_14905, x_14904) -> h_St_cost x_14905 x_14904 | St_const (t, x_14908, x_14907, x_14906) -> h_St_const t x_14908 x_14907 x_14906 | St_op1 (t', t, x_14912, x_14911, x_14910, x_14909) -> h_St_op1 t' t x_14912 x_14911 x_14910 x_14909 | St_op2 (t', t1, t2, x_14917, x_14916, x_14915, x_14914, x_14913) -> h_St_op2 t' t1 t2 x_14917 x_14916 x_14915 x_14914 x_14913 | St_load (x_14921, x_14920, x_14919, x_14918) -> h_St_load x_14921 x_14920 x_14919 x_14918 | St_store (x_14925, x_14924, x_14923, x_14922) -> h_St_store x_14925 x_14924 x_14923 x_14922 | St_call_id (x_14929, x_14928, x_14927, x_14926) -> h_St_call_id x_14929 x_14928 x_14927 x_14926 | St_call_ptr (x_14933, x_14932, x_14931, x_14930) -> h_St_call_ptr x_14933 x_14932 x_14931 x_14930 | St_cond (x_14936, x_14935, x_14934) -> h_St_cond x_14936 x_14935 x_14934 | St_return -> h_St_return (** val statement_rect_Type5 : (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **) let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function | St_skip x_14949 -> h_St_skip x_14949 | St_cost (x_14951, x_14950) -> h_St_cost x_14951 x_14950 | St_const (t, x_14954, x_14953, x_14952) -> h_St_const t x_14954 x_14953 x_14952 | St_op1 (t', t, x_14958, x_14957, x_14956, x_14955) -> h_St_op1 t' t x_14958 x_14957 x_14956 x_14955 | St_op2 (t', t1, t2, x_14963, x_14962, x_14961, x_14960, x_14959) -> h_St_op2 t' t1 t2 x_14963 x_14962 x_14961 x_14960 x_14959 | St_load (x_14967, x_14966, x_14965, x_14964) -> h_St_load x_14967 x_14966 x_14965 x_14964 | St_store (x_14971, x_14970, x_14969, x_14968) -> h_St_store x_14971 x_14970 x_14969 x_14968 | St_call_id (x_14975, x_14974, x_14973, x_14972) -> h_St_call_id x_14975 x_14974 x_14973 x_14972 | St_call_ptr (x_14979, x_14978, x_14977, x_14976) -> h_St_call_ptr x_14979 x_14978 x_14977 x_14976 | St_cond (x_14982, x_14981, x_14980) -> h_St_cond x_14982 x_14981 x_14980 | St_return -> h_St_return (** val statement_rect_Type3 : (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **) let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function | St_skip x_14995 -> h_St_skip x_14995 | St_cost (x_14997, x_14996) -> h_St_cost x_14997 x_14996 | St_const (t, x_15000, x_14999, x_14998) -> h_St_const t x_15000 x_14999 x_14998 | St_op1 (t', t, x_15004, x_15003, x_15002, x_15001) -> h_St_op1 t' t x_15004 x_15003 x_15002 x_15001 | St_op2 (t', t1, t2, x_15009, x_15008, x_15007, x_15006, x_15005) -> h_St_op2 t' t1 t2 x_15009 x_15008 x_15007 x_15006 x_15005 | St_load (x_15013, x_15012, x_15011, x_15010) -> h_St_load x_15013 x_15012 x_15011 x_15010 | St_store (x_15017, x_15016, x_15015, x_15014) -> h_St_store x_15017 x_15016 x_15015 x_15014 | St_call_id (x_15021, x_15020, x_15019, x_15018) -> h_St_call_id x_15021 x_15020 x_15019 x_15018 | St_call_ptr (x_15025, x_15024, x_15023, x_15022) -> h_St_call_ptr x_15025 x_15024 x_15023 x_15022 | St_cond (x_15028, x_15027, x_15026) -> h_St_cond x_15028 x_15027 x_15026 | St_return -> h_St_return (** val statement_rect_Type2 : (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **) let rec statement_rect_Type2 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function | St_skip x_15041 -> h_St_skip x_15041 | St_cost (x_15043, x_15042) -> h_St_cost x_15043 x_15042 | St_const (t, x_15046, x_15045, x_15044) -> h_St_const t x_15046 x_15045 x_15044 | St_op1 (t', t, x_15050, x_15049, x_15048, x_15047) -> h_St_op1 t' t x_15050 x_15049 x_15048 x_15047 | St_op2 (t', t1, t2, x_15055, x_15054, x_15053, x_15052, x_15051) -> h_St_op2 t' t1 t2 x_15055 x_15054 x_15053 x_15052 x_15051 | St_load (x_15059, x_15058, x_15057, x_15056) -> h_St_load x_15059 x_15058 x_15057 x_15056 | St_store (x_15063, x_15062, x_15061, x_15060) -> h_St_store x_15063 x_15062 x_15061 x_15060 | St_call_id (x_15067, x_15066, x_15065, x_15064) -> h_St_call_id x_15067 x_15066 x_15065 x_15064 | St_call_ptr (x_15071, x_15070, x_15069, x_15068) -> h_St_call_ptr x_15071 x_15070 x_15069 x_15068 | St_cond (x_15074, x_15073, x_15072) -> h_St_cond x_15074 x_15073 x_15072 | St_return -> h_St_return (** val statement_rect_Type1 : (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **) let rec statement_rect_Type1 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function | St_skip x_15087 -> h_St_skip x_15087 | St_cost (x_15089, x_15088) -> h_St_cost x_15089 x_15088 | St_const (t, x_15092, x_15091, x_15090) -> h_St_const t x_15092 x_15091 x_15090 | St_op1 (t', t, x_15096, x_15095, x_15094, x_15093) -> h_St_op1 t' t x_15096 x_15095 x_15094 x_15093 | St_op2 (t', t1, t2, x_15101, x_15100, x_15099, x_15098, x_15097) -> h_St_op2 t' t1 t2 x_15101 x_15100 x_15099 x_15098 x_15097 | St_load (x_15105, x_15104, x_15103, x_15102) -> h_St_load x_15105 x_15104 x_15103 x_15102 | St_store (x_15109, x_15108, x_15107, x_15106) -> h_St_store x_15109 x_15108 x_15107 x_15106 | St_call_id (x_15113, x_15112, x_15111, x_15110) -> h_St_call_id x_15113 x_15112 x_15111 x_15110 | St_call_ptr (x_15117, x_15116, x_15115, x_15114) -> h_St_call_ptr x_15117 x_15116 x_15115 x_15114 | St_cond (x_15120, x_15119, x_15118) -> h_St_cond x_15120 x_15119 x_15118 | St_return -> h_St_return (** val statement_rect_Type0 : (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **) let rec statement_rect_Type0 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function | St_skip x_15133 -> h_St_skip x_15133 | St_cost (x_15135, x_15134) -> h_St_cost x_15135 x_15134 | St_const (t, x_15138, x_15137, x_15136) -> h_St_const t x_15138 x_15137 x_15136 | St_op1 (t', t, x_15142, x_15141, x_15140, x_15139) -> h_St_op1 t' t x_15142 x_15141 x_15140 x_15139 | St_op2 (t', t1, t2, x_15147, x_15146, x_15145, x_15144, x_15143) -> h_St_op2 t' t1 t2 x_15147 x_15146 x_15145 x_15144 x_15143 | St_load (x_15151, x_15150, x_15149, x_15148) -> h_St_load x_15151 x_15150 x_15149 x_15148 | St_store (x_15155, x_15154, x_15153, x_15152) -> h_St_store x_15155 x_15154 x_15153 x_15152 | St_call_id (x_15159, x_15158, x_15157, x_15156) -> h_St_call_id x_15159 x_15158 x_15157 x_15156 | St_call_ptr (x_15163, x_15162, x_15161, x_15160) -> h_St_call_ptr x_15163 x_15162 x_15161 x_15160 | St_cond (x_15166, x_15165, x_15164) -> h_St_cond x_15166 x_15165 x_15164 | St_return -> h_St_return (** val statement_inv_rect_Type4 : statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 = let hcut = statement_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in hcut __ (** val statement_inv_rect_Type3 : statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 = let hcut = statement_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in hcut __ (** val statement_inv_rect_Type2 : statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 = let hcut = statement_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in hcut __ (** val statement_inv_rect_Type1 : statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 = let hcut = statement_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in hcut __ (** val statement_inv_rect_Type0 : statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation -> Registers.register -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Registers.register List.list -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 = let hcut = statement_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in hcut __ (** val statement_jmdiscr : statement -> statement -> __ **) let statement_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | St_skip a0 -> Obj.magic (fun _ dH -> dH __) | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __) | St_const (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __) | St_op1 (a0, a1, a2, a3, a4, a5) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __) | St_op2 (a0, a1, a2, a3, a4, a5, a6, a7) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __) | St_load (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __) | St_store (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __) | St_call_id (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __) | St_call_ptr (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __) | St_cond (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __) | St_return -> Obj.magic (fun _ dH -> dH)) y type internal_function = { f_labgen : Identifiers.universe; f_reggen : Identifiers.universe; f_result : (Registers.register, AST.typ) Types.prod Types.option; f_params : (Registers.register, AST.typ) Types.prod List.list; f_locals : (Registers.register, AST.typ) Types.prod List.list; f_stacksize : Nat.nat; f_graph : statement Graphs.graph; f_entry : Graphs.label Types.sig0; f_exit : Graphs.label Types.sig0 } (** val internal_function_rect_Type4 : (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1 **) let rec internal_function_rect_Type4 h_mk_internal_function x_15456 = let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0; f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0; f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15456 in h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __ (** val internal_function_rect_Type5 : (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1 **) let rec internal_function_rect_Type5 h_mk_internal_function x_15458 = let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0; f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0; f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15458 in h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __ (** val internal_function_rect_Type3 : (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1 **) let rec internal_function_rect_Type3 h_mk_internal_function x_15460 = let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0; f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0; f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15460 in h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __ (** val internal_function_rect_Type2 : (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1 **) let rec internal_function_rect_Type2 h_mk_internal_function x_15462 = let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0; f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0; f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15462 in h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __ (** val internal_function_rect_Type1 : (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1 **) let rec internal_function_rect_Type1 h_mk_internal_function x_15464 = let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0; f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0; f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15464 in h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __ (** val internal_function_rect_Type0 : (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> internal_function -> 'a1 **) let rec internal_function_rect_Type0 h_mk_internal_function x_15466 = let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0; f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0; f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15466 in h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0 f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __ (** val f_labgen : internal_function -> Identifiers.universe **) let rec f_labgen xxx = xxx.f_labgen (** val f_reggen : internal_function -> Identifiers.universe **) let rec f_reggen xxx = xxx.f_reggen (** val f_result : internal_function -> (Registers.register, AST.typ) Types.prod Types.option **) let rec f_result xxx = xxx.f_result (** val f_params : internal_function -> (Registers.register, AST.typ) Types.prod List.list **) let rec f_params xxx = xxx.f_params (** val f_locals : internal_function -> (Registers.register, AST.typ) Types.prod List.list **) let rec f_locals xxx = xxx.f_locals (** val f_stacksize : internal_function -> Nat.nat **) let rec f_stacksize xxx = xxx.f_stacksize (** val f_graph : internal_function -> statement Graphs.graph **) let rec f_graph xxx = xxx.f_graph (** val f_entry : internal_function -> Graphs.label Types.sig0 **) let rec f_entry xxx = xxx.f_entry (** val f_exit : internal_function -> Graphs.label Types.sig0 **) let rec f_exit xxx = xxx.f_exit (** val internal_function_inv_rect_Type4 : internal_function -> (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **) let internal_function_inv_rect_Type4 hterm h1 = let hcut = internal_function_rect_Type4 h1 hterm in hcut __ (** val internal_function_inv_rect_Type3 : internal_function -> (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **) let internal_function_inv_rect_Type3 hterm h1 = let hcut = internal_function_rect_Type3 h1 hterm in hcut __ (** val internal_function_inv_rect_Type2 : internal_function -> (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **) let internal_function_inv_rect_Type2 hterm h1 = let hcut = internal_function_rect_Type2 h1 hterm in hcut __ (** val internal_function_inv_rect_Type1 : internal_function -> (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **) let internal_function_inv_rect_Type1 hterm h1 = let hcut = internal_function_rect_Type1 h1 hterm in hcut __ (** val internal_function_inv_rect_Type0 : internal_function -> (Identifiers.universe -> Identifiers.universe -> (Registers.register, AST.typ) Types.prod Types.option -> (Registers.register, AST.typ) Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **) let internal_function_inv_rect_Type0 hterm h1 = let hcut = internal_function_rect_Type0 h1 hterm in hcut __ (** val internal_function_jmdiscr : internal_function -> internal_function -> __ **) let internal_function_jmdiscr x y = Logic.eq_rect_Type2 x (let { f_labgen = a0; f_reggen = a1; f_result = a2; f_params = a3; f_locals = a4; f_stacksize = a5; f_graph = a6; f_entry = a9; f_exit = a10 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y type rTLabs_program = (internal_function AST.fundef, AST.init_data List.list) AST.program