open Preamble

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

open Jmeq

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Nat

open I8051

open Order

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Registers

type register_set = { rs_empty : __; rs_singleton : (I8051.register -> __);
                      rs_fold : (__ -> (I8051.register -> __ -> __) -> __ ->
                                __ -> __);
                      rs_insert : (I8051.register -> __ -> __);
                      rs_exists : (I8051.register -> __ -> Bool.bool);
                      rs_union : (__ -> __ -> __);
                      rs_subset : (__ -> __ -> Bool.bool);
                      rs_to_list : (__ -> I8051.register List.list);
                      rs_from_list : (I8051.register List.list -> __) }

(** val register_set_rect_Type4 :
    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    -> register_set -> 'a1 **)
let rec register_set_rect_Type4 h_mk_register_set x_18453 =
  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    rs_from_list = rs_from_list0 } = x_18453
  in
  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
    rs_union0 rs_subset0 rs_to_list0 rs_from_list0

(** val register_set_rect_Type5 :
    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    -> register_set -> 'a1 **)
let rec register_set_rect_Type5 h_mk_register_set x_18455 =
  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    rs_from_list = rs_from_list0 } = x_18455
  in
  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
    rs_union0 rs_subset0 rs_to_list0 rs_from_list0

(** val register_set_rect_Type3 :
    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    -> register_set -> 'a1 **)
let rec register_set_rect_Type3 h_mk_register_set x_18457 =
  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    rs_from_list = rs_from_list0 } = x_18457
  in
  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
    rs_union0 rs_subset0 rs_to_list0 rs_from_list0

(** val register_set_rect_Type2 :
    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    -> register_set -> 'a1 **)
let rec register_set_rect_Type2 h_mk_register_set x_18459 =
  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    rs_from_list = rs_from_list0 } = x_18459
  in
  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
    rs_union0 rs_subset0 rs_to_list0 rs_from_list0

(** val register_set_rect_Type1 :
    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    -> register_set -> 'a1 **)
let rec register_set_rect_Type1 h_mk_register_set x_18461 =
  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    rs_from_list = rs_from_list0 } = x_18461
  in
  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
    rs_union0 rs_subset0 rs_to_list0 rs_from_list0

(** val register_set_rect_Type0 :
    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
    -> register_set -> 'a1 **)
let rec register_set_rect_Type0 h_mk_register_set x_18463 =
  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
    rs_from_list = rs_from_list0 } = x_18463
  in
  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
    rs_union0 rs_subset0 rs_to_list0 rs_from_list0

type rs_set = __

(** val rs_empty : register_set -> __ **)
let rec rs_empty xxx =
  xxx.rs_empty

(** val rs_singleton : register_set -> I8051.register -> __ **)
let rec rs_singleton xxx =
  xxx.rs_singleton

(** val rs_fold0 :
    register_set -> (I8051.register -> 'a1 -> 'a1) -> __ -> 'a1 -> 'a1 **)
let rec rs_fold0 xxx x_18487 x_18488 x_18489 =
  (let { rs_empty = x0; rs_singleton = x1; rs_fold = yyy; rs_insert = x2;
     rs_exists = x3; rs_union = x4; rs_subset = x5; rs_to_list = x6;
     rs_from_list = x7 } = xxx
   in
  Obj.magic yyy) __ x_18487 x_18488 x_18489

(** val rs_insert : register_set -> I8051.register -> __ -> __ **)
let rec rs_insert xxx =
  xxx.rs_insert

(** val rs_exists : register_set -> I8051.register -> __ -> Bool.bool **)
let rec rs_exists xxx =
  xxx.rs_exists

(** val rs_union : register_set -> __ -> __ -> __ **)
let rec rs_union xxx =
  xxx.rs_union

(** val rs_subset : register_set -> __ -> __ -> Bool.bool **)
let rec rs_subset xxx =
  xxx.rs_subset

(** val rs_to_list : register_set -> __ -> I8051.register List.list **)
let rec rs_to_list xxx =
  xxx.rs_to_list

(** val rs_from_list : register_set -> I8051.register List.list -> __ **)
let rec rs_from_list xxx =
  xxx.rs_from_list

(** val register_set_inv_rect_Type4 :
    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
let register_set_inv_rect_Type4 hterm h1 =
  let hcut = register_set_rect_Type4 h1 hterm in hcut __

(** val register_set_inv_rect_Type3 :
    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
let register_set_inv_rect_Type3 hterm h1 =
  let hcut = register_set_rect_Type3 h1 hterm in hcut __

(** val register_set_inv_rect_Type2 :
    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
let register_set_inv_rect_Type2 hterm h1 =
  let hcut = register_set_rect_Type2 h1 hterm in hcut __

(** val register_set_inv_rect_Type1 :
    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
let register_set_inv_rect_Type1 hterm h1 =
  let hcut = register_set_rect_Type1 h1 hterm in hcut __

(** val register_set_inv_rect_Type0 :
    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
let register_set_inv_rect_Type0 hterm h1 =
  let hcut = register_set_rect_Type0 h1 hterm in hcut __

(** val register_set_jmdiscr : register_set -> register_set -> __ **)
let register_set_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { rs_empty = a1; rs_singleton = a2; rs_fold = a3; rs_insert = a4;
       rs_exists = a5; rs_union = a6; rs_subset = a7; rs_to_list = a8;
       rs_from_list = a9 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y

(** val rs_list_set_empty : I8051.register List.list **)
let rs_list_set_empty =
  List.Nil

(** val rs_list_set_singleton :
    I8051.register -> I8051.register List.list **)
let rs_list_set_singleton r =
  List.Cons (r, List.Nil)

(** val rs_list_set_fold :
    (I8051.register -> 'a1 -> 'a1) -> I8051.register List.list -> 'a1 -> 'a1 **)
let rs_list_set_fold f l a =
  List.foldr f a l

(** val rs_list_set_insert :
    I8051.register -> I8051.register List.list -> I8051.register List.list **)
let rs_list_set_insert r s =
  match Util.member I8051.eq_Register r s with
  | Bool.True -> List.Cons (r, s)
  | Bool.False -> s

(** val rs_list_set_exists :
    I8051.register -> I8051.register List.list -> Bool.bool **)
let rs_list_set_exists r s =
  Util.member I8051.eq_Register r s

(** val rs_list_set_union :
    I8051.register List.list -> I8051.register List.list -> I8051.register
    List.list **)
let rs_list_set_union r s =
  Util.nub_by I8051.eq_Register (List.append r s)

(** val rs_list_set_subset :
    I8051.register List.list -> I8051.register List.list -> Bool.bool **)
let rs_list_set_subset r s =
  Util.forall (fun x -> Util.member I8051.eq_Register x s) r

(** val rs_list_set_from_list :
    I8051.register List.list -> I8051.register List.list **)
let rs_list_set_from_list r =
  Util.nub_by I8051.eq_Register r

(** val register_list_set : register_set **)
let register_list_set =
  { rs_empty = (Obj.magic rs_list_set_empty); rs_singleton =
    (Obj.magic rs_list_set_singleton); rs_fold =
    (Obj.magic (fun _ -> rs_list_set_fold)); rs_insert =
    (Obj.magic rs_list_set_insert); rs_exists =
    (Obj.magic rs_list_set_exists); rs_union = (Obj.magic rs_list_set_union);
    rs_subset = (Obj.magic rs_list_set_subset); rs_to_list = (fun x ->
    Obj.magic x); rs_from_list = (Obj.magic rs_list_set_from_list) }