open Preamble

open Types

open Hints_declaration

open Core_notation

open Pts

open Logic

open Jmeq

open Russell

open BitVectorTrie

open String

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open LabelledObjects

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Util

open List

open Lists

open Bool

open Relations

open Nat

open Positive

open Identifiers

open CostLabel

open ASM

type time = Nat.nat

type serialBufferType =
| Eight of BitVector.byte
| Nine of BitVector.bit * BitVector.byte

(** val serialBufferType_rect_Type4 :
    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
    serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
| Eight x_8 -> h_Eight x_8
| Nine (x_10, x_9) -> h_Nine x_10 x_9

(** val serialBufferType_rect_Type5 :
    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
    serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
| Eight x_14 -> h_Eight x_14
| Nine (x_16, x_15) -> h_Nine x_16 x_15

(** val serialBufferType_rect_Type3 :
    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
    serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
| Eight x_20 -> h_Eight x_20
| Nine (x_22, x_21) -> h_Nine x_22 x_21

(** val serialBufferType_rect_Type2 :
    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
    serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
| Eight x_26 -> h_Eight x_26
| Nine (x_28, x_27) -> h_Nine x_28 x_27

(** val serialBufferType_rect_Type1 :
    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
    serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
| Eight x_32 -> h_Eight x_32
| Nine (x_34, x_33) -> h_Nine x_34 x_33

(** val serialBufferType_rect_Type0 :
    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
    serialBufferType -> 'a1 **)
let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
| Eight x_38 -> h_Eight x_38
| Nine (x_40, x_39) -> h_Nine x_40 x_39

(** val serialBufferType_inv_rect_Type4 :
    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
    BitVector.byte -> __ -> 'a1) -> 'a1 **)
let serialBufferType_inv_rect_Type4 hterm h1 h2 =
  let hcut = serialBufferType_rect_Type4 h1 h2 hterm in hcut __

(** val serialBufferType_inv_rect_Type3 :
    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
    BitVector.byte -> __ -> 'a1) -> 'a1 **)
let serialBufferType_inv_rect_Type3 hterm h1 h2 =
  let hcut = serialBufferType_rect_Type3 h1 h2 hterm in hcut __

(** val serialBufferType_inv_rect_Type2 :
    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
    BitVector.byte -> __ -> 'a1) -> 'a1 **)
let serialBufferType_inv_rect_Type2 hterm h1 h2 =
  let hcut = serialBufferType_rect_Type2 h1 h2 hterm in hcut __

(** val serialBufferType_inv_rect_Type1 :
    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
    BitVector.byte -> __ -> 'a1) -> 'a1 **)
let serialBufferType_inv_rect_Type1 hterm h1 h2 =
  let hcut = serialBufferType_rect_Type1 h1 h2 hterm in hcut __

(** val serialBufferType_inv_rect_Type0 :
    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
    BitVector.byte -> __ -> 'a1) -> 'a1 **)
let serialBufferType_inv_rect_Type0 hterm h1 h2 =
  let hcut = serialBufferType_rect_Type0 h1 h2 hterm in hcut __

(** val serialBufferType_discr :
    serialBufferType -> serialBufferType -> __ **)
let serialBufferType_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Eight a0 -> Obj.magic (fun _ dH -> dH __)
     | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val serialBufferType_jmdiscr :
    serialBufferType -> serialBufferType -> __ **)
let serialBufferType_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Eight a0 -> Obj.magic (fun _ dH -> dH __)
     | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

type lineType =
| P1 of BitVector.byte
| P3 of BitVector.byte
| SerialBuffer of serialBufferType

(** val lineType_rect_Type4 :
    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
    -> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
| P1 x_87 -> h_P1 x_87
| P3 x_88 -> h_P3 x_88
| SerialBuffer x_89 -> h_SerialBuffer x_89

(** val lineType_rect_Type5 :
    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
    -> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
| P1 x_94 -> h_P1 x_94
| P3 x_95 -> h_P3 x_95
| SerialBuffer x_96 -> h_SerialBuffer x_96

(** val lineType_rect_Type3 :
    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
    -> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
| P1 x_101 -> h_P1 x_101
| P3 x_102 -> h_P3 x_102
| SerialBuffer x_103 -> h_SerialBuffer x_103

(** val lineType_rect_Type2 :
    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
    -> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
| P1 x_108 -> h_P1 x_108
| P3 x_109 -> h_P3 x_109
| SerialBuffer x_110 -> h_SerialBuffer x_110

(** val lineType_rect_Type1 :
    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
    -> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
| P1 x_115 -> h_P1 x_115
| P3 x_116 -> h_P3 x_116
| SerialBuffer x_117 -> h_SerialBuffer x_117

(** val lineType_rect_Type0 :
    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
    -> 'a1) -> lineType -> 'a1 **)
let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
| P1 x_122 -> h_P1 x_122
| P3 x_123 -> h_P3 x_123
| SerialBuffer x_124 -> h_SerialBuffer x_124

(** val lineType_inv_rect_Type4 :
    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
let lineType_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = lineType_rect_Type4 h1 h2 h3 hterm in hcut __

(** val lineType_inv_rect_Type3 :
    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
let lineType_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = lineType_rect_Type3 h1 h2 h3 hterm in hcut __

(** val lineType_inv_rect_Type2 :
    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
let lineType_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = lineType_rect_Type2 h1 h2 h3 hterm in hcut __

(** val lineType_inv_rect_Type1 :
    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
let lineType_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = lineType_rect_Type1 h1 h2 h3 hterm in hcut __

(** val lineType_inv_rect_Type0 :
    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
let lineType_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = lineType_rect_Type0 h1 h2 h3 hterm in hcut __

(** val lineType_discr : lineType -> lineType -> __ **)
let lineType_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | P1 a0 -> Obj.magic (fun _ dH -> dH __)
     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val lineType_jmdiscr : lineType -> lineType -> __ **)
let lineType_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | P1 a0 -> Obj.magic (fun _ dH -> dH __)
     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y

type sFR8051 =
| SFR_SP
| SFR_DPL
| SFR_DPH
| SFR_PCON
| SFR_TCON
| SFR_TMOD
| SFR_TL0
| SFR_TL1
| SFR_TH0
| SFR_TH1
| SFR_P1
| SFR_SCON
| SFR_SBUF
| SFR_IE
| SFR_P3
| SFR_IP
| SFR_PSW
| SFR_ACC_A
| SFR_ACC_B

(** val sFR8051_rect_Type4 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
let rec sFR8051_rect_Type4 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
| SFR_SP -> h_SFR_SP
| SFR_DPL -> h_SFR_DPL
| SFR_DPH -> h_SFR_DPH
| SFR_PCON -> h_SFR_PCON
| SFR_TCON -> h_SFR_TCON
| SFR_TMOD -> h_SFR_TMOD
| SFR_TL0 -> h_SFR_TL0
| SFR_TL1 -> h_SFR_TL1
| SFR_TH0 -> h_SFR_TH0
| SFR_TH1 -> h_SFR_TH1
| SFR_P1 -> h_SFR_P1
| SFR_SCON -> h_SFR_SCON
| SFR_SBUF -> h_SFR_SBUF
| SFR_IE -> h_SFR_IE
| SFR_P3 -> h_SFR_P3
| SFR_IP -> h_SFR_IP
| SFR_PSW -> h_SFR_PSW
| SFR_ACC_A -> h_SFR_ACC_A
| SFR_ACC_B -> h_SFR_ACC_B

(** val sFR8051_rect_Type5 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
let rec sFR8051_rect_Type5 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
| SFR_SP -> h_SFR_SP
| SFR_DPL -> h_SFR_DPL
| SFR_DPH -> h_SFR_DPH
| SFR_PCON -> h_SFR_PCON
| SFR_TCON -> h_SFR_TCON
| SFR_TMOD -> h_SFR_TMOD
| SFR_TL0 -> h_SFR_TL0
| SFR_TL1 -> h_SFR_TL1
| SFR_TH0 -> h_SFR_TH0
| SFR_TH1 -> h_SFR_TH1
| SFR_P1 -> h_SFR_P1
| SFR_SCON -> h_SFR_SCON
| SFR_SBUF -> h_SFR_SBUF
| SFR_IE -> h_SFR_IE
| SFR_P3 -> h_SFR_P3
| SFR_IP -> h_SFR_IP
| SFR_PSW -> h_SFR_PSW
| SFR_ACC_A -> h_SFR_ACC_A
| SFR_ACC_B -> h_SFR_ACC_B

(** val sFR8051_rect_Type3 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
let rec sFR8051_rect_Type3 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
| SFR_SP -> h_SFR_SP
| SFR_DPL -> h_SFR_DPL
| SFR_DPH -> h_SFR_DPH
| SFR_PCON -> h_SFR_PCON
| SFR_TCON -> h_SFR_TCON
| SFR_TMOD -> h_SFR_TMOD
| SFR_TL0 -> h_SFR_TL0
| SFR_TL1 -> h_SFR_TL1
| SFR_TH0 -> h_SFR_TH0
| SFR_TH1 -> h_SFR_TH1
| SFR_P1 -> h_SFR_P1
| SFR_SCON -> h_SFR_SCON
| SFR_SBUF -> h_SFR_SBUF
| SFR_IE -> h_SFR_IE
| SFR_P3 -> h_SFR_P3
| SFR_IP -> h_SFR_IP
| SFR_PSW -> h_SFR_PSW
| SFR_ACC_A -> h_SFR_ACC_A
| SFR_ACC_B -> h_SFR_ACC_B

(** val sFR8051_rect_Type2 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
let rec sFR8051_rect_Type2 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
| SFR_SP -> h_SFR_SP
| SFR_DPL -> h_SFR_DPL
| SFR_DPH -> h_SFR_DPH
| SFR_PCON -> h_SFR_PCON
| SFR_TCON -> h_SFR_TCON
| SFR_TMOD -> h_SFR_TMOD
| SFR_TL0 -> h_SFR_TL0
| SFR_TL1 -> h_SFR_TL1
| SFR_TH0 -> h_SFR_TH0
| SFR_TH1 -> h_SFR_TH1
| SFR_P1 -> h_SFR_P1
| SFR_SCON -> h_SFR_SCON
| SFR_SBUF -> h_SFR_SBUF
| SFR_IE -> h_SFR_IE
| SFR_P3 -> h_SFR_P3
| SFR_IP -> h_SFR_IP
| SFR_PSW -> h_SFR_PSW
| SFR_ACC_A -> h_SFR_ACC_A
| SFR_ACC_B -> h_SFR_ACC_B

(** val sFR8051_rect_Type1 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
let rec sFR8051_rect_Type1 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
| SFR_SP -> h_SFR_SP
| SFR_DPL -> h_SFR_DPL
| SFR_DPH -> h_SFR_DPH
| SFR_PCON -> h_SFR_PCON
| SFR_TCON -> h_SFR_TCON
| SFR_TMOD -> h_SFR_TMOD
| SFR_TL0 -> h_SFR_TL0
| SFR_TL1 -> h_SFR_TL1
| SFR_TH0 -> h_SFR_TH0
| SFR_TH1 -> h_SFR_TH1
| SFR_P1 -> h_SFR_P1
| SFR_SCON -> h_SFR_SCON
| SFR_SBUF -> h_SFR_SBUF
| SFR_IE -> h_SFR_IE
| SFR_P3 -> h_SFR_P3
| SFR_IP -> h_SFR_IP
| SFR_PSW -> h_SFR_PSW
| SFR_ACC_A -> h_SFR_ACC_A
| SFR_ACC_B -> h_SFR_ACC_B

(** val sFR8051_rect_Type0 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
let rec sFR8051_rect_Type0 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
| SFR_SP -> h_SFR_SP
| SFR_DPL -> h_SFR_DPL
| SFR_DPH -> h_SFR_DPH
| SFR_PCON -> h_SFR_PCON
| SFR_TCON -> h_SFR_TCON
| SFR_TMOD -> h_SFR_TMOD
| SFR_TL0 -> h_SFR_TL0
| SFR_TL1 -> h_SFR_TL1
| SFR_TH0 -> h_SFR_TH0
| SFR_TH1 -> h_SFR_TH1
| SFR_P1 -> h_SFR_P1
| SFR_SCON -> h_SFR_SCON
| SFR_SBUF -> h_SFR_SBUF
| SFR_IE -> h_SFR_IE
| SFR_P3 -> h_SFR_P3
| SFR_IP -> h_SFR_IP
| SFR_PSW -> h_SFR_PSW
| SFR_ACC_A -> h_SFR_ACC_A
| SFR_ACC_B -> h_SFR_ACC_B

(** val sFR8051_inv_rect_Type4 :
    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
let sFR8051_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    sFR8051_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val sFR8051_inv_rect_Type3 :
    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
let sFR8051_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    sFR8051_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val sFR8051_inv_rect_Type2 :
    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
let sFR8051_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    sFR8051_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val sFR8051_inv_rect_Type1 :
    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
let sFR8051_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    sFR8051_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val sFR8051_inv_rect_Type0 :
    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> 'a1 **)
let sFR8051_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
  let hcut =
    sFR8051_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
      h17 h18 h19 hterm
  in
  hcut __

(** val sFR8051_discr : sFR8051 -> sFR8051 -> __ **)
let sFR8051_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | SFR_SP -> Obj.magic (fun _ dH -> dH)
     | SFR_DPL -> Obj.magic (fun _ dH -> dH)
     | SFR_DPH -> Obj.magic (fun _ dH -> dH)
     | SFR_PCON -> Obj.magic (fun _ dH -> dH)
     | SFR_TCON -> Obj.magic (fun _ dH -> dH)
     | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
     | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
     | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
     | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
     | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
     | SFR_P1 -> Obj.magic (fun _ dH -> dH)
     | SFR_SCON -> Obj.magic (fun _ dH -> dH)
     | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
     | SFR_IE -> Obj.magic (fun _ dH -> dH)
     | SFR_P3 -> Obj.magic (fun _ dH -> dH)
     | SFR_IP -> Obj.magic (fun _ dH -> dH)
     | SFR_PSW -> Obj.magic (fun _ dH -> dH)
     | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
     | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y

(** val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __ **)
let sFR8051_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | SFR_SP -> Obj.magic (fun _ dH -> dH)
     | SFR_DPL -> Obj.magic (fun _ dH -> dH)
     | SFR_DPH -> Obj.magic (fun _ dH -> dH)
     | SFR_PCON -> Obj.magic (fun _ dH -> dH)
     | SFR_TCON -> Obj.magic (fun _ dH -> dH)
     | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
     | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
     | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
     | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
     | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
     | SFR_P1 -> Obj.magic (fun _ dH -> dH)
     | SFR_SCON -> Obj.magic (fun _ dH -> dH)
     | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
     | SFR_IE -> Obj.magic (fun _ dH -> dH)
     | SFR_P3 -> Obj.magic (fun _ dH -> dH)
     | SFR_IP -> Obj.magic (fun _ dH -> dH)
     | SFR_PSW -> Obj.magic (fun _ dH -> dH)
     | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
     | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y

(** val sfr_8051_index : sFR8051 -> Nat.nat **)
let sfr_8051_index = function
| SFR_SP -> Nat.O
| SFR_DPL -> Nat.S Nat.O
| SFR_DPH -> Nat.S (Nat.S Nat.O)
| SFR_PCON -> Nat.S (Nat.S (Nat.S Nat.O))
| SFR_TCON -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
| SFR_TMOD -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
| SFR_TL0 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
| SFR_TL1 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
| SFR_TH0 ->
  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
| SFR_TH1 ->
  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
| SFR_P1 ->
  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))))
| SFR_SCON ->
  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O))))))))))
| SFR_SBUF ->
  Nat.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)))))))))))
