open Preamble

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

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 ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Coqlib

open Values

open FrontEndOps

open CostLabel

type expr =
| Id of AST.typ * AST.ident
| Cst of AST.typ * FrontEndOps.constant
| Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
| Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation * 
   expr * expr
| Mem of AST.typ * expr
| Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
| Ecost of AST.typ * CostLabel.costlabel * expr

(** val expr_rect_Type4 :
    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    -> 'a1) -> AST.typ -> expr -> 'a1 **)
let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13742 = function
| Id (t, x_13744) -> h_Id t x_13744
| Cst (t, x_13745) -> h_Cst t x_13745
| Op1 (t, t', x_13747, x_13746) ->
  h_Op1 t t' x_13747 x_13746
    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13746)
| Op2 (t1, t2, t', x_13750, x_13749, x_13748) ->
  h_Op2 t1 t2 t' x_13750 x_13749 x_13748
    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13749)
    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13748)
| Mem (t, x_13751) ->
  h_Mem t x_13751
    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
      x_13751)
| Cond (sz, sg, t, x_13754, x_13753, x_13752) ->
  h_Cond sz sg t x_13754 x_13753 x_13752
    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
      (sz, sg)) x_13754)
    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13753)
    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13752)
| Ecost (t, x_13756, x_13755) ->
  h_Ecost t x_13756 x_13755
    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13755)

(** val expr_rect_Type3 :
    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    -> 'a1) -> AST.typ -> expr -> 'a1 **)
let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13786 = function
| Id (t, x_13788) -> h_Id t x_13788
| Cst (t, x_13789) -> h_Cst t x_13789
| Op1 (t, t', x_13791, x_13790) ->
  h_Op1 t t' x_13791 x_13790
    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13790)
| Op2 (t1, t2, t', x_13794, x_13793, x_13792) ->
  h_Op2 t1 t2 t' x_13794 x_13793 x_13792
    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13793)
    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13792)
| Mem (t, x_13795) ->
  h_Mem t x_13795
    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
      x_13795)
| Cond (sz, sg, t, x_13798, x_13797, x_13796) ->
  h_Cond sz sg t x_13798 x_13797 x_13796
    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
      (sz, sg)) x_13798)
    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13797)
    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13796)
| Ecost (t, x_13800, x_13799) ->
  h_Ecost t x_13800 x_13799
    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13799)

(** val expr_rect_Type2 :
    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    -> 'a1) -> AST.typ -> expr -> 'a1 **)
let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13808 = function
| Id (t, x_13810) -> h_Id t x_13810
| Cst (t, x_13811) -> h_Cst t x_13811
| Op1 (t, t', x_13813, x_13812) ->
  h_Op1 t t' x_13813 x_13812
    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13812)
| Op2 (t1, t2, t', x_13816, x_13815, x_13814) ->
  h_Op2 t1 t2 t' x_13816 x_13815 x_13814
    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13815)
    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13814)
| Mem (t, x_13817) ->
  h_Mem t x_13817
    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
      x_13817)
| Cond (sz, sg, t, x_13820, x_13819, x_13818) ->
  h_Cond sz sg t x_13820 x_13819 x_13818
    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
      (sz, sg)) x_13820)
    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13819)
    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13818)
| Ecost (t, x_13822, x_13821) ->
  h_Ecost t x_13822 x_13821
    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13821)

(** val expr_rect_Type1 :
    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    -> 'a1) -> AST.typ -> expr -> 'a1 **)
let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13830 = function
| Id (t, x_13832) -> h_Id t x_13832
| Cst (t, x_13833) -> h_Cst t x_13833
| Op1 (t, t', x_13835, x_13834) ->
  h_Op1 t t' x_13835 x_13834
    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13834)
| Op2 (t1, t2, t', x_13838, x_13837, x_13836) ->
  h_Op2 t1 t2 t' x_13838 x_13837 x_13836
    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13837)
    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13836)
| Mem (t, x_13839) ->
  h_Mem t x_13839
    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
      x_13839)
| Cond (sz, sg, t, x_13842, x_13841, x_13840) ->
  h_Cond sz sg t x_13842 x_13841 x_13840
    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
      (sz, sg)) x_13842)
    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13841)
    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13840)
| Ecost (t, x_13844, x_13843) ->
  h_Ecost t x_13844 x_13843
    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13843)

(** val expr_rect_Type0 :
    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    -> 'a1) -> AST.typ -> expr -> 'a1 **)
let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13852 = function
| Id (t, x_13854) -> h_Id t x_13854
| Cst (t, x_13855) -> h_Cst t x_13855
| Op1 (t, t', x_13857, x_13856) ->
  h_Op1 t t' x_13857 x_13856
    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13856)
| Op2 (t1, t2, t', x_13860, x_13859, x_13858) ->
  h_Op2 t1 t2 t' x_13860 x_13859 x_13858
    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13859)
    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13858)
