source: extracted/status.ml @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 251.8 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open BitVectorTrie
8
9open Exp
10
11open Arithmetic
12
13open Integers
14
15open AST
16
17open CostLabel
18
19open Proper
20
21open PositiveMap
22
23open Deqsets
24
25open ErrorMessages
26
27open PreIdentifiers
28
29open Errors
30
31open Extralib
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Lists
40
41open Positive
42
43open Identifiers
44
45open Extranat
46
47open Vector
48
49open Div_and_mod
50
51open Jmeq
52
53open Russell
54
55open Types
56
57open List
58
59open Util
60
61open FoldStuff
62
63open Bool
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Relations
74
75open Nat
76
77open BitVector
78
79open ASM
80
81type time = Nat.nat
82
83type serialBufferType =
84| Eight of BitVector.byte
85| Nine of BitVector.bit * BitVector.byte
86
87(** val serialBufferType_rect_Type4 :
88    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
89    serialBufferType -> 'a1 **)
90let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
91| Eight x_24138 -> h_Eight x_24138
92| Nine (x_24140, x_24139) -> h_Nine x_24140 x_24139
93
94(** val serialBufferType_rect_Type5 :
95    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
96    serialBufferType -> 'a1 **)
97let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
98| Eight x_24144 -> h_Eight x_24144
99| Nine (x_24146, x_24145) -> h_Nine x_24146 x_24145
100
101(** val serialBufferType_rect_Type3 :
102    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
103    serialBufferType -> 'a1 **)
104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
105| Eight x_24150 -> h_Eight x_24150
106| Nine (x_24152, x_24151) -> h_Nine x_24152 x_24151
107
108(** val serialBufferType_rect_Type2 :
109    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
110    serialBufferType -> 'a1 **)
111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
112| Eight x_24156 -> h_Eight x_24156
113| Nine (x_24158, x_24157) -> h_Nine x_24158 x_24157
114
115(** val serialBufferType_rect_Type1 :
116    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
117    serialBufferType -> 'a1 **)
118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
119| Eight x_24162 -> h_Eight x_24162
120| Nine (x_24164, x_24163) -> h_Nine x_24164 x_24163
121
122(** val serialBufferType_rect_Type0 :
123    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
124    serialBufferType -> 'a1 **)
125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
126| Eight x_24168 -> h_Eight x_24168
127| Nine (x_24170, x_24169) -> h_Nine x_24170 x_24169
128
129(** val serialBufferType_inv_rect_Type4 :
130    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
131    BitVector.byte -> __ -> 'a1) -> 'a1 **)
132let serialBufferType_inv_rect_Type4 hterm h1 h2 =
133  let hcut = serialBufferType_rect_Type4 h1 h2 hterm in hcut __
134
135(** val serialBufferType_inv_rect_Type3 :
136    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
137    BitVector.byte -> __ -> 'a1) -> 'a1 **)
138let serialBufferType_inv_rect_Type3 hterm h1 h2 =
139  let hcut = serialBufferType_rect_Type3 h1 h2 hterm in hcut __
140
141(** val serialBufferType_inv_rect_Type2 :
142    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
143    BitVector.byte -> __ -> 'a1) -> 'a1 **)
144let serialBufferType_inv_rect_Type2 hterm h1 h2 =
145  let hcut = serialBufferType_rect_Type2 h1 h2 hterm in hcut __
146
147(** val serialBufferType_inv_rect_Type1 :
148    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
149    BitVector.byte -> __ -> 'a1) -> 'a1 **)
150let serialBufferType_inv_rect_Type1 hterm h1 h2 =
151  let hcut = serialBufferType_rect_Type1 h1 h2 hterm in hcut __
152
153(** val serialBufferType_inv_rect_Type0 :
154    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
155    BitVector.byte -> __ -> 'a1) -> 'a1 **)
156let serialBufferType_inv_rect_Type0 hterm h1 h2 =
157  let hcut = serialBufferType_rect_Type0 h1 h2 hterm in hcut __
158
159(** val serialBufferType_discr :
160    serialBufferType -> serialBufferType -> __ **)
161let serialBufferType_discr x y =
162  Logic.eq_rect_Type2 x
163    (match x with
164     | Eight a0 -> Obj.magic (fun _ dH -> dH __)
165     | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
166
167(** val serialBufferType_jmdiscr :
168    serialBufferType -> serialBufferType -> __ **)
169let serialBufferType_jmdiscr x y =
170  Logic.eq_rect_Type2 x
171    (match x with
172     | Eight a0 -> Obj.magic (fun _ dH -> dH __)
173     | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
174
175type lineType =
176| P2 of BitVector.byte
177| P3 of BitVector.byte
178| SerialBuffer of serialBufferType
179
180(** val lineType_rect_Type4 :
181    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
182    -> 'a1) -> lineType -> 'a1 **)
183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
184| P2 x_24217 -> h_P1 x_24217
185| P3 x_24218 -> h_P3 x_24218
186| SerialBuffer x_24219 -> h_SerialBuffer x_24219
187
188(** val lineType_rect_Type5 :
189    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
190    -> 'a1) -> lineType -> 'a1 **)
191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
192| P2 x_24224 -> h_P1 x_24224
193| P3 x_24225 -> h_P3 x_24225
194| SerialBuffer x_24226 -> h_SerialBuffer x_24226
195
196(** val lineType_rect_Type3 :
197    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
198    -> 'a1) -> lineType -> 'a1 **)
199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
200| P2 x_24231 -> h_P1 x_24231
201| P3 x_24232 -> h_P3 x_24232
202| SerialBuffer x_24233 -> h_SerialBuffer x_24233
203
204(** val lineType_rect_Type2 :
205    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
206    -> 'a1) -> lineType -> 'a1 **)
207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
208| P2 x_24238 -> h_P1 x_24238
209| P3 x_24239 -> h_P3 x_24239
210| SerialBuffer x_24240 -> h_SerialBuffer x_24240
211
212(** val lineType_rect_Type1 :
213    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
214    -> 'a1) -> lineType -> 'a1 **)
215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
216| P2 x_24245 -> h_P1 x_24245
217| P3 x_24246 -> h_P3 x_24246
218| SerialBuffer x_24247 -> h_SerialBuffer x_24247
219
220(** val lineType_rect_Type0 :
221    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
222    -> 'a1) -> lineType -> 'a1 **)
223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
224| P2 x_24252 -> h_P1 x_24252
225| P3 x_24253 -> h_P3 x_24253
226| SerialBuffer x_24254 -> h_SerialBuffer x_24254
227
228(** val lineType_inv_rect_Type4 :
229    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
230    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
231let lineType_inv_rect_Type4 hterm h1 h2 h3 =
232  let hcut = lineType_rect_Type4 h1 h2 h3 hterm in hcut __
233
234(** val lineType_inv_rect_Type3 :
235    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
236    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
237let lineType_inv_rect_Type3 hterm h1 h2 h3 =
238  let hcut = lineType_rect_Type3 h1 h2 h3 hterm in hcut __
239
240(** val lineType_inv_rect_Type2 :
241    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
242    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
243let lineType_inv_rect_Type2 hterm h1 h2 h3 =
244  let hcut = lineType_rect_Type2 h1 h2 h3 hterm in hcut __
245
246(** val lineType_inv_rect_Type1 :
247    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
248    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
249let lineType_inv_rect_Type1 hterm h1 h2 h3 =
250  let hcut = lineType_rect_Type1 h1 h2 h3 hterm in hcut __
251
252(** val lineType_inv_rect_Type0 :
253    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
254    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
255let lineType_inv_rect_Type0 hterm h1 h2 h3 =
256  let hcut = lineType_rect_Type0 h1 h2 h3 hterm in hcut __
257
258(** val lineType_discr : lineType -> lineType -> __ **)
259let lineType_discr x y =
260  Logic.eq_rect_Type2 x
261    (match x with
262     | P2 a0 -> Obj.magic (fun _ dH -> dH __)
263     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
264     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
265
266(** val lineType_jmdiscr : lineType -> lineType -> __ **)
267let lineType_jmdiscr x y =
268  Logic.eq_rect_Type2 x
269    (match x with
270     | P2 a0 -> Obj.magic (fun _ dH -> dH __)
271     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
272     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
273
274type sFR8051 =
275| SFR_SP
276| SFR_DPL
277| SFR_DPH
278| SFR_PCON
279| SFR_TCON
280| SFR_TMOD
281| SFR_TL0
282| SFR_TL1
283| SFR_TH0
284| SFR_TH1
285| SFR_P1
286| SFR_SCON
287| SFR_SBUF
288| SFR_IE
289| SFR_P3
290| SFR_IP
291| SFR_PSW
292| SFR_ACC_A
293| SFR_ACC_B
294
295(** val sFR8051_rect_Type4 :
296    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
297    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
298let 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
299| SFR_SP -> h_SFR_SP
300| SFR_DPL -> h_SFR_DPL
301| SFR_DPH -> h_SFR_DPH
302| SFR_PCON -> h_SFR_PCON
303| SFR_TCON -> h_SFR_TCON
304| SFR_TMOD -> h_SFR_TMOD
305| SFR_TL0 -> h_SFR_TL0
306| SFR_TL1 -> h_SFR_TL1
307| SFR_TH0 -> h_SFR_TH0
308| SFR_TH1 -> h_SFR_TH1
309| SFR_P1 -> h_SFR_P1
310| SFR_SCON -> h_SFR_SCON
311| SFR_SBUF -> h_SFR_SBUF
312| SFR_IE -> h_SFR_IE
313| SFR_P3 -> h_SFR_P3
314| SFR_IP -> h_SFR_IP
315| SFR_PSW -> h_SFR_PSW
316| SFR_ACC_A -> h_SFR_ACC_A
317| SFR_ACC_B -> h_SFR_ACC_B
318
319(** val sFR8051_rect_Type5 :
320    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
321    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
322let 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
323| SFR_SP -> h_SFR_SP
324| SFR_DPL -> h_SFR_DPL
325| SFR_DPH -> h_SFR_DPH
326| SFR_PCON -> h_SFR_PCON
327| SFR_TCON -> h_SFR_TCON
328| SFR_TMOD -> h_SFR_TMOD
329| SFR_TL0 -> h_SFR_TL0
330| SFR_TL1 -> h_SFR_TL1
331| SFR_TH0 -> h_SFR_TH0
332| SFR_TH1 -> h_SFR_TH1
333| SFR_P1 -> h_SFR_P1
334| SFR_SCON -> h_SFR_SCON
335| SFR_SBUF -> h_SFR_SBUF
336| SFR_IE -> h_SFR_IE
337| SFR_P3 -> h_SFR_P3
338| SFR_IP -> h_SFR_IP
339| SFR_PSW -> h_SFR_PSW
340| SFR_ACC_A -> h_SFR_ACC_A
341| SFR_ACC_B -> h_SFR_ACC_B
342
343(** val sFR8051_rect_Type3 :
344    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
345    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
346let 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
347| SFR_SP -> h_SFR_SP
348| SFR_DPL -> h_SFR_DPL
349| SFR_DPH -> h_SFR_DPH
350| SFR_PCON -> h_SFR_PCON
351| SFR_TCON -> h_SFR_TCON
352| SFR_TMOD -> h_SFR_TMOD
353| SFR_TL0 -> h_SFR_TL0
354| SFR_TL1 -> h_SFR_TL1
355| SFR_TH0 -> h_SFR_TH0
356| SFR_TH1 -> h_SFR_TH1
357| SFR_P1 -> h_SFR_P1
358| SFR_SCON -> h_SFR_SCON
359| SFR_SBUF -> h_SFR_SBUF
360| SFR_IE -> h_SFR_IE
361| SFR_P3 -> h_SFR_P3
362| SFR_IP -> h_SFR_IP
363| SFR_PSW -> h_SFR_PSW
364| SFR_ACC_A -> h_SFR_ACC_A
365| SFR_ACC_B -> h_SFR_ACC_B
366
367(** val sFR8051_rect_Type2 :
368    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
369    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
370let 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
371| SFR_SP -> h_SFR_SP
372| SFR_DPL -> h_SFR_DPL
373| SFR_DPH -> h_SFR_DPH
374| SFR_PCON -> h_SFR_PCON
375| SFR_TCON -> h_SFR_TCON
376| SFR_TMOD -> h_SFR_TMOD
377| SFR_TL0 -> h_SFR_TL0
378| SFR_TL1 -> h_SFR_TL1
379| SFR_TH0 -> h_SFR_TH0
380| SFR_TH1 -> h_SFR_TH1
381| SFR_P1 -> h_SFR_P1
382| SFR_SCON -> h_SFR_SCON
383| SFR_SBUF -> h_SFR_SBUF
384| SFR_IE -> h_SFR_IE
385| SFR_P3 -> h_SFR_P3
386| SFR_IP -> h_SFR_IP
387| SFR_PSW -> h_SFR_PSW
388| SFR_ACC_A -> h_SFR_ACC_A
389| SFR_ACC_B -> h_SFR_ACC_B
390
391(** val sFR8051_rect_Type1 :
392    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
393    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
394let 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
395| SFR_SP -> h_SFR_SP
396| SFR_DPL -> h_SFR_DPL
397| SFR_DPH -> h_SFR_DPH
398| SFR_PCON -> h_SFR_PCON
399| SFR_TCON -> h_SFR_TCON
400| SFR_TMOD -> h_SFR_TMOD
401| SFR_TL0 -> h_SFR_TL0
402| SFR_TL1 -> h_SFR_TL1
403| SFR_TH0 -> h_SFR_TH0
404| SFR_TH1 -> h_SFR_TH1
405| SFR_P1 -> h_SFR_P1
406| SFR_SCON -> h_SFR_SCON
407| SFR_SBUF -> h_SFR_SBUF
408| SFR_IE -> h_SFR_IE
409| SFR_P3 -> h_SFR_P3
410| SFR_IP -> h_SFR_IP
411| SFR_PSW -> h_SFR_PSW
412| SFR_ACC_A -> h_SFR_ACC_A
413| SFR_ACC_B -> h_SFR_ACC_B
414
415(** val sFR8051_rect_Type0 :
416    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
417    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
418let 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
419| SFR_SP -> h_SFR_SP
420| SFR_DPL -> h_SFR_DPL
421| SFR_DPH -> h_SFR_DPH
422| SFR_PCON -> h_SFR_PCON
423| SFR_TCON -> h_SFR_TCON
424| SFR_TMOD -> h_SFR_TMOD
425| SFR_TL0 -> h_SFR_TL0
426| SFR_TL1 -> h_SFR_TL1
427| SFR_TH0 -> h_SFR_TH0
428| SFR_TH1 -> h_SFR_TH1
429| SFR_P1 -> h_SFR_P1
430| SFR_SCON -> h_SFR_SCON
431| SFR_SBUF -> h_SFR_SBUF
432| SFR_IE -> h_SFR_IE
433| SFR_P3 -> h_SFR_P3
434| SFR_IP -> h_SFR_IP
435| SFR_PSW -> h_SFR_PSW
436| SFR_ACC_A -> h_SFR_ACC_A
437| SFR_ACC_B -> h_SFR_ACC_B
438
439(** val sFR8051_inv_rect_Type4 :
440    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
441    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
442    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
443    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
444    -> 'a1) -> 'a1 **)
445let sFR8051_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
446  let hcut =
447    sFR8051_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
448      h17 h18 h19 hterm
449  in
450  hcut __
451
452(** val sFR8051_inv_rect_Type3 :
453    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
454    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
455    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
456    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
457    -> 'a1) -> 'a1 **)
458let sFR8051_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
459  let hcut =
460    sFR8051_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
461      h17 h18 h19 hterm
462  in
463  hcut __
464
465(** val sFR8051_inv_rect_Type2 :
466    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
467    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
468    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
469    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
470    -> 'a1) -> 'a1 **)
471let sFR8051_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
472  let hcut =
473    sFR8051_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
474      h17 h18 h19 hterm
475  in
476  hcut __
477
478(** val sFR8051_inv_rect_Type1 :
479    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
480    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
481    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
482    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
483    -> 'a1) -> 'a1 **)
484let sFR8051_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
485  let hcut =
486    sFR8051_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
487      h17 h18 h19 hterm
488  in
489  hcut __
490
491(** val sFR8051_inv_rect_Type0 :
492    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
493    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
494    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
495    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
496    -> 'a1) -> 'a1 **)
497let sFR8051_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
498  let hcut =
499    sFR8051_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
500      h17 h18 h19 hterm
501  in
502  hcut __
503
504(** val sFR8051_discr : sFR8051 -> sFR8051 -> __ **)
505let sFR8051_discr x y =
506  Logic.eq_rect_Type2 x
507    (match x with
508     | SFR_SP -> Obj.magic (fun _ dH -> dH)
509     | SFR_DPL -> Obj.magic (fun _ dH -> dH)
510     | SFR_DPH -> Obj.magic (fun _ dH -> dH)
511     | SFR_PCON -> Obj.magic (fun _ dH -> dH)
512     | SFR_TCON -> Obj.magic (fun _ dH -> dH)
513     | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
514     | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
515     | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
516     | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
517     | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
518     | SFR_P1 -> Obj.magic (fun _ dH -> dH)
519     | SFR_SCON -> Obj.magic (fun _ dH -> dH)
520     | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
521     | SFR_IE -> Obj.magic (fun _ dH -> dH)
522     | SFR_P3 -> Obj.magic (fun _ dH -> dH)
523     | SFR_IP -> Obj.magic (fun _ dH -> dH)
524     | SFR_PSW -> Obj.magic (fun _ dH -> dH)
525     | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
526     | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
527
528(** val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __ **)
529let sFR8051_jmdiscr x y =
530  Logic.eq_rect_Type2 x
531    (match x with
532     | SFR_SP -> Obj.magic (fun _ dH -> dH)
533     | SFR_DPL -> Obj.magic (fun _ dH -> dH)
534     | SFR_DPH -> Obj.magic (fun _ dH -> dH)
535     | SFR_PCON -> Obj.magic (fun _ dH -> dH)
536     | SFR_TCON -> Obj.magic (fun _ dH -> dH)
537     | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
538     | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
539     | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
540     | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
541     | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
542     | SFR_P1 -> Obj.magic (fun _ dH -> dH)
543     | SFR_SCON -> Obj.magic (fun _ dH -> dH)
544     | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
545     | SFR_IE -> Obj.magic (fun _ dH -> dH)
546     | SFR_P3 -> Obj.magic (fun _ dH -> dH)
547     | SFR_IP -> Obj.magic (fun _ dH -> dH)
548     | SFR_PSW -> Obj.magic (fun _ dH -> dH)
549     | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
550     | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
551
552(** val sfr_8051_index : sFR8051 -> Nat.nat **)
553let sfr_8051_index = function
554| SFR_SP -> Nat.O
555| SFR_DPL -> Nat.S Nat.O
556| SFR_DPH -> Nat.S (Nat.S Nat.O)
557| SFR_PCON -> Nat.S (Nat.S (Nat.S Nat.O))
558| SFR_TCON -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
559| SFR_TMOD -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
560| SFR_TL0 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
561| SFR_TL1 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
562| SFR_TH0 ->
563  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
564| SFR_TH1 ->
565  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
566| SFR_P1 ->
567  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
568    Nat.O)))))))))
569| SFR_SCON ->
570  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
571    Nat.O))))))))))
572| SFR_SBUF ->
573  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
574    (Nat.S Nat.O)))))))))))
575| SFR_IE ->
576  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
577    (Nat.S (Nat.S Nat.O))))))))))))
578| SFR_P3 ->
579  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
580    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))
581| SFR_IP ->
582  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
583    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))
584| SFR_PSW ->
585  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
586    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
587| SFR_ACC_A ->
588  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
589    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
590| SFR_ACC_B ->
591  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
592    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))
593
594type sFR8052 =
595| SFR_T2CON
596| SFR_RCAP2L
597| SFR_RCAP2H
598| SFR_TL2
599| SFR_TH2
600
601(** val sFR8052_rect_Type4 :
602    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
603let rec sFR8052_rect_Type4 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
604| SFR_T2CON -> h_SFR_T2CON
605| SFR_RCAP2L -> h_SFR_RCAP2L
606| SFR_RCAP2H -> h_SFR_RCAP2H
607| SFR_TL2 -> h_SFR_TL2
608| SFR_TH2 -> h_SFR_TH2
609
610(** val sFR8052_rect_Type5 :
611    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
612let rec sFR8052_rect_Type5 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
613| SFR_T2CON -> h_SFR_T2CON
614| SFR_RCAP2L -> h_SFR_RCAP2L
615| SFR_RCAP2H -> h_SFR_RCAP2H
616| SFR_TL2 -> h_SFR_TL2
617| SFR_TH2 -> h_SFR_TH2
618
619(** val sFR8052_rect_Type3 :
620    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
621let rec sFR8052_rect_Type3 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
622| SFR_T2CON -> h_SFR_T2CON
623| SFR_RCAP2L -> h_SFR_RCAP2L
624| SFR_RCAP2H -> h_SFR_RCAP2H
625| SFR_TL2 -> h_SFR_TL2
626| SFR_TH2 -> h_SFR_TH2
627
628(** val sFR8052_rect_Type2 :
629    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
630let rec sFR8052_rect_Type2 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
631| SFR_T2CON -> h_SFR_T2CON
632| SFR_RCAP2L -> h_SFR_RCAP2L
633| SFR_RCAP2H -> h_SFR_RCAP2H
634| SFR_TL2 -> h_SFR_TL2
635| SFR_TH2 -> h_SFR_TH2
636
637(** val sFR8052_rect_Type1 :
638    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
639let rec sFR8052_rect_Type1 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
640| SFR_T2CON -> h_SFR_T2CON
641| SFR_RCAP2L -> h_SFR_RCAP2L
642| SFR_RCAP2H -> h_SFR_RCAP2H
643| SFR_TL2 -> h_SFR_TL2
644| SFR_TH2 -> h_SFR_TH2
645
646(** val sFR8052_rect_Type0 :
647    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
648let rec sFR8052_rect_Type0 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
649| SFR_T2CON -> h_SFR_T2CON
650| SFR_RCAP2L -> h_SFR_RCAP2L
651| SFR_RCAP2H -> h_SFR_RCAP2H
652| SFR_TL2 -> h_SFR_TL2
653| SFR_TH2 -> h_SFR_TH2
654
655(** val sFR8052_inv_rect_Type4 :
656    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
657    (__ -> 'a1) -> 'a1 **)
658let sFR8052_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
659  let hcut = sFR8052_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
660
661(** val sFR8052_inv_rect_Type3 :
662    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
663    (__ -> 'a1) -> 'a1 **)
664let sFR8052_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
665  let hcut = sFR8052_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
666
667(** val sFR8052_inv_rect_Type2 :
668    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
669    (__ -> 'a1) -> 'a1 **)
670let sFR8052_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
671  let hcut = sFR8052_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
672
673(** val sFR8052_inv_rect_Type1 :
674    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
675    (__ -> 'a1) -> 'a1 **)
676let sFR8052_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
677  let hcut = sFR8052_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
678
679(** val sFR8052_inv_rect_Type0 :
680    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
681    (__ -> 'a1) -> 'a1 **)
682let sFR8052_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
683  let hcut = sFR8052_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
684
685(** val sFR8052_discr : sFR8052 -> sFR8052 -> __ **)
686let sFR8052_discr x y =
687  Logic.eq_rect_Type2 x
688    (match x with
689     | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
690     | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
691     | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
692     | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
693     | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
694
695(** val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __ **)
696let sFR8052_jmdiscr x y =
697  Logic.eq_rect_Type2 x
698    (match x with
699     | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
700     | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
701     | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
702     | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
703     | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
704
705(** val sfr_8052_index : sFR8052 -> Nat.nat **)
706let sfr_8052_index = function
707| SFR_T2CON -> Nat.O
708| SFR_RCAP2L -> Nat.S Nat.O
709| SFR_RCAP2H -> Nat.S (Nat.S Nat.O)
710| SFR_TL2 -> Nat.S (Nat.S (Nat.S Nat.O))
711| SFR_TH2 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
712
713type 'm preStatus = { low_internal_ram : BitVector.byte
714                                         BitVectorTrie.bitVectorTrie;
715                      high_internal_ram : BitVector.byte
716                                          BitVectorTrie.bitVectorTrie;
717                      external_ram : BitVector.byte
718                                     BitVectorTrie.bitVectorTrie;
719                      program_counter : BitVector.word;
720                      special_function_registers_8051 : BitVector.byte
721                                                        Vector.vector;
722                      special_function_registers_8052 : BitVector.byte
723                                                        Vector.vector;
724                      p1_latch : BitVector.byte; p3_latch : BitVector.byte;
725                      clock : time }
726
727(** val preStatus_rect_Type4 :
728    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
729    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
730    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
731    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
732    preStatus -> 'a2 **)
733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_24640 =
734  let { low_internal_ram = low_internal_ram0; high_internal_ram =
735    high_internal_ram0; external_ram = external_ram0; program_counter =
736    program_counter0; special_function_registers_8051 =
737    special_function_registers_8053; special_function_registers_8052 =
738    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
739    p3_latch0; clock = clock0 } = x_24640
740  in
741  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
742    program_counter0 special_function_registers_8053
743    special_function_registers_8054 p1_latch0 p3_latch0 clock0
744
745(** val preStatus_rect_Type5 :
746    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
747    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
748    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
749    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
750    preStatus -> 'a2 **)
751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_24642 =
752  let { low_internal_ram = low_internal_ram0; high_internal_ram =
753    high_internal_ram0; external_ram = external_ram0; program_counter =
754    program_counter0; special_function_registers_8051 =
755    special_function_registers_8053; special_function_registers_8052 =
756    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
757    p3_latch0; clock = clock0 } = x_24642
758  in
759  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
760    program_counter0 special_function_registers_8053
761    special_function_registers_8054 p1_latch0 p3_latch0 clock0
762
763(** val preStatus_rect_Type3 :
764    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
765    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
766    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
767    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
768    preStatus -> 'a2 **)
769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_24644 =
770  let { low_internal_ram = low_internal_ram0; high_internal_ram =
771    high_internal_ram0; external_ram = external_ram0; program_counter =
772    program_counter0; special_function_registers_8051 =
773    special_function_registers_8053; special_function_registers_8052 =
774    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
775    p3_latch0; clock = clock0 } = x_24644
776  in
777  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
778    program_counter0 special_function_registers_8053
779    special_function_registers_8054 p1_latch0 p3_latch0 clock0
780
781(** val preStatus_rect_Type2 :
782    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
783    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
784    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
785    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
786    preStatus -> 'a2 **)
787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_24646 =
788  let { low_internal_ram = low_internal_ram0; high_internal_ram =
789    high_internal_ram0; external_ram = external_ram0; program_counter =
790    program_counter0; special_function_registers_8051 =
791    special_function_registers_8053; special_function_registers_8052 =
792    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
793    p3_latch0; clock = clock0 } = x_24646
794  in
795  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
796    program_counter0 special_function_registers_8053
797    special_function_registers_8054 p1_latch0 p3_latch0 clock0
798
799(** val preStatus_rect_Type1 :
800    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
801    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
802    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
803    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
804    preStatus -> 'a2 **)
805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_24648 =
806  let { low_internal_ram = low_internal_ram0; high_internal_ram =
807    high_internal_ram0; external_ram = external_ram0; program_counter =
808    program_counter0; special_function_registers_8051 =
809    special_function_registers_8053; special_function_registers_8052 =
810    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
811    p3_latch0; clock = clock0 } = x_24648
812  in
813  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
814    program_counter0 special_function_registers_8053
815    special_function_registers_8054 p1_latch0 p3_latch0 clock0
816
817(** val preStatus_rect_Type0 :
818    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
819    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
820    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
821    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
822    preStatus -> 'a2 **)
823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_24650 =
824  let { low_internal_ram = low_internal_ram0; high_internal_ram =
825    high_internal_ram0; external_ram = external_ram0; program_counter =
826    program_counter0; special_function_registers_8051 =
827    special_function_registers_8053; special_function_registers_8052 =
828    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
829    p3_latch0; clock = clock0 } = x_24650
830  in
831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
832    program_counter0 special_function_registers_8053
833    special_function_registers_8054 p1_latch0 p3_latch0 clock0
834
835(** val low_internal_ram :
836    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
837let rec low_internal_ram code_memory xxx =
838  xxx.low_internal_ram
839
840(** val high_internal_ram :
841    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
842let rec high_internal_ram code_memory xxx =
843  xxx.high_internal_ram
844
845(** val external_ram :
846    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
847let rec external_ram code_memory xxx =
848  xxx.external_ram
849
850(** val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word **)
851let rec program_counter code_memory xxx =
852  xxx.program_counter
853
854(** val special_function_registers_8051 :
855    'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
856let rec special_function_registers_8051 code_memory xxx =
857  xxx.special_function_registers_8051
858
859(** val special_function_registers_8052 :
860    'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
861let rec special_function_registers_8052 code_memory xxx =
862  xxx.special_function_registers_8052
863
864(** val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
865let rec p1_latch code_memory xxx =
866  xxx.p1_latch
867
868(** val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
869let rec p3_latch code_memory xxx =
870  xxx.p3_latch
871
872(** val clock : 'a1 -> 'a1 preStatus -> time **)
873let rec clock code_memory xxx =
874  xxx.clock
875
876(** val preStatus_inv_rect_Type4 :
877    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
878    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
879    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
880    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
881    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
882let preStatus_inv_rect_Type4 x2 hterm h1 =
883  let hcut = preStatus_rect_Type4 x2 h1 hterm in hcut __
884
885(** val preStatus_inv_rect_Type3 :
886    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
887    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
888    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
889    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
890    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
891let preStatus_inv_rect_Type3 x2 hterm h1 =
892  let hcut = preStatus_rect_Type3 x2 h1 hterm in hcut __
893
894(** val preStatus_inv_rect_Type2 :
895    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
896    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
897    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
898    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
899    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
900let preStatus_inv_rect_Type2 x2 hterm h1 =
901  let hcut = preStatus_rect_Type2 x2 h1 hterm in hcut __
902
903(** val preStatus_inv_rect_Type1 :
904    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
905    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
906    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
907    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
908    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
909let preStatus_inv_rect_Type1 x2 hterm h1 =
910  let hcut = preStatus_rect_Type1 x2 h1 hterm in hcut __
911
912(** val preStatus_inv_rect_Type0 :
913    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
914    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
915    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
916    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
917    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
918let preStatus_inv_rect_Type0 x2 hterm h1 =
919  let hcut = preStatus_rect_Type0 x2 h1 hterm in hcut __
920
921(** val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __ **)
922let preStatus_jmdiscr a2 x y =
923  Logic.eq_rect_Type2 x
924    (let { low_internal_ram = a0; high_internal_ram = a10; external_ram =
925       a20; program_counter = a3; special_function_registers_8051 = a4;
926       special_function_registers_8052 = a5; p1_latch = a6; p3_latch = a7;
927       clock = a8 } = x
928     in
929    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y
930
931type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus
932
933type pseudoStatus = ASM.pseudo_assembly_program preStatus
934
935(** val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus **)
936let set_clock code_memory s t =
937  let old_low_internal_ram = s.low_internal_ram in
938  let old_high_internal_ram = s.high_internal_ram in
939  let old_external_ram = s.external_ram in
940  let old_program_counter = s.program_counter in
941  let old_special_function_registers_8051 = s.special_function_registers_8051
942  in
943  let old_special_function_registers_8052 = s.special_function_registers_8052
944  in
945  let old_p1_latch = s.p1_latch in
946  let old_p3_latch = s.p3_latch in
947  { low_internal_ram = old_low_internal_ram; high_internal_ram =
948  old_high_internal_ram; external_ram = old_external_ram; program_counter =
949  old_program_counter; special_function_registers_8051 =
950  old_special_function_registers_8051; special_function_registers_8052 =
951  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
952  old_p3_latch; clock = t }
953
954(** val set_p1_latch :
955    'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
956let set_p1_latch code_memory s b =
957  let old_low_internal_ram = s.low_internal_ram in
958  let old_high_internal_ram = s.high_internal_ram in
959  let old_external_ram = s.external_ram in
960  let old_program_counter = s.program_counter in
961  let old_special_function_registers_8051 = s.special_function_registers_8051
962  in
963  let old_special_function_registers_8052 = s.special_function_registers_8052
964  in
965  let old_p3_latch = s.p3_latch in
966  let old_clock = s.clock in
967  { low_internal_ram = old_low_internal_ram; high_internal_ram =
968  old_high_internal_ram; external_ram = old_external_ram; program_counter =
969  old_program_counter; special_function_registers_8051 =
970  old_special_function_registers_8051; special_function_registers_8052 =
971  old_special_function_registers_8052; p1_latch = b; p3_latch = old_p3_latch;
972  clock = old_clock }
973
974(** val set_p3_latch :
975    'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
976let set_p3_latch code_memory s b =
977  let old_low_internal_ram = s.low_internal_ram in
978  let old_high_internal_ram = s.high_internal_ram in
979  let old_external_ram = s.external_ram in
980  let old_program_counter = s.program_counter in
981  let old_special_function_registers_8051 = s.special_function_registers_8051
982  in
983  let old_special_function_registers_8052 = s.special_function_registers_8052
984  in
985  let old_p1_latch = s.p1_latch in
986  let old_clock = s.clock in
987  { low_internal_ram = old_low_internal_ram; high_internal_ram =
988  old_high_internal_ram; external_ram = old_external_ram; program_counter =
989  old_program_counter; special_function_registers_8051 =
990  old_special_function_registers_8051; special_function_registers_8052 =
991  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch = b;
992  clock = old_clock }
993
994(** val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte **)
995let get_8051_sfr code_memory s i =
996  let sfr = s.special_function_registers_8051 in
997  let index = sfr_8051_index i in
998  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
999    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1000    (Nat.S Nat.O))))))))))))))))))) sfr index
1001
1002(** val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte **)
1003let get_8052_sfr code_memory s i =
1004  let sfr = s.special_function_registers_8052 in
1005  let index = sfr_8052_index i in
1006  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) sfr index
1007
1008(** val set_8051_sfr :
1009    'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus **)
1010let set_8051_sfr code_memory s i b =
1011  let index = sfr_8051_index i in
1012  let old_low_internal_ram = s.low_internal_ram in
1013  let old_high_internal_ram = s.high_internal_ram in
1014  let old_external_ram = s.external_ram in
1015  let old_program_counter = s.program_counter in
1016  let old_special_function_registers_8051 = s.special_function_registers_8051
1017  in
1018  let old_special_function_registers_8052 = s.special_function_registers_8052
1019  in
1020  let new_special_function_registers_8051 =
1021    Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1022      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1023      (Nat.S Nat.O))))))))))))))))))) old_special_function_registers_8051
1024      index b
1025  in
1026  let old_p1_latch = s.p1_latch in
1027  let old_p3_latch = s.p3_latch in
1028  let old_clock = s.clock in
1029  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1030  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1031  old_program_counter; special_function_registers_8051 =
1032  new_special_function_registers_8051; special_function_registers_8052 =
1033  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1034  old_p3_latch; clock = old_clock }
1035
1036(** val set_8052_sfr :
1037    'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus **)
1038let set_8052_sfr code_memory s i b =
1039  let index = sfr_8052_index i in
1040  let old_low_internal_ram = s.low_internal_ram in
1041  let old_high_internal_ram = s.high_internal_ram in
1042  let old_external_ram = s.external_ram in
1043  let old_program_counter = s.program_counter in
1044  let old_special_function_registers_8051 = s.special_function_registers_8051
1045  in
1046  let old_special_function_registers_8052 = s.special_function_registers_8052
1047  in
1048  let new_special_function_registers_8052 =
1049    Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1050      old_special_function_registers_8052 index b
1051  in
1052  let old_p1_latch = s.p1_latch in
1053  let old_p3_latch = s.p3_latch in
1054  let old_clock = s.clock in
1055  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1056  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1057  old_program_counter; special_function_registers_8051 =
1058  old_special_function_registers_8051; special_function_registers_8052 =
1059  new_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1060  old_p3_latch; clock = old_clock }
1061
1062(** val set_program_counter :
1063    'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus **)
1064let set_program_counter code_memory s w =
1065  let old_low_internal_ram = s.low_internal_ram in
1066  let old_high_internal_ram = s.high_internal_ram in
1067  let old_external_ram = s.external_ram in
1068  let old_special_function_registers_8051 = s.special_function_registers_8051
1069  in
1070  let old_special_function_registers_8052 = s.special_function_registers_8052
1071  in
1072  let old_p1_latch = s.p1_latch in
1073  let old_p3_latch = s.p3_latch in
1074  let old_clock = s.clock in
1075  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1076  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1077  w; special_function_registers_8051 = old_special_function_registers_8051;
1078  special_function_registers_8052 = old_special_function_registers_8052;
1079  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1080
1081(** val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus **)
1082let set_code_memory code_memory s r =
1083  let old_low_internal_ram = s.low_internal_ram in
1084  let old_high_internal_ram = s.high_internal_ram in
1085  let old_external_ram = s.external_ram in
1086  let old_program_counter = s.program_counter in
1087  let old_special_function_registers_8051 = s.special_function_registers_8051
1088  in
1089  let old_special_function_registers_8052 = s.special_function_registers_8052
1090  in
1091  let old_p1_latch = s.p1_latch in
1092  let old_p3_latch = s.p3_latch in
1093  let old_clock = s.clock in
1094  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1095  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1096  old_program_counter; special_function_registers_8051 =
1097  old_special_function_registers_8051; special_function_registers_8052 =
1098  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1099  old_p3_latch; clock = old_clock }
1100
1101(** val set_low_internal_ram :
1102    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1103    preStatus **)
1104let set_low_internal_ram code_memory s r =
1105  let old_high_internal_ram = s.high_internal_ram in
1106  let old_external_ram = s.external_ram in
1107  let old_program_counter = s.program_counter in
1108  let old_special_function_registers_8051 = s.special_function_registers_8051
1109  in
1110  let old_special_function_registers_8052 = s.special_function_registers_8052
1111  in
1112  let old_p1_latch = s.p1_latch in
1113  let old_p3_latch = s.p3_latch in
1114  let old_clock = s.clock in
1115  { low_internal_ram = r; high_internal_ram = old_high_internal_ram;
1116  external_ram = old_external_ram; program_counter = old_program_counter;
1117  special_function_registers_8051 = old_special_function_registers_8051;
1118  special_function_registers_8052 = old_special_function_registers_8052;
1119  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1120
1121(** val set_high_internal_ram :
1122    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1123    preStatus **)
1124let set_high_internal_ram code_memory s r =
1125  let old_low_internal_ram = s.low_internal_ram in
1126  let old_high_internal_ram = s.high_internal_ram in
1127  let old_external_ram = s.external_ram in
1128  let old_program_counter = s.program_counter in
1129  let old_special_function_registers_8051 = s.special_function_registers_8051
1130  in
1131  let old_special_function_registers_8052 = s.special_function_registers_8052
1132  in
1133  let old_p1_latch = s.p1_latch in
1134  let old_p3_latch = s.p3_latch in
1135  let old_clock = s.clock in
1136  { low_internal_ram = old_low_internal_ram; high_internal_ram = r;
1137  external_ram = old_external_ram; program_counter = old_program_counter;
1138  special_function_registers_8051 = old_special_function_registers_8051;
1139  special_function_registers_8052 = old_special_function_registers_8052;
1140  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1141
1142(** val set_external_ram :
1143    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1144    preStatus **)
1145let set_external_ram code_memory s r =
1146  let old_low_internal_ram = s.low_internal_ram in
1147  let old_high_internal_ram = s.high_internal_ram in
1148  let old_program_counter = s.program_counter in
1149  let old_special_function_registers_8051 = s.special_function_registers_8051
1150  in
1151  let old_special_function_registers_8052 = s.special_function_registers_8052
1152  in
1153  let old_p1_latch = s.p1_latch in
1154  let old_p3_latch = s.p3_latch in
1155  let old_clock = s.clock in
1156  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1157  old_high_internal_ram; external_ram = r; program_counter =
1158  old_program_counter; special_function_registers_8051 =
1159  old_special_function_registers_8051; special_function_registers_8052 =
1160  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1161  old_p3_latch; clock = old_clock }
1162
1163(** val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1164let get_cy_flag code_memory s =
1165  let sfr = s.special_function_registers_8051 in
1166  let psw =
1167    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1168      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1169      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1170  in
1171  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1172    Nat.O)))))))) psw Nat.O
1173
1174(** val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1175let get_ac_flag code_memory s =
1176  let sfr = s.special_function_registers_8051 in
1177  let psw =
1178    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1179      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1180      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1181  in
1182  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1183    Nat.O)))))))) psw (Nat.S Nat.O)
1184
1185(** val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1186let get_fo_flag code_memory s =
1187  let sfr = s.special_function_registers_8051 in
1188  let psw =
1189    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1190      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1191      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1192  in
1193  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1194    Nat.O)))))))) psw (Nat.S (Nat.S Nat.O))
1195
1196(** val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1197let get_rs1_flag code_memory s =
1198  let sfr = s.special_function_registers_8051 in
1199  let psw =
1200    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1201      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1202      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1203  in
1204  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1205    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S Nat.O)))
1206
1207(** val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1208let get_rs0_flag code_memory s =
1209  let sfr = s.special_function_registers_8051 in
1210  let psw =
1211    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1212      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1213      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1214  in
1215  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1216    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1217
1218(** val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1219let get_ov_flag code_memory s =
1220  let sfr = s.special_function_registers_8051 in
1221  let psw =
1222    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1223      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1224      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1225  in
1226  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1227    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1228
1229(** val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1230let get_ud_flag code_memory s =
1231  let sfr = s.special_function_registers_8051 in
1232  let psw =
1233    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1234      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1235      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1236  in
1237  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1238    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1239
1240(** val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1241let get_p_flag code_memory s =
1242  let sfr = s.special_function_registers_8051 in
1243  let psw =
1244    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1245      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1246      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1247  in
1248  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1249    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1250    Nat.O)))))))
1251
1252(** val set_flags :
1253    'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
1254    BitVector.bit -> 'a1 preStatus **)
1255let set_flags code_memory s cy ac ov =
1256  let sfr_psw = get_8051_sfr code_memory s SFR_PSW in
1257  let old_cy =
1258    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1259      (Nat.S Nat.O)))))))) sfr_psw Nat.O
1260  in
1261  let old_ac =
1262    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1263      (Nat.S Nat.O)))))))) sfr_psw (Nat.S Nat.O)
1264  in
1265  let old_fo =
1266    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1267      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S Nat.O))
1268  in
1269  let old_rs1 =
1270    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1271      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S Nat.O)))
1272  in
1273  let old_rs0 =
1274    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1275      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1276  in
1277  let old_ov =
1278    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1279      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1280      Nat.O)))))
1281  in
1282  let old_ud =
1283    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1284      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1285      Nat.O))))))
1286  in
1287  let old_p =
1288    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1289      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1290      (Nat.S Nat.O)))))))
1291  in
1292  let new_ac =
1293    match ac with
1294    | Types.None -> old_ac
1295    | Types.Some j -> j
1296  in
1297  set_8051_sfr code_memory s SFR_PSW (Vector.VCons ((Nat.S (Nat.S (Nat.S
1298    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), old_cy, (Vector.VCons ((Nat.S
1299    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), new_ac, (Vector.VCons
1300    ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), old_fo, (Vector.VCons
1301    ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), old_rs1, (Vector.VCons ((Nat.S
1302    (Nat.S (Nat.S Nat.O))), old_rs0, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1303    old_ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O,
1304    old_p, Vector.VEmpty))))))))))))))))
1305
1306(** val initialise_status : 'a1 -> 'a1 preStatus **)
1307let initialise_status code_mem =
1308  let status0 = { low_internal_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1309    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))); high_internal_ram =
1310    (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1311    Nat.O)))))))); external_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1312    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1313    (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))); program_counter =
1314    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1315      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1316      Nat.O))))))))))))))))); special_function_registers_8051 =
1317    (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1318      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1319      (Nat.S Nat.O)))))))))))))))))))
1320      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1321        Nat.O)))))))))); special_function_registers_8052 =
1322    (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1323      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1324        Nat.O)))))))))); p1_latch =
1325    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1326      Nat.O))))))))); p3_latch =
1327    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1328      Nat.O))))))))); clock = Nat.O }
1329  in
1330  set_8051_sfr code_mem status0 SFR_SP
1331    (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1332      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1333      (Nat.S Nat.O))))))))
1334
1335(** val sfr_of_Byte :
1336    BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option **)
1337let sfr_of_Byte b =
1338  let address =
1339    Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1340      (Nat.S (Nat.S Nat.O)))))))) b
1341  in
1342  (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1343           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1344           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1345           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1346           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1347           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1348           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1349           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1350           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1351           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1352           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1353           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1354           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1355           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1356           (Nat.S (Nat.S (Nat.S (Nat.S
1357           Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1358   | Bool.True -> Types.None
1359   | Bool.False ->
1360     (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1361              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1362              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1363              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1364              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1365              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1366              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1367              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1368              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1369              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1370              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1371              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1372              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1373              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1374              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1375              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1376              (Nat.S (Nat.S
1377              Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1378      | Bool.True -> Types.Some (Types.Inl SFR_P1)
1379      | Bool.False ->
1380        (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1381                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1382                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1383                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1384                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1385                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1386                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1387                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1388                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1389                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1390                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1391                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1392                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1393                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1394                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1395                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1396                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1397                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1398                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1399                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1400                 (Nat.S (Nat.S
1401                 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1402         | Bool.True -> Types.None
1403         | Bool.False ->
1404           (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1405                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1406                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1407                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1408                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1409                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1410                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1411                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1412                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1413                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1414                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1415                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1416                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1417                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1418                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1419                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1420                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1421                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1422                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1423                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1424                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1425                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1426                    (Nat.S (Nat.S
1427                    Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1428            | Bool.True -> Types.Some (Types.Inl SFR_P3)
1429            | Bool.False ->
1430              (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1431                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1432                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1433                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1434                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1435                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1436                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1437                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1438                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1439                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1440                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1441                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1442                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1443                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1444                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1445                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1446                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1447                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1448                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1449                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1450                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1451                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1452                       (Nat.S
1453                       Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1454               | Bool.True -> Types.Some (Types.Inl SFR_SBUF)
1455               | Bool.False ->
1456                 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1457                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1458                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1459                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1460                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1461                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1462                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1463                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1464                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1465                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1466                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1467                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1468                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1469                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1470                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1471                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1472                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1473                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1474                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1475                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1476                          Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1477                  | Bool.True -> Types.Some (Types.Inl SFR_TL0)
1478                  | Bool.False ->
1479                    (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1480                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1481                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1482                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1483                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1484                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1485                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1486                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1487                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1488                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1489                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1490                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1491                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1492                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1493                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1494                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1495                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1496                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1497                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1498                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1499                             (Nat.S
1500                             Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1501                     | Bool.True -> Types.Some (Types.Inl SFR_TL1)
1502                     | Bool.False ->
1503                       (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1504                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1505                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1506                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1507                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1508                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1509                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1510                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1511                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1512                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1513                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1514                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1515                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1516                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1517                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1518                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1519                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1520                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1521                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1522                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1523                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1524                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1525                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1526                                (Nat.S (Nat.S (Nat.S (Nat.S
1527                                Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1528                        | Bool.True -> Types.Some (Types.Inl SFR_TH0)
1529                        | Bool.False ->
1530                          (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1531                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1532                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1533                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1534                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1535                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1536                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1537                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1538                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1539                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1540                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1541                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1542                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1543                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1544                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1545                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1546                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1547                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1548                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1549                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1550                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1551                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1552                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1553                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1554                                   Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1555                           | Bool.True -> Types.Some (Types.Inl SFR_TH1)
1556                           | Bool.False ->
1557                             (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1558                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1559                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1560                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1561                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1562                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1563                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1564                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1565                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1566                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1567                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1568                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1569                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1570                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1571                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1572                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1573                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1574                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1575                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1576                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1577                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1578                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1579                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1580                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1581                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1582                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1583                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1584                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1585                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1586                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1587                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1588                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1589                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1590                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1591                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1592                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1593                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1594                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1595                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1596                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1597                                      (Nat.S (Nat.S
1598                                      Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1599                              | Bool.True -> Types.Some (Types.Inr SFR_T2CON)
1600                              | Bool.False ->
1601                                (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1602                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1603                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1604                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1605                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1606                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1607                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1608                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1609                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1610                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1611                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1612                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1613                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1614                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1615                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1616                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1617                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1618                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1619                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1620                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1621                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1622                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1623                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1624                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1625                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1626                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1627                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1628                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1629                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1630                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1631                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1632                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1633                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1634                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1635                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1636                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1637                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1638                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1639                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1640                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1641                                         (Nat.S (Nat.S (Nat.S (Nat.S
1642                                         Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1643                                 | Bool.True ->
1644                                   Types.Some (Types.Inr SFR_RCAP2L)
1645                                 | Bool.False ->
1646                                   (match Nat.eqb address (Nat.S (Nat.S
1647                                            (Nat.S (Nat.S (Nat.S (Nat.S
1648                                            (Nat.S (Nat.S (Nat.S (Nat.S
1649                                            (Nat.S (Nat.S (Nat.S (Nat.S
1650                                            (Nat.S (Nat.S (Nat.S (Nat.S
1651                                            (Nat.S (Nat.S (Nat.S (Nat.S
1652                                            (Nat.S (Nat.S (Nat.S (Nat.S
1653                                            (Nat.S (Nat.S (Nat.S (Nat.S
1654                                            (Nat.S (Nat.S (Nat.S (Nat.S
1655                                            (Nat.S (Nat.S (Nat.S (Nat.S
1656                                            (Nat.S (Nat.S (Nat.S (Nat.S
1657                                            (Nat.S (Nat.S (Nat.S (Nat.S
1658                                            (Nat.S (Nat.S (Nat.S (Nat.S
1659                                            (Nat.S (Nat.S (Nat.S (Nat.S
1660                                            (Nat.S (Nat.S (Nat.S (Nat.S
1661                                            (Nat.S (Nat.S (Nat.S (Nat.S
1662                                            (Nat.S (Nat.S (Nat.S (Nat.S
1663                                            (Nat.S (Nat.S (Nat.S (Nat.S
1664                                            (Nat.S (Nat.S (Nat.S (Nat.S
1665                                            (Nat.S (Nat.S (Nat.S (Nat.S
1666                                            (Nat.S (Nat.S (Nat.S (Nat.S
1667                                            (Nat.S (Nat.S (Nat.S (Nat.S
1668                                            (Nat.S (Nat.S (Nat.S (Nat.S
1669                                            (Nat.S (Nat.S (Nat.S (Nat.S
1670                                            (Nat.S (Nat.S (Nat.S (Nat.S
1671                                            (Nat.S (Nat.S (Nat.S (Nat.S
1672                                            (Nat.S (Nat.S (Nat.S (Nat.S
1673                                            (Nat.S (Nat.S (Nat.S (Nat.S
1674                                            (Nat.S (Nat.S (Nat.S (Nat.S
1675                                            (Nat.S (Nat.S (Nat.S (Nat.S
1676                                            (Nat.S (Nat.S (Nat.S (Nat.S
1677                                            (Nat.S (Nat.S (Nat.S (Nat.S
1678                                            (Nat.S (Nat.S (Nat.S (Nat.S
1679                                            (Nat.S (Nat.S (Nat.S (Nat.S
1680                                            (Nat.S (Nat.S (Nat.S (Nat.S
1681                                            (Nat.S (Nat.S (Nat.S (Nat.S
1682                                            (Nat.S (Nat.S (Nat.S (Nat.S
1683                                            (Nat.S (Nat.S (Nat.S (Nat.S
1684                                            (Nat.S (Nat.S (Nat.S (Nat.S
1685                                            (Nat.S (Nat.S (Nat.S (Nat.S
1686                                            (Nat.S (Nat.S (Nat.S (Nat.S
1687                                            (Nat.S (Nat.S (Nat.S (Nat.S
1688                                            (Nat.S (Nat.S (Nat.S (Nat.S
1689                                            (Nat.S (Nat.S (Nat.S (Nat.S
1690                                            (Nat.S (Nat.S (Nat.S (Nat.S
1691                                            (Nat.S (Nat.S (Nat.S (Nat.S
1692                                            (Nat.S (Nat.S (Nat.S (Nat.S
1693                                            (Nat.S (Nat.S (Nat.S (Nat.S
1694                                            (Nat.S (Nat.S (Nat.S (Nat.S
1695                                            (Nat.S (Nat.S (Nat.S (Nat.S
1696                                            (Nat.S (Nat.S (Nat.S (Nat.S
1697                                            (Nat.S
1698                                            Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1699                                    | Bool.True ->
1700                                      Types.Some (Types.Inr SFR_RCAP2H)
1701                                    | Bool.False ->
1702                                      (match Nat.eqb address (Nat.S (Nat.S
1703                                               (Nat.S (Nat.S (Nat.S (Nat.S
1704                                               (Nat.S (Nat.S (Nat.S (Nat.S
1705                                               (Nat.S (Nat.S (Nat.S (Nat.S
1706                                               (Nat.S (Nat.S (Nat.S (Nat.S
1707                                               (Nat.S (Nat.S (Nat.S (Nat.S
1708                                               (Nat.S (Nat.S (Nat.S (Nat.S
1709                                               (Nat.S (Nat.S (Nat.S (Nat.S
1710                                               (Nat.S (Nat.S (Nat.S (Nat.S
1711                                               (Nat.S (Nat.S (Nat.S (Nat.S
1712                                               (Nat.S (Nat.S (Nat.S (Nat.S
1713                                               (Nat.S (Nat.S (Nat.S (Nat.S
1714                                               (Nat.S (Nat.S (Nat.S (Nat.S
1715                                               (Nat.S (Nat.S (Nat.S (Nat.S
1716                                               (Nat.S (Nat.S (Nat.S (Nat.S
1717                                               (Nat.S (Nat.S (Nat.S (Nat.S
1718                                               (Nat.S (Nat.S (Nat.S (Nat.S
1719                                               (Nat.S (Nat.S (Nat.S (Nat.S
1720                                               (Nat.S (Nat.S (Nat.S (Nat.S
1721                                               (Nat.S (Nat.S (Nat.S (Nat.S
1722                                               (Nat.S (Nat.S (Nat.S (Nat.S
1723                                               (Nat.S (Nat.S (Nat.S (Nat.S
1724                                               (Nat.S (Nat.S (Nat.S (Nat.S
1725                                               (Nat.S (Nat.S (Nat.S (Nat.S
1726                                               (Nat.S (Nat.S (Nat.S (Nat.S
1727                                               (Nat.S (Nat.S (Nat.S (Nat.S
1728                                               (Nat.S (Nat.S (Nat.S (Nat.S
1729                                               (Nat.S (Nat.S (Nat.S (Nat.S
1730                                               (Nat.S (Nat.S (Nat.S (Nat.S
1731                                               (Nat.S (Nat.S (Nat.S (Nat.S
1732                                               (Nat.S (Nat.S (Nat.S (Nat.S
1733                                               (Nat.S (Nat.S (Nat.S (Nat.S
1734                                               (Nat.S (Nat.S (Nat.S (Nat.S
1735                                               (Nat.S (Nat.S (Nat.S (Nat.S
1736                                               (Nat.S (Nat.S (Nat.S (Nat.S
1737                                               (Nat.S (Nat.S (Nat.S (Nat.S
1738                                               (Nat.S (Nat.S (Nat.S (Nat.S
1739                                               (Nat.S (Nat.S (Nat.S (Nat.S
1740                                               (Nat.S (Nat.S (Nat.S (Nat.S
1741                                               (Nat.S (Nat.S (Nat.S (Nat.S
1742                                               (Nat.S (Nat.S (Nat.S (Nat.S
1743                                               (Nat.S (Nat.S (Nat.S (Nat.S
1744                                               (Nat.S (Nat.S (Nat.S (Nat.S
1745                                               (Nat.S (Nat.S (Nat.S (Nat.S
1746                                               (Nat.S (Nat.S (Nat.S (Nat.S
1747                                               (Nat.S (Nat.S (Nat.S (Nat.S
1748                                               (Nat.S (Nat.S (Nat.S (Nat.S
1749                                               (Nat.S (Nat.S (Nat.S (Nat.S
1750                                               (Nat.S (Nat.S (Nat.S (Nat.S
1751                                               (Nat.S (Nat.S (Nat.S (Nat.S
1752                                               (Nat.S (Nat.S (Nat.S (Nat.S
1753                                               (Nat.S (Nat.S
1754                                               Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1755                                       | Bool.True ->
1756                                         Types.Some (Types.Inr SFR_TL2)
1757                                       | Bool.False ->
1758                                         (match Nat.eqb address (Nat.S (Nat.S
1759                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1760                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1761                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1762                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1763                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1764                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1765                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1766                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1767                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1768                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1769                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1770                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1771                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1772                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1773                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1774                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1775                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1776                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1777                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1778                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1779                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1780                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1781                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1782                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1783                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1784                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1785                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1786                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1787                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1788                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1789                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1790                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1791                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1792                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1793                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1794                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1795                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1796                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1797                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1798                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1799                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1800                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1801                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1802                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1803                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1804                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1805                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1806                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1807                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1808                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1809                                                  (Nat.S (Nat.S (Nat.S
1810                                                  Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1811                                          | Bool.True ->
1812                                            Types.Some (Types.Inr SFR_TH2)
1813                                          | Bool.False ->
1814                                            (match Nat.eqb address (Nat.S
1815                                                     (Nat.S (Nat.S (Nat.S
1816                                                     (Nat.S (Nat.S (Nat.S
1817                                                     (Nat.S (Nat.S (Nat.S
1818                                                     (Nat.S (Nat.S (Nat.S
1819                                                     (Nat.S (Nat.S (Nat.S
1820                                                     (Nat.S (Nat.S (Nat.S
1821                                                     (Nat.S (Nat.S (Nat.S
1822                                                     (Nat.S (Nat.S (Nat.S
1823                                                     (Nat.S (Nat.S (Nat.S
1824                                                     (Nat.S (Nat.S (Nat.S
1825                                                     (Nat.S (Nat.S (Nat.S
1826                                                     (Nat.S (Nat.S (Nat.S
1827                                                     (Nat.S (Nat.S (Nat.S
1828                                                     (Nat.S (Nat.S (Nat.S
1829                                                     (Nat.S (Nat.S (Nat.S
1830                                                     (Nat.S (Nat.S (Nat.S
1831                                                     (Nat.S (Nat.S (Nat.S
1832                                                     (Nat.S (Nat.S (Nat.S
1833                                                     (Nat.S (Nat.S (Nat.S
1834                                                     (Nat.S (Nat.S (Nat.S
1835                                                     (Nat.S (Nat.S (Nat.S
1836                                                     (Nat.S (Nat.S (Nat.S
1837                                                     (Nat.S (Nat.S (Nat.S
1838                                                     (Nat.S (Nat.S (Nat.S
1839                                                     (Nat.S (Nat.S (Nat.S
1840                                                     (Nat.S (Nat.S (Nat.S
1841                                                     (Nat.S (Nat.S (Nat.S
1842                                                     (Nat.S (Nat.S (Nat.S
1843                                                     (Nat.S (Nat.S (Nat.S
1844                                                     (Nat.S (Nat.S (Nat.S
1845                                                     (Nat.S (Nat.S (Nat.S
1846                                                     (Nat.S (Nat.S (Nat.S
1847                                                     (Nat.S (Nat.S (Nat.S
1848                                                     (Nat.S (Nat.S (Nat.S
1849                                                     (Nat.S (Nat.S (Nat.S
1850                                                     (Nat.S (Nat.S (Nat.S
1851                                                     (Nat.S (Nat.S (Nat.S
1852                                                     (Nat.S (Nat.S (Nat.S
1853                                                     (Nat.S (Nat.S (Nat.S
1854                                                     (Nat.S (Nat.S (Nat.S
1855                                                     (Nat.S (Nat.S (Nat.S
1856                                                     (Nat.S (Nat.S (Nat.S
1857                                                     (Nat.S (Nat.S (Nat.S
1858                                                     (Nat.S (Nat.S (Nat.S
1859                                                     (Nat.S (Nat.S
1860                                                     Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1861                                             | Bool.True ->
1862                                               Types.Some (Types.Inl
1863                                                 SFR_PCON)
1864                                             | Bool.False ->
1865                                               (match Nat.eqb address (Nat.S
1866                                                        (Nat.S (Nat.S (Nat.S
1867                                                        (Nat.S (Nat.S (Nat.S
1868                                                        (Nat.S (Nat.S (Nat.S
1869                                                        (Nat.S (Nat.S (Nat.S
1870                                                        (Nat.S (Nat.S (Nat.S
1871                                                        (Nat.S (Nat.S (Nat.S
1872                                                        (Nat.S (Nat.S (Nat.S
1873                                                        (Nat.S (Nat.S (Nat.S
1874                                                        (Nat.S (Nat.S (Nat.S
1875                                                        (Nat.S (Nat.S (Nat.S
1876                                                        (Nat.S (Nat.S (Nat.S
1877                                                        (Nat.S (Nat.S (Nat.S
1878                                                        (Nat.S (Nat.S (Nat.S
1879                                                        (Nat.S (Nat.S (Nat.S
1880                                                        (Nat.S (Nat.S (Nat.S
1881                                                        (Nat.S (Nat.S (Nat.S
1882                                                        (Nat.S (Nat.S (Nat.S
1883                                                        (Nat.S (Nat.S (Nat.S
1884                                                        (Nat.S (Nat.S (Nat.S
1885                                                        (Nat.S (Nat.S (Nat.S
1886                                                        (Nat.S (Nat.S (Nat.S
1887                                                        (Nat.S (Nat.S (Nat.S
1888                                                        (Nat.S (Nat.S (Nat.S
1889                                                        (Nat.S (Nat.S (Nat.S
1890                                                        (Nat.S (Nat.S (Nat.S
1891                                                        (Nat.S (Nat.S (Nat.S
1892                                                        (Nat.S (Nat.S (Nat.S
1893                                                        (Nat.S (Nat.S (Nat.S
1894                                                        (Nat.S (Nat.S (Nat.S
1895                                                        (Nat.S (Nat.S (Nat.S
1896                                                        (Nat.S (Nat.S (Nat.S
1897                                                        (Nat.S (Nat.S (Nat.S
1898                                                        (Nat.S (Nat.S (Nat.S
1899                                                        (Nat.S (Nat.S (Nat.S
1900                                                        (Nat.S (Nat.S (Nat.S
1901                                                        (Nat.S (Nat.S (Nat.S
1902                                                        (Nat.S (Nat.S (Nat.S
1903                                                        (Nat.S (Nat.S (Nat.S
1904                                                        (Nat.S (Nat.S (Nat.S
1905                                                        (Nat.S (Nat.S (Nat.S
1906                                                        (Nat.S (Nat.S (Nat.S
1907                                                        (Nat.S (Nat.S (Nat.S
1908                                                        (Nat.S (Nat.S (Nat.S
1909                                                        (Nat.S (Nat.S (Nat.S
1910                                                        (Nat.S (Nat.S (Nat.S
1911                                                        Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1912                                                | Bool.True ->
1913                                                  Types.Some (Types.Inl
1914                                                    SFR_TCON)
1915                                                | Bool.False ->
1916                                                  (match Nat.eqb address
1917                                                           (Nat.S (Nat.S
1918                                                           (Nat.S (Nat.S
1919                                                           (Nat.S (Nat.S
1920                                                           (Nat.S (Nat.S
1921                                                           (Nat.S (Nat.S
1922                                                           (Nat.S (Nat.S
1923                                                           (Nat.S (Nat.S
1924                                                           (Nat.S (Nat.S
1925                                                           (Nat.S (Nat.S
1926                                                           (Nat.S (Nat.S
1927                                                           (Nat.S (Nat.S
1928                                                           (Nat.S (Nat.S
1929                                                           (Nat.S (Nat.S
1930                                                           (Nat.S (Nat.S
1931                                                           (Nat.S (Nat.S
1932                                                           (Nat.S (Nat.S
1933                                                           (Nat.S (Nat.S
1934                                                           (Nat.S (Nat.S
1935                                                           (Nat.S (Nat.S
1936                                                           (Nat.S (Nat.S
1937                                                           (Nat.S (Nat.S
1938                                                           (Nat.S (Nat.S
1939                                                           (Nat.S (Nat.S
1940                                                           (Nat.S (Nat.S
1941                                                           (Nat.S (Nat.S
1942                                                           (Nat.S (Nat.S
1943                                                           (Nat.S (Nat.S
1944                                                           (Nat.S (Nat.S
1945                                                           (Nat.S (Nat.S
1946                                                           (Nat.S (Nat.S
1947                                                           (Nat.S (Nat.S
1948                                                           (Nat.S (Nat.S
1949                                                           (Nat.S (Nat.S
1950                                                           (Nat.S (Nat.S
1951                                                           (Nat.S (Nat.S
1952                                                           (Nat.S (Nat.S
1953                                                           (Nat.S (Nat.S
1954                                                           (Nat.S (Nat.S
1955                                                           (Nat.S (Nat.S
1956                                                           (Nat.S (Nat.S
1957                                                           (Nat.S (Nat.S
1958                                                           (Nat.S (Nat.S
1959                                                           (Nat.S (Nat.S
1960                                                           (Nat.S (Nat.S
1961                                                           (Nat.S (Nat.S
1962                                                           (Nat.S (Nat.S
1963                                                           (Nat.S (Nat.S
1964                                                           (Nat.S (Nat.S
1965                                                           (Nat.S (Nat.S
1966                                                           (Nat.S (Nat.S
1967                                                           (Nat.S (Nat.S
1968                                                           (Nat.S (Nat.S
1969                                                           (Nat.S (Nat.S
1970                                                           (Nat.S (Nat.S
1971                                                           (Nat.S (Nat.S
1972                                                           (Nat.S (Nat.S
1973                                                           (Nat.S (Nat.S
1974                                                           (Nat.S (Nat.S
1975                                                           (Nat.S (Nat.S
1976                                                           (Nat.S (Nat.S
1977                                                           (Nat.S (Nat.S
1978                                                           (Nat.S (Nat.S
1979                                                           (Nat.S (Nat.S
1980                                                           (Nat.S (Nat.S
1981                                                           (Nat.S (Nat.S
1982                                                           (Nat.S (Nat.S
1983                                                           (Nat.S (Nat.S
1984                                                           (Nat.S (Nat.S
1985                                                           (Nat.S
1986                                                           Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1987                                                   | Bool.True ->
1988                                                     Types.Some (Types.Inl
1989                                                       SFR_TMOD)
1990                                                   | Bool.False ->
1991                                                     (match Nat.eqb address
1992                                                              (Nat.S (Nat.S
1993                                                              (Nat.S (Nat.S
1994                                                              (Nat.S (Nat.S
1995                                                              (Nat.S (Nat.S
1996                                                              (Nat.S (Nat.S
1997                                                              (Nat.S (Nat.S
1998                                                              (Nat.S (Nat.S
1999                                                              (Nat.S (Nat.S
2000                                                              (Nat.S (Nat.S
2001                                                              (Nat.S (Nat.S
2002                                                              (Nat.S (Nat.S
2003                                                              (Nat.S (Nat.S
2004                                                              (Nat.S (Nat.S
2005                                                              (Nat.S (Nat.S
2006                                                              (Nat.S (Nat.S
2007                                                              (Nat.S (Nat.S
2008                                                              (Nat.S (Nat.S
2009                                                              (Nat.S (Nat.S
2010                                                              (Nat.S (Nat.S
2011                                                              (Nat.S (Nat.S
2012                                                              (Nat.S (Nat.S
2013                                                              (Nat.S (Nat.S
2014                                                              (Nat.S (Nat.S
2015                                                              (Nat.S (Nat.S
2016                                                              (Nat.S (Nat.S
2017                                                              (Nat.S (Nat.S
2018                                                              (Nat.S (Nat.S
2019                                                              (Nat.S (Nat.S
2020                                                              (Nat.S (Nat.S
2021                                                              (Nat.S (Nat.S
2022                                                              (Nat.S (Nat.S
2023                                                              (Nat.S (Nat.S
2024                                                              (Nat.S (Nat.S
2025                                                              (Nat.S (Nat.S
2026                                                              (Nat.S (Nat.S
2027                                                              (Nat.S (Nat.S
2028                                                              (Nat.S (Nat.S
2029                                                              (Nat.S (Nat.S
2030                                                              (Nat.S (Nat.S
2031                                                              (Nat.S (Nat.S
2032                                                              (Nat.S (Nat.S
2033                                                              (Nat.S (Nat.S
2034                                                              (Nat.S (Nat.S
2035                                                              (Nat.S (Nat.S
2036                                                              (Nat.S (Nat.S
2037                                                              (Nat.S (Nat.S
2038                                                              (Nat.S (Nat.S
2039                                                              (Nat.S (Nat.S
2040                                                              (Nat.S (Nat.S
2041                                                              (Nat.S (Nat.S
2042                                                              (Nat.S (Nat.S
2043                                                              (Nat.S (Nat.S
2044                                                              (Nat.S (Nat.S
2045                                                              (Nat.S (Nat.S
2046                                                              (Nat.S (Nat.S
2047                                                              (Nat.S (Nat.S
2048                                                              (Nat.S (Nat.S
2049                                                              (Nat.S (Nat.S
2050                                                              (Nat.S (Nat.S
2051                                                              (Nat.S (Nat.S
2052                                                              (Nat.S (Nat.S
2053                                                              (Nat.S (Nat.S
2054                                                              (Nat.S (Nat.S
2055                                                              (Nat.S (Nat.S
2056                                                              (Nat.S (Nat.S
2057                                                              (Nat.S (Nat.S
2058                                                              (Nat.S (Nat.S
2059                                                              (Nat.S (Nat.S
2060                                                              (Nat.S (Nat.S
2061                                                              (Nat.S (Nat.S
2062                                                              (Nat.S (Nat.S
2063                                                              (Nat.S (Nat.S
2064                                                              (Nat.S (Nat.S
2065                                                              (Nat.S (Nat.S
2066                                                              (Nat.S (Nat.S
2067                                                              (Nat.S (Nat.S
2068                                                              Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2069                                                      | Bool.True ->
2070                                                        Types.Some (Types.Inl
2071                                                          SFR_SCON)
2072                                                      | Bool.False ->
2073                                                        (match Nat.eqb
2074                                                                 address
2075                                                                 (Nat.S
2076                                                                 (Nat.S
2077                                                                 (Nat.S
2078                                                                 (Nat.S
2079                                                                 (Nat.S
2080                                                                 (Nat.S
2081                                                                 (Nat.S
2082                                                                 (Nat.S
2083                                                                 (Nat.S
2084                                                                 (Nat.S
2085                                                                 (Nat.S
2086                                                                 (Nat.S
2087                                                                 (Nat.S
2088                                                                 (Nat.S
2089                                                                 (Nat.S
2090                                                                 (Nat.S
2091                                                                 (Nat.S
2092                                                                 (Nat.S
2093                                                                 (Nat.S
2094                                                                 (Nat.S
2095                                                                 (Nat.S
2096                                                                 (Nat.S
2097                                                                 (Nat.S
2098                                                                 (Nat.S
2099                                                                 (Nat.S
2100                                                                 (Nat.S
2101                                                                 (Nat.S
2102                                                                 (Nat.S
2103                                                                 (Nat.S
2104                                                                 (Nat.S
2105                                                                 (Nat.S
2106                                                                 (Nat.S
2107                                                                 (Nat.S
2108                                                                 (Nat.S
2109                                                                 (Nat.S
2110                                                                 (Nat.S
2111                                                                 (Nat.S
2112                                                                 (Nat.S
2113                                                                 (Nat.S
2114                                                                 (Nat.S
2115                                                                 (Nat.S
2116                                                                 (Nat.S
2117                                                                 (Nat.S
2118                                                                 (Nat.S
2119                                                                 (Nat.S
2120                                                                 (Nat.S
2121                                                                 (Nat.S
2122                                                                 (Nat.S
2123                                                                 (Nat.S
2124                                                                 (Nat.S
2125                                                                 (Nat.S
2126                                                                 (Nat.S
2127                                                                 (Nat.S
2128                                                                 (Nat.S
2129                                                                 (Nat.S
2130                                                                 (Nat.S
2131                                                                 (Nat.S
2132                                                                 (Nat.S
2133                                                                 (Nat.S
2134                                                                 (Nat.S
2135                                                                 (Nat.S
2136                                                                 (Nat.S
2137                                                                 (Nat.S
2138                                                                 (Nat.S
2139                                                                 (Nat.S
2140                                                                 (Nat.S
2141                                                                 (Nat.S
2142                                                                 (Nat.S
2143                                                                 (Nat.S
2144                                                                 (Nat.S
2145                                                                 (Nat.S
2146                                                                 (Nat.S
2147                                                                 (Nat.S
2148                                                                 (Nat.S
2149                                                                 (Nat.S
2150                                                                 (Nat.S
2151                                                                 (Nat.S
2152                                                                 (Nat.S
2153                                                                 (Nat.S
2154                                                                 (Nat.S
2155                                                                 (Nat.S
2156                                                                 (Nat.S
2157                                                                 (Nat.S
2158                                                                 (Nat.S
2159                                                                 (Nat.S
2160                                                                 (Nat.S
2161                                                                 (Nat.S
2162                                                                 (Nat.S
2163                                                                 (Nat.S
2164                                                                 (Nat.S
2165                                                                 (Nat.S
2166                                                                 (Nat.S
2167                                                                 (Nat.S
2168                                                                 (Nat.S
2169                                                                 (Nat.S
2170                                                                 (Nat.S
2171                                                                 (Nat.S
2172                                                                 (Nat.S
2173                                                                 (Nat.S
2174                                                                 (Nat.S
2175                                                                 (Nat.S
2176                                                                 (Nat.S
2177                                                                 (Nat.S
2178                                                                 (Nat.S
2179                                                                 (Nat.S
2180                                                                 (Nat.S
2181                                                                 (Nat.S
2182                                                                 (Nat.S
2183                                                                 (Nat.S
2184                                                                 (Nat.S
2185                                                                 (Nat.S
2186                                                                 (Nat.S
2187                                                                 (Nat.S
2188                                                                 (Nat.S
2189                                                                 (Nat.S
2190                                                                 (Nat.S
2191                                                                 (Nat.S
2192                                                                 (Nat.S
2193                                                                 (Nat.S
2194                                                                 (Nat.S
2195                                                                 (Nat.S
2196                                                                 (Nat.S
2197                                                                 (Nat.S
2198                                                                 (Nat.S
2199                                                                 (Nat.S
2200                                                                 (Nat.S
2201                                                                 (Nat.S
2202                                                                 (Nat.S
2203                                                                 (Nat.S
2204                                                                 (Nat.S
2205                                                                 (Nat.S
2206                                                                 (Nat.S
2207                                                                 (Nat.S
2208                                                                 (Nat.S
2209                                                                 (Nat.S
2210                                                                 (Nat.S
2211                                                                 (Nat.S
2212                                                                 (Nat.S
2213                                                                 (Nat.S
2214                                                                 (Nat.S
2215                                                                 (Nat.S
2216                                                                 (Nat.S
2217                                                                 (Nat.S
2218                                                                 (Nat.S
2219                                                                 (Nat.S
2220                                                                 (Nat.S
2221                                                                 (Nat.S
2222                                                                 (Nat.S
2223                                                                 (Nat.S
2224                                                                 (Nat.S
2225                                                                 (Nat.S
2226                                                                 (Nat.S
2227                                                                 (Nat.S
2228                                                                 (Nat.S
2229                                                                 (Nat.S
2230                                                                 (Nat.S
2231                                                                 (Nat.S
2232                                                                 (Nat.S
2233                                                                 (Nat.S
2234                                                                 (Nat.S
2235                                                                 (Nat.S
2236                                                                 (Nat.S
2237                                                                 (Nat.S
2238                                                                 (Nat.S
2239                                                                 (Nat.S
2240                                                                 (Nat.S
2241                                                                 (Nat.S
2242                                                                 (Nat.S
2243                                                                 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2244                                                         | Bool.True ->
2245                                                           Types.Some
2246                                                             (Types.Inl
2247                                                             SFR_IE)
2248                                                         | Bool.False ->
2249                                                           (match Nat.eqb
2250                                                                    address
2251                                                                    (Nat.S
2252                                                                    (Nat.S
2253                                                                    (Nat.S
2254                                                                    (Nat.S
2255                                                                    (Nat.S
2256                                                                    (Nat.S
2257                                                                    (Nat.S
2258                                                                    (Nat.S
2259                                                                    (Nat.S
2260                                                                    (Nat.S
2261                                                                    (Nat.S
2262                                                                    (Nat.S
2263                                                                    (Nat.S
2264                                                                    (Nat.S
2265                                                                    (Nat.S
2266                                                                    (Nat.S
2267                                                                    (Nat.S
2268                                                                    (Nat.S
2269                                                                    (Nat.S
2270                                                                    (Nat.S
2271                                                                    (Nat.S
2272                                                                    (Nat.S
2273                                                                    (Nat.S
2274                                                                    (Nat.S
2275                                                                    (Nat.S
2276                                                                    (Nat.S
2277                                                                    (Nat.S
2278                                                                    (Nat.S
2279                                                                    (Nat.S
2280                                                                    (Nat.S
2281                                                                    (Nat.S
2282                                                                    (Nat.S
2283                                                                    (Nat.S
2284                                                                    (Nat.S
2285                                                                    (Nat.S
2286                                                                    (Nat.S
2287                                                                    (Nat.S
2288                                                                    (Nat.S
2289                                                                    (Nat.S
2290                                                                    (Nat.S
2291                                                                    (Nat.S
2292                                                                    (Nat.S
2293                                                                    (Nat.S
2294                                                                    (Nat.S
2295                                                                    (Nat.S
2296                                                                    (Nat.S
2297                                                                    (Nat.S
2298                                                                    (Nat.S
2299                                                                    (Nat.S
2300                                                                    (Nat.S
2301                                                                    (Nat.S
2302                                                                    (Nat.S
2303                                                                    (Nat.S
2304                                                                    (Nat.S
2305                                                                    (Nat.S
2306                                                                    (Nat.S
2307                                                                    (Nat.S
2308                                                                    (Nat.S
2309                                                                    (Nat.S
2310                                                                    (Nat.S
2311                                                                    (Nat.S
2312                                                                    (Nat.S
2313                                                                    (Nat.S
2314                                                                    (Nat.S
2315                                                                    (Nat.S
2316                                                                    (Nat.S
2317                                                                    (Nat.S
2318                                                                    (Nat.S
2319                                                                    (Nat.S
2320                                                                    (Nat.S
2321                                                                    (Nat.S
2322                                                                    (Nat.S
2323                                                                    (Nat.S
2324                                                                    (Nat.S
2325                                                                    (Nat.S
2326                                                                    (Nat.S
2327                                                                    (Nat.S
2328                                                                    (Nat.S
2329                                                                    (Nat.S
2330                                                                    (Nat.S
2331                                                                    (Nat.S
2332                                                                    (Nat.S
2333                                                                    (Nat.S
2334                                                                    (Nat.S
2335                                                                    (Nat.S
2336                                                                    (Nat.S
2337                                                                    (Nat.S
2338                                                                    (Nat.S
2339                                                                    (Nat.S
2340                                                                    (Nat.S
2341                                                                    (Nat.S
2342                                                                    (Nat.S
2343                                                                    (Nat.S
2344                                                                    (Nat.S
2345                                                                    (Nat.S
2346                                                                    (Nat.S
2347                                                                    (Nat.S
2348                                                                    (Nat.S
2349                                                                    (Nat.S
2350                                                                    (Nat.S
2351                                                                    (Nat.S
2352                                                                    (Nat.S
2353                                                                    (Nat.S
2354                                                                    (Nat.S
2355                                                                    (Nat.S
2356                                                                    (Nat.S
2357                                                                    (Nat.S
2358                                                                    (Nat.S
2359                                                                    (Nat.S
2360                                                                    (Nat.S
2361                                                                    (Nat.S
2362                                                                    (Nat.S
2363                                                                    (Nat.S
2364                                                                    (Nat.S
2365                                                                    (Nat.S
2366                                                                    (Nat.S
2367                                                                    (Nat.S
2368                                                                    (Nat.S
2369                                                                    (Nat.S
2370                                                                    (Nat.S
2371                                                                    (Nat.S
2372                                                                    (Nat.S
2373                                                                    (Nat.S
2374                                                                    (Nat.S
2375                                                                    (Nat.S
2376                                                                    (Nat.S
2377                                                                    (Nat.S
2378                                                                    (Nat.S
2379                                                                    (Nat.S
2380                                                                    (Nat.S
2381                                                                    (Nat.S
2382                                                                    (Nat.S
2383                                                                    (Nat.S
2384                                                                    (Nat.S
2385                                                                    (Nat.S
2386                                                                    (Nat.S
2387                                                                    (Nat.S
2388                                                                    (Nat.S
2389                                                                    (Nat.S
2390                                                                    (Nat.S
2391                                                                    (Nat.S
2392                                                                    (Nat.S
2393                                                                    (Nat.S
2394                                                                    (Nat.S
2395                                                                    (Nat.S
2396                                                                    (Nat.S
2397                                                                    (Nat.S
2398                                                                    (Nat.S
2399                                                                    (Nat.S
2400                                                                    (Nat.S
2401                                                                    (Nat.S
2402                                                                    (Nat.S
2403                                                                    (Nat.S
2404                                                                    (Nat.S
2405                                                                    (Nat.S
2406                                                                    (Nat.S
2407                                                                    (Nat.S
2408                                                                    (Nat.S
2409                                                                    (Nat.S
2410                                                                    (Nat.S
2411                                                                    (Nat.S
2412                                                                    (Nat.S
2413                                                                    (Nat.S
2414                                                                    (Nat.S
2415                                                                    (Nat.S
2416                                                                    (Nat.S
2417                                                                    (Nat.S
2418                                                                    (Nat.S
2419                                                                    (Nat.S
2420                                                                    (Nat.S
2421                                                                    (Nat.S
2422                                                                    (Nat.S
2423                                                                    (Nat.S
2424                                                                    (Nat.S
2425                                                                    (Nat.S
2426                                                                    (Nat.S
2427                                                                    (Nat.S
2428                                                                    (Nat.S
2429                                                                    (Nat.S
2430                                                                    (Nat.S
2431                                                                    (Nat.S
2432                                                                    (Nat.S
2433                                                                    (Nat.S
2434                                                                    (Nat.S
2435                                                                    Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2436                                                            | Bool.True ->
2437                                                              Types.Some
2438                                                                (Types.Inl
2439                                                                SFR_IP)
2440                                                            | Bool.False ->
2441                                                              (match 
2442                                                               Nat.eqb
2443                                                                 address
2444                                                                 (Nat.S
2445                                                                 (Nat.S
2446                                                                 (Nat.S
2447                                                                 (Nat.S
2448                                                                 (Nat.S
2449                                                                 (Nat.S
2450                                                                 (Nat.S
2451                                                                 (Nat.S
2452                                                                 (Nat.S
2453                                                                 (Nat.S
2454                                                                 (Nat.S
2455                                                                 (Nat.S
2456                                                                 (Nat.S
2457                                                                 (Nat.S
2458                                                                 (Nat.S
2459                                                                 (Nat.S
2460                                                                 (Nat.S
2461                                                                 (Nat.S
2462                                                                 (Nat.S
2463                                                                 (Nat.S
2464                                                                 (Nat.S
2465                                                                 (Nat.S
2466                                                                 (Nat.S
2467                                                                 (Nat.S
2468                                                                 (Nat.S
2469                                                                 (Nat.S
2470                                                                 (Nat.S
2471                                                                 (Nat.S
2472                                                                 (Nat.S
2473                                                                 (Nat.S
2474                                                                 (Nat.S
2475                                                                 (Nat.S
2476                                                                 (Nat.S
2477                                                                 (Nat.S
2478                                                                 (Nat.S
2479                                                                 (Nat.S
2480                                                                 (Nat.S
2481                                                                 (Nat.S
2482                                                                 (Nat.S
2483                                                                 (Nat.S
2484                                                                 (Nat.S
2485                                                                 (Nat.S
2486                                                                 (Nat.S
2487                                                                 (Nat.S
2488                                                                 (Nat.S
2489                                                                 (Nat.S
2490                                                                 (Nat.S
2491                                                                 (Nat.S
2492                                                                 (Nat.S
2493                                                                 (Nat.S
2494                                                                 (Nat.S
2495                                                                 (Nat.S
2496                                                                 (Nat.S
2497                                                                 (Nat.S
2498                                                                 (Nat.S
2499                                                                 (Nat.S
2500                                                                 (Nat.S
2501                                                                 (Nat.S
2502                                                                 (Nat.S
2503                                                                 (Nat.S
2504                                                                 (Nat.S
2505                                                                 (Nat.S
2506                                                                 (Nat.S
2507                                                                 (Nat.S
2508                                                                 (Nat.S
2509                                                                 (Nat.S
2510                                                                 (Nat.S
2511                                                                 (Nat.S
2512                                                                 (Nat.S
2513                                                                 (Nat.S
2514                                                                 (Nat.S
2515                                                                 (Nat.S
2516                                                                 (Nat.S
2517                                                                 (Nat.S
2518                                                                 (Nat.S
2519                                                                 (Nat.S
2520                                                                 (Nat.S
2521                                                                 (Nat.S
2522                                                                 (Nat.S
2523                                                                 (Nat.S
2524                                                                 (Nat.S
2525                                                                 (Nat.S
2526                                                                 (Nat.S
2527                                                                 (Nat.S
2528                                                                 (Nat.S
2529                                                                 (Nat.S
2530                                                                 (Nat.S
2531                                                                 (Nat.S
2532                                                                 (Nat.S
2533                                                                 (Nat.S
2534                                                                 (Nat.S
2535                                                                 (Nat.S
2536                                                                 (Nat.S
2537                                                                 (Nat.S
2538                                                                 (Nat.S
2539                                                                 (Nat.S
2540                                                                 (Nat.S
2541                                                                 (Nat.S
2542                                                                 (Nat.S
2543                                                                 (Nat.S
2544                                                                 (Nat.S
2545                                                                 (Nat.S
2546                                                                 (Nat.S
2547                                                                 (Nat.S
2548                                                                 (Nat.S
2549                                                                 (Nat.S
2550                                                                 (Nat.S
2551                                                                 (Nat.S
2552                                                                 (Nat.S
2553                                                                 (Nat.S
2554                                                                 (Nat.S
2555                                                                 (Nat.S
2556                                                                 (Nat.S
2557                                                                 (Nat.S
2558                                                                 (Nat.S
2559                                                                 (Nat.S
2560                                                                 (Nat.S
2561                                                                 (Nat.S
2562                                                                 (Nat.S
2563                                                                 (Nat.S
2564                                                                 (Nat.S
2565                                                                 (Nat.S
2566                                                                 (Nat.S
2567                                                                 (Nat.S
2568                                                                 (Nat.S
2569                                                                 (Nat.S
2570                                                                 (Nat.S
2571                                                                 (Nat.S
2572                                                                 (Nat.S
2573                                                                 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2574                                                               | Bool.True ->
2575                                                                 Types.Some
2576                                                                   (Types.Inl
2577                                                                   SFR_SP)
2578                                                               | Bool.False ->
2579                                                                 (match 
2580                                                                  Nat.eqb
2581                                                                    address
2582                                                                    (Nat.S
2583                                                                    (Nat.S
2584                                                                    (Nat.S
2585                                                                    (Nat.S
2586                                                                    (Nat.S
2587                                                                    (Nat.S
2588                                                                    (Nat.S
2589                                                                    (Nat.S
2590                                                                    (Nat.S
2591                                                                    (Nat.S
2592                                                                    (Nat.S
2593                                                                    (Nat.S
2594                                                                    (Nat.S
2595                                                                    (Nat.S
2596                                                                    (Nat.S
2597                                                                    (Nat.S
2598                                                                    (Nat.S
2599                                                                    (Nat.S
2600                                                                    (Nat.S
2601                                                                    (Nat.S
2602                                                                    (Nat.S
2603                                                                    (Nat.S
2604                                                                    (Nat.S
2605                                                                    (Nat.S
2606                                                                    (Nat.S
2607                                                                    (Nat.S
2608                                                                    (Nat.S
2609                                                                    (Nat.S
2610                                                                    (Nat.S
2611                                                                    (Nat.S
2612                                                                    (Nat.S
2613                                                                    (Nat.S
2614                                                                    (Nat.S
2615                                                                    (Nat.S
2616                                                                    (Nat.S
2617                                                                    (Nat.S
2618                                                                    (Nat.S
2619                                                                    (Nat.S
2620                                                                    (Nat.S
2621                                                                    (Nat.S
2622                                                                    (Nat.S
2623                                                                    (Nat.S
2624                                                                    (Nat.S
2625                                                                    (Nat.S
2626                                                                    (Nat.S
2627                                                                    (Nat.S
2628                                                                    (Nat.S
2629                                                                    (Nat.S
2630                                                                    (Nat.S
2631                                                                    (Nat.S
2632                                                                    (Nat.S
2633                                                                    (Nat.S
2634                                                                    (Nat.S
2635                                                                    (Nat.S
2636                                                                    (Nat.S
2637                                                                    (Nat.S
2638                                                                    (Nat.S
2639                                                                    (Nat.S
2640                                                                    (Nat.S
2641                                                                    (Nat.S
2642                                                                    (Nat.S
2643                                                                    (Nat.S
2644                                                                    (Nat.S
2645                                                                    (Nat.S
2646                                                                    (Nat.S
2647                                                                    (Nat.S
2648                                                                    (Nat.S
2649                                                                    (Nat.S
2650                                                                    (Nat.S
2651                                                                    (Nat.S
2652                                                                    (Nat.S
2653                                                                    (Nat.S
2654                                                                    (Nat.S
2655                                                                    (Nat.S
2656                                                                    (Nat.S
2657                                                                    (Nat.S
2658                                                                    (Nat.S
2659                                                                    (Nat.S
2660                                                                    (Nat.S
2661                                                                    (Nat.S
2662                                                                    (Nat.S
2663                                                                    (Nat.S
2664                                                                    (Nat.S
2665                                                                    (Nat.S
2666                                                                    (Nat.S
2667                                                                    (Nat.S
2668                                                                    (Nat.S
2669                                                                    (Nat.S
2670                                                                    (Nat.S
2671                                                                    (Nat.S
2672                                                                    (Nat.S
2673                                                                    (Nat.S
2674                                                                    (Nat.S
2675                                                                    (Nat.S
2676                                                                    (Nat.S
2677                                                                    (Nat.S
2678                                                                    (Nat.S
2679                                                                    (Nat.S
2680                                                                    (Nat.S
2681                                                                    (Nat.S
2682                                                                    (Nat.S
2683                                                                    (Nat.S
2684                                                                    (Nat.S
2685                                                                    (Nat.S
2686                                                                    (Nat.S
2687                                                                    (Nat.S
2688                                                                    (Nat.S
2689                                                                    (Nat.S
2690                                                                    (Nat.S
2691                                                                    (Nat.S
2692                                                                    (Nat.S
2693                                                                    (Nat.S
2694                                                                    (Nat.S
2695                                                                    (Nat.S
2696                                                                    (Nat.S
2697                                                                    (Nat.S
2698                                                                    (Nat.S
2699                                                                    (Nat.S
2700                                                                    (Nat.S
2701                                                                    (Nat.S
2702                                                                    (Nat.S
2703                                                                    (Nat.S
2704                                                                    (Nat.S
2705                                                                    (Nat.S
2706                                                                    (Nat.S
2707                                                                    (Nat.S
2708                                                                    (Nat.S
2709                                                                    (Nat.S
2710                                                                    (Nat.S
2711                                                                    (Nat.S
2712                                                                    Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2713                                                                  | Bool.True ->
2714                                                                    Types.Some
2715                                                                    (Types.Inl
2716                                                                    SFR_DPL)
2717                                                                  | Bool.False ->
2718                                                                    (match 
2719                                                                    Nat.eqb
2720                                                                    address
2721                                                                    (Nat.S
2722                                                                    (Nat.S
2723                                                                    (Nat.S
2724                                                                    (Nat.S
2725                                                                    (Nat.S
2726                                                                    (Nat.S
2727                                                                    (Nat.S
2728                                                                    (Nat.S
2729                                                                    (Nat.S
2730                                                                    (Nat.S
2731                                                                    (Nat.S
2732                                                                    (Nat.S
2733                                                                    (Nat.S
2734                                                                    (Nat.S
2735                                                                    (Nat.S
2736                                                                    (Nat.S
2737                                                                    (Nat.S
2738                                                                    (Nat.S
2739                                                                    (Nat.S
2740                                                                    (Nat.S
2741                                                                    (Nat.S
2742                                                                    (Nat.S
2743                                                                    (Nat.S
2744                                                                    (Nat.S
2745                                                                    (Nat.S
2746                                                                    (Nat.S
2747                                                                    (Nat.S
2748                                                                    (Nat.S
2749                                                                    (Nat.S
2750                                                                    (Nat.S
2751                                                                    (Nat.S
2752                                                                    (Nat.S
2753                                                                    (Nat.S
2754                                                                    (Nat.S
2755                                                                    (Nat.S
2756                                                                    (Nat.S
2757                                                                    (Nat.S
2758                                                                    (Nat.S
2759                                                                    (Nat.S
2760                                                                    (Nat.S
2761                                                                    (Nat.S
2762                                                                    (Nat.S
2763                                                                    (Nat.S
2764                                                                    (Nat.S
2765                                                                    (Nat.S
2766                                                                    (Nat.S
2767                                                                    (Nat.S
2768                                                                    (Nat.S
2769                                                                    (Nat.S
2770                                                                    (Nat.S
2771                                                                    (Nat.S
2772                                                                    (Nat.S
2773                                                                    (Nat.S
2774                                                                    (Nat.S
2775                                                                    (Nat.S
2776                                                                    (Nat.S
2777                                                                    (Nat.S
2778                                                                    (Nat.S
2779                                                                    (Nat.S
2780                                                                    (Nat.S
2781                                                                    (Nat.S
2782                                                                    (Nat.S
2783                                                                    (Nat.S
2784                                                                    (Nat.S
2785                                                                    (Nat.S
2786                                                                    (Nat.S
2787                                                                    (Nat.S
2788                                                                    (Nat.S
2789                                                                    (Nat.S
2790                                                                    (Nat.S
2791                                                                    (Nat.S
2792                                                                    (Nat.S
2793                                                                    (Nat.S
2794                                                                    (Nat.S
2795                                                                    (Nat.S
2796                                                                    (Nat.S
2797                                                                    (Nat.S
2798                                                                    (Nat.S
2799                                                                    (Nat.S
2800                                                                    (Nat.S
2801                                                                    (Nat.S
2802                                                                    (Nat.S
2803                                                                    (Nat.S
2804                                                                    (Nat.S
2805                                                                    (Nat.S
2806                                                                    (Nat.S
2807                                                                    (Nat.S
2808                                                                    (Nat.S
2809                                                                    (Nat.S
2810                                                                    (Nat.S
2811                                                                    (Nat.S
2812                                                                    (Nat.S
2813                                                                    (Nat.S
2814                                                                    (Nat.S
2815                                                                    (Nat.S
2816                                                                    (Nat.S
2817                                                                    (Nat.S
2818                                                                    (Nat.S
2819                                                                    (Nat.S
2820                                                                    (Nat.S
2821                                                                    (Nat.S
2822                                                                    (Nat.S
2823                                                                    (Nat.S
2824                                                                    (Nat.S
2825                                                                    (Nat.S
2826                                                                    (Nat.S
2827                                                                    (Nat.S
2828                                                                    (Nat.S
2829                                                                    (Nat.S
2830                                                                    (Nat.S
2831                                                                    (Nat.S
2832                                                                    (Nat.S
2833                                                                    (Nat.S
2834                                                                    (Nat.S
2835                                                                    (Nat.S
2836                                                                    (Nat.S
2837                                                                    (Nat.S
2838                                                                    (Nat.S
2839                                                                    (Nat.S
2840                                                                    (Nat.S
2841                                                                    (Nat.S
2842                                                                    (Nat.S
2843                                                                    (Nat.S
2844                                                                    (Nat.S
2845                                                                    (Nat.S
2846                                                                    (Nat.S
2847                                                                    (Nat.S
2848                                                                    (Nat.S
2849                                                                    (Nat.S
2850                                                                    (Nat.S
2851                                                                    (Nat.S
2852                                                                    Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2853                                                                    | Bool.True ->
2854                                                                    Types.Some
2855                                                                    (Types.Inl
2856                                                                    SFR_DPH)
2857                                                                    | Bool.False ->
2858                                                                    (match 
2859                                                                    Nat.eqb
2860                                                                    address
2861                                                                    (Nat.S
2862                                                                    (Nat.S
2863                                                                    (Nat.S
2864                                                                    (Nat.S
2865                                                                    (Nat.S
2866                                                                    (Nat.S
2867                                                                    (Nat.S
2868                                                                    (Nat.S
2869                                                                    (Nat.S
2870                                                                    (Nat.S
2871                                                                    (Nat.S
2872                                                                    (Nat.S
2873                                                                    (Nat.S
2874                                                                    (Nat.S
2875                                                                    (Nat.S
2876                                                                    (Nat.S
2877                                                                    (Nat.S
2878                                                                    (Nat.S
2879                                                                    (Nat.S
2880                                                                    (Nat.S
2881                                                                    (Nat.S
2882                                                                    (Nat.S
2883                                                                    (Nat.S
2884                                                                    (Nat.S
2885                                                                    (Nat.S
2886                                                                    (Nat.S
2887                                                                    (Nat.S
2888                                                                    (Nat.S
2889                                                                    (Nat.S
2890                                                                    (Nat.S
2891                                                                    (Nat.S
2892                                                                    (Nat.S
2893                                                                    (Nat.S
2894                                                                    (Nat.S
2895                                                                    (Nat.S
2896                                                                    (Nat.S
2897                                                                    (Nat.S
2898                                                                    (Nat.S
2899                                                                    (Nat.S
2900                                                                    (Nat.S
2901                                                                    (Nat.S
2902                                                                    (Nat.S
2903                                                                    (Nat.S
2904                                                                    (Nat.S
2905                                                                    (Nat.S
2906                                                                    (Nat.S
2907                                                                    (Nat.S
2908                                                                    (Nat.S
2909                                                                    (Nat.S
2910                                                                    (Nat.S
2911                                                                    (Nat.S
2912                                                                    (Nat.S
2913                                                                    (Nat.S
2914                                                                    (Nat.S
2915                                                                    (Nat.S
2916                                                                    (Nat.S
2917                                                                    (Nat.S
2918                                                                    (Nat.S
2919                                                                    (Nat.S
2920                                                                    (Nat.S
2921                                                                    (Nat.S
2922                                                                    (Nat.S
2923                                                                    (Nat.S
2924                                                                    (Nat.S
2925                                                                    (Nat.S
2926                                                                    (Nat.S
2927                                                                    (Nat.S
2928                                                                    (Nat.S
2929                                                                    (Nat.S
2930                                                                    (Nat.S
2931                                                                    (Nat.S
2932                                                                    (Nat.S
2933                                                                    (Nat.S
2934                                                                    (Nat.S
2935                                                                    (Nat.S
2936                                                                    (Nat.S
2937                                                                    (Nat.S
2938                                                                    (Nat.S
2939                                                                    (Nat.S
2940                                                                    (Nat.S
2941                                                                    (Nat.S
2942                                                                    (Nat.S
2943                                                                    (Nat.S
2944                                                                    (Nat.S
2945                                                                    (Nat.S
2946                                                                    (Nat.S
2947                                                                    (Nat.S
2948                                                                    (Nat.S
2949                                                                    (Nat.S
2950                                                                    (Nat.S
2951                                                                    (Nat.S
2952                                                                    (Nat.S
2953                                                                    (Nat.S
2954                                                                    (Nat.S
2955                                                                    (Nat.S
2956                                                                    (Nat.S
2957                                                                    (Nat.S
2958                                                                    (Nat.S
2959                                                                    (Nat.S
2960                                                                    (Nat.S
2961                                                                    (Nat.S
2962                                                                    (Nat.S
2963                                                                    (Nat.S
2964                                                                    (Nat.S
2965                                                                    (Nat.S
2966                                                                    (Nat.S
2967                                                                    (Nat.S
2968                                                                    (Nat.S
2969                                                                    (Nat.S
2970                                                                    (Nat.S
2971                                                                    (Nat.S
2972                                                                    (Nat.S
2973                                                                    (Nat.S
2974                                                                    (Nat.S
2975                                                                    (Nat.S
2976                                                                    (Nat.S
2977                                                                    (Nat.S
2978                                                                    (Nat.S
2979                                                                    (Nat.S
2980                                                                    (Nat.S
2981                                                                    (Nat.S
2982                                                                    (Nat.S
2983                                                                    (Nat.S
2984                                                                    (Nat.S
2985                                                                    (Nat.S
2986                                                                    (Nat.S
2987                                                                    (Nat.S
2988                                                                    (Nat.S
2989                                                                    (Nat.S
2990                                                                    (Nat.S
2991                                                                    (Nat.S
2992                                                                    (Nat.S
2993                                                                    (Nat.S
2994                                                                    (Nat.S
2995                                                                    (Nat.S
2996                                                                    (Nat.S
2997                                                                    (Nat.S
2998                                                                    (Nat.S
2999                                                                    (Nat.S
3000                                                                    (Nat.S
3001                                                                    (Nat.S
3002                                                                    (Nat.S
3003                                                                    (Nat.S
3004                                                                    (Nat.S
3005                                                                    (Nat.S
3006                                                                    (Nat.S
3007                                                                    (Nat.S
3008                                                                    (Nat.S
3009                                                                    (Nat.S
3010                                                                    (Nat.S
3011                                                                    (Nat.S
3012                                                                    (Nat.S
3013                                                                    (Nat.S
3014                                                                    (Nat.S
3015                                                                    (Nat.S
3016                                                                    (Nat.S
3017                                                                    (Nat.S
3018                                                                    (Nat.S
3019                                                                    (Nat.S
3020                                                                    (Nat.S
3021                                                                    (Nat.S
3022                                                                    (Nat.S
3023                                                                    (Nat.S
3024                                                                    (Nat.S
3025                                                                    (Nat.S
3026                                                                    (Nat.S
3027                                                                    (Nat.S
3028                                                                    (Nat.S
3029                                                                    (Nat.S
3030                                                                    (Nat.S
3031                                                                    (Nat.S
3032                                                                    (Nat.S
3033                                                                    (Nat.S
3034                                                                    (Nat.S
3035                                                                    (Nat.S
3036                                                                    (Nat.S
3037                                                                    (Nat.S
3038                                                                    (Nat.S
3039                                                                    (Nat.S
3040                                                                    (Nat.S
3041                                                                    (Nat.S
3042                                                                    (Nat.S
3043                                                                    (Nat.S
3044                                                                    (Nat.S
3045                                                                    (Nat.S
3046                                                                    (Nat.S
3047                                                                    (Nat.S
3048                                                                    (Nat.S
3049                                                                    (Nat.S
3050                                                                    (Nat.S
3051                                                                    (Nat.S
3052                                                                    (Nat.S
3053                                                                    (Nat.S
3054                                                                    (Nat.S
3055                                                                    (Nat.S
3056                                                                    (Nat.S
3057                                                                    (Nat.S
3058                                                                    (Nat.S
3059                                                                    (Nat.S
3060                                                                    (Nat.S
3061                                                                    (Nat.S
3062                                                                    (Nat.S
3063                                                                    (Nat.S
3064                                                                    (Nat.S
3065                                                                    (Nat.S
3066                                                                    (Nat.S
3067                                                                    (Nat.S
3068                                                                    (Nat.S
3069                                                                    Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3070                                                                    | Bool.True ->
3071                                                                    Types.Some
3072                                                                    (Types.Inl
3073                                                                    SFR_PSW)
3074                                                                    | Bool.False ->
3075                                                                    (match 
3076                                                                    Nat.eqb
3077                                                                    address
3078                                                                    (Nat.S
3079                                                                    (Nat.S
3080                                                                    (Nat.S
3081                                                                    (Nat.S
3082                                                                    (Nat.S
3083                                                                    (Nat.S
3084                                                                    (Nat.S
3085                                                                    (Nat.S
3086                                                                    (Nat.S
3087                                                                    (Nat.S
3088                                                                    (Nat.S
3089                                                                    (Nat.S
3090                                                                    (Nat.S
3091                                                                    (Nat.S
3092                                                                    (Nat.S
3093                                                                    (Nat.S
3094                                                                    (Nat.S
3095                                                                    (Nat.S
3096                                                                    (Nat.S
3097                                                                    (Nat.S
3098                                                                    (Nat.S
3099                                                                    (Nat.S
3100                                                                    (Nat.S
3101                                                                    (Nat.S
3102                                                                    (Nat.S
3103                                                                    (Nat.S
3104                                                                    (Nat.S
3105                                                                    (Nat.S
3106                                                                    (Nat.S
3107                                                                    (Nat.S
3108                                                                    (Nat.S
3109                                                                    (Nat.S
3110                                                                    (Nat.S
3111                                                                    (Nat.S
3112                                                                    (Nat.S
3113                                                                    (Nat.S
3114                                                                    (Nat.S
3115                                                                    (Nat.S
3116                                                                    (Nat.S
3117                                                                    (Nat.S
3118                                                                    (Nat.S
3119                                                                    (Nat.S
3120                                                                    (Nat.S
3121                                                                    (Nat.S
3122                                                                    (Nat.S
3123                                                                    (Nat.S
3124                                                                    (Nat.S
3125                                                                    (Nat.S
3126                                                                    (Nat.S
3127                                                                    (Nat.S
3128                                                                    (Nat.S
3129                                                                    (Nat.S
3130                                                                    (Nat.S
3131                                                                    (Nat.S
3132                                                                    (Nat.S
3133                                                                    (Nat.S
3134                                                                    (Nat.S
3135                                                                    (Nat.S
3136                                                                    (Nat.S
3137                                                                    (Nat.S
3138                                                                    (Nat.S
3139                                                                    (Nat.S
3140                                                                    (Nat.S
3141                                                                    (Nat.S
3142                                                                    (Nat.S
3143                                                                    (Nat.S
3144                                                                    (Nat.S
3145                                                                    (Nat.S
3146                                                                    (Nat.S
3147                                                                    (Nat.S
3148                                                                    (Nat.S
3149                                                                    (Nat.S
3150                                                                    (Nat.S
3151                                                                    (Nat.S
3152                                                                    (Nat.S
3153                                                                    (Nat.S
3154                                                                    (Nat.S
3155                                                                    (Nat.S
3156                                                                    (Nat.S
3157                                                                    (Nat.S
3158                                                                    (Nat.S
3159                                                                    (Nat.S
3160                                                                    (Nat.S
3161                                                                    (Nat.S
3162                                                                    (Nat.S
3163                                                                    (Nat.S
3164                                                                    (Nat.S
3165                                                                    (Nat.S
3166                                                                    (Nat.S
3167                                                                    (Nat.S
3168                                                                    (Nat.S
3169                                                                    (Nat.S
3170                                                                    (Nat.S
3171                                                                    (Nat.S
3172                                                                    (Nat.S
3173                                                                    (Nat.S
3174                                                                    (Nat.S
3175                                                                    (Nat.S
3176                                                                    (Nat.S
3177                                                                    (Nat.S
3178                                                                    (Nat.S
3179                                                                    (Nat.S
3180                                                                    (Nat.S
3181                                                                    (Nat.S
3182                                                                    (Nat.S
3183                                                                    (Nat.S
3184                                                                    (Nat.S
3185                                                                    (Nat.S
3186                                                                    (Nat.S
3187                                                                    (Nat.S
3188                                                                    (Nat.S
3189                                                                    (Nat.S
3190                                                                    (Nat.S
3191                                                                    (Nat.S
3192                                                                    (Nat.S
3193                                                                    (Nat.S
3194                                                                    (Nat.S
3195                                                                    (Nat.S
3196                                                                    (Nat.S
3197                                                                    (Nat.S
3198                                                                    (Nat.S
3199                                                                    (Nat.S
3200                                                                    (Nat.S
3201                                                                    (Nat.S
3202                                                                    (Nat.S
3203                                                                    (Nat.S
3204                                                                    (Nat.S
3205                                                                    (Nat.S
3206                                                                    (Nat.S
3207                                                                    (Nat.S
3208                                                                    (Nat.S
3209                                                                    (Nat.S
3210                                                                    (Nat.S
3211                                                                    (Nat.S
3212                                                                    (Nat.S
3213                                                                    (Nat.S
3214                                                                    (Nat.S
3215                                                                    (Nat.S
3216                                                                    (Nat.S
3217                                                                    (Nat.S
3218                                                                    (Nat.S
3219                                                                    (Nat.S
3220                                                                    (Nat.S
3221                                                                    (Nat.S
3222                                                                    (Nat.S
3223                                                                    (Nat.S
3224                                                                    (Nat.S
3225                                                                    (Nat.S
3226                                                                    (Nat.S
3227                                                                    (Nat.S
3228                                                                    (Nat.S
3229                                                                    (Nat.S
3230                                                                    (Nat.S
3231                                                                    (Nat.S
3232                                                                    (Nat.S
3233                                                                    (Nat.S
3234                                                                    (Nat.S
3235                                                                    (Nat.S
3236                                                                    (Nat.S
3237                                                                    (Nat.S
3238                                                                    (Nat.S
3239                                                                    (Nat.S
3240                                                                    (Nat.S
3241                                                                    (Nat.S
3242                                                                    (Nat.S
3243                                                                    (Nat.S
3244                                                                    (Nat.S
3245                                                                    (Nat.S
3246                                                                    (Nat.S
3247                                                                    (Nat.S
3248                                                                    (Nat.S
3249                                                                    (Nat.S
3250                                                                    (Nat.S
3251                                                                    (Nat.S
3252                                                                    (Nat.S
3253                                                                    (Nat.S
3254                                                                    (Nat.S
3255                                                                    (Nat.S
3256                                                                    (Nat.S
3257                                                                    (Nat.S
3258                                                                    (Nat.S
3259                                                                    (Nat.S
3260                                                                    (Nat.S
3261                                                                    (Nat.S
3262                                                                    (Nat.S
3263                                                                    (Nat.S
3264                                                                    (Nat.S
3265                                                                    (Nat.S
3266                                                                    (Nat.S
3267                                                                    (Nat.S
3268                                                                    (Nat.S
3269                                                                    (Nat.S
3270                                                                    (Nat.S
3271                                                                    (Nat.S
3272                                                                    (Nat.S
3273                                                                    (Nat.S
3274                                                                    (Nat.S
3275                                                                    (Nat.S
3276                                                                    (Nat.S
3277                                                                    (Nat.S
3278                                                                    (Nat.S
3279                                                                    (Nat.S
3280                                                                    (Nat.S
3281                                                                    (Nat.S
3282                                                                    (Nat.S
3283                                                                    (Nat.S
3284                                                                    (Nat.S
3285                                                                    (Nat.S
3286                                                                    (Nat.S
3287                                                                    (Nat.S
3288                                                                    (Nat.S
3289                                                                    (Nat.S
3290                                                                    (Nat.S
3291                                                                    (Nat.S
3292                                                                    (Nat.S
3293                                                                    (Nat.S
3294                                                                    (Nat.S
3295                                                                    (Nat.S
3296                                                                    (Nat.S
3297                                                                    (Nat.S
3298                                                                    (Nat.S
3299                                                                    (Nat.S
3300                                                                    (Nat.S
3301                                                                    (Nat.S
3302                                                                    Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3303                                                                    | Bool.True ->
3304                                                                    Types.Some
3305                                                                    (Types.Inl
3306                                                                    SFR_ACC_A)
3307                                                                    | Bool.False ->
3308                                                                    (match 
3309                                                                    Nat.eqb
3310                                                                    address
3311                                                                    (Nat.S
3312                                                                    (Nat.S
3313                                                                    (Nat.S
3314                                                                    (Nat.S
3315                                                                    (Nat.S
3316                                                                    (Nat.S
3317                                                                    (Nat.S
3318                                                                    (Nat.S
3319                                                                    (Nat.S
3320                                                                    (Nat.S
3321                                                                    (Nat.S
3322                                                                    (Nat.S
3323                                                                    (Nat.S
3324                                                                    (Nat.S
3325                                                                    (Nat.S
3326                                                                    (Nat.S
3327                                                                    (Nat.S
3328                                                                    (Nat.S
3329                                                                    (Nat.S
3330                                                                    (Nat.S
3331                                                                    (Nat.S
3332                                                                    (Nat.S
3333                                                                    (Nat.S
3334                                                                    (Nat.S
3335                                                                    (Nat.S
3336                                                                    (Nat.S
3337                                                                    (Nat.S
3338                                                                    (Nat.S
3339                                                                    (Nat.S
3340                                                                    (Nat.S
3341                                                                    (Nat.S
3342                                                                    (Nat.S
3343                                                                    (Nat.S
3344                                                                    (Nat.S
3345                                                                    (Nat.S
3346                                                                    (Nat.S
3347                                                                    (Nat.S
3348                                                                    (Nat.S
3349                                                                    (Nat.S
3350                                                                    (Nat.S
3351                                                                    (Nat.S
3352                                                                    (Nat.S
3353                                                                    (Nat.S
3354                                                                    (Nat.S
3355                                                                    (Nat.S
3356                                                                    (Nat.S
3357                                                                    (Nat.S
3358                                                                    (Nat.S
3359                                                                    (Nat.S
3360                                                                    (Nat.S
3361                                                                    (Nat.S
3362                                                                    (Nat.S
3363                                                                    (Nat.S
3364                                                                    (Nat.S
3365                                                                    (Nat.S
3366                                                                    (Nat.S
3367                                                                    (Nat.S
3368                                                                    (Nat.S
3369                                                                    (Nat.S
3370                                                                    (Nat.S
3371                                                                    (Nat.S
3372                                                                    (Nat.S
3373                                                                    (Nat.S
3374                                                                    (Nat.S
3375                                                                    (Nat.S
3376                                                                    (Nat.S
3377                                                                    (Nat.S
3378                                                                    (Nat.S
3379                                                                    (Nat.S
3380                                                                    (Nat.S
3381                                                                    (Nat.S
3382                                                                    (Nat.S
3383                                                                    (Nat.S
3384                                                                    (Nat.S
3385                                                                    (Nat.S
3386                                                                    (Nat.S
3387                                                                    (Nat.S
3388                                                                    (Nat.S
3389                                                                    (Nat.S
3390                                                                    (Nat.S
3391                                                                    (Nat.S
3392