| SFR_IE ->
  Nat.S (Nat.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))))))))))))
| SFR_P3 ->
  Nat.S (Nat.S (Nat.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)))))))))))))
| SFR_IP ->
  Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))
| SFR_PSW ->
  Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))
| SFR_ACC_A ->
  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))
| SFR_ACC_B ->
  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))))

type sFR8052 =
| SFR_T2CON
| SFR_RCAP2L
| SFR_RCAP2H
| SFR_TL2
| SFR_TH2

(** val sFR8052_rect_Type4 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
let rec sFR8052_rect_Type4 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
| SFR_T2CON -> h_SFR_T2CON
| SFR_RCAP2L -> h_SFR_RCAP2L
| SFR_RCAP2H -> h_SFR_RCAP2H
| SFR_TL2 -> h_SFR_TL2
| SFR_TH2 -> h_SFR_TH2

(** val sFR8052_rect_Type5 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
let rec sFR8052_rect_Type5 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
| SFR_T2CON -> h_SFR_T2CON
| SFR_RCAP2L -> h_SFR_RCAP2L
| SFR_RCAP2H -> h_SFR_RCAP2H
| SFR_TL2 -> h_SFR_TL2
| SFR_TH2 -> h_SFR_TH2

(** val sFR8052_rect_Type3 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
let rec sFR8052_rect_Type3 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
| SFR_T2CON -> h_SFR_T2CON
| SFR_RCAP2L -> h_SFR_RCAP2L
| SFR_RCAP2H -> h_SFR_RCAP2H
| SFR_TL2 -> h_SFR_TL2
| SFR_TH2 -> h_SFR_TH2

(** val sFR8052_rect_Type2 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
let rec sFR8052_rect_Type2 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
| SFR_T2CON -> h_SFR_T2CON
| SFR_RCAP2L -> h_SFR_RCAP2L
| SFR_RCAP2H -> h_SFR_RCAP2H
| SFR_TL2 -> h_SFR_TL2
| SFR_TH2 -> h_SFR_TH2

(** val sFR8052_rect_Type1 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
let rec sFR8052_rect_Type1 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
| SFR_T2CON -> h_SFR_T2CON
| SFR_RCAP2L -> h_SFR_RCAP2L
| SFR_RCAP2H -> h_SFR_RCAP2H
| SFR_TL2 -> h_SFR_TL2
| SFR_TH2 -> h_SFR_TH2

(** val sFR8052_rect_Type0 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
let rec sFR8052_rect_Type0 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
| SFR_T2CON -> h_SFR_T2CON
| SFR_RCAP2L -> h_SFR_RCAP2L
| SFR_RCAP2H -> h_SFR_RCAP2H
| SFR_TL2 -> h_SFR_TL2
| SFR_TH2 -> h_SFR_TH2

(** val sFR8052_inv_rect_Type4 :
    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let sFR8052_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
  let hcut = sFR8052_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __

(** val sFR8052_inv_rect_Type3 :
    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let sFR8052_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
  let hcut = sFR8052_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __

(** val sFR8052_inv_rect_Type2 :
    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let sFR8052_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
  let hcut = sFR8052_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __

(** val sFR8052_inv_rect_Type1 :
    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let sFR8052_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
  let hcut = sFR8052_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __

(** val sFR8052_inv_rect_Type0 :
    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> 'a1 **)
let sFR8052_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
  let hcut = sFR8052_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __

(** val sFR8052_discr : sFR8052 -> sFR8052 -> __ **)
let sFR8052_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
     | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
     | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
     | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
     | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y

(** val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __ **)
let sFR8052_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
     | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
     | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
     | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
     | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y

(** val sfr_8052_index : sFR8052 -> Nat.nat **)
let sfr_8052_index = function
| SFR_T2CON -> Nat.O
| SFR_RCAP2L -> Nat.S Nat.O
| SFR_RCAP2H -> Nat.S (Nat.S Nat.O)
| SFR_TL2 -> Nat.S (Nat.S (Nat.S Nat.O))
| SFR_TH2 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))

type 'm preStatus = { low_internal_ram : BitVector.byte
                                         BitVectorTrie.bitVectorTrie;
                      high_internal_ram : BitVector.byte
                                          BitVectorTrie.bitVectorTrie;
                      external_ram : BitVector.byte
                                     BitVectorTrie.bitVectorTrie;
                      program_counter : BitVector.word;
                      special_function_registers_8051 : BitVector.byte
                                                        Vector.vector;
                      special_function_registers_8052 : BitVector.byte
                                                        Vector.vector;
                      p1_latch : BitVector.byte; p3_latch : BitVector.byte;
                      clock : time }

(** val preStatus_rect_Type4 :
    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    preStatus -> 'a2 **)
let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_510 =
  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    high_internal_ram0; external_ram = external_ram0; program_counter =
    program_counter0; special_function_registers_8051 =
    special_function_registers_8053; special_function_registers_8052 =
    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    p3_latch0; clock = clock0 } = x_510
  in
  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
    program_counter0 special_function_registers_8053
    special_function_registers_8054 p1_latch0 p3_latch0 clock0

(** val preStatus_rect_Type5 :
    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    preStatus -> 'a2 **)
let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_512 =
  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    high_internal_ram0; external_ram = external_ram0; program_counter =
    program_counter0; special_function_registers_8051 =
    special_function_registers_8053; special_function_registers_8052 =
    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    p3_latch0; clock = clock0 } = x_512
  in
  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
    program_counter0 special_function_registers_8053
    special_function_registers_8054 p1_latch0 p3_latch0 clock0

(** val preStatus_rect_Type3 :
    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    preStatus -> 'a2 **)
let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_514 =
  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    high_internal_ram0; external_ram = external_ram0; program_counter =
    program_counter0; special_function_registers_8051 =
    special_function_registers_8053; special_function_registers_8052 =
    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    p3_latch0; clock = clock0 } = x_514
  in
  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
    program_counter0 special_function_registers_8053
    special_function_registers_8054 p1_latch0 p3_latch0 clock0

(** val preStatus_rect_Type2 :
    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    preStatus -> 'a2 **)
let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_516 =
  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    high_internal_ram0; external_ram = external_ram0; program_counter =
    program_counter0; special_function_registers_8051 =
    special_function_registers_8053; special_function_registers_8052 =
    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    p3_latch0; clock = clock0 } = x_516
  in
  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
    program_counter0 special_function_registers_8053
    special_function_registers_8054 p1_latch0 p3_latch0 clock0

(** val preStatus_rect_Type1 :
    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    preStatus -> 'a2 **)
let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_518 =
  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    high_internal_ram0; external_ram = external_ram0; program_counter =
    program_counter0; special_function_registers_8051 =
    special_function_registers_8053; special_function_registers_8052 =
    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    p3_latch0; clock = clock0 } = x_518
  in
  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
    program_counter0 special_function_registers_8053
    special_function_registers_8054 p1_latch0 p3_latch0 clock0

(** val preStatus_rect_Type0 :
    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    preStatus -> 'a2 **)
let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_520 =
  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    high_internal_ram0; external_ram = external_ram0; program_counter =
    program_counter0; special_function_registers_8051 =
    special_function_registers_8053; special_function_registers_8052 =
    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    p3_latch0; clock = clock0 } = x_520
  in
  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
    program_counter0 special_function_registers_8053
    special_function_registers_8054 p1_latch0 p3_latch0 clock0

(** val low_internal_ram :
    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
let rec low_internal_ram code_memory xxx =
  xxx.low_internal_ram

(** val high_internal_ram :
    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
let rec high_internal_ram code_memory xxx =
  xxx.high_internal_ram

(** val external_ram :
    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
let rec external_ram code_memory xxx =
  xxx.external_ram

(** val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word **)
let rec program_counter code_memory xxx =
  xxx.program_counter

(** val special_function_registers_8051 :
    'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
let rec special_function_registers_8051 code_memory xxx =
  xxx.special_function_registers_8051

(** val special_function_registers_8052 :
    'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
let rec special_function_registers_8052 code_memory xxx =
  xxx.special_function_registers_8052

(** val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
let rec p1_latch code_memory xxx =
  xxx.p1_latch

(** val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
let rec p3_latch code_memory xxx =
  xxx.p3_latch

(** val clock : 'a1 -> 'a1 preStatus -> time **)
let rec clock code_memory xxx =
  xxx.clock

(** val preStatus_inv_rect_Type4 :
    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
let preStatus_inv_rect_Type4 x2 hterm h1 =
  let hcut = preStatus_rect_Type4 x2 h1 hterm in hcut __

(** val preStatus_inv_rect_Type3 :
    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
let preStatus_inv_rect_Type3 x2 hterm h1 =
  let hcut = preStatus_rect_Type3 x2 h1 hterm in hcut __

(** val preStatus_inv_rect_Type2 :
    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
let preStatus_inv_rect_Type2 x2 hterm h1 =
  let hcut = preStatus_rect_Type2 x2 h1 hterm in hcut __

(** val preStatus_inv_rect_Type1 :
    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
let preStatus_inv_rect_Type1 x2 hterm h1 =
  let hcut = preStatus_rect_Type1 x2 h1 hterm in hcut __

(** val preStatus_inv_rect_Type0 :
    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
let preStatus_inv_rect_Type0 x2 hterm h1 =
  let hcut = preStatus_rect_Type0 x2 h1 hterm in hcut __

(** val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __ **)
let preStatus_jmdiscr a2 x y =
  Logic.eq_rect_Type2 x
    (let { low_internal_ram = a0; high_internal_ram = a10; external_ram =
       a20; program_counter = a3; special_function_registers_8051 = a4;
       special_function_registers_8052 = a5; p1_latch = a6; p3_latch = a7;
       clock = a8 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y

type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus

type pseudoStatus = ASM.pseudo_assembly_program preStatus

(** val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus **)
let set_clock code_memory s t =
  let old_low_internal_ram = s.low_internal_ram in
  let old_high_internal_ram = s.high_internal_ram in
  let old_external_ram = s.external_ram in
  let old_program_counter = s.program_counter in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let old_p1_latch = s.p1_latch in
  let old_p3_latch = s.p3_latch in
  { low_internal_ram = old_low_internal_ram; high_internal_ram =
  old_high_internal_ram; external_ram = old_external_ram; program_counter =
  old_program_counter; special_function_registers_8051 =
  old_special_function_registers_8051; special_function_registers_8052 =
  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
  old_p3_latch; clock = t }

(** val set_p1_latch :
    'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
let set_p1_latch code_memory s b =
  let old_low_internal_ram = s.low_internal_ram in
  let old_high_internal_ram = s.high_internal_ram in
  let old_external_ram = s.external_ram in
  let old_program_counter = s.program_counter in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let old_p3_latch = s.p3_latch in
  let old_clock = s.clock in
  { low_internal_ram = old_low_internal_ram; high_internal_ram =
  old_high_internal_ram; external_ram = old_external_ram; program_counter =
  old_program_counter; special_function_registers_8051 =
  old_special_function_registers_8051; special_function_registers_8052 =
  old_special_function_registers_8052; p1_latch = b; p3_latch = old_p3_latch;
  clock = old_clock }

(** val set_p3_latch :
    'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
let set_p3_latch code_memory s b =
  let old_low_internal_ram = s.low_internal_ram in
  let old_high_internal_ram = s.high_internal_ram in
  let old_external_ram = s.external_ram in
  let old_program_counter = s.program_counter in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let old_p1_latch = s.p1_latch in
  let old_clock = s.clock in
  { low_internal_ram = old_low_internal_ram; high_internal_ram =
  old_high_internal_ram; external_ram = old_external_ram; program_counter =
  old_program_counter; special_function_registers_8051 =
  old_special_function_registers_8051; special_function_registers_8052 =
  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch = b;
  clock = old_clock }

(** val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte **)
let get_8051_sfr code_memory s i =
  let sfr = s.special_function_registers_8051 in
  let index = sfr_8051_index i in
  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))))) sfr index

(** val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte **)
let get_8052_sfr code_memory s i =
  let sfr = s.special_function_registers_8052 in
  let index = sfr_8052_index i in
  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) sfr index

(** val set_8051_sfr :
    'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus **)
let set_8051_sfr code_memory s i b =
  let index = sfr_8051_index i in
  let old_low_internal_ram = s.low_internal_ram in
  let old_high_internal_ram = s.high_internal_ram in
  let old_external_ram = s.external_ram in
  let old_program_counter = s.program_counter in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let new_special_function_registers_8051 =
    Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))))) old_special_function_registers_8051
      index b
  in
  let old_p1_latch = s.p1_latch in
  let old_p3_latch = s.p3_latch in
  let old_clock = s.clock in
  { low_internal_ram = old_low_internal_ram; high_internal_ram =
  old_high_internal_ram; external_ram = old_external_ram; program_counter =
  old_program_counter; special_function_registers_8051 =
  new_special_function_registers_8051; special_function_registers_8052 =
  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
  old_p3_latch; clock = old_clock }

(** val set_8052_sfr :
    'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus **)
let set_8052_sfr code_memory s i b =
  let index = sfr_8052_index i in
  let old_low_internal_ram = s.low_internal_ram in
  let old_high_internal_ram = s.high_internal_ram in
  let old_external_ram = s.external_ram in
  let old_program_counter = s.program_counter in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let new_special_function_registers_8052 =
    Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
      old_special_function_registers_8052 index b
  in
  let old_p1_latch = s.p1_latch in
  let old_p3_latch = s.p3_latch in
  let old_clock = s.clock in
  { low_internal_ram = old_low_internal_ram; high_internal_ram =
  old_high_internal_ram; external_ram = old_external_ram; program_counter =
  old_program_counter; special_function_registers_8051 =
  old_special_function_registers_8051; special_function_registers_8052 =
  new_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
  old_p3_latch; clock = old_clock }

(** val set_program_counter :
    'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus **)
let set_program_counter code_memory s w =
  let old_low_internal_ram = s.low_internal_ram in
  let old_high_internal_ram = s.high_internal_ram in
  let old_external_ram = s.external_ram in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let old_p1_latch = s.p1_latch in
  let old_p3_latch = s.p3_latch in
  let old_clock = s.clock in
  { low_internal_ram = old_low_internal_ram; high_internal_ram =
  old_high_internal_ram; external_ram = old_external_ram; program_counter =
  w; special_function_registers_8051 = old_special_function_registers_8051;
  special_function_registers_8052 = old_special_function_registers_8052;
  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }

(** val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus **)
let set_code_memory code_memory s r =
  let old_low_internal_ram = s.low_internal_ram in
  let old_high_internal_ram = s.high_internal_ram in
  let old_external_ram = s.external_ram in
  let old_program_counter = s.program_counter in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let old_p1_latch = s.p1_latch in
  let old_p3_latch = s.p3_latch in
  let old_clock = s.clock in
  { low_internal_ram = old_low_internal_ram; high_internal_ram =
  old_high_internal_ram; external_ram = old_external_ram; program_counter =
  old_program_counter; special_function_registers_8051 =
  old_special_function_registers_8051; special_function_registers_8052 =
  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
  old_p3_latch; clock = old_clock }

(** val set_low_internal_ram :
    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
    preStatus **)
let set_low_internal_ram code_memory s r =
  let old_high_internal_ram = s.high_internal_ram in
  let old_external_ram = s.external_ram in
  let old_program_counter = s.program_counter in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let old_p1_latch = s.p1_latch in
  let old_p3_latch = s.p3_latch in
  let old_clock = s.clock in
  { low_internal_ram = r; high_internal_ram = old_high_internal_ram;
  external_ram = old_external_ram; program_counter = old_program_counter;
  special_function_registers_8051 = old_special_function_registers_8051;
  special_function_registers_8052 = old_special_function_registers_8052;
  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }

(** val update_low_internal_ram :
    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
    preStatus **)
let update_low_internal_ram code_memory s addr v =
  let old_low_internal_ram = s.low_internal_ram in
  let new_low_internal_ram =
    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O))))))) addr v old_low_internal_ram
  in
  set_low_internal_ram code_memory s new_low_internal_ram

(** val set_high_internal_ram :
    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
    preStatus **)
let set_high_internal_ram code_memory s r =
  let old_low_internal_ram = s.low_internal_ram in
  let old_high_internal_ram = s.high_internal_ram in
  let old_external_ram = s.external_ram in
  let old_program_counter = s.program_counter in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let old_p1_latch = s.p1_latch in
  let old_p3_latch = s.p3_latch in
  let old_clock = s.clock in
  { low_internal_ram = old_low_internal_ram; high_internal_ram = r;
  external_ram = old_external_ram; program_counter = old_program_counter;
  special_function_registers_8051 = old_special_function_registers_8051;
  special_function_registers_8052 = old_special_function_registers_8052;
  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }

(** val update_high_internal_ram :
    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
    preStatus **)
let update_high_internal_ram code_memory s addr v =
  let old_high_internal_ram = s.high_internal_ram in
  let new_high_internal_ram =
    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O))))))) addr v old_high_internal_ram
  in
  set_high_internal_ram code_memory s new_high_internal_ram

(** val set_external_ram :
    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
    preStatus **)
let set_external_ram code_memory s r =
  let old_low_internal_ram = s.low_internal_ram in
  let old_high_internal_ram = s.high_internal_ram in
  let old_program_counter = s.program_counter in
  let old_special_function_registers_8051 = s.special_function_registers_8051
  in
  let old_special_function_registers_8052 = s.special_function_registers_8052
  in
  let old_p1_latch = s.p1_latch in
  let old_p3_latch = s.p3_latch in
  let old_clock = s.clock in
  { low_internal_ram = old_low_internal_ram; high_internal_ram =
  old_high_internal_ram; external_ram = r; program_counter =
  old_program_counter; special_function_registers_8051 =
  old_special_function_registers_8051; special_function_registers_8052 =
  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
  old_p3_latch; clock = old_clock }

(** val update_external_ram :
    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
    preStatus **)
let update_external_ram code_memory s addr v =
  let old_external_ram = s.external_ram in
  let new_external_ram =
    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))) addr v old_external_ram
  in
  set_external_ram code_memory s new_external_ram

