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

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

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

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

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

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

type rs_set 

val rs_empty : register_set -> __

val rs_singleton : register_set -> I8051.register -> __

val rs_fold0 :
  register_set -> (I8051.register -> 'a1 -> 'a1) -> __ -> 'a1 -> 'a1

val rs_insert : register_set -> I8051.register -> __ -> __

val rs_exists : register_set -> I8051.register -> __ -> Bool.bool

val rs_union : register_set -> __ -> __ -> __

val rs_subset : register_set -> __ -> __ -> Bool.bool

val rs_to_list : register_set -> __ -> I8051.register List.list

val rs_from_list : register_set -> I8051.register List.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

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

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

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

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

val register_set_jmdiscr : register_set -> register_set -> __

val rs_list_set_empty : I8051.register List.list

val rs_list_set_singleton : I8051.register -> I8051.register List.list

val rs_list_set_fold :
  (I8051.register -> 'a1 -> 'a1) -> I8051.register List.list -> 'a1 -> 'a1

val rs_list_set_insert :
  I8051.register -> I8051.register List.list -> I8051.register List.list

val rs_list_set_exists :
  I8051.register -> I8051.register List.list -> Bool.bool

val rs_list_set_union :
  I8051.register List.list -> I8051.register List.list -> I8051.register
  List.list

val rs_list_set_subset :
  I8051.register List.list -> I8051.register List.list -> Bool.bool

val rs_list_set_from_list :
  I8051.register List.list -> I8051.register List.list

val register_list_set : register_set