| Mem (t, x_13861) ->
  h_Mem t x_13861
    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
      x_13861)
| Cond (sz, sg, t, x_13864, x_13863, x_13862) ->
  h_Cond sz sg t x_13864 x_13863 x_13862
    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
      (sz, sg)) x_13864)
    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13863)
    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13862)
| Ecost (t, x_13866, x_13865) ->
  h_Ecost t x_13866 x_13865
    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13865)

(** val expr_inv_rect_Type4 :
    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
    __ -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type4 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = expr_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __

(** val expr_inv_rect_Type3 :
    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
    __ -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type3 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = expr_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __

(** val expr_inv_rect_Type2 :
    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
    __ -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type2 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = expr_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __

(** val expr_inv_rect_Type1 :
    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
    __ -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type1 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = expr_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __

(** val expr_inv_rect_Type0 :
    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
    __ -> __ -> 'a1) -> 'a1 **)
let expr_inv_rect_Type0 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = expr_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __

(** val expr_jmdiscr : AST.typ -> expr -> expr -> __ **)
let expr_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Id (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Cst (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Op1 (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Op2 (a0, a10, a2, a3, a4, a5) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
     | Mem (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Cond (a0, a10, a2, a3, a4, a5) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
     | Ecost (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y

type stmt =
| St_skip
| St_assign of AST.typ * AST.ident * expr
| St_store of AST.typ * expr * expr
| St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
   * (AST.typ, expr) Types.dPair List.list
| St_seq of stmt * stmt
| St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
| St_return of (AST.typ, expr) Types.dPair Types.option
| St_label of PreIdentifiers.identifier * stmt
| St_goto of PreIdentifiers.identifier
| St_cost of CostLabel.costlabel * stmt

(** val stmt_rect_Type4 :
    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
    -> 'a1) -> stmt -> 'a1 **)
let rec stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
| St_skip -> h_St_skip
| St_assign (t, x_14037, x_14036) -> h_St_assign t x_14037 x_14036
| St_store (t, x_14039, x_14038) -> h_St_store t x_14039 x_14038
| St_call (x_14042, x_14041, x_14040) -> h_St_call x_14042 x_14041 x_14040
| St_seq (x_14044, x_14043) ->
  h_St_seq x_14044 x_14043
    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14044)
    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14043)
| St_ifthenelse (sz, sg, x_14047, x_14046, x_14045) ->
  h_St_ifthenelse sz sg x_14047 x_14046 x_14045
    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14046)
    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14045)
| St_return x_14048 -> h_St_return x_14048
| St_label (x_14050, x_14049) ->
  h_St_label x_14050 x_14049
    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14049)
| St_goto x_14051 -> h_St_goto x_14051
| St_cost (x_14053, x_14052) ->
  h_St_cost x_14053 x_14052
    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14052)

(** val stmt_rect_Type3 :
    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
    -> 'a1) -> stmt -> 'a1 **)
let rec stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
| St_skip -> h_St_skip
| St_assign (t, x_14095, x_14094) -> h_St_assign t x_14095 x_14094
| St_store (t, x_14097, x_14096) -> h_St_store t x_14097 x_14096
| St_call (x_14100, x_14099, x_14098) -> h_St_call x_14100 x_14099 x_14098
| St_seq (x_14102, x_14101) ->
  h_St_seq x_14102 x_14101
    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14102)
    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14101)
| St_ifthenelse (sz, sg, x_14105, x_14104, x_14103) ->
  h_St_ifthenelse sz sg x_14105 x_14104 x_14103
    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14104)
    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14103)
| St_return x_14106 -> h_St_return x_14106
| St_label (x_14108, x_14107) ->
  h_St_label x_14108 x_14107
    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14107)
| St_goto x_14109 -> h_St_goto x_14109
| St_cost (x_14111, x_14110) ->
  h_St_cost x_14111 x_14110
    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14110)

(** val stmt_rect_Type2 :
    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
    -> 'a1) -> stmt -> 'a1 **)
let rec stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
| St_skip -> h_St_skip
| St_assign (t, x_14124, x_14123) -> h_St_assign t x_14124 x_14123
| St_store (t, x_14126, x_14125) -> h_St_store t x_14126 x_14125
| St_call (x_14129, x_14128, x_14127) -> h_St_call x_14129 x_14128 x_14127
| St_seq (x_14131, x_14130) ->
  h_St_seq x_14131 x_14130
    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14131)
    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14130)
| St_ifthenelse (sz, sg, x_14134, x_14133, x_14132) ->
  h_St_ifthenelse sz sg x_14134 x_14133 x_14132
    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14133)
    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14132)
| St_return x_14135 -> h_St_return x_14135
| St_label (x_14137, x_14136) ->
  h_St_label x_14137 x_14136
    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14136)