(** val get_psw_flags : 'a1 -> 'a1 preStatus -> Nat.nat -> Bool.bool **)
let get_psw_flags code_memory s flag =
  let psw = get_8051_sfr code_memory s SFR_PSW in
  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))) psw flag

(** val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
let get_cy_flag code_memory s =
  get_psw_flags code_memory s Nat.O

(** val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
let get_ac_flag code_memory s =
  get_psw_flags code_memory s (Nat.S Nat.O)

(** val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
let get_fo_flag code_memory s =
  get_psw_flags code_memory s (Nat.S (Nat.S Nat.O))

(** val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
let get_rs1_flag code_memory s =
  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S Nat.O)))

(** val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
let get_rs0_flag code_memory s =
  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))

(** val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
let get_ov_flag code_memory s =
  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))

(** val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
let get_ud_flag code_memory s =
  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O))))))

(** val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
let get_p_flag code_memory s =
  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S Nat.O)))))))

(** val set_flags :
    'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
    BitVector.bit -> 'a1 preStatus **)
let set_flags code_memory s cy ac ov =
  let old_cy = get_cy_flag code_memory s in
  let old_ac = get_ac_flag code_memory s in
  let old_fo = get_fo_flag code_memory s in
  let old_rs1 = get_rs1_flag code_memory s in
  let old_rs0 = get_rs0_flag code_memory s in
  let old_ov = get_ov_flag code_memory s in
  let old_ud = get_ud_flag code_memory s in
  let old_p = get_p_flag code_memory s in
  let new_ac =
    match ac with
    | Types.None -> old_ac
    | Types.Some j -> j
  in
  set_8051_sfr code_memory s SFR_PSW (Vector.VCons ((Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), cy, (Vector.VCons ((Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), new_ac, (Vector.VCons
    ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), old_fo, (Vector.VCons
    ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), old_rs1, (Vector.VCons ((Nat.S
    (Nat.S (Nat.S Nat.O))), old_rs0, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
    ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O, old_p,
    Vector.VEmpty))))))))))))))))

