open Preamble open Bool open Hints_declaration open Core_notation open Pts open Logic open Relations open Nat open Jmeq open Exp open Setoids open Monad open Option open Extranat open Vector open Div_and_mod open Russell open Types open List open Util open FoldStuff open BitVector open Arithmetic (** val int_size : BitVector.bitVector **) let int_size = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O) (** val ptr_size : BitVector.bitVector **) let ptr_size = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S Nat.O)) (** val alignment : 'a1 Types.option **) let alignment = Types.None type register = | Register00 | Register01 | Register02 | Register03 | Register04 | Register05 | Register06 | Register07 | Register10 | Register11 | Register12 | Register13 | Register14 | Register15 | Register16 | Register17 | Register20 | Register21 | Register22 | Register23 | Register24 | Register25 | Register26 | Register27 | Register30 | Register31 | Register32 | Register33 | Register34 | Register35 | Register36 | Register37 | RegisterA | RegisterB | RegisterDPL | RegisterDPH | RegisterCarry (** val register_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **) let rec register_rect_Type4 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function | Register00 -> h_Register00 | Register01 -> h_Register01 | Register02 -> h_Register02 | Register03 -> h_Register03 | Register04 -> h_Register04 | Register05 -> h_Register05 | Register06 -> h_Register06 | Register07 -> h_Register07 | Register10 -> h_Register10 | Register11 -> h_Register11 | Register12 -> h_Register12 | Register13 -> h_Register13 | Register14 -> h_Register14 | Register15 -> h_Register15 | Register16 -> h_Register16 | Register17 -> h_Register17 | Register20 -> h_Register20 | Register21 -> h_Register21 | Register22 -> h_Register22 | Register23 -> h_Register23 | Register24 -> h_Register24 | Register25 -> h_Register25 | Register26 -> h_Register26 | Register27 -> h_Register27 | Register30 -> h_Register30 | Register31 -> h_Register31 | Register32 -> h_Register32 | Register33 -> h_Register33 | Register34 -> h_Register34 | Register35 -> h_Register35 | Register36 -> h_Register36 | Register37 -> h_Register37 | RegisterA -> h_RegisterA | RegisterB -> h_RegisterB | RegisterDPL -> h_RegisterDPL | RegisterDPH -> h_RegisterDPH | RegisterCarry -> h_RegisterCarry (** val register_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **) let rec register_rect_Type5 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function | Register00 -> h_Register00 | Register01 -> h_Register01 | Register02 -> h_Register02 | Register03 -> h_Register03 | Register04 -> h_Register04 | Register05 -> h_Register05 | Register06 -> h_Register06 | Register07 -> h_Register07 | Register10 -> h_Register10 | Register11 -> h_Register11 | Register12 -> h_Register12 | Register13 -> h_Register13 | Register14 -> h_Register14 | Register15 -> h_Register15 | Register16 -> h_Register16 | Register17 -> h_Register17 | Register20 -> h_Register20 | Register21 -> h_Register21 | Register22 -> h_Register22 | Register23 -> h_Register23 | Register24 -> h_Register24 | Register25 -> h_Register25 | Register26 -> h_Register26 | Register27 -> h_Register27 | Register30 -> h_Register30 | Register31 -> h_Register31 | Register32 -> h_Register32 | Register33 -> h_Register33 | Register34 -> h_Register34 | Register35 -> h_Register35 | Register36 -> h_Register36 | Register37 -> h_Register37 | RegisterA -> h_RegisterA | RegisterB -> h_RegisterB | RegisterDPL -> h_RegisterDPL | RegisterDPH -> h_RegisterDPH | RegisterCarry -> h_RegisterCarry (** val register_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **) let rec register_rect_Type3 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function | Register00 -> h_Register00 | Register01 -> h_Register01 | Register02 -> h_Register02 | Register03 -> h_Register03 | Register04 -> h_Register04 | Register05 -> h_Register05 | Register06 -> h_Register06 | Register07 -> h_Register07 | Register10 -> h_Register10 | Register11 -> h_Register11 | Register12 -> h_Register12 | Register13 -> h_Register13 | Register14 -> h_Register14 | Register15 -> h_Register15 | Register16 -> h_Register16 | Register17 -> h_Register17 | Register20 -> h_Register20 | Register21 -> h_Register21 | Register22 -> h_Register22 | Register23 -> h_Register23 | Register24 -> h_Register24 | Register25 -> h_Register25 | Register26 -> h_Register26 | Register27 -> h_Register27 | Register30 -> h_Register30 | Register31 -> h_Register31 | Register32 -> h_Register32 | Register33 -> h_Register33 | Register34 -> h_Register34 | Register35 -> h_Register35 | Register36 -> h_Register36 | Register37 -> h_Register37 | RegisterA -> h_RegisterA | RegisterB -> h_RegisterB | RegisterDPL -> h_RegisterDPL | RegisterDPH -> h_RegisterDPH | RegisterCarry -> h_RegisterCarry (** val register_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **) let rec register_rect_Type2 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function | Register00 -> h_Register00 | Register01 -> h_Register01 | Register02 -> h_Register02 | Register03 -> h_Register03 | Register04 -> h_Register04 | Register05 -> h_Register05 | Register06 -> h_Register06 | Register07 -> h_Register07 | Register10 -> h_Register10 | Register11 -> h_Register11 | Register12 -> h_Register12 | Register13 -> h_Register13 | Register14 -> h_Register14 | Register15 -> h_Register15 | Register16 -> h_Register16 | Register17 -> h_Register17 | Register20 -> h_Register20 | Register21 -> h_Register21 | Register22 -> h_Register22 | Register23 -> h_Register23 | Register24 -> h_Register24 | Register25 -> h_Register25 | Register26 -> h_Register26 | Register27 -> h_Register27 | Register30 -> h_Register30 | Register31 -> h_Register31 | Register32 -> h_Register32 | Register33 -> h_Register33 | Register34 -> h_Register34 | Register35 -> h_Register35 | Register36 -> h_Register36 | Register37 -> h_Register37 | RegisterA -> h_RegisterA | RegisterB -> h_RegisterB | RegisterDPL -> h_RegisterDPL | RegisterDPH -> h_RegisterDPH | RegisterCarry -> h_RegisterCarry (** val register_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **) let rec register_rect_Type1 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function | Register00 -> h_Register00 | Register01 -> h_Register01 | Register02 -> h_Register02 | Register03 -> h_Register03 | Register04 -> h_Register04 | Register05 -> h_Register05 | Register06 -> h_Register06 | Register07 -> h_Register07 | Register10 -> h_Register10 | Register11 -> h_Register11 | Register12 -> h_Register12 | Register13 -> h_Register13 | Register14 -> h_Register14 | Register15 -> h_Register15 | Register16 -> h_Register16 | Register17 -> h_Register17 | Register20 -> h_Register20 | Register21 -> h_Register21 | Register22 -> h_Register22 | Register23 -> h_Register23 | Register24 -> h_Register24 | Register25 -> h_Register25 | Register26 -> h_Register26 | Register27 -> h_Register27 | Register30 -> h_Register30 | Register31 -> h_Register31 | Register32 -> h_Register32 | Register33 -> h_Register33 | Register34 -> h_Register34 | Register35 -> h_Register35 | Register36 -> h_Register36 | Register37 -> h_Register37 | RegisterA -> h_RegisterA | RegisterB -> h_RegisterB | RegisterDPL -> h_RegisterDPL | RegisterDPH -> h_RegisterDPH | RegisterCarry -> h_RegisterCarry (** val register_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **) let rec register_rect_Type0 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function | Register00 -> h_Register00 | Register01 -> h_Register01 | Register02 -> h_Register02 | Register03 -> h_Register03 | Register04 -> h_Register04 | Register05 -> h_Register05 | Register06 -> h_Register06 | Register07 -> h_Register07 | Register10 -> h_Register10 | Register11 -> h_Register11 | Register12 -> h_Register12 | Register13 -> h_Register13 | Register14 -> h_Register14 | Register15 -> h_Register15 | Register16 -> h_Register16 | Register17 -> h_Register17 | Register20 -> h_Register20 | Register21 -> h_Register21 | Register22 -> h_Register22 | Register23 -> h_Register23 | Register24 -> h_Register24 | Register25 -> h_Register25 | Register26 -> h_Register26 | Register27 -> h_Register27 | Register30 -> h_Register30 | Register31 -> h_Register31 | Register32 -> h_Register32 | Register33 -> h_Register33 | Register34 -> h_Register34 | Register35 -> h_Register35 | Register36 -> h_Register36 | Register37 -> h_Register37 | RegisterA -> h_RegisterA | RegisterB -> h_RegisterB | RegisterDPL -> h_RegisterDPL | RegisterDPH -> h_RegisterDPH | RegisterCarry -> h_RegisterCarry (** val register_inv_rect_Type4 : register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let register_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 = let hcut = register_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 hterm in hcut __ (** val register_inv_rect_Type3 : register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let register_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 = let hcut = register_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 hterm in hcut __ (** val register_inv_rect_Type2 : register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let register_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 = let hcut = register_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 hterm in hcut __ (** val register_inv_rect_Type1 : register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let register_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 = let hcut = register_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 hterm in hcut __ (** val register_inv_rect_Type0 : register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let register_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 = let hcut = register_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 hterm in hcut __ (** val register_discr : register -> register -> __ **) let register_discr x y = Logic.eq_rect_Type2 x (match x with | Register00 -> Obj.magic (fun _ dH -> dH) | Register01 -> Obj.magic (fun _ dH -> dH) | Register02 -> Obj.magic (fun _ dH -> dH) | Register03 -> Obj.magic (fun _ dH -> dH) | Register04 -> Obj.magic (fun _ dH -> dH) | Register05 -> Obj.magic (fun _ dH -> dH) | Register06 -> Obj.magic (fun _ dH -> dH) | Register07 -> Obj.magic (fun _ dH -> dH) | Register10 -> Obj.magic (fun _ dH -> dH) | Register11 -> Obj.magic (fun _ dH -> dH) | Register12 -> Obj.magic (fun _ dH -> dH) | Register13 -> Obj.magic (fun _ dH -> dH) | Register14 -> Obj.magic (fun _ dH -> dH) | Register15 -> Obj.magic (fun _ dH -> dH) | Register16 -> Obj.magic (fun _ dH -> dH) | Register17 -> Obj.magic (fun _ dH -> dH) | Register20 -> Obj.magic (fun _ dH -> dH) | Register21 -> Obj.magic (fun _ dH -> dH) | Register22 -> Obj.magic (fun _ dH -> dH) | Register23 -> Obj.magic (fun _ dH -> dH) | Register24 -> Obj.magic (fun _ dH -> dH) | Register25 -> Obj.magic (fun _ dH -> dH) | Register26 -> Obj.magic (fun _ dH -> dH) | Register27 -> Obj.magic (fun _ dH -> dH) | Register30 -> Obj.magic (fun _ dH -> dH) | Register31 -> Obj.magic (fun _ dH -> dH) | Register32 -> Obj.magic (fun _ dH -> dH) | Register33 -> Obj.magic (fun _ dH -> dH) | Register34 -> Obj.magic (fun _ dH -> dH) | Register35 -> Obj.magic (fun _ dH -> dH) | Register36 -> Obj.magic (fun _ dH -> dH) | Register37 -> Obj.magic (fun _ dH -> dH) | RegisterA -> Obj.magic (fun _ dH -> dH) | RegisterB -> Obj.magic (fun _ dH -> dH) | RegisterDPL -> Obj.magic (fun _ dH -> dH) | RegisterDPH -> Obj.magic (fun _ dH -> dH) | RegisterCarry -> Obj.magic (fun _ dH -> dH)) y (** val register_jmdiscr : register -> register -> __ **) let register_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | Register00 -> Obj.magic (fun _ dH -> dH) | Register01 -> Obj.magic (fun _ dH -> dH) | Register02 -> Obj.magic (fun _ dH -> dH) | Register03 -> Obj.magic (fun _ dH -> dH) | Register04 -> Obj.magic (fun _ dH -> dH) | Register05 -> Obj.magic (fun _ dH -> dH) | Register06 -> Obj.magic (fun _ dH -> dH) | Register07 -> Obj.magic (fun _ dH -> dH) | Register10 -> Obj.magic (fun _ dH -> dH) | Register11 -> Obj.magic (fun _ dH -> dH) | Register12 -> Obj.magic (fun _ dH -> dH) | Register13 -> Obj.magic (fun _ dH -> dH) | Register14 -> Obj.magic (fun _ dH -> dH) | Register15 -> Obj.magic (fun _ dH -> dH) | Register16 -> Obj.magic (fun _ dH -> dH) | Register17 -> Obj.magic (fun _ dH -> dH) | Register20 -> Obj.magic (fun _ dH -> dH) | Register21 -> Obj.magic (fun _ dH -> dH) | Register22 -> Obj.magic (fun _ dH -> dH) | Register23 -> Obj.magic (fun _ dH -> dH) | Register24 -> Obj.magic (fun _ dH -> dH) | Register25 -> Obj.magic (fun _ dH -> dH) | Register26 -> Obj.magic (fun _ dH -> dH) | Register27 -> Obj.magic (fun _ dH -> dH) | Register30 -> Obj.magic (fun _ dH -> dH) | Register31 -> Obj.magic (fun _ dH -> dH) | Register32 -> Obj.magic (fun _ dH -> dH) | Register33 -> Obj.magic (fun _ dH -> dH) | Register34 -> Obj.magic (fun _ dH -> dH) | Register35 -> Obj.magic (fun _ dH -> dH) | Register36 -> Obj.magic (fun _ dH -> dH) | Register37 -> Obj.magic (fun _ dH -> dH) | RegisterA -> Obj.magic (fun _ dH -> dH) | RegisterB -> Obj.magic (fun _ dH -> dH) | RegisterDPL -> Obj.magic (fun _ dH -> dH) | RegisterDPH -> Obj.magic (fun _ dH -> dH) | RegisterCarry -> Obj.magic (fun _ dH -> dH)) y (** val nat_of_register : register -> Nat.nat **) let nat_of_register = function | Register00 -> Nat.O | Register01 -> Nat.S Nat.O | Register02 -> Nat.S (Nat.S Nat.O) | Register03 -> Nat.S (Nat.S (Nat.S Nat.O)) | Register04 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))) | Register05 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) | Register06 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) | Register07 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) | Register10 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) | Register11 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) | Register12 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) | Register13 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) | Register14 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) | Register15 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))) | Register16 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))) | Register17 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))) | Register20 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))) | Register21 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) | Register22 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) | Register23 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) | Register24 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))) | Register25 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))) | Register26 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))) | Register27 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))) | Register30 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))) | Register31 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))) | Register32 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))) | Register33 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))) | Register34 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))) | Register35 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))) | Register36 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))) | Register37 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))) | RegisterA -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))) | RegisterB -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))) | RegisterDPL -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))) | RegisterDPH -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))))) | RegisterCarry -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))) (** val physical_register_count : Nat.nat **) let physical_register_count = Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))) (** val bitvector_of_register : register -> BitVector.bitVector **) let bitvector_of_register register0 = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (nat_of_register register0) (** val eq_Register : register -> register -> Bool.bool **) let eq_Register r s = let r_as_nat = nat_of_register r in let s_as_nat = nat_of_register s in Nat.eqb r_as_nat s_as_nat (** val registerSST : register **) let registerSST = Register10 (** val registerST0 : register **) let registerST0 = Register02 (** val registerST1 : register **) let registerST1 = Register03 (** val registerST2 : register **) let registerST2 = Register04 (** val registerST3 : register **) let registerST3 = Register05 (** val registerSTS : register List.list **) let registerSTS = List.Cons (registerST0, (List.Cons (registerST1, (List.Cons (registerST2, (List.Cons (registerST3, List.Nil))))))) (** val registerSPL : register **) let registerSPL = Register06 (** val registerSPH : register **) let registerSPH = Register07 (** val registerParams : register List.list **) let registerParams = List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32, (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35, (List.Cons (Register36, (List.Cons (Register37, List.Nil))))))))))))))) (** val registers : register List.list **) let registers = List.Cons (Register00, (List.Cons (Register01, (List.Cons (Register02, (List.Cons (Register03, (List.Cons (Register04, (List.Cons (Register05, (List.Cons (Register06, (List.Cons (Register07, (List.Cons (Register10, (List.Cons (Register11, (List.Cons (Register12, (List.Cons (Register13, (List.Cons (Register14, (List.Cons (Register15, (List.Cons (Register16, (List.Cons (Register17, (List.Cons (Register20, (List.Cons (Register21, (List.Cons (Register22, (List.Cons (Register23, (List.Cons (Register24, (List.Cons (Register25, (List.Cons (Register26, (List.Cons (Register27, (List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32, (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35, (List.Cons (Register36, (List.Cons (Register37, (List.Cons (RegisterA, (List.Cons (RegisterB, (List.Cons (RegisterDPL, (List.Cons (RegisterDPH, (List.Cons (registerSPL, (List.Cons (registerSPH, (List.Cons (registerST0, (List.Cons (registerST1, (List.Cons (registerSST, List.Nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (** val registerRets : register List.list **) let registerRets = List.Cons (RegisterDPL, (List.Cons (RegisterDPH, (List.Cons (Register00, (List.Cons (Register01, List.Nil))))))) (** val registerCallerSaved : register List.list **) let registerCallerSaved = List.Cons (Register00, (List.Cons (Register01, (List.Cons (Register02, (List.Cons (Register03, (List.Cons (Register04, (List.Cons (Register05, (List.Cons (Register06, (List.Cons (Register07, (List.Cons (Register10, (List.Cons (Register11, (List.Cons (Register12, (List.Cons (Register13, (List.Cons (Register14, (List.Cons (Register15, (List.Cons (Register16, (List.Cons (Register17, (List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32, (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35, (List.Cons (Register36, (List.Cons (Register37, List.Nil))))))))))))))))))))))))))))))))))))))))))))))) (** val registerCalleeSaved : register List.list **) let registerCalleeSaved = List.Cons (Register20, (List.Cons (Register21, (List.Cons (Register22, (List.Cons (Register23, (List.Cons (Register24, (List.Cons (Register25, (List.Cons (Register26, (List.Cons (Register27, List.Nil))))))))))))))) (** val registersForbidden : register List.list **) let registersForbidden = List.Cons (RegisterA, (List.Cons (RegisterB, (List.Cons (RegisterDPL, (List.Cons (RegisterDPH, (List.Cons (registerSPL, (List.Cons (registerSPH, (List.Cons (registerST0, (List.Cons (registerST1, (List.Cons (registerST2, (List.Cons (registerST3, (List.Cons (registerSST, List.Nil))))))))))))))))))))) (** val registersAllocatable : register List.list **) let registersAllocatable = List.Cons (Register00, (List.Cons (Register01, (List.Cons (Register02, (List.Cons (Register03, (List.Cons (Register04, (List.Cons (Register05, (List.Cons (Register06, (List.Cons (Register07, (List.Cons (Register10, (List.Cons (Register11, (List.Cons (Register12, (List.Cons (Register13, (List.Cons (Register14, (List.Cons (Register15, (List.Cons (Register16, (List.Cons (Register17, (List.Cons (Register20, (List.Cons (Register21, (List.Cons (Register22, (List.Cons (Register23, (List.Cons (Register24, (List.Cons (Register25, (List.Cons (Register26, (List.Cons (Register27, (List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32, (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35, (List.Cons (Register36, (List.Cons (Register37, List.Nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))