| St_goto x_14138 -> h_St_goto x_14138
| St_cost (x_14140, x_14139) ->
  h_St_cost x_14140 x_14139
    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14139)

(** val stmt_rect_Type1 :
    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
    -> 'a1) -> stmt -> 'a1 **)
let rec stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
| St_skip -> h_St_skip
| St_assign (t, x_14153, x_14152) -> h_St_assign t x_14153 x_14152
| St_store (t, x_14155, x_14154) -> h_St_store t x_14155 x_14154
| St_call (x_14158, x_14157, x_14156) -> h_St_call x_14158 x_14157 x_14156
| St_seq (x_14160, x_14159) ->
  h_St_seq x_14160 x_14159
    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14160)
    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14159)
| St_ifthenelse (sz, sg, x_14163, x_14162, x_14161) ->
  h_St_ifthenelse sz sg x_14163 x_14162 x_14161
    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14162)
    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14161)
| St_return x_14164 -> h_St_return x_14164
| St_label (x_14166, x_14165) ->
  h_St_label x_14166 x_14165
    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14165)
| St_goto x_14167 -> h_St_goto x_14167
| St_cost (x_14169, x_14168) ->
  h_St_cost x_14169 x_14168
    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14168)

(** val stmt_rect_Type0 :
    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
    -> 'a1) -> stmt -> 'a1 **)
let rec stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
| St_skip -> h_St_skip
| St_assign (t, x_14182, x_14181) -> h_St_assign t x_14182 x_14181
| St_store (t, x_14184, x_14183) -> h_St_store t x_14184 x_14183
| St_call (x_14187, x_14186, x_14185) -> h_St_call x_14187 x_14186 x_14185
| St_seq (x_14189, x_14188) ->
  h_St_seq x_14189 x_14188
    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14189)
    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14188)
| St_ifthenelse (sz, sg, x_14192, x_14191, x_14190) ->
  h_St_ifthenelse sz sg x_14192 x_14191 x_14190
    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14191)
    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14190)
| St_return x_14193 -> h_St_return x_14193
| St_label (x_14195, x_14194) ->
  h_St_label x_14195 x_14194
    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14194)
| St_goto x_14196 -> h_St_goto x_14196
| St_cost (x_14198, x_14197) ->
  h_St_cost x_14198 x_14197
    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14197)