(** val initialise_status : 'a1 -> 'a1 preStatus **)
let initialise_status code_mem =
  let status0 = { low_internal_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))); high_internal_ram =
    (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))); external_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.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))))))))))))))))); program_counter =
    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))); special_function_registers_8051 =
    (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))))))
      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))); special_function_registers_8052 =
    (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))); p1_latch =
    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O))))))))); p3_latch =
    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O))))))))); clock = Nat.O }
  in
  set_8051_sfr code_mem status0 SFR_SP
    (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.S (Nat.S (Nat.S (Nat.S
      (Nat.S Nat.O))))))))

(** val sfr_of_Byte :
    BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option **)
let sfr_of_Byte b =
  let address =
    Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S Nat.O)))))))) b
  in
  (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
   | Bool.True -> Types.None
   | Bool.False ->
     (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
      | Bool.True -> Types.Some (Types.Inl SFR_P1)
      | Bool.False ->
        (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
         | Bool.True -> Types.None
         | Bool.False ->
           (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
            | Bool.True -> Types.Some (Types.Inl SFR_P3)
            | Bool.False ->
              (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
               | Bool.True -> Types.Some (Types.Inl SFR_SBUF)
               | Bool.False ->
                 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                  | Bool.True -> Types.Some (Types.Inl SFR_TL0)
                  | Bool.False ->
                    (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                             (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                     | Bool.True -> Types.Some (Types.Inl SFR_TL1)
                     | Bool.False ->
                       (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                        | Bool.True -> Types.Some (Types.Inl SFR_TH0)
                        | Bool.False ->
                          (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                           | Bool.True -> Types.Some (Types.Inl SFR_TH1)
                           | Bool.False ->
                             (match Nat.eqb address (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                      (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                              | Bool.True -> Types.Some (Types.Inr SFR_T2CON)
                              | Bool.False ->
                                (match Nat.eqb address (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                                         (Nat.S (Nat.S (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                 | Bool.True ->
                                   Types.Some (Types.Inr SFR_RCAP2L)
                                 | Bool.False ->
                                   (match Nat.eqb address (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.S (Nat.S (Nat.S
                                            (Nat.S (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                    | Bool.True ->
                                      Types.Some (Types.Inr SFR_RCAP2H)
                                    | Bool.False ->
                                      (match Nat.eqb address (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.S (Nat.S
                                               (Nat.S (Nat.S (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                       | Bool.True ->
                                         Types.Some (Types.Inr SFR_TL2)
                                       | Bool.False ->
                                         (match Nat.eqb address (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.S
                                                  (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                          | Bool.True ->
                                            Types.Some (Types.Inr SFR_TH2)
                                          | Bool.False ->
                                            (match Nat.eqb address (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.S
                                                     (Nat.S (Nat.S (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                             | Bool.True ->
                                               Types.Some (Types.Inl
                                                 SFR_PCON)
                                             | Bool.False ->
                                               (match Nat.eqb address (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.S (Nat.S (Nat.S
                                                        (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                | Bool.True ->
                                                  Types.Some (Types.Inl
                                                    SFR_TCON)
                                                | Bool.False ->
                                                  (match Nat.eqb address
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.S
                                                           (Nat.S (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                   | Bool.True ->
                                                     Types.Some (Types.Inl
                                                       SFR_TMOD)
                                                   | Bool.False ->
                                                     (match Nat.eqb address
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.S (Nat.S
                                                              (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                      | Bool.True ->
                                                        Types.Some (Types.Inl
                                                          SFR_SCON)
                                                      | Bool.False ->
                                                        (match Nat.eqb
                                                                 address
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                         | Bool.True ->
                                                           Types.Some
                                                             (Types.Inl
                                                             SFR_IE)
                                                         | Bool.False ->
                                                           (match Nat.eqb
                                                                    address
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                            | Bool.True ->
                                                              Types.Some
                                                                (Types.Inl
                                                                SFR_IP)
                                                            | Bool.False ->
                                                              (match 
                                                               Nat.eqb
                                                                 address
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.S
                                                                 (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                               | Bool.True ->
                                                                 Types.Some
                                                                   (Types.Inl
                                                                   SFR_SP)
                                                               | Bool.False ->
                                                                 (match 
                                                                  Nat.eqb
                                                                    address
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                                  | Bool.True ->
                                                                    Types.Some
                                                                    (Types.Inl
                                                                    SFR_DPL)
                                                                  | Bool.False ->
                                                                    (match 
                                                                    Nat.eqb
                                                                    address
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                                    | Bool.True ->
                                                                    Types.Some
                                                                    (Types.Inl
                                                                    SFR_DPH)
                                                                    | Bool.False ->
                                                                    (match 
                                                                    Nat.eqb
                                                                    address
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                                    | Bool.True ->
                                                                    Types.Some
                                                                    (Types.Inl
                                                                    SFR_PSW)
                                                                    | Bool.False ->
                                                                    (match 
                                                                    Nat.eqb
                                                                    address
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                                    | Bool.True ->
                                                                    Types.Some
                                                                    (Types.Inl
                                                                    SFR_ACC_A)
                                                                    | Bool.False ->
                                                                    (match 
                                                                    Nat.eqb
                                                                    address
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.S
                                                                    (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
                                                                    | Bool.True ->
                                                                    Types.Some
                                                                    (Types.Inl
                                                                    SFR_ACC_B)
                                                                    | Bool.False ->
                                                                    Types.None))))))))))))))))))))))))))

(** val get_bit_addressable_sfr :
    'a1 -> 'a1 preStatus -> BitVector.byte -> Bool.bool -> BitVector.byte **)
let get_bit_addressable_sfr code_memory s b l =
  match sfr_of_Byte b with
  | Types.None -> assert false (* absurd case *)
  | Types.Some sfr8051_8052 ->
    (match sfr8051_8052 with
     | Types.Inl sfr ->
       (match sfr with
        | SFR_SP -> get_8051_sfr code_memory s sfr
        | SFR_DPL -> get_8051_sfr code_memory s sfr
        | SFR_DPH -> get_8051_sfr code_memory s sfr
        | SFR_PCON -> get_8051_sfr code_memory s sfr
        | SFR_TCON -> get_8051_sfr code_memory s sfr
        | SFR_TMOD -> get_8051_sfr code_memory s sfr
        | SFR_TL0 -> get_8051_sfr code_memory s sfr
        | SFR_TL1 -> get_8051_sfr code_memory s sfr
        | SFR_TH0 -> get_8051_sfr code_memory s sfr
        | SFR_TH1 -> get_8051_sfr code_memory s sfr
        | SFR_P1 ->
          (match l with
           | Bool.True -> s.p1_latch
           | Bool.False -> get_8051_sfr code_memory s SFR_P1)
        | SFR_SCON -> get_8051_sfr code_memory s sfr
        | SFR_SBUF -> get_8051_sfr code_memory s sfr
        | SFR_IE -> get_8051_sfr code_memory s sfr
        | SFR_P3 ->
          (match l with
           | Bool.True -> s.p3_latch
           | Bool.False -> get_8051_sfr code_memory s SFR_P3)
        | SFR_IP -> get_8051_sfr code_memory s sfr
        | SFR_PSW -> get_8051_sfr code_memory s sfr
        | SFR_ACC_A -> get_8051_sfr code_memory s sfr
        | SFR_ACC_B -> get_8051_sfr code_memory s sfr)
     | Types.Inr sfr -> get_8052_sfr code_memory s sfr)

(** val set_bit_addressable_sfr :
    'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte -> 'a1 preStatus **)
let set_bit_addressable_sfr code_memory s b v =
  match sfr_of_Byte b with
  | Types.None -> assert false (* absurd case *)
  | Types.Some sfr8051_8052 ->
    (match sfr8051_8052 with
     | Types.Inl sfr ->
       (match sfr with
        | SFR_SP -> set_8051_sfr code_memory s sfr v
        | SFR_DPL -> set_8051_sfr code_memory s sfr v
        | SFR_DPH -> set_8051_sfr code_memory s sfr v
        | SFR_PCON -> set_8051_sfr code_memory s sfr v
        | SFR_TCON -> set_8051_sfr code_memory s sfr v
        | SFR_TMOD -> set_8051_sfr code_memory s sfr v
        | SFR_TL0 -> set_8051_sfr code_memory s sfr v
        | SFR_TL1 -> set_8051_sfr code_memory s sfr v
        | SFR_TH0 -> set_8051_sfr code_memory s sfr v
        | SFR_TH1 -> set_8051_sfr code_memory s sfr v
        | SFR_P1 ->
          let status_1 = set_8051_sfr code_memory s SFR_P1 v in
          set_p1_latch code_memory s v
        | SFR_SCON -> set_8051_sfr code_memory s sfr v
        | SFR_SBUF -> set_8051_sfr code_memory s sfr v
        | SFR_IE -> set_8051_sfr code_memory s sfr v
        | SFR_P3 ->
          let status_1 = set_8051_sfr code_memory s SFR_P3 v in
          set_p3_latch code_memory s v
        | SFR_IP -> set_8051_sfr code_memory s sfr v
        | SFR_PSW -> set_8051_sfr code_memory s sfr v
        | SFR_ACC_A -> set_8051_sfr code_memory s sfr v
        | SFR_ACC_B -> set_8051_sfr code_memory s sfr v)
     | Types.Inr sfr -> set_8052_sfr code_memory s sfr v)

(** val bit_address_of_register :
    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.bitVector **)
let bit_address_of_register code_memory s r =
  let b = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r Nat.O in
  let c = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r (Nat.S Nat.O) in
  let d =
    Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r (Nat.S (Nat.S Nat.O))
  in
  let r1 = get_rs1_flag code_memory s in
  let r0 = get_rs0_flag code_memory s in
  let offset =
    match Bool.andb (Bool.notb r1) (Bool.notb r0) with
    | Bool.True -> Nat.O
    | Bool.False ->
      (match Bool.andb (Bool.notb r1) r0 with
       | Bool.True ->
         Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
       | Bool.False ->
         (match Bool.andb r1 r0 with
          | Bool.True ->
            Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))))))))))
          | Bool.False ->
            Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))))
  in
  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S Nat.O)))))))
    (Nat.plus offset
      (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
        (Vector.VCons ((Nat.S (Nat.S Nat.O)), b, (Vector.VCons ((Nat.S
        Nat.O), c, (Vector.VCons (Nat.O, d, Vector.VEmpty))))))))))

(** val get_register :
    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte **)
let get_register code_memory s r =
  let address = bit_address_of_register code_memory s r in
  BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O))))))) address s.low_internal_ram
    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))

(** val set_register :
    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
    preStatus **)
let set_register code_memory s r v =
  let address = bit_address_of_register code_memory s r in
  update_low_internal_ram code_memory s address v

(** val read_from_external_ram :
    'a1 -> 'a1 preStatus -> BitVector.word -> BitVector.byte **)
let read_from_external_ram code_memory s addr =
  BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))) addr s.external_ram
    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))

