open Preamble

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 FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

type constant =
| Ointconst of AST.intsize * AST.signedness * AST.bvint
| Oaddrsymbol of AST.ident * Nat.nat
| Oaddrstack of Nat.nat

(** val constant_rect_Type4 :
    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13118 = function
| Ointconst (sz, sg, x_13120) -> h_Ointconst sz sg x_13120
| Oaddrsymbol (x_13122, x_13121) -> h_Oaddrsymbol x_13122 x_13121
| Oaddrstack x_13123 -> h_Oaddrstack x_13123

(** val constant_rect_Type5 :
    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13127 = function
| Ointconst (sz, sg, x_13129) -> h_Ointconst sz sg x_13129
| Oaddrsymbol (x_13131, x_13130) -> h_Oaddrsymbol x_13131 x_13130
| Oaddrstack x_13132 -> h_Oaddrstack x_13132

(** val constant_rect_Type3 :
    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13136 = function
| Ointconst (sz, sg, x_13138) -> h_Ointconst sz sg x_13138
| Oaddrsymbol (x_13140, x_13139) -> h_Oaddrsymbol x_13140 x_13139
| Oaddrstack x_13141 -> h_Oaddrstack x_13141

(** val constant_rect_Type2 :
    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13145 = function
| Ointconst (sz, sg, x_13147) -> h_Ointconst sz sg x_13147
| Oaddrsymbol (x_13149, x_13148) -> h_Oaddrsymbol x_13149 x_13148
| Oaddrstack x_13150 -> h_Oaddrstack x_13150

(** val constant_rect_Type1 :
    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13154 = function
| Ointconst (sz, sg, x_13156) -> h_Ointconst sz sg x_13156
| Oaddrsymbol (x_13158, x_13157) -> h_Oaddrsymbol x_13158 x_13157
| Oaddrstack x_13159 -> h_Oaddrstack x_13159

(** val constant_rect_Type0 :
    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13163 = function
| Ointconst (sz, sg, x_13165) -> h_Ointconst sz sg x_13165
| Oaddrsymbol (x_13167, x_13166) -> h_Oaddrsymbol x_13167 x_13166
| Oaddrstack x_13168 -> h_Oaddrstack x_13168

(** val constant_inv_rect_Type4 :
    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
    __ -> __ -> 'a1) -> 'a1 **)
let constant_inv_rect_Type4 x1 hterm h1 h2 h3 =
  let hcut = constant_rect_Type4 h1 h2 h3 x1 hterm in hcut __ __

(** val constant_inv_rect_Type3 :
    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
    __ -> __ -> 'a1) -> 'a1 **)
let constant_inv_rect_Type3 x1 hterm h1 h2 h3 =
  let hcut = constant_rect_Type3 h1 h2 h3 x1 hterm in hcut __ __

(** val constant_inv_rect_Type2 :
    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
    __ -> __ -> 'a1) -> 'a1 **)
let constant_inv_rect_Type2 x1 hterm h1 h2 h3 =
  let hcut = constant_rect_Type2 h1 h2 h3 x1 hterm in hcut __ __

(** val constant_inv_rect_Type1 :
    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
    __ -> __ -> 'a1) -> 'a1 **)
let constant_inv_rect_Type1 x1 hterm h1 h2 h3 =
  let hcut = constant_rect_Type1 h1 h2 h3 x1 hterm in hcut __ __

(** val constant_inv_rect_Type0 :
    AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
    -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
    __ -> __ -> 'a1) -> 'a1 **)
let constant_inv_rect_Type0 x1 hterm h1 h2 h3 =
  let hcut = constant_rect_Type0 h1 h2 h3 x1 hterm in hcut __ __

(** val constant_discr : AST.typ -> constant -> constant -> __ **)
let constant_discr a1 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ointconst (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Oaddrsymbol (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oaddrstack a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val constant_jmdiscr : AST.typ -> constant -> constant -> __ **)
let constant_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ointconst (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Oaddrsymbol (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oaddrstack a0 -> Obj.magic (fun _ dH -> dH __)) y

type unary_operation =
| Ocastint of AST.intsize * AST.signedness * AST.intsize * AST.signedness
| Onegint of AST.intsize * AST.signedness
| Onotbool of AST.typ * AST.intsize * AST.signedness
| Onotint of AST.intsize * AST.signedness
| Oid of AST.typ
| Optrofint of AST.intsize * AST.signedness
| Ointofptr of AST.intsize * AST.signedness

(** val unary_operation_rect_Type4 :
    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    unary_operation -> 'a1 **)
let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13238 x_13237 = function
| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
| Onegint (sz, sg) -> h_Onegint sz sg
| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
| Onotint (sz, sg) -> h_Onotint sz sg
| Oid t -> h_Oid t
| Optrofint (sz, sg) -> h_Optrofint sz sg
| Ointofptr (sz, sg) -> h_Ointofptr sz sg

(** val unary_operation_rect_Type5 :
    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    unary_operation -> 'a1 **)
let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13249 x_13248 = function
| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
| Onegint (sz, sg) -> h_Onegint sz sg
| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
| Onotint (sz, sg) -> h_Onotint sz sg
| Oid t -> h_Oid t
| Optrofint (sz, sg) -> h_Optrofint sz sg
| Ointofptr (sz, sg) -> h_Ointofptr sz sg

(** val unary_operation_rect_Type3 :
    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    unary_operation -> 'a1 **)
let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13260 x_13259 = function
| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
| Onegint (sz, sg) -> h_Onegint sz sg
| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
| Onotint (sz, sg) -> h_Onotint sz sg
| Oid t -> h_Oid t
| Optrofint (sz, sg) -> h_Optrofint sz sg
| Ointofptr (sz, sg) -> h_Ointofptr sz sg

(** val unary_operation_rect_Type2 :
    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    unary_operation -> 'a1 **)
let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13271 x_13270 = function
| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
| Onegint (sz, sg) -> h_Onegint sz sg
| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
| Onotint (sz, sg) -> h_Onotint sz sg
| Oid t -> h_Oid t
| Optrofint (sz, sg) -> h_Optrofint sz sg
| Ointofptr (sz, sg) -> h_Ointofptr sz sg

(** val unary_operation_rect_Type1 :
    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    unary_operation -> 'a1 **)
let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13282 x_13281 = function
| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
| Onegint (sz, sg) -> h_Onegint sz sg
| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
| Onotint (sz, sg) -> h_Onotint sz sg
| Oid t -> h_Oid t
| Optrofint (sz, sg) -> h_Optrofint sz sg
| Ointofptr (sz, sg) -> h_Ointofptr sz sg

(** val unary_operation_rect_Type0 :
    (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
    AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    unary_operation -> 'a1 **)
let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13293 x_13292 = function
| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
| Onegint (sz, sg) -> h_Onegint sz sg
| Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
| Onotint (sz, sg) -> h_Onotint sz sg
| Oid t -> h_Oid t
| Optrofint (sz, sg) -> h_Optrofint sz sg
| Ointofptr (sz, sg) -> h_Ointofptr sz sg

(** val unary_operation_inv_rect_Type4 :
    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let unary_operation_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = unary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
  hcut __ __ __

(** val unary_operation_inv_rect_Type3 :
    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let unary_operation_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = unary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
  hcut __ __ __

(** val unary_operation_inv_rect_Type2 :
    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let unary_operation_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = unary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
  hcut __ __ __

(** val unary_operation_inv_rect_Type1 :
    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let unary_operation_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = unary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
  hcut __ __ __

(** val unary_operation_inv_rect_Type0 :
    AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
    -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
    __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let unary_operation_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = unary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
  hcut __ __ __

(** val unary_operation_discr :
    AST.typ -> AST.typ -> unary_operation -> unary_operation -> __ **)
let unary_operation_discr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ocastint (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Onegint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Onotbool (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Onotint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oid a0 -> Obj.magic (fun _ dH -> dH __)
     | Optrofint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Ointofptr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val unary_operation_jmdiscr :
    AST.typ -> AST.typ -> unary_operation -> unary_operation -> __ **)
let unary_operation_jmdiscr a1 a2 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ocastint (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Onegint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Onotbool (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Onotint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oid a0 -> Obj.magic (fun _ dH -> dH __)
     | Optrofint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Ointofptr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

type binary_operation =
| Oadd of AST.intsize * AST.signedness
| Osub of AST.intsize * AST.signedness
| Omul of AST.intsize * AST.signedness
| Odiv of AST.intsize
| Odivu of AST.intsize
| Omod of AST.intsize
| Omodu of AST.intsize
| Oand of AST.intsize * AST.signedness
| Oor of AST.intsize * AST.signedness
| Oxor of AST.intsize * AST.signedness
| Oshl of AST.intsize * AST.signedness
| Oshr of AST.intsize * AST.signedness
| Oshru of AST.intsize * AST.signedness
| Ocmp of AST.intsize * AST.signedness * AST.signedness * Integers.comparison
| Ocmpu of AST.intsize * AST.signedness * Integers.comparison
| Oaddpi of AST.intsize
| Oaddip of AST.intsize
| Osubpi of AST.intsize
| Osubpp of AST.intsize
| Ocmpp of AST.signedness * Integers.comparison

(** val binary_operation_rect_Type4 :
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13398 x_13397 x_13396 = function
| Oadd (sz, sg) -> h_Oadd sz sg
| Osub (sz, sg) -> h_Osub sz sg
| Omul (sz, sg) -> h_Omul sz sg
| Odiv sz -> h_Odiv sz
| Odivu sz -> h_Odivu sz
| Omod sz -> h_Omod sz
| Omodu sz -> h_Omodu sz
| Oand (sz, sg) -> h_Oand sz sg
| Oor (sz, sg) -> h_Oor sz sg
| Oxor (sz, sg) -> h_Oxor sz sg
| Oshl (sz, sg) -> h_Oshl sz sg
| Oshr (sz, sg) -> h_Oshr sz sg
| Oshru (sz, sg) -> h_Oshru sz sg
| Ocmp (sz, sg, sg', x_13400) -> h_Ocmp sz sg sg' x_13400
| Ocmpu (sz, sg', x_13401) -> h_Ocmpu sz sg' x_13401
| Oaddpi sz -> h_Oaddpi sz
| Oaddip sz -> h_Oaddip sz
| Osubpi sz -> h_Osubpi sz
| Osubpp sz -> h_Osubpp sz
| Ocmpp (sg', x_13402) -> h_Ocmpp sg' x_13402

(** val binary_operation_rect_Type5 :
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13425 x_13424 x_13423 = function
| Oadd (sz, sg) -> h_Oadd sz sg
| Osub (sz, sg) -> h_Osub sz sg
| Omul (sz, sg) -> h_Omul sz sg
| Odiv sz -> h_Odiv sz
| Odivu sz -> h_Odivu sz
| Omod sz -> h_Omod sz
| Omodu sz -> h_Omodu sz
| Oand (sz, sg) -> h_Oand sz sg
| Oor (sz, sg) -> h_Oor sz sg
| Oxor (sz, sg) -> h_Oxor sz sg
| Oshl (sz, sg) -> h_Oshl sz sg
| Oshr (sz, sg) -> h_Oshr sz sg
| Oshru (sz, sg) -> h_Oshru sz sg
| Ocmp (sz, sg, sg', x_13427) -> h_Ocmp sz sg sg' x_13427
| Ocmpu (sz, sg', x_13428) -> h_Ocmpu sz sg' x_13428
| Oaddpi sz -> h_Oaddpi sz
| Oaddip sz -> h_Oaddip sz
| Osubpi sz -> h_Osubpi sz
| Osubpp sz -> h_Osubpp sz
| Ocmpp (sg', x_13429) -> h_Ocmpp sg' x_13429

(** val binary_operation_rect_Type3 :
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13452 x_13451 x_13450 = function
| Oadd (sz, sg) -> h_Oadd sz sg
| Osub (sz, sg) -> h_Osub sz sg
| Omul (sz, sg) -> h_Omul sz sg
| Odiv sz -> h_Odiv sz
| Odivu sz -> h_Odivu sz
| Omod sz -> h_Omod sz
| Omodu sz -> h_Omodu sz
| Oand (sz, sg) -> h_Oand sz sg
| Oor (sz, sg) -> h_Oor sz sg
| Oxor (sz, sg) -> h_Oxor sz sg
| Oshl (sz, sg) -> h_Oshl sz sg
| Oshr (sz, sg) -> h_Oshr sz sg
| Oshru (sz, sg) -> h_Oshru sz sg
| Ocmp (sz, sg, sg', x_13454) -> h_Ocmp sz sg sg' x_13454
| Ocmpu (sz, sg', x_13455) -> h_Ocmpu sz sg' x_13455
| Oaddpi sz -> h_Oaddpi sz
| Oaddip sz -> h_Oaddip sz
| Osubpi sz -> h_Osubpi sz
| Osubpp sz -> h_Osubpp sz
| Ocmpp (sg', x_13456) -> h_Ocmpp sg' x_13456

(** val binary_operation_rect_Type2 :
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13479 x_13478 x_13477 = function
| Oadd (sz, sg) -> h_Oadd sz sg
| Osub (sz, sg) -> h_Osub sz sg
| Omul (sz, sg) -> h_Omul sz sg
| Odiv sz -> h_Odiv sz
| Odivu sz -> h_Odivu sz
| Omod sz -> h_Omod sz
| Omodu sz -> h_Omodu sz
| Oand (sz, sg) -> h_Oand sz sg
| Oor (sz, sg) -> h_Oor sz sg
| Oxor (sz, sg) -> h_Oxor sz sg
| Oshl (sz, sg) -> h_Oshl sz sg
| Oshr (sz, sg) -> h_Oshr sz sg
| Oshru (sz, sg) -> h_Oshru sz sg
| Ocmp (sz, sg, sg', x_13481) -> h_Ocmp sz sg sg' x_13481
| Ocmpu (sz, sg', x_13482) -> h_Ocmpu sz sg' x_13482
| Oaddpi sz -> h_Oaddpi sz
| Oaddip sz -> h_Oaddip sz
| Osubpi sz -> h_Osubpi sz
| Osubpp sz -> h_Osubpp sz
| Ocmpp (sg', x_13483) -> h_Ocmpp sg' x_13483

(** val binary_operation_rect_Type1 :
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13506 x_13505 x_13504 = function
| Oadd (sz, sg) -> h_Oadd sz sg
| Osub (sz, sg) -> h_Osub sz sg
| Omul (sz, sg) -> h_Omul sz sg
| Odiv sz -> h_Odiv sz
| Odivu sz -> h_Odivu sz
| Omod sz -> h_Omod sz
| Omodu sz -> h_Omodu sz
| Oand (sz, sg) -> h_Oand sz sg
| Oor (sz, sg) -> h_Oor sz sg
| Oxor (sz, sg) -> h_Oxor sz sg
| Oshl (sz, sg) -> h_Oshl sz sg
| Oshr (sz, sg) -> h_Oshr sz sg
| Oshru (sz, sg) -> h_Oshru sz sg
| Ocmp (sz, sg, sg', x_13508) -> h_Ocmp sz sg sg' x_13508
| Ocmpu (sz, sg', x_13509) -> h_Ocmpu sz sg' x_13509
| Oaddpi sz -> h_Oaddpi sz
| Oaddip sz -> h_Oaddip sz
| Osubpi sz -> h_Osubpi sz
| Osubpp sz -> h_Osubpp sz
| Ocmpp (sg', x_13510) -> h_Ocmpp sg' x_13510

(** val binary_operation_rect_Type0 :
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
    -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
    (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
    -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
    AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13533 x_13532 x_13531 = function
| Oadd (sz, sg) -> h_Oadd sz sg
| Osub (sz, sg) -> h_Osub sz sg
| Omul (sz, sg) -> h_Omul sz sg
| Odiv sz -> h_Odiv sz
| Odivu sz -> h_Odivu sz
| Omod sz -> h_Omod sz
| Omodu sz -> h_Omodu sz
| Oand (sz, sg) -> h_Oand sz sg
| Oor (sz, sg) -> h_Oor sz sg
| Oxor (sz, sg) -> h_Oxor sz sg
| Oshl (sz, sg) -> h_Oshl sz sg
| Oshr (sz, sg) -> h_Oshr sz sg
| Oshru (sz, sg) -> h_Oshru sz sg
| Ocmp (sz, sg, sg', x_13535) -> h_Ocmp sz sg sg' x_13535
| Ocmpu (sz, sg', x_13536) -> h_Ocmpu sz sg' x_13536
| Oaddpi sz -> h_Oaddpi sz
| Oaddip sz -> h_Oaddip sz
| Osubpi sz -> h_Osubpi sz
| Osubpp sz -> h_Osubpp sz
| Ocmpp (sg', x_13537) -> h_Ocmpp sg' x_13537

(** val binary_operation_inv_rect_Type4 :
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
  let hcut =
    binary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
  in
  hcut __ __ __ __

(** val binary_operation_inv_rect_Type3 :
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
  let hcut =
    binary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
  in
  hcut __ __ __ __

(** val binary_operation_inv_rect_Type2 :
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
  let hcut =
    binary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
  in
  hcut __ __ __ __

(** val binary_operation_inv_rect_Type1 :
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
  let hcut =
    binary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
  in
  hcut __ __ __ __

(** val binary_operation_inv_rect_Type0 :
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
    AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
    -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
    -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
    -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
    (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
    -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
    Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
    -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
    -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
    __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
    __ -> __ -> __ -> 'a1) -> 'a1 **)
let binary_operation_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
  let hcut =
    binary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
      h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
  in
  hcut __ __ __ __

(** val binary_operation_discr :
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation ->
    __ **)
let binary_operation_discr a1 a2 a3 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Oadd (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Osub (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Omul (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Odiv a0 -> Obj.magic (fun _ dH -> dH __)
     | Odivu a0 -> Obj.magic (fun _ dH -> dH __)
     | Omod a0 -> Obj.magic (fun _ dH -> dH __)
     | Omodu a0 -> Obj.magic (fun _ dH -> dH __)
     | Oand (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oxor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oshl (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oshr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oshru (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Ocmp (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Ocmpu (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Oaddpi a0 -> Obj.magic (fun _ dH -> dH __)
     | Oaddip a0 -> Obj.magic (fun _ dH -> dH __)
     | Osubpi a0 -> Obj.magic (fun _ dH -> dH __)
     | Osubpp a0 -> Obj.magic (fun _ dH -> dH __)
     | Ocmpp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val binary_operation_jmdiscr :
    AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation ->
    __ **)
let binary_operation_jmdiscr a1 a2 a3 x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Oadd (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Osub (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Omul (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Odiv a0 -> Obj.magic (fun _ dH -> dH __)
     | Odivu a0 -> Obj.magic (fun _ dH -> dH __)
     | Omod a0 -> Obj.magic (fun _ dH -> dH __)
     | Omodu a0 -> Obj.magic (fun _ dH -> dH __)
     | Oand (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oxor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oshl (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oshr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Oshru (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     | Ocmp (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Ocmpu (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Oaddpi a0 -> Obj.magic (fun _ dH -> dH __)
     | Oaddip a0 -> Obj.magic (fun _ dH -> dH __)
     | Osubpi a0 -> Obj.magic (fun _ dH -> dH __)
     | Osubpp a0 -> Obj.magic (fun _ dH -> dH __)
     | Ocmpp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val eval_constant :
    AST.typ -> (AST.ident -> Pointers.block Types.option) -> Pointers.block
    -> constant -> Values.val0 Types.option **)
let eval_constant t find_symbol sp = function
| Ointconst (sz, sg, n) -> Types.Some (Values.Vint (sz, n))
| Oaddrsymbol (s, ofs) ->
  (match find_symbol s with
   | Types.None -> Types.None
   | Types.Some b ->
     Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff =
       (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
         Pointers.zero_offset (AST.repr AST.I16 ofs)) }))
| Oaddrstack ofs ->
  Types.Some (Values.Vptr { Pointers.pblock = sp; Pointers.poff =
    (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
      Pointers.zero_offset (AST.repr AST.I16 ofs)) })

(** val eval_unop :
    AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
    Types.option **)
let eval_unop t t' op arg =
  match op with
  | Ocastint (sz, sg, sz', sg') ->
    (match sg with
     | AST.Signed -> Types.Some (Values.sign_ext sz' arg)
     | AST.Unsigned -> Types.Some (Values.zero_ext sz' arg))
  | Onegint (sz, sg) ->
    (match arg with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       Types.Some (Values.Vint (sz1,
         (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz1) n1)))
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Onotbool (t0, sz, sg) ->
    (match arg with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       Types.Some (Values.Vint (sz,
         (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
                  (BitVector.zero (AST.bitsize_of_intsize sz1)) with
          | Bool.True -> AST.repr sz (Nat.S Nat.O)
          | Bool.False -> BitVector.zero (AST.bitsize_of_intsize sz))))
     | Values.Vnull ->
       Types.Some (Values.Vint (sz, (AST.repr sz (Nat.S Nat.O))))
     | Values.Vptr x0 ->
       Types.Some (Values.Vint (sz,
         (BitVector.zero (AST.bitsize_of_intsize sz)))))
  | Onotint (sz, sg) ->
    (match arg with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       Types.Some (Values.Vint (sz1,
         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz1) n1
           (Values.mone sz1))))
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Oid t0 -> Types.Some arg
  | Optrofint (sz, sg) ->
    (match arg with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
                (BitVector.zero (AST.bitsize_of_intsize sz1)) with
        | Bool.True -> Types.Some Values.Vnull
        | Bool.False -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Ointofptr (sz, sg) ->
    (match arg with
     | Values.Vundef -> Types.None
     | Values.Vint (x, x0) -> Types.None
     | Values.Vnull ->
       Types.Some (Values.Vint (sz,
         (BitVector.zero (AST.bitsize_of_intsize sz))))
     | Values.Vptr x -> Types.None)

(** val eval_compare_mismatch :
    Integers.comparison -> Values.val0 Types.option **)
let eval_compare_mismatch = function
| Integers.Ceq -> Types.Some Values.vfalse
| Integers.Cne -> Types.Some Values.vtrue
| Integers.Clt -> Types.None
| Integers.Cle -> Types.None
| Integers.Cgt -> Types.None
| Integers.Cge -> Types.None

(** val ev_add : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_add v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
         (sz2, (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_sub : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_sub v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
         (sz2,
         (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2))))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_addpi : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_addpi v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (x, x0) -> Types.None
  | Values.Vnull ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
                (BitVector.zero (AST.bitsize_of_intsize sz2)) with
        | Bool.True -> Types.Some Values.Vnull
        | Bool.False -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vptr ptr1 ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       Types.Some (Values.Vptr
         (Pointers.shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2))
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)

(** val ev_subpi : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_subpi v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (x, x0) -> Types.None
  | Values.Vnull ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
                (BitVector.zero (AST.bitsize_of_intsize sz2)) with
        | Bool.True -> Types.Some Values.Vnull
        | Bool.False -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vptr ptr1 ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       Types.Some (Values.Vptr
         (Pointers.neg_shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2))
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)

(** val ev_subpp :
    AST.intsize -> Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_subpp sz v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (x, x0) -> Types.None
  | Values.Vnull ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (x, x0) -> Types.None
     | Values.Vnull ->
       Types.Some (Values.Vint (sz,
         (BitVector.zero (AST.bitsize_of_intsize sz))))
     | Values.Vptr x -> Types.None)
  | Values.Vptr ptr1 ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (x, x0) -> Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr ptr2 ->
       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
        | Bool.True ->
          Types.Some (Values.Vint (sz,
            (Pointers.sub_offset (AST.bitsize_of_intsize sz)
              ptr1.Pointers.poff ptr2.Pointers.poff)))
        | Bool.False -> Types.None))

(** val ev_mul : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_mul v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
         (sz2,
         (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
           n2)))) Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_divs : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_divs v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
         Types.option_map (fun x -> Values.Vint (sz2, x))
           (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_mods : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_mods v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
         Types.option_map (fun x -> Values.Vint (sz2, x))
           (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_divu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_divu v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
         Types.option_map (fun x -> Values.Vint (sz2, x))
           (Arithmetic.division_u
             (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
               Nat.O)))))))
               (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_modu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_modu v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
         Types.option_map (fun x -> Values.Vint (sz2, x))
           (Arithmetic.modulus_u
             (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
               Nat.O)))))))
               (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_and v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
         (sz2,
         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_or v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
         (sz2,
         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
           n2)))) Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_xor v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
         (sz2,
         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
           n2)))) Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_shl v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
                  (AST.bitsize_of_intsize sz1)) with
        | Bool.True ->
          Types.Some (Values.Vint (sz1,
            (Vector.shift_left (AST.bitsize_of_intsize sz1)
              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
              n1 Bool.False)))
        | Bool.False -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_shr : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_shr v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
                  (AST.bitsize_of_intsize sz1)) with
        | Bool.True ->
          Types.Some (Values.Vint (sz1,
            (Vector.shift_right
              (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                Nat.O)))))))
                (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
              n1
              (Vector.head'
                (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                  Nat.O)))))))
                  (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n1))))
        | Bool.False -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_shru : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let ev_shru v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
                  (AST.bitsize_of_intsize sz1)) with
        | Bool.True ->
          Types.Some (Values.Vint (sz1,
            (Vector.shift_right
              (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                Nat.O)))))))
                (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
              n1 Bool.False)))
        | Bool.False -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val fEtrue : Values.val0 **)
let fEtrue =
  Values.Vint (AST.I8, (AST.repr AST.I8 (Nat.S Nat.O)))

(** val fEfalse : Values.val0 **)
let fEfalse =
  Values.Vint (AST.I8, (AST.repr AST.I8 Nat.O))

(** val fE_of_bool : Bool.bool -> Values.val0 **)
let fE_of_bool = function
| Bool.True -> fEtrue
| Bool.False -> fEfalse

(** val ev_cmp_match : Integers.comparison -> Values.val0 Types.option **)
let ev_cmp_match = function
| Integers.Ceq -> Types.Some fEtrue
| Integers.Cne -> Types.Some fEfalse
| Integers.Clt -> Types.None
| Integers.Cle -> Types.None
| Integers.Cgt -> Types.None
| Integers.Cge -> Types.None

(** val ev_cmp_mismatch : Integers.comparison -> Values.val0 Types.option **)
let ev_cmp_mismatch = function
| Integers.Ceq -> Types.Some fEfalse
| Integers.Cne -> Types.Some fEtrue
| Integers.Clt -> Types.None
| Integers.Cle -> Types.None
| Integers.Cgt -> Types.None
| Integers.Cge -> Types.None

(** val ev_cmp :
    Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
    Types.option **)
let ev_cmp c v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
         (fE_of_bool (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val ev_cmpp :
    GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
    Values.val0 Types.option **)
let ev_cmpp m c v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (x, x0) -> Types.None
  | Values.Vnull ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (x, x0) -> Types.None
     | Values.Vnull -> ev_cmp_match c
     | Values.Vptr x -> ev_cmp_mismatch c)
  | Values.Vptr ptr1 ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (x, x0) -> Types.None
     | Values.Vnull -> ev_cmp_mismatch c
     | Values.Vptr ptr2 ->
       (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
                (FrontEndMem.valid_pointer m ptr2) with
        | Bool.True ->
          (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
           | Bool.True ->
             Types.Some
               (fE_of_bool
                 (Values.cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff))
           | Bool.False -> ev_cmp_mismatch c)
        | Bool.False -> Types.None))

(** val ev_cmpu :
    Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
    Types.option **)
let ev_cmpu c v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
         (fE_of_bool (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val eval_binop :
    GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
    Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let eval_binop m t1 t2 t' = function
| Oadd (x, x0) -> ev_add
| Osub (x, x0) -> ev_sub
| Omul (x, x0) -> ev_mul
| Odiv x -> ev_divs
| Odivu x -> ev_divu
| Omod x -> ev_mods
| Omodu x -> ev_modu
| Oand (x, x0) -> ev_and
| Oor (x, x0) -> ev_or
| Oxor (x, x0) -> ev_xor
| Oshl (x, x0) -> ev_shl
| Oshr (x, x0) -> ev_shr
| Oshru (x, x0) -> ev_shru
| Ocmp (x, x0, x1, c) -> ev_cmp c
| Ocmpu (x, x0, c) -> ev_cmpu c
| Oaddpi x -> ev_addpi
| Oaddip x -> (fun x0 y -> ev_addpi y x0)
| Osubpi x -> ev_subpi
| Osubpp sz -> ev_subpp sz
| Ocmpp (x, c) -> ev_cmpp m c