(** val stmt_inv_rect_Type4 :
    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stmt_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
  let hcut = stmt_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __

(** val stmt_inv_rect_Type3 :
    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stmt_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
  let hcut = stmt_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __

(** val stmt_inv_rect_Type2 :
    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stmt_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
  let hcut = stmt_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __

(** val stmt_inv_rect_Type1 :
    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stmt_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
  let hcut = stmt_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __

(** val stmt_inv_rect_Type0 :
    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let stmt_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
  let hcut = stmt_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __

(** val stmt_discr : stmt -> stmt -> __ **)
let stmt_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | St_skip -> Obj.magic (fun _ dH -> dH)
     | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | St_ifthenelse (a0, a1, a2, a3, a4) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __)
     | St_return a0 -> Obj.magic (fun _ dH -> dH __)
     | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val stmt_jmdiscr : stmt -> stmt -> __ **)
let stmt_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | St_skip -> Obj.magic (fun _ dH -> dH)
     | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | St_ifthenelse (a0, a1, a2, a3, a4) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __)
     | St_return a0 -> Obj.magic (fun _ dH -> dH __)
     | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val labels_of : stmt -> PreIdentifiers.identifier List.list **)
let rec labels_of = function
| St_skip -> List.Nil
| St_assign (x, x0, x1) -> List.Nil
| St_store (x, x0, x1) -> List.Nil
| St_call (x, x0, x1) -> List.Nil
| St_seq (s1, s2) -> List.append (labels_of s1) (labels_of s2)
| St_ifthenelse (x, x0, x1, s1, s2) ->
  List.append (labels_of s1) (labels_of s2)
| St_return x -> List.Nil
| St_label (l, s0) -> List.Cons (l, (labels_of s0))
| St_goto x -> List.Nil
| St_cost (x, s0) -> labels_of s0

(** val cminor_stmt_inv_rect_Type4 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let rec cminor_stmt_inv_rect_Type4 env labels rettyp s h_mk_cminor_stmt_inv =
  h_mk_cminor_stmt_inv __ __ __

(** val cminor_stmt_inv_rect_Type5 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let rec cminor_stmt_inv_rect_Type5 env labels rettyp s h_mk_cminor_stmt_inv =
  h_mk_cminor_stmt_inv __ __ __

(** val cminor_stmt_inv_rect_Type3 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let rec cminor_stmt_inv_rect_Type3 env labels rettyp s h_mk_cminor_stmt_inv =
  h_mk_cminor_stmt_inv __ __ __

(** val cminor_stmt_inv_rect_Type2 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let rec cminor_stmt_inv_rect_Type2 env labels rettyp s h_mk_cminor_stmt_inv =
  h_mk_cminor_stmt_inv __ __ __

(** val cminor_stmt_inv_rect_Type1 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let rec cminor_stmt_inv_rect_Type1 env labels rettyp s h_mk_cminor_stmt_inv =
  h_mk_cminor_stmt_inv __ __ __

(** val cminor_stmt_inv_rect_Type0 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
    'a1 **)
let rec cminor_stmt_inv_rect_Type0 env labels rettyp s h_mk_cminor_stmt_inv =
  h_mk_cminor_stmt_inv __ __ __

(** val cminor_stmt_inv_inv_rect_Type4 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let cminor_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
  let hcut = cminor_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __

(** val cminor_stmt_inv_inv_rect_Type3 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let cminor_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
  let hcut = cminor_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __

(** val cminor_stmt_inv_inv_rect_Type2 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let cminor_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
  let hcut = cminor_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __

(** val cminor_stmt_inv_inv_rect_Type1 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let cminor_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
  let hcut = cminor_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __

(** val cminor_stmt_inv_inv_rect_Type0 :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
    'a1) -> 'a1 **)
let cminor_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
  let hcut = cminor_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __

(** val cminor_stmt_inv_discr :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> __ **)
let cminor_stmt_inv_discr a1 a2 a3 a4 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val cminor_stmt_inv_jmdiscr :
    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
    List.list -> AST.typ Types.option -> stmt -> __ **)
let cminor_stmt_inv_jmdiscr a1 a2 a3 a4 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

type internal_function = { f_return : AST.typ Types.option;
                           f_params : (AST.ident, AST.typ) Types.prod
                                      List.list;
                           f_vars : (AST.ident, AST.typ) Types.prod List.list;
                           f_stacksize : Nat.nat; f_body : stmt }

(** val internal_function_rect_Type4 :
    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    -> 'a1) -> internal_function -> 'a1 **)
let rec internal_function_rect_Type4 h_mk_internal_function x_14493 =
  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14493
  in
  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
    __

(** val internal_function_rect_Type5 :
    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    -> 'a1) -> internal_function -> 'a1 **)
let rec internal_function_rect_Type5 h_mk_internal_function x_14495 =
  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14495
  in
  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
    __

(** val internal_function_rect_Type3 :
    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    -> 'a1) -> internal_function -> 'a1 **)
let rec internal_function_rect_Type3 h_mk_internal_function x_14497 =
  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14497
  in
  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
    __

(** val internal_function_rect_Type2 :
    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    -> 'a1) -> internal_function -> 'a1 **)
let rec internal_function_rect_Type2 h_mk_internal_function x_14499 =
  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14499
  in
  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
    __

(** val internal_function_rect_Type1 :
    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    -> 'a1) -> internal_function -> 'a1 **)
let rec internal_function_rect_Type1 h_mk_internal_function x_14501 =
  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14501
  in
  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
    __

(** val internal_function_rect_Type0 :
    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    -> 'a1) -> internal_function -> 'a1 **)
let rec internal_function_rect_Type0 h_mk_internal_function x_14503 =
  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14503
  in
  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
    __

(** val f_return : internal_function -> AST.typ Types.option **)
let rec f_return xxx =
  xxx.f_return

(** val f_params :
    internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
let rec f_params xxx =
  xxx.f_params

(** val f_vars :
    internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
let rec f_vars xxx =
  xxx.f_vars

(** val f_stacksize : internal_function -> Nat.nat **)
let rec f_stacksize xxx =
  xxx.f_stacksize

(** val f_body : internal_function -> stmt **)
let rec f_body xxx =
  xxx.f_body

(** val internal_function_inv_rect_Type4 :
    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
    -> Nat.nat -> stmt -> __ -> __ -> '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 -> (AST.typ Types.option -> (AST.ident, AST.typ)
    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
    -> Nat.nat -> stmt -> __ -> __ -> '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 -> (AST.typ Types.option -> (AST.ident, AST.typ)
    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
    -> Nat.nat -> stmt -> __ -> __ -> '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 -> (AST.typ Types.option -> (AST.ident, AST.typ)
    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
    -> Nat.nat -> stmt -> __ -> __ -> '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 -> (AST.typ Types.option -> (AST.ident, AST.typ)
    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
    -> Nat.nat -> stmt -> __ -> __ -> '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_return = a0; f_params = a1; f_vars = a2; f_stacksize = a4;
       f_body = a5 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y

type cminor_program =
  (internal_function AST.fundef, AST.init_data List.list) AST.program

type cminor_noinit_program =
  (internal_function AST.fundef, Nat.nat) AST.program