(** val read_from_internal_ram :
    'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte **)
let read_from_internal_ram code_memory s addr =
  let { Types.fst = bit_one; Types.snd = seven_bits } =
    Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S Nat.O))))))) addr
  in
  let memory =
    match Vector.head' Nat.O bit_one with
    | Bool.True -> s.high_internal_ram
    | Bool.False -> s.low_internal_ram
  in
  BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O))))))) seven_bits memory
    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))

(** val read_at_stack_pointer : 'a1 -> 'a1 preStatus -> BitVector.byte **)
let read_at_stack_pointer code_memory s =
  read_from_internal_ram code_memory s (get_8051_sfr code_memory s SFR_SP)

(** val write_at_stack_pointer :
    'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
let write_at_stack_pointer code_memory s v =
  let { Types.fst = bit_one; Types.snd = seven_bits } =
    Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S Nat.O))))))) (get_8051_sfr code_memory s SFR_SP)
  in
  (match Vector.head' Nat.O bit_one with
   | Bool.True -> update_high_internal_ram code_memory s seven_bits v
   | Bool.False -> update_low_internal_ram code_memory s seven_bits v)

(** val set_arg_16' :
    'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
    preStatus Types.sig0 **)
let set_arg_16' code_memory s v a =
  (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Dptr,
           Vector.VEmpty)) a with
   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
   | ASM.DPTR ->
     (fun _ ->
       (let { Types.fst = bu; Types.snd = bl } =
          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))) v
        in
       (fun _ ->
       let status0 = set_8051_sfr code_memory s SFR_DPH bu in
       let status1 = set_8051_sfr code_memory status0 SFR_DPL bl in status1))
         __)
   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __

