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

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

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

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

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

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

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

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

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

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

val expr_jmdiscr : AST.typ -> expr -> expr -> __

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

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

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

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

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

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

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

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

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

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

val stmt_discr : stmt -> stmt -> __

val stmt_jmdiscr : stmt -> stmt -> __

val labels_of : stmt -> PreIdentifiers.identifier List.list

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

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

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

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

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

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

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

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

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

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

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

val cminor_stmt_inv_discr :
  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
  List.list -> AST.typ Types.option -> stmt -> __

val cminor_stmt_inv_jmdiscr :
  (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
  List.list -> AST.typ Types.option -> stmt -> __

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

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

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

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

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

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

val f_return : internal_function -> AST.typ Types.option

val f_params : internal_function -> (AST.ident, AST.typ) Types.prod List.list

val f_vars : internal_function -> (AST.ident, AST.typ) Types.prod List.list

val f_stacksize : internal_function -> Nat.nat

val f_body : internal_function -> stmt

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

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

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

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

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

val internal_function_jmdiscr : internal_function -> internal_function -> __

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