source: extracted/status.ml @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 251.7 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open Arithmetic
8
9open Integers
10
11open AST
12
13open CostLabel
14
15open Proper
16
17open PositiveMap
18
19open Deqsets
20
21open ErrorMessages
22
23open PreIdentifiers
24
25open Errors
26
27open Extralib
28
29open Setoids
30
31open Monad
32
33open Option
34
35open Lists
36
37open Positive
38
39open Identifiers
40
41open Extranat
42
43open Vector
44
45open Div_and_mod
46
47open Jmeq
48
49open Russell
50
51open Types
52
53open List
54
55open Util
56
57open FoldStuff
58
59open Bool
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Relations
70
71open Nat
72
73open BitVector
74
75open ASM
76
77open BitVectorTrie
78
79type time = Nat.nat
80
81type serialBufferType =
82| Eight of BitVector.byte
83| Nine of BitVector.bit * BitVector.byte
84
85(** val serialBufferType_rect_Type4 :
86    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
87    serialBufferType -> 'a1 **)
88let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
89| Eight x_2231 -> h_Eight x_2231
90| Nine (x_2233, x_2232) -> h_Nine x_2233 x_2232
91
92(** val serialBufferType_rect_Type5 :
93    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
94    serialBufferType -> 'a1 **)
95let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
96| Eight x_2237 -> h_Eight x_2237
97| Nine (x_2239, x_2238) -> h_Nine x_2239 x_2238
98
99(** val serialBufferType_rect_Type3 :
100    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
101    serialBufferType -> 'a1 **)
102let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
103| Eight x_2243 -> h_Eight x_2243
104| Nine (x_2245, x_2244) -> h_Nine x_2245 x_2244
105
106(** val serialBufferType_rect_Type2 :
107    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
108    serialBufferType -> 'a1 **)
109let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
110| Eight x_2249 -> h_Eight x_2249
111| Nine (x_2251, x_2250) -> h_Nine x_2251 x_2250
112
113(** val serialBufferType_rect_Type1 :
114    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
115    serialBufferType -> 'a1 **)
116let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
117| Eight x_2255 -> h_Eight x_2255
118| Nine (x_2257, x_2256) -> h_Nine x_2257 x_2256
119
120(** val serialBufferType_rect_Type0 :
121    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
122    serialBufferType -> 'a1 **)
123let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
124| Eight x_2261 -> h_Eight x_2261
125| Nine (x_2263, x_2262) -> h_Nine x_2263 x_2262
126
127(** val serialBufferType_inv_rect_Type4 :
128    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
129    BitVector.byte -> __ -> 'a1) -> 'a1 **)
130let serialBufferType_inv_rect_Type4 hterm h1 h2 =
131  let hcut = serialBufferType_rect_Type4 h1 h2 hterm in hcut __
132
133(** val serialBufferType_inv_rect_Type3 :
134    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
135    BitVector.byte -> __ -> 'a1) -> 'a1 **)
136let serialBufferType_inv_rect_Type3 hterm h1 h2 =
137  let hcut = serialBufferType_rect_Type3 h1 h2 hterm in hcut __
138
139(** val serialBufferType_inv_rect_Type2 :
140    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
141    BitVector.byte -> __ -> 'a1) -> 'a1 **)
142let serialBufferType_inv_rect_Type2 hterm h1 h2 =
143  let hcut = serialBufferType_rect_Type2 h1 h2 hterm in hcut __
144
145(** val serialBufferType_inv_rect_Type1 :
146    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
147    BitVector.byte -> __ -> 'a1) -> 'a1 **)
148let serialBufferType_inv_rect_Type1 hterm h1 h2 =
149  let hcut = serialBufferType_rect_Type1 h1 h2 hterm in hcut __
150
151(** val serialBufferType_inv_rect_Type0 :
152    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
153    BitVector.byte -> __ -> 'a1) -> 'a1 **)
154let serialBufferType_inv_rect_Type0 hterm h1 h2 =
155  let hcut = serialBufferType_rect_Type0 h1 h2 hterm in hcut __
156
157(** val serialBufferType_discr :
158    serialBufferType -> serialBufferType -> __ **)
159let serialBufferType_discr x y =
160  Logic.eq_rect_Type2 x
161    (match x with
162     | Eight a0 -> Obj.magic (fun _ dH -> dH __)
163     | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
164
165(** val serialBufferType_jmdiscr :
166    serialBufferType -> serialBufferType -> __ **)
167let serialBufferType_jmdiscr x y =
168  Logic.eq_rect_Type2 x
169    (match x with
170     | Eight a0 -> Obj.magic (fun _ dH -> dH __)
171     | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
172
173type lineType =
174| P2 of BitVector.byte
175| P3 of BitVector.byte
176| SerialBuffer of serialBufferType
177
178(** val lineType_rect_Type4 :
179    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
180    -> 'a1) -> lineType -> 'a1 **)
181let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
182| P2 x_2310 -> h_P1 x_2310
183| P3 x_2311 -> h_P3 x_2311
184| SerialBuffer x_2312 -> h_SerialBuffer x_2312
185
186(** val lineType_rect_Type5 :
187    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
188    -> 'a1) -> lineType -> 'a1 **)
189let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
190| P2 x_2317 -> h_P1 x_2317
191| P3 x_2318 -> h_P3 x_2318
192| SerialBuffer x_2319 -> h_SerialBuffer x_2319
193
194(** val lineType_rect_Type3 :
195    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
196    -> 'a1) -> lineType -> 'a1 **)
197let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
198| P2 x_2324 -> h_P1 x_2324
199| P3 x_2325 -> h_P3 x_2325
200| SerialBuffer x_2326 -> h_SerialBuffer x_2326
201
202(** val lineType_rect_Type2 :
203    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
204    -> 'a1) -> lineType -> 'a1 **)
205let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
206| P2 x_2331 -> h_P1 x_2331
207| P3 x_2332 -> h_P3 x_2332
208| SerialBuffer x_2333 -> h_SerialBuffer x_2333
209
210(** val lineType_rect_Type1 :
211    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
212    -> 'a1) -> lineType -> 'a1 **)
213let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
214| P2 x_2338 -> h_P1 x_2338
215| P3 x_2339 -> h_P3 x_2339
216| SerialBuffer x_2340 -> h_SerialBuffer x_2340
217
218(** val lineType_rect_Type0 :
219    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
220    -> 'a1) -> lineType -> 'a1 **)
221let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
222| P2 x_2345 -> h_P1 x_2345
223| P3 x_2346 -> h_P3 x_2346
224| SerialBuffer x_2347 -> h_SerialBuffer x_2347
225
226(** val lineType_inv_rect_Type4 :
227    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
228    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
229let lineType_inv_rect_Type4 hterm h1 h2 h3 =
230  let hcut = lineType_rect_Type4 h1 h2 h3 hterm in hcut __
231
232(** val lineType_inv_rect_Type3 :
233    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
234    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
235let lineType_inv_rect_Type3 hterm h1 h2 h3 =
236  let hcut = lineType_rect_Type3 h1 h2 h3 hterm in hcut __
237
238(** val lineType_inv_rect_Type2 :
239    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
240    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
241let lineType_inv_rect_Type2 hterm h1 h2 h3 =
242  let hcut = lineType_rect_Type2 h1 h2 h3 hterm in hcut __
243
244(** val lineType_inv_rect_Type1 :
245    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
246    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
247let lineType_inv_rect_Type1 hterm h1 h2 h3 =
248  let hcut = lineType_rect_Type1 h1 h2 h3 hterm in hcut __
249
250(** val lineType_inv_rect_Type0 :
251    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
252    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
253let lineType_inv_rect_Type0 hterm h1 h2 h3 =
254  let hcut = lineType_rect_Type0 h1 h2 h3 hterm in hcut __
255
256(** val lineType_discr : lineType -> lineType -> __ **)
257let lineType_discr x y =
258  Logic.eq_rect_Type2 x
259    (match x with
260     | P2 a0 -> Obj.magic (fun _ dH -> dH __)
261     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
262     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
263
264(** val lineType_jmdiscr : lineType -> lineType -> __ **)
265let lineType_jmdiscr x y =
266  Logic.eq_rect_Type2 x
267    (match x with
268     | P2 a0 -> Obj.magic (fun _ dH -> dH __)
269     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
270     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
271
272type sFR8051 =
273| SFR_SP
274| SFR_DPL
275| SFR_DPH
276| SFR_PCON
277| SFR_TCON
278| SFR_TMOD
279| SFR_TL0
280| SFR_TL1
281| SFR_TH0
282| SFR_TH1
283| SFR_P1
284| SFR_SCON
285| SFR_SBUF
286| SFR_IE
287| SFR_P3
288| SFR_IP
289| SFR_PSW
290| SFR_ACC_A
291| SFR_ACC_B
292
293(** val sFR8051_rect_Type4 :
294    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
295    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
296let 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
297| SFR_SP -> h_SFR_SP
298| SFR_DPL -> h_SFR_DPL
299| SFR_DPH -> h_SFR_DPH
300| SFR_PCON -> h_SFR_PCON
301| SFR_TCON -> h_SFR_TCON
302| SFR_TMOD -> h_SFR_TMOD
303| SFR_TL0 -> h_SFR_TL0
304| SFR_TL1 -> h_SFR_TL1
305| SFR_TH0 -> h_SFR_TH0
306| SFR_TH1 -> h_SFR_TH1
307| SFR_P1 -> h_SFR_P1
308| SFR_SCON -> h_SFR_SCON
309| SFR_SBUF -> h_SFR_SBUF
310| SFR_IE -> h_SFR_IE
311| SFR_P3 -> h_SFR_P3
312| SFR_IP -> h_SFR_IP
313| SFR_PSW -> h_SFR_PSW
314| SFR_ACC_A -> h_SFR_ACC_A
315| SFR_ACC_B -> h_SFR_ACC_B
316
317(** val sFR8051_rect_Type5 :
318    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
319    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
320let 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
321| SFR_SP -> h_SFR_SP
322| SFR_DPL -> h_SFR_DPL
323| SFR_DPH -> h_SFR_DPH
324| SFR_PCON -> h_SFR_PCON
325| SFR_TCON -> h_SFR_TCON
326| SFR_TMOD -> h_SFR_TMOD
327| SFR_TL0 -> h_SFR_TL0
328| SFR_TL1 -> h_SFR_TL1
329| SFR_TH0 -> h_SFR_TH0
330| SFR_TH1 -> h_SFR_TH1
331| SFR_P1 -> h_SFR_P1
332| SFR_SCON -> h_SFR_SCON
333| SFR_SBUF -> h_SFR_SBUF
334| SFR_IE -> h_SFR_IE
335| SFR_P3 -> h_SFR_P3
336| SFR_IP -> h_SFR_IP
337| SFR_PSW -> h_SFR_PSW
338| SFR_ACC_A -> h_SFR_ACC_A
339| SFR_ACC_B -> h_SFR_ACC_B
340
341(** val sFR8051_rect_Type3 :
342    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
343    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
344let 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
345| SFR_SP -> h_SFR_SP
346| SFR_DPL -> h_SFR_DPL
347| SFR_DPH -> h_SFR_DPH
348| SFR_PCON -> h_SFR_PCON
349| SFR_TCON -> h_SFR_TCON
350| SFR_TMOD -> h_SFR_TMOD
351| SFR_TL0 -> h_SFR_TL0
352| SFR_TL1 -> h_SFR_TL1
353| SFR_TH0 -> h_SFR_TH0
354| SFR_TH1 -> h_SFR_TH1
355| SFR_P1 -> h_SFR_P1
356| SFR_SCON -> h_SFR_SCON
357| SFR_SBUF -> h_SFR_SBUF
358| SFR_IE -> h_SFR_IE
359| SFR_P3 -> h_SFR_P3
360| SFR_IP -> h_SFR_IP
361| SFR_PSW -> h_SFR_PSW
362| SFR_ACC_A -> h_SFR_ACC_A
363| SFR_ACC_B -> h_SFR_ACC_B
364
365(** val sFR8051_rect_Type2 :
366    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
367    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
368let 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
369| SFR_SP -> h_SFR_SP
370| SFR_DPL -> h_SFR_DPL
371| SFR_DPH -> h_SFR_DPH
372| SFR_PCON -> h_SFR_PCON
373| SFR_TCON -> h_SFR_TCON
374| SFR_TMOD -> h_SFR_TMOD
375| SFR_TL0 -> h_SFR_TL0
376| SFR_TL1 -> h_SFR_TL1
377| SFR_TH0 -> h_SFR_TH0
378| SFR_TH1 -> h_SFR_TH1
379| SFR_P1 -> h_SFR_P1
380| SFR_SCON -> h_SFR_SCON
381| SFR_SBUF -> h_SFR_SBUF
382| SFR_IE -> h_SFR_IE
383| SFR_P3 -> h_SFR_P3
384| SFR_IP -> h_SFR_IP
385| SFR_PSW -> h_SFR_PSW
386| SFR_ACC_A -> h_SFR_ACC_A
387| SFR_ACC_B -> h_SFR_ACC_B
388
389(** val sFR8051_rect_Type1 :
390    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
391    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
392let 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
393| SFR_SP -> h_SFR_SP
394| SFR_DPL -> h_SFR_DPL
395| SFR_DPH -> h_SFR_DPH
396| SFR_PCON -> h_SFR_PCON
397| SFR_TCON -> h_SFR_TCON
398| SFR_TMOD -> h_SFR_TMOD
399| SFR_TL0 -> h_SFR_TL0
400| SFR_TL1 -> h_SFR_TL1
401| SFR_TH0 -> h_SFR_TH0
402| SFR_TH1 -> h_SFR_TH1
403| SFR_P1 -> h_SFR_P1
404| SFR_SCON -> h_SFR_SCON
405| SFR_SBUF -> h_SFR_SBUF
406| SFR_IE -> h_SFR_IE
407| SFR_P3 -> h_SFR_P3
408| SFR_IP -> h_SFR_IP
409| SFR_PSW -> h_SFR_PSW
410| SFR_ACC_A -> h_SFR_ACC_A
411| SFR_ACC_B -> h_SFR_ACC_B
412
413(** val sFR8051_rect_Type0 :
414    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
415    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
416let 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
417| SFR_SP -> h_SFR_SP
418| SFR_DPL -> h_SFR_DPL
419| SFR_DPH -> h_SFR_DPH
420| SFR_PCON -> h_SFR_PCON
421| SFR_TCON -> h_SFR_TCON
422| SFR_TMOD -> h_SFR_TMOD
423| SFR_TL0 -> h_SFR_TL0
424| SFR_TL1 -> h_SFR_TL1
425| SFR_TH0 -> h_SFR_TH0
426| SFR_TH1 -> h_SFR_TH1
427| SFR_P1 -> h_SFR_P1
428| SFR_SCON -> h_SFR_SCON
429| SFR_SBUF -> h_SFR_SBUF
430| SFR_IE -> h_SFR_IE
431| SFR_P3 -> h_SFR_P3
432| SFR_IP -> h_SFR_IP
433| SFR_PSW -> h_SFR_PSW
434| SFR_ACC_A -> h_SFR_ACC_A
435| SFR_ACC_B -> h_SFR_ACC_B
436
437(** val sFR8051_inv_rect_Type4 :
438    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
439    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
440    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
441    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
442    -> 'a1) -> 'a1 **)
443let sFR8051_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
444  let hcut =
445    sFR8051_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
446      h17 h18 h19 hterm
447  in
448  hcut __
449
450(** val sFR8051_inv_rect_Type3 :
451    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
452    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
453    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
454    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
455    -> 'a1) -> 'a1 **)
456let sFR8051_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
457  let hcut =
458    sFR8051_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
459      h17 h18 h19 hterm
460  in
461  hcut __
462
463(** val sFR8051_inv_rect_Type2 :
464    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
465    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
466    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
467    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
468    -> 'a1) -> 'a1 **)
469let sFR8051_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
470  let hcut =
471    sFR8051_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
472      h17 h18 h19 hterm
473  in
474  hcut __
475
476(** val sFR8051_inv_rect_Type1 :
477    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
478    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
479    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
480    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
481    -> 'a1) -> 'a1 **)
482let sFR8051_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
483  let hcut =
484    sFR8051_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
485      h17 h18 h19 hterm
486  in
487  hcut __
488
489(** val sFR8051_inv_rect_Type0 :
490    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
491    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
492    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
493    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
494    -> 'a1) -> 'a1 **)
495let sFR8051_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
496  let hcut =
497    sFR8051_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
498      h17 h18 h19 hterm
499  in
500  hcut __
501
502(** val sFR8051_discr : sFR8051 -> sFR8051 -> __ **)
503let sFR8051_discr x y =
504  Logic.eq_rect_Type2 x
505    (match x with
506     | SFR_SP -> Obj.magic (fun _ dH -> dH)
507     | SFR_DPL -> Obj.magic (fun _ dH -> dH)
508     | SFR_DPH -> Obj.magic (fun _ dH -> dH)
509     | SFR_PCON -> Obj.magic (fun _ dH -> dH)
510     | SFR_TCON -> Obj.magic (fun _ dH -> dH)
511     | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
512     | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
513     | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
514     | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
515     | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
516     | SFR_P1 -> Obj.magic (fun _ dH -> dH)
517     | SFR_SCON -> Obj.magic (fun _ dH -> dH)
518     | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
519     | SFR_IE -> Obj.magic (fun _ dH -> dH)
520     | SFR_P3 -> Obj.magic (fun _ dH -> dH)
521     | SFR_IP -> Obj.magic (fun _ dH -> dH)
522     | SFR_PSW -> Obj.magic (fun _ dH -> dH)
523     | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
524     | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
525
526(** val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __ **)
527let sFR8051_jmdiscr x y =
528  Logic.eq_rect_Type2 x
529    (match x with
530     | SFR_SP -> Obj.magic (fun _ dH -> dH)
531     | SFR_DPL -> Obj.magic (fun _ dH -> dH)
532     | SFR_DPH -> Obj.magic (fun _ dH -> dH)
533     | SFR_PCON -> Obj.magic (fun _ dH -> dH)
534     | SFR_TCON -> Obj.magic (fun _ dH -> dH)
535     | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
536     | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
537     | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
538     | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
539     | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
540     | SFR_P1 -> Obj.magic (fun _ dH -> dH)
541     | SFR_SCON -> Obj.magic (fun _ dH -> dH)
542     | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
543     | SFR_IE -> Obj.magic (fun _ dH -> dH)
544     | SFR_P3 -> Obj.magic (fun _ dH -> dH)
545     | SFR_IP -> Obj.magic (fun _ dH -> dH)
546     | SFR_PSW -> Obj.magic (fun _ dH -> dH)
547     | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
548     | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
549
550(** val sfr_8051_index : sFR8051 -> Nat.nat **)
551let sfr_8051_index = function
552| SFR_SP -> Nat.O
553| SFR_DPL -> Nat.S Nat.O
554| SFR_DPH -> Nat.S (Nat.S Nat.O)
555| SFR_PCON -> Nat.S (Nat.S (Nat.S Nat.O))
556| SFR_TCON -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
557| SFR_TMOD -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
558| SFR_TL0 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
559| SFR_TL1 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
560| SFR_TH0 ->
561  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
562| SFR_TH1 ->
563  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
564| SFR_P1 ->
565  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
566    Nat.O)))))))))
567| SFR_SCON ->
568  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
569    Nat.O))))))))))
570| SFR_SBUF ->
571  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
572    (Nat.S Nat.O)))))))))))
573| SFR_IE ->
574  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
575    (Nat.S (Nat.S Nat.O))))))))))))
576| SFR_P3 ->
577  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
578    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))
579| SFR_IP ->
580  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
581    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))
582| SFR_PSW ->
583  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
584    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
585| SFR_ACC_A ->
586  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
587    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
588| SFR_ACC_B ->
589  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
590    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))
591
592type sFR8052 =
593| SFR_T2CON
594| SFR_RCAP2L
595| SFR_RCAP2H
596| SFR_TL2
597| SFR_TH2
598
599(** val sFR8052_rect_Type4 :
600    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
601let rec sFR8052_rect_Type4 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
602| SFR_T2CON -> h_SFR_T2CON
603| SFR_RCAP2L -> h_SFR_RCAP2L
604| SFR_RCAP2H -> h_SFR_RCAP2H
605| SFR_TL2 -> h_SFR_TL2
606| SFR_TH2 -> h_SFR_TH2
607
608(** val sFR8052_rect_Type5 :
609    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
610let rec sFR8052_rect_Type5 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
611| SFR_T2CON -> h_SFR_T2CON
612| SFR_RCAP2L -> h_SFR_RCAP2L
613| SFR_RCAP2H -> h_SFR_RCAP2H
614| SFR_TL2 -> h_SFR_TL2
615| SFR_TH2 -> h_SFR_TH2
616
617(** val sFR8052_rect_Type3 :
618    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
619let rec sFR8052_rect_Type3 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
620| SFR_T2CON -> h_SFR_T2CON
621| SFR_RCAP2L -> h_SFR_RCAP2L
622| SFR_RCAP2H -> h_SFR_RCAP2H
623| SFR_TL2 -> h_SFR_TL2
624| SFR_TH2 -> h_SFR_TH2
625
626(** val sFR8052_rect_Type2 :
627    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
628let rec sFR8052_rect_Type2 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
629| SFR_T2CON -> h_SFR_T2CON
630| SFR_RCAP2L -> h_SFR_RCAP2L
631| SFR_RCAP2H -> h_SFR_RCAP2H
632| SFR_TL2 -> h_SFR_TL2
633| SFR_TH2 -> h_SFR_TH2
634
635(** val sFR8052_rect_Type1 :
636    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
637let rec sFR8052_rect_Type1 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
638| SFR_T2CON -> h_SFR_T2CON
639| SFR_RCAP2L -> h_SFR_RCAP2L
640| SFR_RCAP2H -> h_SFR_RCAP2H
641| SFR_TL2 -> h_SFR_TL2
642| SFR_TH2 -> h_SFR_TH2
643
644(** val sFR8052_rect_Type0 :
645    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
646let rec sFR8052_rect_Type0 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
647| SFR_T2CON -> h_SFR_T2CON
648| SFR_RCAP2L -> h_SFR_RCAP2L
649| SFR_RCAP2H -> h_SFR_RCAP2H
650| SFR_TL2 -> h_SFR_TL2
651| SFR_TH2 -> h_SFR_TH2
652
653(** val sFR8052_inv_rect_Type4 :
654    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
655    (__ -> 'a1) -> 'a1 **)
656let sFR8052_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
657  let hcut = sFR8052_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
658
659(** val sFR8052_inv_rect_Type3 :
660    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
661    (__ -> 'a1) -> 'a1 **)
662let sFR8052_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
663  let hcut = sFR8052_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
664
665(** val sFR8052_inv_rect_Type2 :
666    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
667    (__ -> 'a1) -> 'a1 **)
668let sFR8052_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
669  let hcut = sFR8052_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
670
671(** val sFR8052_inv_rect_Type1 :
672    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
673    (__ -> 'a1) -> 'a1 **)
674let sFR8052_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
675  let hcut = sFR8052_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
676
677(** val sFR8052_inv_rect_Type0 :
678    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
679    (__ -> 'a1) -> 'a1 **)
680let sFR8052_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
681  let hcut = sFR8052_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
682
683(** val sFR8052_discr : sFR8052 -> sFR8052 -> __ **)
684let sFR8052_discr x y =
685  Logic.eq_rect_Type2 x
686    (match x with
687     | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
688     | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
689     | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
690     | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
691     | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
692
693(** val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __ **)
694let sFR8052_jmdiscr x y =
695  Logic.eq_rect_Type2 x
696    (match x with
697     | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
698     | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
699     | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
700     | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
701     | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
702
703(** val sfr_8052_index : sFR8052 -> Nat.nat **)
704let sfr_8052_index = function
705| SFR_T2CON -> Nat.O
706| SFR_RCAP2L -> Nat.S Nat.O
707| SFR_RCAP2H -> Nat.S (Nat.S Nat.O)
708| SFR_TL2 -> Nat.S (Nat.S (Nat.S Nat.O))
709| SFR_TH2 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
710
711type 'm preStatus = { low_internal_ram : BitVector.byte
712                                         BitVectorTrie.bitVectorTrie;
713                      high_internal_ram : BitVector.byte
714                                          BitVectorTrie.bitVectorTrie;
715                      external_ram : BitVector.byte
716                                     BitVectorTrie.bitVectorTrie;
717                      program_counter : BitVector.word;
718                      special_function_registers_8051 : BitVector.byte
719                                                        Vector.vector;
720                      special_function_registers_8052 : BitVector.byte
721                                                        Vector.vector;
722                      p1_latch : BitVector.byte; p3_latch : BitVector.byte;
723                      clock : time }
724
725(** val preStatus_rect_Type4 :
726    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
727    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
728    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
729    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
730    preStatus -> 'a2 **)
731let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_2733 =
732  let { low_internal_ram = low_internal_ram0; high_internal_ram =
733    high_internal_ram0; external_ram = external_ram0; program_counter =
734    program_counter0; special_function_registers_8051 =
735    special_function_registers_8053; special_function_registers_8052 =
736    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
737    p3_latch0; clock = clock0 } = x_2733
738  in
739  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
740    program_counter0 special_function_registers_8053
741    special_function_registers_8054 p1_latch0 p3_latch0 clock0
742
743(** val preStatus_rect_Type5 :
744    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
745    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
746    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
747    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
748    preStatus -> 'a2 **)
749let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_2735 =
750  let { low_internal_ram = low_internal_ram0; high_internal_ram =
751    high_internal_ram0; external_ram = external_ram0; program_counter =
752    program_counter0; special_function_registers_8051 =
753    special_function_registers_8053; special_function_registers_8052 =
754    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
755    p3_latch0; clock = clock0 } = x_2735
756  in
757  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
758    program_counter0 special_function_registers_8053
759    special_function_registers_8054 p1_latch0 p3_latch0 clock0
760
761(** val preStatus_rect_Type3 :
762    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
763    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
764    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
765    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
766    preStatus -> 'a2 **)
767let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_2737 =
768  let { low_internal_ram = low_internal_ram0; high_internal_ram =
769    high_internal_ram0; external_ram = external_ram0; program_counter =
770    program_counter0; special_function_registers_8051 =
771    special_function_registers_8053; special_function_registers_8052 =
772    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
773    p3_latch0; clock = clock0 } = x_2737
774  in
775  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
776    program_counter0 special_function_registers_8053
777    special_function_registers_8054 p1_latch0 p3_latch0 clock0
778
779(** val preStatus_rect_Type2 :
780    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
781    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
782    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
783    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
784    preStatus -> 'a2 **)
785let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_2739 =
786  let { low_internal_ram = low_internal_ram0; high_internal_ram =
787    high_internal_ram0; external_ram = external_ram0; program_counter =
788    program_counter0; special_function_registers_8051 =
789    special_function_registers_8053; special_function_registers_8052 =
790    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
791    p3_latch0; clock = clock0 } = x_2739
792  in
793  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
794    program_counter0 special_function_registers_8053
795    special_function_registers_8054 p1_latch0 p3_latch0 clock0
796
797(** val preStatus_rect_Type1 :
798    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
799    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
800    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
801    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
802    preStatus -> 'a2 **)
803let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_2741 =
804  let { low_internal_ram = low_internal_ram0; high_internal_ram =
805    high_internal_ram0; external_ram = external_ram0; program_counter =
806    program_counter0; special_function_registers_8051 =
807    special_function_registers_8053; special_function_registers_8052 =
808    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
809    p3_latch0; clock = clock0 } = x_2741
810  in
811  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
812    program_counter0 special_function_registers_8053
813    special_function_registers_8054 p1_latch0 p3_latch0 clock0
814
815(** val preStatus_rect_Type0 :
816    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
817    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
818    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
819    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
820    preStatus -> 'a2 **)
821let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_2743 =
822  let { low_internal_ram = low_internal_ram0; high_internal_ram =
823    high_internal_ram0; external_ram = external_ram0; program_counter =
824    program_counter0; special_function_registers_8051 =
825    special_function_registers_8053; special_function_registers_8052 =
826    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
827    p3_latch0; clock = clock0 } = x_2743
828  in
829  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
830    program_counter0 special_function_registers_8053
831    special_function_registers_8054 p1_latch0 p3_latch0 clock0
832
833(** val low_internal_ram :
834    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
835let rec low_internal_ram code_memory xxx =
836  xxx.low_internal_ram
837
838(** val high_internal_ram :
839    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
840let rec high_internal_ram code_memory xxx =
841  xxx.high_internal_ram
842
843(** val external_ram :
844    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
845let rec external_ram code_memory xxx =
846  xxx.external_ram
847
848(** val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word **)
849let rec program_counter code_memory xxx =
850  xxx.program_counter
851
852(** val special_function_registers_8051 :
853    'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
854let rec special_function_registers_8051 code_memory xxx =
855  xxx.special_function_registers_8051
856
857(** val special_function_registers_8052 :
858    'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
859let rec special_function_registers_8052 code_memory xxx =
860  xxx.special_function_registers_8052
861
862(** val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
863let rec p1_latch code_memory xxx =
864  xxx.p1_latch
865
866(** val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
867let rec p3_latch code_memory xxx =
868  xxx.p3_latch
869
870(** val clock : 'a1 -> 'a1 preStatus -> time **)
871let rec clock code_memory xxx =
872  xxx.clock
873
874(** val preStatus_inv_rect_Type4 :
875    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
876    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
877    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
878    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
879    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
880let preStatus_inv_rect_Type4 x2 hterm h1 =
881  let hcut = preStatus_rect_Type4 x2 h1 hterm in hcut __
882
883(** val preStatus_inv_rect_Type3 :
884    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
885    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
886    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
887    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
888    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
889let preStatus_inv_rect_Type3 x2 hterm h1 =
890  let hcut = preStatus_rect_Type3 x2 h1 hterm in hcut __
891
892(** val preStatus_inv_rect_Type2 :
893    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
894    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
895    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
896    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
897    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
898let preStatus_inv_rect_Type2 x2 hterm h1 =
899  let hcut = preStatus_rect_Type2 x2 h1 hterm in hcut __
900
901(** val preStatus_inv_rect_Type1 :
902    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
903    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
904    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
905    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
906    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
907let preStatus_inv_rect_Type1 x2 hterm h1 =
908  let hcut = preStatus_rect_Type1 x2 h1 hterm in hcut __
909
910(** val preStatus_inv_rect_Type0 :
911    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
912    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
913    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
914    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
915    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
916let preStatus_inv_rect_Type0 x2 hterm h1 =
917  let hcut = preStatus_rect_Type0 x2 h1 hterm in hcut __
918
919(** val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __ **)
920let preStatus_jmdiscr a2 x y =
921  Logic.eq_rect_Type2 x
922    (let { low_internal_ram = a0; high_internal_ram = a10; external_ram =
923       a20; program_counter = a3; special_function_registers_8051 = a4;
924       special_function_registers_8052 = a5; p1_latch = a6; p3_latch = a7;
925       clock = a8 } = x
926     in
927    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y
928
929type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus
930
931type pseudoStatus = ASM.pseudo_assembly_program preStatus
932
933(** val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus **)
934let set_clock code_memory s t =
935  let old_low_internal_ram = s.low_internal_ram in
936  let old_high_internal_ram = s.high_internal_ram in
937  let old_external_ram = s.external_ram in
938  let old_program_counter = s.program_counter in
939  let old_special_function_registers_8051 = s.special_function_registers_8051
940  in
941  let old_special_function_registers_8052 = s.special_function_registers_8052
942  in
943  let old_p1_latch = s.p1_latch in
944  let old_p3_latch = s.p3_latch in
945  { low_internal_ram = old_low_internal_ram; high_internal_ram =
946  old_high_internal_ram; external_ram = old_external_ram; program_counter =
947  old_program_counter; special_function_registers_8051 =
948  old_special_function_registers_8051; special_function_registers_8052 =
949  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
950  old_p3_latch; clock = t }
951
952(** val set_p1_latch :
953    'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
954let set_p1_latch code_memory s b =
955  let old_low_internal_ram = s.low_internal_ram in
956  let old_high_internal_ram = s.high_internal_ram in
957  let old_external_ram = s.external_ram in
958  let old_program_counter = s.program_counter in
959  let old_special_function_registers_8051 = s.special_function_registers_8051
960  in
961  let old_special_function_registers_8052 = s.special_function_registers_8052
962  in
963  let old_p3_latch = s.p3_latch in
964  let old_clock = s.clock in
965  { low_internal_ram = old_low_internal_ram; high_internal_ram =
966  old_high_internal_ram; external_ram = old_external_ram; program_counter =
967  old_program_counter; special_function_registers_8051 =
968  old_special_function_registers_8051; special_function_registers_8052 =
969  old_special_function_registers_8052; p1_latch = b; p3_latch = old_p3_latch;
970  clock = old_clock }
971
972(** val set_p3_latch :
973    'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
974let set_p3_latch code_memory s b =
975  let old_low_internal_ram = s.low_internal_ram in
976  let old_high_internal_ram = s.high_internal_ram in
977  let old_external_ram = s.external_ram in
978  let old_program_counter = s.program_counter in
979  let old_special_function_registers_8051 = s.special_function_registers_8051
980  in
981  let old_special_function_registers_8052 = s.special_function_registers_8052
982  in
983  let old_p1_latch = s.p1_latch in
984  let old_clock = s.clock in
985  { low_internal_ram = old_low_internal_ram; high_internal_ram =
986  old_high_internal_ram; external_ram = old_external_ram; program_counter =
987  old_program_counter; special_function_registers_8051 =
988  old_special_function_registers_8051; special_function_registers_8052 =
989  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch = b;
990  clock = old_clock }
991
992(** val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte **)
993let get_8051_sfr code_memory s i =
994  let sfr = s.special_function_registers_8051 in
995  let index = sfr_8051_index i in
996  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
997    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
998    (Nat.S Nat.O))))))))))))))))))) sfr index
999
1000(** val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte **)
1001let get_8052_sfr code_memory s i =
1002  let sfr = s.special_function_registers_8052 in
1003  let index = sfr_8052_index i in
1004  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) sfr index
1005
1006(** val set_8051_sfr :
1007    'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus **)
1008let set_8051_sfr code_memory s i b =
1009  let index = sfr_8051_index i in
1010  let old_low_internal_ram = s.low_internal_ram in
1011  let old_high_internal_ram = s.high_internal_ram in
1012  let old_external_ram = s.external_ram in
1013  let old_program_counter = s.program_counter in
1014  let old_special_function_registers_8051 = s.special_function_registers_8051
1015  in
1016  let old_special_function_registers_8052 = s.special_function_registers_8052
1017  in
1018  let new_special_function_registers_8051 =
1019    Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1020      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1021      (Nat.S Nat.O))))))))))))))))))) old_special_function_registers_8051
1022      index b
1023  in
1024  let old_p1_latch = s.p1_latch in
1025  let old_p3_latch = s.p3_latch in
1026  let old_clock = s.clock in
1027  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1028  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1029  old_program_counter; special_function_registers_8051 =
1030  new_special_function_registers_8051; special_function_registers_8052 =
1031  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1032  old_p3_latch; clock = old_clock }
1033
1034(** val set_8052_sfr :
1035    'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus **)
1036let set_8052_sfr code_memory s i b =
1037  let index = sfr_8052_index i in
1038  let old_low_internal_ram = s.low_internal_ram in
1039  let old_high_internal_ram = s.high_internal_ram in
1040  let old_external_ram = s.external_ram in
1041  let old_program_counter = s.program_counter in
1042  let old_special_function_registers_8051 = s.special_function_registers_8051
1043  in
1044  let old_special_function_registers_8052 = s.special_function_registers_8052
1045  in
1046  let new_special_function_registers_8052 =
1047    Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1048      old_special_function_registers_8052 index b
1049  in
1050  let old_p1_latch = s.p1_latch in
1051  let old_p3_latch = s.p3_latch in
1052  let old_clock = s.clock in
1053  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1054  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1055  old_program_counter; special_function_registers_8051 =
1056  old_special_function_registers_8051; special_function_registers_8052 =
1057  new_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1058  old_p3_latch; clock = old_clock }
1059
1060(** val set_program_counter :
1061    'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus **)
1062let set_program_counter code_memory s w =
1063  let old_low_internal_ram = s.low_internal_ram in
1064  let old_high_internal_ram = s.high_internal_ram in
1065  let old_external_ram = s.external_ram in
1066  let old_special_function_registers_8051 = s.special_function_registers_8051
1067  in
1068  let old_special_function_registers_8052 = s.special_function_registers_8052
1069  in
1070  let old_p1_latch = s.p1_latch in
1071  let old_p3_latch = s.p3_latch in
1072  let old_clock = s.clock in
1073  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1074  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1075  w; special_function_registers_8051 = old_special_function_registers_8051;
1076  special_function_registers_8052 = old_special_function_registers_8052;
1077  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1078
1079(** val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus **)
1080let set_code_memory code_memory s r =
1081  let old_low_internal_ram = s.low_internal_ram in
1082  let old_high_internal_ram = s.high_internal_ram in
1083  let old_external_ram = s.external_ram in
1084  let old_program_counter = s.program_counter in
1085  let old_special_function_registers_8051 = s.special_function_registers_8051
1086  in
1087  let old_special_function_registers_8052 = s.special_function_registers_8052
1088  in
1089  let old_p1_latch = s.p1_latch in
1090  let old_p3_latch = s.p3_latch in
1091  let old_clock = s.clock in
1092  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1093  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1094  old_program_counter; special_function_registers_8051 =
1095  old_special_function_registers_8051; special_function_registers_8052 =
1096  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1097  old_p3_latch; clock = old_clock }
1098
1099(** val set_low_internal_ram :
1100    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1101    preStatus **)
1102let set_low_internal_ram code_memory s r =
1103  let old_high_internal_ram = s.high_internal_ram in
1104  let old_external_ram = s.external_ram in
1105  let old_program_counter = s.program_counter in
1106  let old_special_function_registers_8051 = s.special_function_registers_8051
1107  in
1108  let old_special_function_registers_8052 = s.special_function_registers_8052
1109  in
1110  let old_p1_latch = s.p1_latch in
1111  let old_p3_latch = s.p3_latch in
1112  let old_clock = s.clock in
1113  { low_internal_ram = r; high_internal_ram = old_high_internal_ram;
1114  external_ram = old_external_ram; program_counter = old_program_counter;
1115  special_function_registers_8051 = old_special_function_registers_8051;
1116  special_function_registers_8052 = old_special_function_registers_8052;
1117  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1118
1119(** val set_high_internal_ram :
1120    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1121    preStatus **)
1122let set_high_internal_ram code_memory s r =
1123  let old_low_internal_ram = s.low_internal_ram in
1124  let old_high_internal_ram = s.high_internal_ram in
1125  let old_external_ram = s.external_ram in
1126  let old_program_counter = s.program_counter in
1127  let old_special_function_registers_8051 = s.special_function_registers_8051
1128  in
1129  let old_special_function_registers_8052 = s.special_function_registers_8052
1130  in
1131  let old_p1_latch = s.p1_latch in
1132  let old_p3_latch = s.p3_latch in
1133  let old_clock = s.clock in
1134  { low_internal_ram = old_low_internal_ram; high_internal_ram = r;
1135  external_ram = old_external_ram; program_counter = old_program_counter;
1136  special_function_registers_8051 = old_special_function_registers_8051;
1137  special_function_registers_8052 = old_special_function_registers_8052;
1138  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1139
1140(** val set_external_ram :
1141    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1142    preStatus **)
1143let set_external_ram code_memory s r =
1144  let old_low_internal_ram = s.low_internal_ram in
1145  let old_high_internal_ram = s.high_internal_ram in
1146  let old_program_counter = s.program_counter in
1147  let old_special_function_registers_8051 = s.special_function_registers_8051
1148  in
1149  let old_special_function_registers_8052 = s.special_function_registers_8052
1150  in
1151  let old_p1_latch = s.p1_latch in
1152  let old_p3_latch = s.p3_latch in
1153  let old_clock = s.clock in
1154  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1155  old_high_internal_ram; external_ram = r; program_counter =
1156  old_program_counter; special_function_registers_8051 =
1157  old_special_function_registers_8051; special_function_registers_8052 =
1158  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1159  old_p3_latch; clock = old_clock }
1160
1161(** val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1162let get_cy_flag code_memory s =
1163  let sfr = s.special_function_registers_8051 in
1164  let psw =
1165    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1166      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1167      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1168  in
1169  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1170    Nat.O)))))))) psw Nat.O
1171
1172(** val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1173let get_ac_flag code_memory s =
1174  let sfr = s.special_function_registers_8051 in
1175  let psw =
1176    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1177      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1178      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1179  in
1180  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1181    Nat.O)))))))) psw (Nat.S Nat.O)
1182
1183(** val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1184let get_fo_flag code_memory s =
1185  let sfr = s.special_function_registers_8051 in
1186  let psw =
1187    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1188      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1189      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1190  in
1191  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1192    Nat.O)))))))) psw (Nat.S (Nat.S Nat.O))
1193
1194(** val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1195let get_rs1_flag code_memory s =
1196  let sfr = s.special_function_registers_8051 in
1197  let psw =
1198    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1199      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1200      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1201  in
1202  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1203    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S Nat.O)))
1204
1205(** val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1206let get_rs0_flag code_memory s =
1207  let sfr = s.special_function_registers_8051 in
1208  let psw =
1209    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1210      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1211      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1212  in
1213  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1214    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1215
1216(** val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1217let get_ov_flag code_memory s =
1218  let sfr = s.special_function_registers_8051 in
1219  let psw =
1220    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1221      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1222      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1223  in
1224  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1225    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1226
1227(** val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1228let get_ud_flag code_memory s =
1229  let sfr = s.special_function_registers_8051 in
1230  let psw =
1231    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1232      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1233      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1234  in
1235  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1236    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1237
1238(** val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1239let get_p_flag code_memory s =
1240  let sfr = s.special_function_registers_8051 in
1241  let psw =
1242    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1243      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1244      (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
1245  in
1246  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1247    Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1248    Nat.O)))))))
1249
1250(** val set_flags :
1251    'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
1252    BitVector.bit -> 'a1 preStatus **)
1253let set_flags code_memory s cy ac ov =
1254  let sfr_psw = get_8051_sfr code_memory s SFR_PSW in
1255  let old_cy =
1256    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1257      (Nat.S Nat.O)))))))) sfr_psw Nat.O
1258  in
1259  let old_ac =
1260    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1261      (Nat.S Nat.O)))))))) sfr_psw (Nat.S Nat.O)
1262  in
1263  let old_fo =
1264    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1265      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S Nat.O))
1266  in
1267  let old_rs1 =
1268    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1269      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S Nat.O)))
1270  in
1271  let old_rs0 =
1272    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1273      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1274  in
1275  let old_ov =
1276    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1277      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1278      Nat.O)))))
1279  in
1280  let old_ud =
1281    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1282      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1283      Nat.O))))))
1284  in
1285  let old_p =
1286    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1287      (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1288      (Nat.S Nat.O)))))))
1289  in
1290  let new_ac =
1291    match ac with
1292    | Types.None -> old_ac
1293    | Types.Some j -> j
1294  in
1295  set_8051_sfr code_memory s SFR_PSW (Vector.VCons ((Nat.S (Nat.S (Nat.S
1296    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), old_cy, (Vector.VCons ((Nat.S
1297    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), new_ac, (Vector.VCons
1298    ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), old_fo, (Vector.VCons
1299    ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), old_rs1, (Vector.VCons ((Nat.S
1300    (Nat.S (Nat.S Nat.O))), old_rs0, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1301    old_ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O,
1302    old_p, Vector.VEmpty))))))))))))))))
1303
1304(** val initialise_status : 'a1 -> 'a1 preStatus **)
1305let initialise_status code_mem =
1306  let status0 = { low_internal_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1307    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))); high_internal_ram =
1308    (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1309    Nat.O)))))))); external_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1310    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1311    (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))); program_counter =
1312    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1313      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1314      Nat.O))))))))))))))))); special_function_registers_8051 =
1315    (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1316      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1317      (Nat.S Nat.O)))))))))))))))))))
1318      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1319        Nat.O)))))))))); special_function_registers_8052 =
1320    (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1321      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1322        Nat.O)))))))))); p1_latch =
1323    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1324      Nat.O))))))))); p3_latch =
1325    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1326      Nat.O))))))))); clock = Nat.O }
1327  in
1328  set_8051_sfr code_mem status0 SFR_SP
1329    (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1330      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1331      (Nat.S Nat.O))))))))
1332
1333(** val sfr_of_Byte :
1334    BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option **)
1335let sfr_of_Byte b =
1336  let address =
1337    Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1338      (Nat.S (Nat.S Nat.O)))))))) b
1339  in
1340  (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1341           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1342           (Nat.S (Nat.S (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
1355           Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1356   | Bool.True -> Types.None
1357   | Bool.False ->
1358     (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1359              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1360              (Nat.S (Nat.S (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
1375              Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1376      | Bool.True -> Types.Some (Types.Inl SFR_P1)
1377      | Bool.False ->
1378        (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1379                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1380                 (Nat.S (Nat.S (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
1399                 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1400         | Bool.True -> Types.None
1401         | Bool.False ->
1402           (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1403                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1404                    (Nat.S (Nat.S (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
1425                    Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1426            | Bool.True -> Types.Some (Types.Inl SFR_P3)
1427            | Bool.False ->
1428              (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1429                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1430                       (Nat.S (Nat.S (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
1451                       Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1452               | Bool.True -> Types.Some (Types.Inl SFR_SBUF)
1453               | Bool.False ->
1454                 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1455                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1456                          (Nat.S (Nat.S (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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1475                  | Bool.True -> Types.Some (Types.Inl SFR_TL0)
1476                  | Bool.False ->
1477                    (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1478                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1479                             (Nat.S (Nat.S (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
1498                             Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1499                     | Bool.True -> Types.Some (Types.Inl SFR_TL1)
1500                     | Bool.False ->
1501                       (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1502                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1503                                (Nat.S (Nat.S (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
1525                                Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1526                        | Bool.True -> Types.Some (Types.Inl SFR_TH0)
1527                        | Bool.False ->
1528                          (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1529                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1530                                   (Nat.S (Nat.S (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
1552                                   Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1553                           | Bool.True -> Types.Some (Types.Inl SFR_TH1)
1554                           | Bool.False ->
1555                             (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1556                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1557                                      (Nat.S (Nat.S (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
1596                                      Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1597                              | Bool.True -> Types.Some (Types.Inr SFR_T2CON)
1598                              | Bool.False ->
1599                                (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1600                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1601                                         (Nat.S (Nat.S (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
1640                                         Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1641                                 | Bool.True ->
1642                                   Types.Some (Types.Inr SFR_RCAP2L)
1643                                 | Bool.False ->
1644                                   (match Nat.eqb address (Nat.S (Nat.S
1645                                            (Nat.S (Nat.S (Nat.S (Nat.S
1646                                            (Nat.S (Nat.S (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
1696                                            Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1697                                    | Bool.True ->
1698                                      Types.Some (Types.Inr SFR_RCAP2H)
1699                                    | Bool.False ->
1700                                      (match Nat.eqb address (Nat.S (Nat.S
1701                                               (Nat.S (Nat.S (Nat.S (Nat.S
1702                                               (Nat.S (Nat.S (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
1752                                               Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1753                                       | Bool.True ->
1754                                         Types.Some (Types.Inr SFR_TL2)
1755                                       | Bool.False ->
1756                                         (match Nat.eqb address (Nat.S (Nat.S
1757                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1758                                                  (Nat.S (Nat.S (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
1808                                                  Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1809                                          | Bool.True ->
1810                                            Types.Some (Types.Inr SFR_TH2)
1811                                          | Bool.False ->
1812                                            (match Nat.eqb address (Nat.S
1813                                                     (Nat.S (Nat.S (Nat.S
1814                                                     (Nat.S (Nat.S (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
1858                                                     Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1859                                             | Bool.True ->
1860                                               Types.Some (Types.Inl
1861                                                 SFR_PCON)
1862                                             | Bool.False ->
1863                                               (match Nat.eqb address (Nat.S
1864                                                        (Nat.S (Nat.S (Nat.S
1865                                                        (Nat.S (Nat.S (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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1910                                                | Bool.True ->
1911                                                  Types.Some (Types.Inl
1912                                                    SFR_TCON)
1913                                                | Bool.False ->
1914                                                  (match Nat.eqb address
1915                                                           (Nat.S (Nat.S
1916                                                           (Nat.S (Nat.S
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
1984                                                           Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1985                                                   | Bool.True ->
1986                                                     Types.Some (Types.Inl
1987                                                       SFR_TMOD)
1988                                                   | Bool.False ->
1989                                                     (match Nat.eqb address
1990                                                              (Nat.S (Nat.S
1991                                                              (Nat.S (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2067                                                      | Bool.True ->
2068                                                        Types.Some (Types.Inl
2069                                                          SFR_SCON)
2070                                                      | Bool.False ->
2071                                                        (match Nat.eqb
2072                                                                 address
2073                                                                 (Nat.S
2074                                                                 (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2242                                                         | Bool.True ->
2243                                                           Types.Some
2244                                                             (Types.Inl
2245                                                             SFR_IE)
2246                                                         | Bool.False ->
2247                                                           (match Nat.eqb
2248                                                                    address
2249                                                                    (Nat.S
2250                                                                    (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2434                                                            | Bool.True ->
2435                                                              Types.Some
2436                                                                (Types.Inl
2437                                                                SFR_IP)
2438                                                            | Bool.False ->
2439                                                              (match 
2440                                                               Nat.eqb
2441                                                                 address
2442                                                                 (Nat.S
2443                                                                 (Nat.S
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.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2572                                                               | Bool.True ->
2573                                                                 Types.Some
2574                                                                   (Types.Inl
2575                                                                   SFR_SP)
2576                                                               | Bool.False ->
2577                                                                 (match 
2578                                                                  Nat.eqb
2579                                                                    address
2580                                                                    (Nat.S
2581                                                                    (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2711                                                                  | Bool.True ->
2712                                                                    Types.Some
2713                                                                    (Types.Inl
2714                                                                    SFR_DPL)
2715                                                                  | Bool.False ->
2716                                                                    (match 
2717                                                                    Nat.eqb
2718                                                                    address
2719                                                                    (Nat.S
2720                                                                    (Nat.S
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.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2851                                                                    | Bool.True ->
2852                                                                    Types.Some
2853                                                                    (Types.Inl
2854                                                                    SFR_DPH)
2855                                                                    | Bool.False ->
2856                                                                    (match 
2857                                                                    Nat.eqb
2858                                                                    address
2859                                                                    (Nat.S
2860                                                                    (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3068                                                                    | Bool.True ->
3069                                                                    Types.Some
3070                                                                    (Types.Inl
3071                                                                    SFR_PSW)
3072                                                                    | Bool.False ->
3073                                                                    (match 
3074                                                                    Nat.eqb
3075                                                                    address
3076                                                                    (Nat.S
3077                                                                    (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3301                                                                    | Bool.True ->
3302                                                                    Types.Some
3303                                                                    (Types.Inl
3304                                                                    SFR_ACC_A)
3305                                                                    | Bool.False ->
3306                                                                    (match 
3307                                                                    Nat.eqb
3308                                                                    address
3309                                                                    (Nat.S
3310                                                                    (Nat.S
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