(** val set_arg_16 :
    'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
    preStatus **)
let set_arg_16 code_memory s h h1 =
  Types.pi1 (set_arg_16' code_memory s h h1)

(** val get_arg_16 :
    'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.word **)
let get_arg_16 cm s a =
  (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
           ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty))))
           a with
   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA16 d -> (fun _ -> d)
   | ASM.ACC_DPTR ->
     (fun _ ->
       let dptr =
         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
           (get_8051_sfr cm s SFR_DPL)
       in
       let big_acc =
         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O))))))))
           (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S Nat.O))))))))) (get_8051_sfr cm s SFR_ACC_A)
       in
       Arithmetic.add
         (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O))))))))) big_acc dptr)
   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __

(** val get_arg_8 :
    'a1 -> 'a1 preStatus -> Bool.bool -> ASM.subaddressing_mode ->
    BitVector.byte **)
let get_arg_8 cm s l a =
  (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
           ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
           ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
           (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
           Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
           ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
           Vector.VEmpty)))))))))))))))))))) a with
   | ASM.DIRECT d ->
     (fun _ ->
       let { Types.fst = hd; Types.snd = seven_bits } =
         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O))))))) d
       in
       (match Vector.head' Nat.O hd with
        | Bool.True ->
          get_bit_addressable_sfr cm s (Vector.VCons ((Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, seven_bits))
            l
        | Bool.False ->
          BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S Nat.O))))))) seven_bits s.low_internal_ram
            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O)))))))))))
   | ASM.INDIRECT i ->
     (fun _ ->
       let { Types.fst = hd; Types.snd = seven_bits } =
         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))))))
           (get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)),
             Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False,
             (Vector.VCons (Nat.O, i, Vector.VEmpty)))))))
       in
       (match Vector.head' Nat.O hd with
        | Bool.True ->
          BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S Nat.O))))))) seven_bits s.high_internal_ram
            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O)))))))))
        | Bool.False ->
          BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S Nat.O))))))) seven_bits s.low_internal_ram
            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O)))))))))))
   | ASM.EXT_INDIRECT e ->
     (fun _ ->
       let address =
         get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e,
           Vector.VEmpty))))))
       in
       let padded_address =
         BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))))))) address
       in
       read_from_external_ram cm s padded_address)
   | ASM.REGISTER r -> (fun _ -> get_register cm s r)
   | ASM.ACC_A -> (fun _ -> get_8051_sfr cm s SFR_ACC_A)
   | ASM.ACC_B -> (fun _ -> get_8051_sfr cm s SFR_ACC_B)
   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA d -> (fun _ -> d)
   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_DPTR ->
     (fun _ ->
       let dptr =
         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
           (get_8051_sfr cm s SFR_DPL)
       in
       let padded_acc =
         BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_ACC_A)
       in
       let { Types.fst = carry; Types.snd = address } =
         Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))) dptr padded_acc
       in
       read_from_external_ram cm s address)
   | ASM.ACC_PC ->
     (fun _ ->
       let padded_acc =
         BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_ACC_A)
       in
       let { Types.fst = carry; Types.snd = address } =
         Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))) s.program_counter padded_acc
       in
       read_from_external_ram cm s address)
   | ASM.EXT_INDIRECT_DPTR ->
     (fun _ ->
       let address =
         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
           (get_8051_sfr cm s SFR_DPL)
       in
       read_from_external_ram cm s address)
   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __

(** val set_arg_8 :
    'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.byte -> 'a1
    preStatus **)
let set_arg_8 cm s a v =
  (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
           ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons
           ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S
           (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
           ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
           Vector.VEmpty)))))))))))))) a with
   | ASM.DIRECT d ->
     (fun _ ->
       let { Types.fst = bit_one; Types.snd = seven_bits } =
         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O))))))) d
       in
       (match Vector.head' Nat.O bit_one with
        | Bool.True ->
          set_bit_addressable_sfr cm s (Vector.VCons ((Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, seven_bits))
            v
        | Bool.False -> update_low_internal_ram cm s seven_bits v))
   | ASM.INDIRECT i ->
     (fun _ ->
       let register =
         get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, i,
           Vector.VEmpty))))))
       in
       let { Types.fst = bit_one; Types.snd = seven_bits } =
         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O))))))) register
       in
       (match Vector.head' Nat.O bit_one with
        | Bool.True -> update_high_internal_ram cm s seven_bits v
        | Bool.False -> update_low_internal_ram cm s seven_bits v))
   | ASM.EXT_INDIRECT e ->
     (fun _ ->
       let address =
         get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e,
           Vector.VEmpty))))))
       in
       let padded_address =
         BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))))))) address
       in
       update_external_ram cm s padded_address v)
   | ASM.REGISTER r -> (fun _ -> set_register cm s r v)
   | ASM.ACC_A -> (fun _ -> set_8051_sfr cm s SFR_ACC_A v)
   | ASM.ACC_B -> (fun _ -> set_8051_sfr cm s SFR_ACC_B v)
   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
   | ASM.EXT_INDIRECT_DPTR ->
     (fun _ ->
       let address =
         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
           (get_8051_sfr cm s SFR_DPL)
       in
       update_external_ram cm s address v)
   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
   | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __

(** val get_arg_1 :
    'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> Bool.bool -> Bool.bool **)
let get_arg_1 cm s a l =
  (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
           (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O),
           ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry,
           Vector.VEmpty)))))) a with
   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.CARRY -> (fun _ -> get_cy_flag cm s)
   | ASM.BIT_ADDR b ->
     (fun _ ->
       let { Types.fst = bit_1; Types.snd = seven_bits } =
         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O))))))) b
       in
       let { Types.fst = four_bits; Types.snd = three_bits } =
         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
           (Nat.S Nat.O))) seven_bits
       in
       (match Vector.head' Nat.O bit_1 with
        | Bool.True ->
          let trans =
            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
              (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
              (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
              ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
              Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
              Vector.VEmpty))))))
          in
          let sfr = get_bit_addressable_sfr cm s trans l in
          Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S Nat.O)))))))) sfr
            (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
              three_bits)
        | Bool.False ->
          let address' =
            Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
              Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
              (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) four_bits
          in
          let t =
            BitVectorTrie.lookup
              (Nat.plus (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
                (Nat.S Nat.O))))) address' s.low_internal_ram
              (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                (Nat.S (Nat.S Nat.O)))))))))
          in
          Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S Nat.O)))))))) t
            (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
              three_bits)))
   | ASM.N_BIT_ADDR n ->
     (fun _ ->
       let { Types.fst = bit_1; Types.snd = seven_bits } =
         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O))))))) n
       in
       let { Types.fst = four_bits; Types.snd = three_bits } =
         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
           (Nat.S Nat.O))) seven_bits
       in
       (match Vector.head' Nat.O bit_1 with
        | Bool.True ->
          let trans =
            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
              (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
              (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
              ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
              Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
              Vector.VEmpty))))))
          in
          let sfr = get_bit_addressable_sfr cm s trans l in
          Bool.notb
            (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S Nat.O)))))))) sfr
              (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
                three_bits))
        | Bool.False ->
          let address' =
            Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
              Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
              (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) four_bits
          in
          let t =
            BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O))))))) address' s.low_internal_ram
              (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                (Nat.S (Nat.S Nat.O)))))))))
          in
          Bool.notb
            (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S Nat.O)))))))) t
              (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
                three_bits))))
   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __

(** val set_arg_1 :
    'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.bit -> 'a1
    preStatus **)
let set_arg_1 cm s a v =
  (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
           ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) a with
   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
   | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
   | ASM.CARRY ->
     (fun _ ->
       let { Types.fst = ignore; Types.snd = seven_bits } =
         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O))))))) (get_8051_sfr cm s SFR_PSW)
       in
       let new_psw = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S Nat.O))))))), v, seven_bits)
       in
       set_8051_sfr cm s SFR_PSW new_psw)
   | ASM.BIT_ADDR b ->
     (fun _ ->
       let { Types.fst = bit_1; Types.snd = seven_bits } =
         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S Nat.O))))))) b
       in
       let { Types.fst = four_bits; Types.snd = three_bits } =
         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
           (Nat.S Nat.O))) seven_bits
       in
       (match Vector.head' Nat.O bit_1 with
        | Bool.True ->
          let trans =
            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
              (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
              (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
              ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
              Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
              Vector.VEmpty))))))
          in
          let sfr = get_bit_addressable_sfr cm s trans Bool.True in
          let new_sfr =
            Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O)))))))) sfr
              (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
                three_bits) v
          in
          set_bit_addressable_sfr cm s new_sfr trans
        | Bool.False ->
          let address' =
            Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
              Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
              (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) four_bits
          in
          let t =
            BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O))))))) address' s.low_internal_ram
              (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                (Nat.S (Nat.S Nat.O)))))))))
          in
          let n_bit =
            Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S Nat.O)))))))) t
              (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
                three_bits) v
          in
          update_low_internal_ram cm s address' n_bit))
   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __

(** val construct_datalabels :
    (ASM.identifier, BitVector.word) Types.prod List.list -> BitVector.word
    Identifiers.identifier_map **)
let construct_datalabels the_preamble =
  (Util.foldl (fun t preamble ->
    let { Types.fst = datalabels; Types.snd = addr } = t in
    let { Types.fst = name; Types.snd = size } = preamble in
    let { Types.fst = addr0; Types.snd = carry } =
      Arithmetic.sub_16_with_carry addr size Bool.False
    in
    { Types.fst =
    (Identifiers.add PreIdentifiers.ASMTag datalabels name addr0);
    Types.snd = addr0 }) { Types.fst =
    (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd =
    (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))) } the_preamble).Types.fst