source: extracted/status.ml @ 3080

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

New extraction.

File size: 246.3 KB
Line 
1open Preamble
2
3open Types
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Jmeq
14
15open Russell
16
17open BitVectorTrie
18
19open String
20
21open Exp
22
23open Arithmetic
24
25open Vector
26
27open FoldStuff
28
29open BitVector
30
31open Extranat
32
33open Integers
34
35open AST
36
37open LabelledObjects
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Div_and_mod
60
61open Util
62
63open List
64
65open Lists
66
67open Bool
68
69open Relations
70
71open Nat
72
73open Positive
74
75open Identifiers
76
77open CostLabel
78
79open ASM
80
81type time = Nat.nat
82
83type serialBufferType =
84| Eight of BitVector.byte
85| Nine of BitVector.bit * BitVector.byte
86
87(** val serialBufferType_rect_Type4 :
88    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
89    serialBufferType -> 'a1 **)
90let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
91| Eight x_21722 -> h_Eight x_21722
92| Nine (x_21724, x_21723) -> h_Nine x_21724 x_21723
93
94(** val serialBufferType_rect_Type5 :
95    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
96    serialBufferType -> 'a1 **)
97let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
98| Eight x_21728 -> h_Eight x_21728
99| Nine (x_21730, x_21729) -> h_Nine x_21730 x_21729
100
101(** val serialBufferType_rect_Type3 :
102    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
103    serialBufferType -> 'a1 **)
104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
105| Eight x_21734 -> h_Eight x_21734
106| Nine (x_21736, x_21735) -> h_Nine x_21736 x_21735
107
108(** val serialBufferType_rect_Type2 :
109    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
110    serialBufferType -> 'a1 **)
111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
112| Eight x_21740 -> h_Eight x_21740
113| Nine (x_21742, x_21741) -> h_Nine x_21742 x_21741
114
115(** val serialBufferType_rect_Type1 :
116    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
117    serialBufferType -> 'a1 **)
118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
119| Eight x_21746 -> h_Eight x_21746
120| Nine (x_21748, x_21747) -> h_Nine x_21748 x_21747
121
122(** val serialBufferType_rect_Type0 :
123    (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
124    serialBufferType -> 'a1 **)
125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
126| Eight x_21752 -> h_Eight x_21752
127| Nine (x_21754, x_21753) -> h_Nine x_21754 x_21753
128
129(** val serialBufferType_inv_rect_Type4 :
130    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
131    BitVector.byte -> __ -> 'a1) -> 'a1 **)
132let serialBufferType_inv_rect_Type4 hterm h1 h2 =
133  let hcut = serialBufferType_rect_Type4 h1 h2 hterm in hcut __
134
135(** val serialBufferType_inv_rect_Type3 :
136    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
137    BitVector.byte -> __ -> 'a1) -> 'a1 **)
138let serialBufferType_inv_rect_Type3 hterm h1 h2 =
139  let hcut = serialBufferType_rect_Type3 h1 h2 hterm in hcut __
140
141(** val serialBufferType_inv_rect_Type2 :
142    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
143    BitVector.byte -> __ -> 'a1) -> 'a1 **)
144let serialBufferType_inv_rect_Type2 hterm h1 h2 =
145  let hcut = serialBufferType_rect_Type2 h1 h2 hterm in hcut __
146
147(** val serialBufferType_inv_rect_Type1 :
148    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
149    BitVector.byte -> __ -> 'a1) -> 'a1 **)
150let serialBufferType_inv_rect_Type1 hterm h1 h2 =
151  let hcut = serialBufferType_rect_Type1 h1 h2 hterm in hcut __
152
153(** val serialBufferType_inv_rect_Type0 :
154    serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
155    BitVector.byte -> __ -> 'a1) -> 'a1 **)
156let serialBufferType_inv_rect_Type0 hterm h1 h2 =
157  let hcut = serialBufferType_rect_Type0 h1 h2 hterm in hcut __
158
159(** val serialBufferType_discr :
160    serialBufferType -> serialBufferType -> __ **)
161let serialBufferType_discr x y =
162  Logic.eq_rect_Type2 x
163    (match x with
164     | Eight a0 -> Obj.magic (fun _ dH -> dH __)
165     | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
166
167(** val serialBufferType_jmdiscr :
168    serialBufferType -> serialBufferType -> __ **)
169let serialBufferType_jmdiscr x y =
170  Logic.eq_rect_Type2 x
171    (match x with
172     | Eight a0 -> Obj.magic (fun _ dH -> dH __)
173     | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
174
175type lineType =
176| P1 of BitVector.byte
177| P3 of BitVector.byte
178| SerialBuffer of serialBufferType
179
180(** val lineType_rect_Type4 :
181    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
182    -> 'a1) -> lineType -> 'a1 **)
183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
184| P1 x_21801 -> h_P1 x_21801
185| P3 x_21802 -> h_P3 x_21802
186| SerialBuffer x_21803 -> h_SerialBuffer x_21803
187
188(** val lineType_rect_Type5 :
189    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
190    -> 'a1) -> lineType -> 'a1 **)
191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
192| P1 x_21808 -> h_P1 x_21808
193| P3 x_21809 -> h_P3 x_21809
194| SerialBuffer x_21810 -> h_SerialBuffer x_21810
195
196(** val lineType_rect_Type3 :
197    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
198    -> 'a1) -> lineType -> 'a1 **)
199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
200| P1 x_21815 -> h_P1 x_21815
201| P3 x_21816 -> h_P3 x_21816
202| SerialBuffer x_21817 -> h_SerialBuffer x_21817
203
204(** val lineType_rect_Type2 :
205    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
206    -> 'a1) -> lineType -> 'a1 **)
207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
208| P1 x_21822 -> h_P1 x_21822
209| P3 x_21823 -> h_P3 x_21823
210| SerialBuffer x_21824 -> h_SerialBuffer x_21824
211
212(** val lineType_rect_Type1 :
213    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
214    -> 'a1) -> lineType -> 'a1 **)
215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
216| P1 x_21829 -> h_P1 x_21829
217| P3 x_21830 -> h_P3 x_21830
218| SerialBuffer x_21831 -> h_SerialBuffer x_21831
219
220(** val lineType_rect_Type0 :
221    (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
222    -> 'a1) -> lineType -> 'a1 **)
223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
224| P1 x_21836 -> h_P1 x_21836
225| P3 x_21837 -> h_P3 x_21837
226| SerialBuffer x_21838 -> h_SerialBuffer x_21838
227
228(** val lineType_inv_rect_Type4 :
229    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
230    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
231let lineType_inv_rect_Type4 hterm h1 h2 h3 =
232  let hcut = lineType_rect_Type4 h1 h2 h3 hterm in hcut __
233
234(** val lineType_inv_rect_Type3 :
235    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
236    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
237let lineType_inv_rect_Type3 hterm h1 h2 h3 =
238  let hcut = lineType_rect_Type3 h1 h2 h3 hterm in hcut __
239
240(** val lineType_inv_rect_Type2 :
241    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
242    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
243let lineType_inv_rect_Type2 hterm h1 h2 h3 =
244  let hcut = lineType_rect_Type2 h1 h2 h3 hterm in hcut __
245
246(** val lineType_inv_rect_Type1 :
247    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
248    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
249let lineType_inv_rect_Type1 hterm h1 h2 h3 =
250  let hcut = lineType_rect_Type1 h1 h2 h3 hterm in hcut __
251
252(** val lineType_inv_rect_Type0 :
253    lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
254    'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
255let lineType_inv_rect_Type0 hterm h1 h2 h3 =
256  let hcut = lineType_rect_Type0 h1 h2 h3 hterm in hcut __
257
258(** val lineType_discr : lineType -> lineType -> __ **)
259let lineType_discr x y =
260  Logic.eq_rect_Type2 x
261    (match x with
262     | P1 a0 -> Obj.magic (fun _ dH -> dH __)
263     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
264     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
265
266(** val lineType_jmdiscr : lineType -> lineType -> __ **)
267let lineType_jmdiscr x y =
268  Logic.eq_rect_Type2 x
269    (match x with
270     | P1 a0 -> Obj.magic (fun _ dH -> dH __)
271     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
272     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
273
274type sFR8051 =
275| SFR_SP
276| SFR_DPL
277| SFR_DPH
278| SFR_PCON
279| SFR_TCON
280| SFR_TMOD
281| SFR_TL0
282| SFR_TL1
283| SFR_TH0
284| SFR_TH1
285| SFR_P1
286| SFR_SCON
287| SFR_SBUF
288| SFR_IE
289| SFR_P3
290| SFR_IP
291| SFR_PSW
292| SFR_ACC_A
293| SFR_ACC_B
294
295(** val sFR8051_rect_Type4 :
296    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
297    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
298let rec sFR8051_rect_Type4 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
299| SFR_SP -> h_SFR_SP
300| SFR_DPL -> h_SFR_DPL
301| SFR_DPH -> h_SFR_DPH
302| SFR_PCON -> h_SFR_PCON
303| SFR_TCON -> h_SFR_TCON
304| SFR_TMOD -> h_SFR_TMOD
305| SFR_TL0 -> h_SFR_TL0
306| SFR_TL1 -> h_SFR_TL1
307| SFR_TH0 -> h_SFR_TH0
308| SFR_TH1 -> h_SFR_TH1
309| SFR_P1 -> h_SFR_P1
310| SFR_SCON -> h_SFR_SCON
311| SFR_SBUF -> h_SFR_SBUF
312| SFR_IE -> h_SFR_IE
313| SFR_P3 -> h_SFR_P3
314| SFR_IP -> h_SFR_IP
315| SFR_PSW -> h_SFR_PSW
316| SFR_ACC_A -> h_SFR_ACC_A
317| SFR_ACC_B -> h_SFR_ACC_B
318
319(** val sFR8051_rect_Type5 :
320    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
321    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
322let rec sFR8051_rect_Type5 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
323| SFR_SP -> h_SFR_SP
324| SFR_DPL -> h_SFR_DPL
325| SFR_DPH -> h_SFR_DPH
326| SFR_PCON -> h_SFR_PCON
327| SFR_TCON -> h_SFR_TCON
328| SFR_TMOD -> h_SFR_TMOD
329| SFR_TL0 -> h_SFR_TL0
330| SFR_TL1 -> h_SFR_TL1
331| SFR_TH0 -> h_SFR_TH0
332| SFR_TH1 -> h_SFR_TH1
333| SFR_P1 -> h_SFR_P1
334| SFR_SCON -> h_SFR_SCON
335| SFR_SBUF -> h_SFR_SBUF
336| SFR_IE -> h_SFR_IE
337| SFR_P3 -> h_SFR_P3
338| SFR_IP -> h_SFR_IP
339| SFR_PSW -> h_SFR_PSW
340| SFR_ACC_A -> h_SFR_ACC_A
341| SFR_ACC_B -> h_SFR_ACC_B
342
343(** val sFR8051_rect_Type3 :
344    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
345    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
346let rec sFR8051_rect_Type3 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
347| SFR_SP -> h_SFR_SP
348| SFR_DPL -> h_SFR_DPL
349| SFR_DPH -> h_SFR_DPH
350| SFR_PCON -> h_SFR_PCON
351| SFR_TCON -> h_SFR_TCON
352| SFR_TMOD -> h_SFR_TMOD
353| SFR_TL0 -> h_SFR_TL0
354| SFR_TL1 -> h_SFR_TL1
355| SFR_TH0 -> h_SFR_TH0
356| SFR_TH1 -> h_SFR_TH1
357| SFR_P1 -> h_SFR_P1
358| SFR_SCON -> h_SFR_SCON
359| SFR_SBUF -> h_SFR_SBUF
360| SFR_IE -> h_SFR_IE
361| SFR_P3 -> h_SFR_P3
362| SFR_IP -> h_SFR_IP
363| SFR_PSW -> h_SFR_PSW
364| SFR_ACC_A -> h_SFR_ACC_A
365| SFR_ACC_B -> h_SFR_ACC_B
366
367(** val sFR8051_rect_Type2 :
368    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
369    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
370let rec sFR8051_rect_Type2 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
371| SFR_SP -> h_SFR_SP
372| SFR_DPL -> h_SFR_DPL
373| SFR_DPH -> h_SFR_DPH
374| SFR_PCON -> h_SFR_PCON
375| SFR_TCON -> h_SFR_TCON
376| SFR_TMOD -> h_SFR_TMOD
377| SFR_TL0 -> h_SFR_TL0
378| SFR_TL1 -> h_SFR_TL1
379| SFR_TH0 -> h_SFR_TH0
380| SFR_TH1 -> h_SFR_TH1
381| SFR_P1 -> h_SFR_P1
382| SFR_SCON -> h_SFR_SCON
383| SFR_SBUF -> h_SFR_SBUF
384| SFR_IE -> h_SFR_IE
385| SFR_P3 -> h_SFR_P3
386| SFR_IP -> h_SFR_IP
387| SFR_PSW -> h_SFR_PSW
388| SFR_ACC_A -> h_SFR_ACC_A
389| SFR_ACC_B -> h_SFR_ACC_B
390
391(** val sFR8051_rect_Type1 :
392    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
393    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
394let rec sFR8051_rect_Type1 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
395| SFR_SP -> h_SFR_SP
396| SFR_DPL -> h_SFR_DPL
397| SFR_DPH -> h_SFR_DPH
398| SFR_PCON -> h_SFR_PCON
399| SFR_TCON -> h_SFR_TCON
400| SFR_TMOD -> h_SFR_TMOD
401| SFR_TL0 -> h_SFR_TL0
402| SFR_TL1 -> h_SFR_TL1
403| SFR_TH0 -> h_SFR_TH0
404| SFR_TH1 -> h_SFR_TH1
405| SFR_P1 -> h_SFR_P1
406| SFR_SCON -> h_SFR_SCON
407| SFR_SBUF -> h_SFR_SBUF
408| SFR_IE -> h_SFR_IE
409| SFR_P3 -> h_SFR_P3
410| SFR_IP -> h_SFR_IP
411| SFR_PSW -> h_SFR_PSW
412| SFR_ACC_A -> h_SFR_ACC_A
413| SFR_ACC_B -> h_SFR_ACC_B
414
415(** val sFR8051_rect_Type0 :
416    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
417    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
418let rec sFR8051_rect_Type0 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
419| SFR_SP -> h_SFR_SP
420| SFR_DPL -> h_SFR_DPL
421| SFR_DPH -> h_SFR_DPH
422| SFR_PCON -> h_SFR_PCON
423| SFR_TCON -> h_SFR_TCON
424| SFR_TMOD -> h_SFR_TMOD
425| SFR_TL0 -> h_SFR_TL0
426| SFR_TL1 -> h_SFR_TL1
427| SFR_TH0 -> h_SFR_TH0
428| SFR_TH1 -> h_SFR_TH1
429| SFR_P1 -> h_SFR_P1
430| SFR_SCON -> h_SFR_SCON
431| SFR_SBUF -> h_SFR_SBUF
432| SFR_IE -> h_SFR_IE
433| SFR_P3 -> h_SFR_P3
434| SFR_IP -> h_SFR_IP
435| SFR_PSW -> h_SFR_PSW
436| SFR_ACC_A -> h_SFR_ACC_A
437| SFR_ACC_B -> h_SFR_ACC_B
438
439(** val sFR8051_inv_rect_Type4 :
440    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
441    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
442    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
443    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
444    -> 'a1) -> 'a1 **)
445let sFR8051_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
446  let hcut =
447    sFR8051_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
448      h17 h18 h19 hterm
449  in
450  hcut __
451
452(** val sFR8051_inv_rect_Type3 :
453    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
454    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
455    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
456    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
457    -> 'a1) -> 'a1 **)
458let sFR8051_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
459  let hcut =
460    sFR8051_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
461      h17 h18 h19 hterm
462  in
463  hcut __
464
465(** val sFR8051_inv_rect_Type2 :
466    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
467    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
468    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
469    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
470    -> 'a1) -> 'a1 **)
471let sFR8051_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
472  let hcut =
473    sFR8051_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
474      h17 h18 h19 hterm
475  in
476  hcut __
477
478(** val sFR8051_inv_rect_Type1 :
479    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
480    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
481    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
482    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
483    -> 'a1) -> 'a1 **)
484let sFR8051_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
485  let hcut =
486    sFR8051_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
487      h17 h18 h19 hterm
488  in
489  hcut __
490
491(** val sFR8051_inv_rect_Type0 :
492    sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
493    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
494    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
495    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
496    -> 'a1) -> 'a1 **)
497let sFR8051_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
498  let hcut =
499    sFR8051_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
500      h17 h18 h19 hterm
501  in
502  hcut __
503
504(** val sFR8051_discr : sFR8051 -> sFR8051 -> __ **)
505let sFR8051_discr x y =
506  Logic.eq_rect_Type2 x
507    (match x with
508     | SFR_SP -> Obj.magic (fun _ dH -> dH)
509     | SFR_DPL -> Obj.magic (fun _ dH -> dH)
510     | SFR_DPH -> Obj.magic (fun _ dH -> dH)
511     | SFR_PCON -> Obj.magic (fun _ dH -> dH)
512     | SFR_TCON -> Obj.magic (fun _ dH -> dH)
513     | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
514     | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
515     | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
516     | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
517     | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
518     | SFR_P1 -> Obj.magic (fun _ dH -> dH)
519     | SFR_SCON -> Obj.magic (fun _ dH -> dH)
520     | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
521     | SFR_IE -> Obj.magic (fun _ dH -> dH)
522     | SFR_P3 -> Obj.magic (fun _ dH -> dH)
523     | SFR_IP -> Obj.magic (fun _ dH -> dH)
524     | SFR_PSW -> Obj.magic (fun _ dH -> dH)
525     | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
526     | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
527
528(** val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __ **)
529let sFR8051_jmdiscr x y =
530  Logic.eq_rect_Type2 x
531    (match x with
532     | SFR_SP -> Obj.magic (fun _ dH -> dH)
533     | SFR_DPL -> Obj.magic (fun _ dH -> dH)
534     | SFR_DPH -> Obj.magic (fun _ dH -> dH)
535     | SFR_PCON -> Obj.magic (fun _ dH -> dH)
536     | SFR_TCON -> Obj.magic (fun _ dH -> dH)
537     | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
538     | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
539     | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
540     | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
541     | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
542     | SFR_P1 -> Obj.magic (fun _ dH -> dH)
543     | SFR_SCON -> Obj.magic (fun _ dH -> dH)
544     | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
545     | SFR_IE -> Obj.magic (fun _ dH -> dH)
546     | SFR_P3 -> Obj.magic (fun _ dH -> dH)
547     | SFR_IP -> Obj.magic (fun _ dH -> dH)
548     | SFR_PSW -> Obj.magic (fun _ dH -> dH)
549     | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
550     | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
551
552(** val sfr_8051_index : sFR8051 -> Nat.nat **)
553let sfr_8051_index = function
554| SFR_SP -> Nat.O
555| SFR_DPL -> Nat.S Nat.O
556| SFR_DPH -> Nat.S (Nat.S Nat.O)
557| SFR_PCON -> Nat.S (Nat.S (Nat.S Nat.O))
558| SFR_TCON -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
559| SFR_TMOD -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
560| SFR_TL0 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
561| SFR_TL1 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
562| SFR_TH0 ->
563  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
564| SFR_TH1 ->
565  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
566| SFR_P1 ->
567  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
568    Nat.O)))))))))
569| SFR_SCON ->
570  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
571    Nat.O))))))))))
572| SFR_SBUF ->
573  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
574    (Nat.S Nat.O)))))))))))
575| SFR_IE ->
576  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
577    (Nat.S (Nat.S Nat.O))))))))))))
578| SFR_P3 ->
579  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
580    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))
581| SFR_IP ->
582  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
583    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))
584| SFR_PSW ->
585  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
586    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
587| SFR_ACC_A ->
588  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
589    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
590| SFR_ACC_B ->
591  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
592    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))
593
594type sFR8052 =
595| SFR_T2CON
596| SFR_RCAP2L
597| SFR_RCAP2H
598| SFR_TL2
599| SFR_TH2
600
601(** val sFR8052_rect_Type4 :
602    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
603let rec sFR8052_rect_Type4 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
604| SFR_T2CON -> h_SFR_T2CON
605| SFR_RCAP2L -> h_SFR_RCAP2L
606| SFR_RCAP2H -> h_SFR_RCAP2H
607| SFR_TL2 -> h_SFR_TL2
608| SFR_TH2 -> h_SFR_TH2
609
610(** val sFR8052_rect_Type5 :
611    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
612let rec sFR8052_rect_Type5 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
613| SFR_T2CON -> h_SFR_T2CON
614| SFR_RCAP2L -> h_SFR_RCAP2L
615| SFR_RCAP2H -> h_SFR_RCAP2H
616| SFR_TL2 -> h_SFR_TL2
617| SFR_TH2 -> h_SFR_TH2
618
619(** val sFR8052_rect_Type3 :
620    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
621let rec sFR8052_rect_Type3 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
622| SFR_T2CON -> h_SFR_T2CON
623| SFR_RCAP2L -> h_SFR_RCAP2L
624| SFR_RCAP2H -> h_SFR_RCAP2H
625| SFR_TL2 -> h_SFR_TL2
626| SFR_TH2 -> h_SFR_TH2
627
628(** val sFR8052_rect_Type2 :
629    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
630let rec sFR8052_rect_Type2 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
631| SFR_T2CON -> h_SFR_T2CON
632| SFR_RCAP2L -> h_SFR_RCAP2L
633| SFR_RCAP2H -> h_SFR_RCAP2H
634| SFR_TL2 -> h_SFR_TL2
635| SFR_TH2 -> h_SFR_TH2
636
637(** val sFR8052_rect_Type1 :
638    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
639let rec sFR8052_rect_Type1 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
640| SFR_T2CON -> h_SFR_T2CON
641| SFR_RCAP2L -> h_SFR_RCAP2L
642| SFR_RCAP2H -> h_SFR_RCAP2H
643| SFR_TL2 -> h_SFR_TL2
644| SFR_TH2 -> h_SFR_TH2
645
646(** val sFR8052_rect_Type0 :
647    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
648let rec sFR8052_rect_Type0 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
649| SFR_T2CON -> h_SFR_T2CON
650| SFR_RCAP2L -> h_SFR_RCAP2L
651| SFR_RCAP2H -> h_SFR_RCAP2H
652| SFR_TL2 -> h_SFR_TL2
653| SFR_TH2 -> h_SFR_TH2
654
655(** val sFR8052_inv_rect_Type4 :
656    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
657    (__ -> 'a1) -> 'a1 **)
658let sFR8052_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
659  let hcut = sFR8052_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
660
661(** val sFR8052_inv_rect_Type3 :
662    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
663    (__ -> 'a1) -> 'a1 **)
664let sFR8052_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
665  let hcut = sFR8052_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
666
667(** val sFR8052_inv_rect_Type2 :
668    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
669    (__ -> 'a1) -> 'a1 **)
670let sFR8052_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
671  let hcut = sFR8052_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
672
673(** val sFR8052_inv_rect_Type1 :
674    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
675    (__ -> 'a1) -> 'a1 **)
676let sFR8052_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
677  let hcut = sFR8052_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
678
679(** val sFR8052_inv_rect_Type0 :
680    sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
681    (__ -> 'a1) -> 'a1 **)
682let sFR8052_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
683  let hcut = sFR8052_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
684
685(** val sFR8052_discr : sFR8052 -> sFR8052 -> __ **)
686let sFR8052_discr x y =
687  Logic.eq_rect_Type2 x
688    (match x with
689     | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
690     | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
691     | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
692     | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
693     | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
694
695(** val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __ **)
696let sFR8052_jmdiscr x y =
697  Logic.eq_rect_Type2 x
698    (match x with
699     | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
700     | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
701     | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
702     | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
703     | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
704
705(** val sfr_8052_index : sFR8052 -> Nat.nat **)
706let sfr_8052_index = function
707| SFR_T2CON -> Nat.O
708| SFR_RCAP2L -> Nat.S Nat.O
709| SFR_RCAP2H -> Nat.S (Nat.S Nat.O)
710| SFR_TL2 -> Nat.S (Nat.S (Nat.S Nat.O))
711| SFR_TH2 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
712
713type 'm preStatus = { low_internal_ram : BitVector.byte
714                                         BitVectorTrie.bitVectorTrie;
715                      high_internal_ram : BitVector.byte
716                                          BitVectorTrie.bitVectorTrie;
717                      external_ram : BitVector.byte
718                                     BitVectorTrie.bitVectorTrie;
719                      program_counter : BitVector.word;
720                      special_function_registers_8051 : BitVector.byte
721                                                        Vector.vector;
722                      special_function_registers_8052 : BitVector.byte
723                                                        Vector.vector;
724                      p1_latch : BitVector.byte; p3_latch : BitVector.byte;
725                      clock : time }
726
727(** val preStatus_rect_Type4 :
728    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
729    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
730    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
731    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
732    preStatus -> 'a2 **)
733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_22224 =
734  let { low_internal_ram = low_internal_ram0; high_internal_ram =
735    high_internal_ram0; external_ram = external_ram0; program_counter =
736    program_counter0; special_function_registers_8051 =
737    special_function_registers_8053; special_function_registers_8052 =
738    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
739    p3_latch0; clock = clock0 } = x_22224
740  in
741  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
742    program_counter0 special_function_registers_8053
743    special_function_registers_8054 p1_latch0 p3_latch0 clock0
744
745(** val preStatus_rect_Type5 :
746    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
747    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
748    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
749    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
750    preStatus -> 'a2 **)
751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_22226 =
752  let { low_internal_ram = low_internal_ram0; high_internal_ram =
753    high_internal_ram0; external_ram = external_ram0; program_counter =
754    program_counter0; special_function_registers_8051 =
755    special_function_registers_8053; special_function_registers_8052 =
756    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
757    p3_latch0; clock = clock0 } = x_22226
758  in
759  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
760    program_counter0 special_function_registers_8053
761    special_function_registers_8054 p1_latch0 p3_latch0 clock0
762
763(** val preStatus_rect_Type3 :
764    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
765    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
766    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
767    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
768    preStatus -> 'a2 **)
769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_22228 =
770  let { low_internal_ram = low_internal_ram0; high_internal_ram =
771    high_internal_ram0; external_ram = external_ram0; program_counter =
772    program_counter0; special_function_registers_8051 =
773    special_function_registers_8053; special_function_registers_8052 =
774    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
775    p3_latch0; clock = clock0 } = x_22228
776  in
777  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
778    program_counter0 special_function_registers_8053
779    special_function_registers_8054 p1_latch0 p3_latch0 clock0
780
781(** val preStatus_rect_Type2 :
782    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
783    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
784    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
785    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
786    preStatus -> 'a2 **)
787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_22230 =
788  let { low_internal_ram = low_internal_ram0; high_internal_ram =
789    high_internal_ram0; external_ram = external_ram0; program_counter =
790    program_counter0; special_function_registers_8051 =
791    special_function_registers_8053; special_function_registers_8052 =
792    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
793    p3_latch0; clock = clock0 } = x_22230
794  in
795  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
796    program_counter0 special_function_registers_8053
797    special_function_registers_8054 p1_latch0 p3_latch0 clock0
798
799(** val preStatus_rect_Type1 :
800    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
801    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
802    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
803    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
804    preStatus -> 'a2 **)
805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_22232 =
806  let { low_internal_ram = low_internal_ram0; high_internal_ram =
807    high_internal_ram0; external_ram = external_ram0; program_counter =
808    program_counter0; special_function_registers_8051 =
809    special_function_registers_8053; special_function_registers_8052 =
810    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
811    p3_latch0; clock = clock0 } = x_22232
812  in
813  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
814    program_counter0 special_function_registers_8053
815    special_function_registers_8054 p1_latch0 p3_latch0 clock0
816
817(** val preStatus_rect_Type0 :
818    'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
819    BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
820    -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
821    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
822    preStatus -> 'a2 **)
823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_22234 =
824  let { low_internal_ram = low_internal_ram0; high_internal_ram =
825    high_internal_ram0; external_ram = external_ram0; program_counter =
826    program_counter0; special_function_registers_8051 =
827    special_function_registers_8053; special_function_registers_8052 =
828    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
829    p3_latch0; clock = clock0 } = x_22234
830  in
831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
832    program_counter0 special_function_registers_8053
833    special_function_registers_8054 p1_latch0 p3_latch0 clock0
834
835(** val low_internal_ram :
836    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
837let rec low_internal_ram code_memory xxx =
838  xxx.low_internal_ram
839
840(** val high_internal_ram :
841    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
842let rec high_internal_ram code_memory xxx =
843  xxx.high_internal_ram
844
845(** val external_ram :
846    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
847let rec external_ram code_memory xxx =
848  xxx.external_ram
849
850(** val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word **)
851let rec program_counter code_memory xxx =
852  xxx.program_counter
853
854(** val special_function_registers_8051 :
855    'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
856let rec special_function_registers_8051 code_memory xxx =
857  xxx.special_function_registers_8051
858
859(** val special_function_registers_8052 :
860    'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
861let rec special_function_registers_8052 code_memory xxx =
862  xxx.special_function_registers_8052
863
864(** val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
865let rec p1_latch code_memory xxx =
866  xxx.p1_latch
867
868(** val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
869let rec p3_latch code_memory xxx =
870  xxx.p3_latch
871
872(** val clock : 'a1 -> 'a1 preStatus -> time **)
873let rec clock code_memory xxx =
874  xxx.clock
875
876(** val preStatus_inv_rect_Type4 :
877    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
878    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
879    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
880    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
881    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
882let preStatus_inv_rect_Type4 x2 hterm h1 =
883  let hcut = preStatus_rect_Type4 x2 h1 hterm in hcut __
884
885(** val preStatus_inv_rect_Type3 :
886    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
887    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
888    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
889    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
890    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
891let preStatus_inv_rect_Type3 x2 hterm h1 =
892  let hcut = preStatus_rect_Type3 x2 h1 hterm in hcut __
893
894(** val preStatus_inv_rect_Type2 :
895    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
896    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
897    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
898    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
899    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
900let preStatus_inv_rect_Type2 x2 hterm h1 =
901  let hcut = preStatus_rect_Type2 x2 h1 hterm in hcut __
902
903(** val preStatus_inv_rect_Type1 :
904    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
905    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
906    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
907    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
908    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
909let preStatus_inv_rect_Type1 x2 hterm h1 =
910  let hcut = preStatus_rect_Type1 x2 h1 hterm in hcut __
911
912(** val preStatus_inv_rect_Type0 :
913    'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
914    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
915    BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
916    Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
917    BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
918let preStatus_inv_rect_Type0 x2 hterm h1 =
919  let hcut = preStatus_rect_Type0 x2 h1 hterm in hcut __
920
921(** val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __ **)
922let preStatus_jmdiscr a2 x y =
923  Logic.eq_rect_Type2 x
924    (let { low_internal_ram = a0; high_internal_ram = a10; external_ram =
925       a20; program_counter = a3; special_function_registers_8051 = a4;
926       special_function_registers_8052 = a5; p1_latch = a6; p3_latch = a7;
927       clock = a8 } = x
928     in
929    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y
930
931type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus
932
933type pseudoStatus = ASM.pseudo_assembly_program preStatus
934
935(** val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus **)
936let set_clock code_memory s t =
937  let old_low_internal_ram = s.low_internal_ram in
938  let old_high_internal_ram = s.high_internal_ram in
939  let old_external_ram = s.external_ram in
940  let old_program_counter = s.program_counter in
941  let old_special_function_registers_8051 = s.special_function_registers_8051
942  in
943  let old_special_function_registers_8052 = s.special_function_registers_8052
944  in
945  let old_p1_latch = s.p1_latch in
946  let old_p3_latch = s.p3_latch in
947  { low_internal_ram = old_low_internal_ram; high_internal_ram =
948  old_high_internal_ram; external_ram = old_external_ram; program_counter =
949  old_program_counter; special_function_registers_8051 =
950  old_special_function_registers_8051; special_function_registers_8052 =
951  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
952  old_p3_latch; clock = t }
953
954(** val set_p1_latch :
955    'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
956let set_p1_latch code_memory s b =
957  let old_low_internal_ram = s.low_internal_ram in
958  let old_high_internal_ram = s.high_internal_ram in
959  let old_external_ram = s.external_ram in
960  let old_program_counter = s.program_counter in
961  let old_special_function_registers_8051 = s.special_function_registers_8051
962  in
963  let old_special_function_registers_8052 = s.special_function_registers_8052
964  in
965  let old_p3_latch = s.p3_latch in
966  let old_clock = s.clock in
967  { low_internal_ram = old_low_internal_ram; high_internal_ram =
968  old_high_internal_ram; external_ram = old_external_ram; program_counter =
969  old_program_counter; special_function_registers_8051 =
970  old_special_function_registers_8051; special_function_registers_8052 =
971  old_special_function_registers_8052; p1_latch = b; p3_latch = old_p3_latch;
972  clock = old_clock }
973
974(** val set_p3_latch :
975    'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
976let set_p3_latch code_memory s b =
977  let old_low_internal_ram = s.low_internal_ram in
978  let old_high_internal_ram = s.high_internal_ram in
979  let old_external_ram = s.external_ram in
980  let old_program_counter = s.program_counter in
981  let old_special_function_registers_8051 = s.special_function_registers_8051
982  in
983  let old_special_function_registers_8052 = s.special_function_registers_8052
984  in
985  let old_p1_latch = s.p1_latch in
986  let old_clock = s.clock in
987  { low_internal_ram = old_low_internal_ram; high_internal_ram =
988  old_high_internal_ram; external_ram = old_external_ram; program_counter =
989  old_program_counter; special_function_registers_8051 =
990  old_special_function_registers_8051; special_function_registers_8052 =
991  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch = b;
992  clock = old_clock }
993
994(** val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte **)
995let get_8051_sfr code_memory s i =
996  let sfr = s.special_function_registers_8051 in
997  let index = sfr_8051_index i in
998  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
999    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1000    (Nat.S Nat.O))))))))))))))))))) sfr index
1001
1002(** val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte **)
1003let get_8052_sfr code_memory s i =
1004  let sfr = s.special_function_registers_8052 in
1005  let index = sfr_8052_index i in
1006  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) sfr index
1007
1008(** val set_8051_sfr :
1009    'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus **)
1010let set_8051_sfr code_memory s i b =
1011  let index = sfr_8051_index i in
1012  let old_low_internal_ram = s.low_internal_ram in
1013  let old_high_internal_ram = s.high_internal_ram in
1014  let old_external_ram = s.external_ram in
1015  let old_program_counter = s.program_counter in
1016  let old_special_function_registers_8051 = s.special_function_registers_8051
1017  in
1018  let old_special_function_registers_8052 = s.special_function_registers_8052
1019  in
1020  let new_special_function_registers_8051 =
1021    Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1022      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1023      (Nat.S Nat.O))))))))))))))))))) old_special_function_registers_8051
1024      index b
1025  in
1026  let old_p1_latch = s.p1_latch in
1027  let old_p3_latch = s.p3_latch in
1028  let old_clock = s.clock in
1029  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1030  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1031  old_program_counter; special_function_registers_8051 =
1032  new_special_function_registers_8051; special_function_registers_8052 =
1033  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1034  old_p3_latch; clock = old_clock }
1035
1036(** val set_8052_sfr :
1037    'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus **)
1038let set_8052_sfr code_memory s i b =
1039  let index = sfr_8052_index i in
1040  let old_low_internal_ram = s.low_internal_ram in
1041  let old_high_internal_ram = s.high_internal_ram in
1042  let old_external_ram = s.external_ram in
1043  let old_program_counter = s.program_counter in
1044  let old_special_function_registers_8051 = s.special_function_registers_8051
1045  in
1046  let old_special_function_registers_8052 = s.special_function_registers_8052
1047  in
1048  let new_special_function_registers_8052 =
1049    Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1050      old_special_function_registers_8052 index b
1051  in
1052  let old_p1_latch = s.p1_latch in
1053  let old_p3_latch = s.p3_latch in
1054  let old_clock = s.clock in
1055  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1056  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1057  old_program_counter; special_function_registers_8051 =
1058  old_special_function_registers_8051; special_function_registers_8052 =
1059  new_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1060  old_p3_latch; clock = old_clock }
1061
1062(** val set_program_counter :
1063    'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus **)
1064let set_program_counter code_memory s w =
1065  let old_low_internal_ram = s.low_internal_ram in
1066  let old_high_internal_ram = s.high_internal_ram in
1067  let old_external_ram = s.external_ram in
1068  let old_special_function_registers_8051 = s.special_function_registers_8051
1069  in
1070  let old_special_function_registers_8052 = s.special_function_registers_8052
1071  in
1072  let old_p1_latch = s.p1_latch in
1073  let old_p3_latch = s.p3_latch in
1074  let old_clock = s.clock in
1075  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1076  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1077  w; special_function_registers_8051 = old_special_function_registers_8051;
1078  special_function_registers_8052 = old_special_function_registers_8052;
1079  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1080
1081(** val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus **)
1082let set_code_memory code_memory s r =
1083  let old_low_internal_ram = s.low_internal_ram in
1084  let old_high_internal_ram = s.high_internal_ram in
1085  let old_external_ram = s.external_ram in
1086  let old_program_counter = s.program_counter in
1087  let old_special_function_registers_8051 = s.special_function_registers_8051
1088  in
1089  let old_special_function_registers_8052 = s.special_function_registers_8052
1090  in
1091  let old_p1_latch = s.p1_latch in
1092  let old_p3_latch = s.p3_latch in
1093  let old_clock = s.clock in
1094  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1095  old_high_internal_ram; external_ram = old_external_ram; program_counter =
1096  old_program_counter; special_function_registers_8051 =
1097  old_special_function_registers_8051; special_function_registers_8052 =
1098  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1099  old_p3_latch; clock = old_clock }
1100
1101(** val set_low_internal_ram :
1102    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1103    preStatus **)
1104let set_low_internal_ram code_memory s r =
1105  let old_high_internal_ram = s.high_internal_ram in
1106  let old_external_ram = s.external_ram in
1107  let old_program_counter = s.program_counter in
1108  let old_special_function_registers_8051 = s.special_function_registers_8051
1109  in
1110  let old_special_function_registers_8052 = s.special_function_registers_8052
1111  in
1112  let old_p1_latch = s.p1_latch in
1113  let old_p3_latch = s.p3_latch in
1114  let old_clock = s.clock in
1115  { low_internal_ram = r; high_internal_ram = old_high_internal_ram;
1116  external_ram = old_external_ram; program_counter = old_program_counter;
1117  special_function_registers_8051 = old_special_function_registers_8051;
1118  special_function_registers_8052 = old_special_function_registers_8052;
1119  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1120
1121(** val update_low_internal_ram :
1122    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
1123    preStatus **)
1124let update_low_internal_ram code_memory s addr v =
1125  let old_low_internal_ram = s.low_internal_ram in
1126  let new_low_internal_ram =
1127    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1128      Nat.O))))))) addr v old_low_internal_ram
1129  in
1130  set_low_internal_ram code_memory s new_low_internal_ram
1131
1132(** val set_high_internal_ram :
1133    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1134    preStatus **)
1135let set_high_internal_ram code_memory s r =
1136  let old_low_internal_ram = s.low_internal_ram in
1137  let old_high_internal_ram = s.high_internal_ram in
1138  let old_external_ram = s.external_ram in
1139  let old_program_counter = s.program_counter in
1140  let old_special_function_registers_8051 = s.special_function_registers_8051
1141  in
1142  let old_special_function_registers_8052 = s.special_function_registers_8052
1143  in
1144  let old_p1_latch = s.p1_latch in
1145  let old_p3_latch = s.p3_latch in
1146  let old_clock = s.clock in
1147  { low_internal_ram = old_low_internal_ram; high_internal_ram = r;
1148  external_ram = old_external_ram; program_counter = old_program_counter;
1149  special_function_registers_8051 = old_special_function_registers_8051;
1150  special_function_registers_8052 = old_special_function_registers_8052;
1151  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1152
1153(** val update_high_internal_ram :
1154    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
1155    preStatus **)
1156let update_high_internal_ram code_memory s addr v =
1157  let old_high_internal_ram = s.high_internal_ram in
1158  let new_high_internal_ram =
1159    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1160      Nat.O))))))) addr v old_high_internal_ram
1161  in
1162  set_high_internal_ram code_memory s new_high_internal_ram
1163
1164(** val set_external_ram :
1165    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1166    preStatus **)
1167let set_external_ram code_memory s r =
1168  let old_low_internal_ram = s.low_internal_ram in
1169  let old_high_internal_ram = s.high_internal_ram in
1170  let old_program_counter = s.program_counter in
1171  let old_special_function_registers_8051 = s.special_function_registers_8051
1172  in
1173  let old_special_function_registers_8052 = s.special_function_registers_8052
1174  in
1175  let old_p1_latch = s.p1_latch in
1176  let old_p3_latch = s.p3_latch in
1177  let old_clock = s.clock in
1178  { low_internal_ram = old_low_internal_ram; high_internal_ram =
1179  old_high_internal_ram; external_ram = r; program_counter =
1180  old_program_counter; special_function_registers_8051 =
1181  old_special_function_registers_8051; special_function_registers_8052 =
1182  old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1183  old_p3_latch; clock = old_clock }
1184
1185(** val update_external_ram :
1186    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
1187    preStatus **)
1188let update_external_ram code_memory s addr v =
1189  let old_external_ram = s.external_ram in
1190  let new_external_ram =
1191    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1192      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1193      Nat.O)))))))))))))))) addr v old_external_ram
1194  in
1195  set_external_ram code_memory s new_external_ram
1196
1197(** val get_psw_flags : 'a1 -> 'a1 preStatus -> Nat.nat -> Bool.bool **)
1198let get_psw_flags code_memory s flag =
1199  let psw = get_8051_sfr code_memory s SFR_PSW in
1200  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1201    Nat.O)))))))) psw flag
1202
1203(** val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1204let get_cy_flag code_memory s =
1205  get_psw_flags code_memory s Nat.O
1206
1207(** val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1208let get_ac_flag code_memory s =
1209  get_psw_flags code_memory s (Nat.S Nat.O)
1210
1211(** val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1212let get_fo_flag code_memory s =
1213  get_psw_flags code_memory s (Nat.S (Nat.S Nat.O))
1214
1215(** val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1216let get_rs1_flag code_memory s =
1217  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S Nat.O)))
1218
1219(** val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1220let get_rs0_flag code_memory s =
1221  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1222
1223(** val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1224let get_ov_flag code_memory s =
1225  get_psw_flags code_memory s (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  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1230    Nat.O))))))
1231
1232(** val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1233let get_p_flag code_memory s =
1234  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1235    (Nat.S Nat.O)))))))
1236
1237(** val set_flags :
1238    'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
1239    BitVector.bit -> 'a1 preStatus **)
1240let set_flags code_memory s cy ac ov =
1241  let old_cy = get_cy_flag code_memory s in
1242  let old_ac = get_ac_flag code_memory s in
1243  let old_fo = get_fo_flag code_memory s in
1244  let old_rs1 = get_rs1_flag code_memory s in
1245  let old_rs0 = get_rs0_flag code_memory s in
1246  let old_ov = get_ov_flag code_memory s in
1247  let old_ud = get_ud_flag code_memory s in
1248  let old_p = get_p_flag code_memory s in
1249  let new_ac =
1250    match ac with
1251    | Types.None -> old_ac
1252    | Types.Some j -> j
1253  in
1254  set_8051_sfr code_memory s SFR_PSW (Vector.VCons ((Nat.S (Nat.S (Nat.S
1255    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), cy, (Vector.VCons ((Nat.S
1256    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), new_ac, (Vector.VCons
1257    ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), old_fo, (Vector.VCons
1258    ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), old_rs1, (Vector.VCons ((Nat.S
1259    (Nat.S (Nat.S Nat.O))), old_rs0, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1260    ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O, old_p,
1261    Vector.VEmpty))))))))))))))))
1262
1263(** val initialise_status : 'a1 -> 'a1 preStatus **)
1264let initialise_status code_mem =
1265  let status0 = { low_internal_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1266    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))); high_internal_ram =
1267    (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1268    Nat.O)))))))); external_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1269    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1270    (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))); program_counter =
1271    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1272      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1273      Nat.O))))))))))))))))); special_function_registers_8051 =
1274    (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1275      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1276      (Nat.S Nat.O)))))))))))))))))))
1277      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1278        Nat.O)))))))))); special_function_registers_8052 =
1279    (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1280      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1281        Nat.O)))))))))); p1_latch =
1282    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1283      Nat.O))))))))); p3_latch =
1284    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1285      Nat.O))))))))); clock = Nat.O }
1286  in
1287  set_8051_sfr code_mem status0 SFR_SP
1288    (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1289      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1290      (Nat.S Nat.O))))))))
1291
1292(** val sfr_of_Byte :
1293    BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option **)
1294let sfr_of_Byte b =
1295  let address =
1296    Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1297      (Nat.S (Nat.S Nat.O)))))))) b
1298  in
1299  (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1300           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1301           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1302           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1303           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1304           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1305           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1306           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1307           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1308           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1309           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (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
1311           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1312           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1313           (Nat.S (Nat.S (Nat.S (Nat.S
1314           Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1315   | Bool.True -> Types.None
1316   | Bool.False ->
1317     (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1318              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1319              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1320              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1321              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1322              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1323              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1324              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1325              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1326              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1327              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1328              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1329              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1330              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1331              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1332              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1333              (Nat.S (Nat.S
1334              Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1335      | Bool.True -> Types.Some (Types.Inl SFR_P1)
1336      | Bool.False ->
1337        (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1338                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1339                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1340                 (Nat.S (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
1342                 (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
1344                 (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
1346                 (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
1348                 (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
1350                 (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
1352                 (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
1354                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1355                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1356                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1357                 (Nat.S (Nat.S
1358                 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1359         | Bool.True -> Types.None
1360         | Bool.False ->
1361           (match Nat.eqb address (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
1363                    (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
1365                    (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
1367                    (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
1369                    (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
1371                    (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
1373                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1374                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1375                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1376                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1377                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1378                    (Nat.S (Nat.S (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
1384                    Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1385            | Bool.True -> Types.Some (Types.Inl SFR_P3)
1386            | Bool.False ->
1387              (match Nat.eqb address (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
1389                       (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
1391                       (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
1393                       (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
1395                       (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
1397                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1398                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1399                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1400                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1401                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1402                       (Nat.S (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
1404                       (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
1406                       (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
1408                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1409                       (Nat.S
1410                       Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1411               | Bool.True -> Types.Some (Types.Inl SFR_SBUF)
1412               | Bool.False ->
1413                 (match Nat.eqb address (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
1415                          (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
1417                          (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
1419                          (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
1421                          (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
1423                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1424                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1425                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1426                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1427                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1428                          (Nat.S (Nat.S (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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1434                  | Bool.True -> Types.Some (Types.Inl SFR_TL0)
1435                  | Bool.False ->
1436                    (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1437                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1438                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1439                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1440                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1441                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1442                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1443                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1444                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1445                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1446                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1447                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1448                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1449                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1450                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1451                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1452                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1453                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1454                             (Nat.S (Nat.S (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
1457                             Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1458                     | Bool.True -> Types.Some (Types.Inl SFR_TL1)
1459                     | Bool.False ->
1460                       (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1461                                (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
1463                                (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
1465                                (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
1467                                (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
1469                                (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
1471                                (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
1473                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1474                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1475                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1476                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1477                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1478                                (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
1480                                (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
1482                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1483                                (Nat.S (Nat.S (Nat.S (Nat.S
1484                                Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1485                        | Bool.True -> Types.Some (Types.Inl SFR_TH0)
1486                        | Bool.False ->
1487                          (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1488                                   (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
1490                                   (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
1492                                   (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
1494                                   (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
1496                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1497                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1498                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1499                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1500                                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1501                                   (Nat.S (Nat.S (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
1511                                   Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1512                           | Bool.True -> Types.Some (Types.Inl SFR_TH1)
1513                           | Bool.False ->
1514                             (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1515                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1516                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1517                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1518                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1519                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1520                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1521                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1522                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1523                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1524                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1525                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1526                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1527                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1528                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1529                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1530                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1531                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1532                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1533                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1534                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1535                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1536                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1537                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1538                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1539                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1540                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1541                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1542                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1543                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1544                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1545                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1546                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1547                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1548                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1549                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1550                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1551                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1552                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1553                                      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1554                                      (Nat.S (Nat.S
1555                                      Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1556                              | Bool.True -> Types.Some (Types.Inr SFR_T2CON)
1557                              | Bool.False ->
1558                                (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1559                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1560                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1561                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1562                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1563                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1564                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1565                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1566                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1567                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1568                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1569                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1570                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1571                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1572                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1573                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1574                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1575                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1576                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1577                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1578                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1579                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1580                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1581                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1582                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1583                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1584                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1585                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1586                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1587                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1588                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1589                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1590                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1591                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1592                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1593                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1594                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1595                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1596                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1597                                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1598                                         (Nat.S (Nat.S (Nat.S (Nat.S
1599                                         Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1600                                 | Bool.True ->
1601                                   Types.Some (Types.Inr SFR_RCAP2L)
1602                                 | Bool.False ->
1603                                   (match Nat.eqb address (Nat.S (Nat.S
1604                                            (Nat.S (Nat.S (Nat.S (Nat.S
1605                                            (Nat.S (Nat.S (Nat.S (Nat.S
1606                                            (Nat.S (Nat.S (Nat.S (Nat.S
1607                                            (Nat.S (Nat.S (Nat.S (Nat.S
1608                                            (Nat.S (Nat.S (Nat.S (Nat.S
1609                                            (Nat.S (Nat.S (Nat.S (Nat.S
1610                                            (Nat.S (Nat.S (Nat.S (Nat.S
1611                                            (Nat.S (Nat.S (Nat.S (Nat.S
1612                                            (Nat.S (Nat.S (Nat.S (Nat.S
1613                                            (Nat.S (Nat.S (Nat.S (Nat.S
1614                                            (Nat.S (Nat.S (Nat.S (Nat.S
1615                                            (Nat.S (Nat.S (Nat.S (Nat.S
1616                                            (Nat.S (Nat.S (Nat.S (Nat.S
1617                                            (Nat.S (Nat.S (Nat.S (Nat.S
1618                                            (Nat.S (Nat.S (Nat.S (Nat.S
1619                                            (Nat.S (Nat.S (Nat.S (Nat.S
1620                                            (Nat.S (Nat.S (Nat.S (Nat.S
1621                                            (Nat.S (Nat.S (Nat.S (Nat.S
1622                                            (Nat.S (Nat.S (Nat.S (Nat.S
1623                                            (Nat.S (Nat.S (Nat.S (Nat.S
1624                                            (Nat.S (Nat.S (Nat.S (Nat.S
1625                                            (Nat.S (Nat.S (Nat.S (Nat.S
1626                                            (Nat.S (Nat.S (Nat.S (Nat.S
1627                                            (Nat.S (Nat.S (Nat.S (Nat.S
1628                                            (Nat.S (Nat.S (Nat.S (Nat.S
1629                                            (Nat.S (Nat.S (Nat.S (Nat.S
1630                                            (Nat.S (Nat.S (Nat.S (Nat.S
1631                                            (Nat.S (Nat.S (Nat.S (Nat.S
1632                                            (Nat.S (Nat.S (Nat.S (Nat.S
1633                                            (Nat.S (Nat.S (Nat.S (Nat.S
1634                                            (Nat.S (Nat.S (Nat.S (Nat.S
1635                                            (Nat.S (Nat.S (Nat.S (Nat.S
1636                                            (Nat.S (Nat.S (Nat.S (Nat.S
1637                                            (Nat.S (Nat.S (Nat.S (Nat.S
1638                                            (Nat.S (Nat.S (Nat.S (Nat.S
1639                                            (Nat.S (Nat.S (Nat.S (Nat.S
1640                                            (Nat.S (Nat.S (Nat.S (Nat.S
1641                                            (Nat.S (Nat.S (Nat.S (Nat.S
1642                                            (Nat.S (Nat.S (Nat.S (Nat.S
1643                                            (Nat.S (Nat.S (Nat.S (Nat.S
1644                                            (Nat.S (Nat.S (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
1655                                            Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1656                                    | Bool.True ->
1657                                      Types.Some (Types.Inr SFR_RCAP2H)
1658                                    | Bool.False ->
1659                                      (match Nat.eqb address (Nat.S (Nat.S
1660                                               (Nat.S (Nat.S (Nat.S (Nat.S
1661                                               (Nat.S (Nat.S (Nat.S (Nat.S
1662                                               (Nat.S (Nat.S (Nat.S (Nat.S
1663                                               (Nat.S (Nat.S (Nat.S (Nat.S
1664                                               (Nat.S (Nat.S (Nat.S (Nat.S
1665                                               (Nat.S (Nat.S (Nat.S (Nat.S
1666                                               (Nat.S (Nat.S (Nat.S (Nat.S
1667                                               (Nat.S (Nat.S (Nat.S (Nat.S
1668                                               (Nat.S (Nat.S (Nat.S (Nat.S
1669                                               (Nat.S (Nat.S (Nat.S (Nat.S
1670                                               (Nat.S (Nat.S (Nat.S (Nat.S
1671                                               (Nat.S (Nat.S (Nat.S (Nat.S
1672                                               (Nat.S (Nat.S (Nat.S (Nat.S
1673                                               (Nat.S (Nat.S (Nat.S (Nat.S
1674                                               (Nat.S (Nat.S (Nat.S (Nat.S
1675                                               (Nat.S (Nat.S (Nat.S (Nat.S
1676                                               (Nat.S (Nat.S (Nat.S (Nat.S
1677                                               (Nat.S (Nat.S (Nat.S (Nat.S
1678                                               (Nat.S (Nat.S (Nat.S (Nat.S
1679                                               (Nat.S (Nat.S (Nat.S (Nat.S
1680                                               (Nat.S (Nat.S (Nat.S (Nat.S
1681                                               (Nat.S (Nat.S (Nat.S (Nat.S
1682                                               (Nat.S (Nat.S (Nat.S (Nat.S
1683                                               (Nat.S (Nat.S (Nat.S (Nat.S
1684                                               (Nat.S (Nat.S (Nat.S (Nat.S
1685                                               (Nat.S (Nat.S (Nat.S (Nat.S
1686                                               (Nat.S (Nat.S (Nat.S (Nat.S
1687                                               (Nat.S (Nat.S (Nat.S (Nat.S
1688                                               (Nat.S (Nat.S (Nat.S (Nat.S
1689                                               (Nat.S (Nat.S (Nat.S (Nat.S
1690                                               (Nat.S (Nat.S (Nat.S (Nat.S
1691                                               (Nat.S (Nat.S (Nat.S (Nat.S
1692                                               (Nat.S (Nat.S (Nat.S (Nat.S
1693                                               (Nat.S (Nat.S (Nat.S (Nat.S
1694                                               (Nat.S (Nat.S (Nat.S (Nat.S
1695                                               (Nat.S (Nat.S (Nat.S (Nat.S
1696                                               (Nat.S (Nat.S (Nat.S (Nat.S
1697                                               (Nat.S (Nat.S (Nat.S (Nat.S
1698                                               (Nat.S (Nat.S (Nat.S (Nat.S
1699                                               (Nat.S (Nat.S (Nat.S (Nat.S
1700                                               (Nat.S (Nat.S (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
1711                                               Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1712                                       | Bool.True ->
1713                                         Types.Some (Types.Inr SFR_TL2)
1714                                       | Bool.False ->
1715                                         (match Nat.eqb address (Nat.S (Nat.S
1716                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1717                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1718                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1719                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1720                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1721                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1722                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1723                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1724                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1725                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1726                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1727                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1728                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1729                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1730                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1731                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1732                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1733                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1734                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1735                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1736                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1737                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1738                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1739                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1740                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1741                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1742                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1743                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1744                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1745                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1746                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1747                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1748                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1749                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1750                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1751                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1752                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1753                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1754                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1755                                                  (Nat.S (Nat.S (Nat.S (Nat.S
1756                                                  (Nat.S (Nat.S (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
1767                                                  Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1768                                          | Bool.True ->
1769                                            Types.Some (Types.Inr SFR_TH2)
1770                                          | Bool.False ->
1771                                            (match Nat.eqb address (Nat.S
1772                                                     (Nat.S (Nat.S (Nat.S
1773                                                     (Nat.S (Nat.S (Nat.S
1774                                                     (Nat.S (Nat.S (Nat.S
1775                                                     (Nat.S (Nat.S (Nat.S
1776                                                     (Nat.S (Nat.S (Nat.S
1777                                                     (Nat.S (Nat.S (Nat.S
1778                                                     (Nat.S (Nat.S (Nat.S
1779                                                     (Nat.S (Nat.S (Nat.S
1780                                                     (Nat.S (Nat.S (Nat.S
1781                                                     (Nat.S (Nat.S (Nat.S
1782                                                     (Nat.S (Nat.S (Nat.S
1783                                                     (Nat.S (Nat.S (Nat.S
1784                                                     (Nat.S (Nat.S (Nat.S
1785                                                     (Nat.S (Nat.S (Nat.S
1786                                                     (Nat.S (Nat.S (Nat.S
1787                                                     (Nat.S (Nat.S (Nat.S
1788                                                     (Nat.S (Nat.S (Nat.S
1789                                                     (Nat.S (Nat.S (Nat.S
1790                                                     (Nat.S (Nat.S (Nat.S
1791                                                     (Nat.S (Nat.S (Nat.S
1792                                                     (Nat.S (Nat.S (Nat.S
1793                                                     (Nat.S (Nat.S (Nat.S
1794                                                     (Nat.S (Nat.S (Nat.S
1795                                                     (Nat.S (Nat.S (Nat.S
1796                                                     (Nat.S (Nat.S (Nat.S
1797                                                     (Nat.S (Nat.S (Nat.S
1798                                                     (Nat.S (Nat.S (Nat.S
1799                                                     (Nat.S (Nat.S (Nat.S
1800                                                     (Nat.S (Nat.S (Nat.S
1801                                                     (Nat.S (Nat.S (Nat.S
1802                                                     (Nat.S (Nat.S (Nat.S
1803                                                     (Nat.S (Nat.S (Nat.S
1804                                                     (Nat.S (Nat.S (Nat.S
1805                                                     (Nat.S (Nat.S (Nat.S
1806                                                     (Nat.S (Nat.S (Nat.S
1807                                                     (Nat.S (Nat.S (Nat.S
1808                                                     (Nat.S (Nat.S (Nat.S
1809                                                     (Nat.S (Nat.S (Nat.S
1810                                                     (Nat.S (Nat.S (Nat.S
1811                                                     (Nat.S (Nat.S (Nat.S
1812                                                     (Nat.S (Nat.S (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
1817                                                     Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1818                                             | Bool.True ->
1819                                               Types.Some (Types.Inl
1820                                                 SFR_PCON)
1821                                             | Bool.False ->
1822                                               (match Nat.eqb address (Nat.S
1823                                                        (Nat.S (Nat.S (Nat.S
1824                                                        (Nat.S (Nat.S (Nat.S
1825                                                        (Nat.S (Nat.S (Nat.S
1826                                                        (Nat.S (Nat.S (Nat.S
1827                                                        (Nat.S (Nat.S (Nat.S
1828                                                        (Nat.S (Nat.S (Nat.S
1829                                                        (Nat.S (Nat.S (Nat.S
1830                                                        (Nat.S (Nat.S (Nat.S
1831                                                        (Nat.S (Nat.S (Nat.S
1832                                                        (Nat.S (Nat.S (Nat.S
1833                                                        (Nat.S (Nat.S (Nat.S
1834                                                        (Nat.S (Nat.S (Nat.S
1835                                                        (Nat.S (Nat.S (Nat.S
1836                                                        (Nat.S (Nat.S (Nat.S
1837                                                        (Nat.S (Nat.S (Nat.S
1838                                                        (Nat.S (Nat.S (Nat.S
1839                                                        (Nat.S (Nat.S (Nat.S
1840                                                        (Nat.S (Nat.S (Nat.S
1841                                                        (Nat.S (Nat.S (Nat.S
1842                                                        (Nat.S (Nat.S (Nat.S
1843                                                        (Nat.S (Nat.S (Nat.S
1844                                                        (Nat.S (Nat.S (Nat.S
1845                                                        (Nat.S (Nat.S (Nat.S
1846                                                        (Nat.S (Nat.S (Nat.S
1847                                                        (Nat.S (Nat.S (Nat.S
1848                                                        (Nat.S (Nat.S (Nat.S
1849                                                        (Nat.S (Nat.S (Nat.S
1850                                                        (Nat.S (Nat.S (Nat.S
1851                                                        (Nat.S (Nat.S (Nat.S
1852                                                        (Nat.S (Nat.S (Nat.S
1853                                                        (Nat.S (Nat.S (Nat.S
1854                                                        (Nat.S (Nat.S (Nat.S
1855                                                        (Nat.S (Nat.S (Nat.S
1856                                                        (Nat.S (Nat.S (Nat.S
1857                                                        (Nat.S (Nat.S (Nat.S
1858                                                        (Nat.S (Nat.S (Nat.S
1859                                                        (Nat.S (Nat.S (Nat.S
1860                                                        (Nat.S (Nat.S (Nat.S
1861                                                        (Nat.S (Nat.S (Nat.S
1862                                                        (Nat.S (Nat.S (Nat.S
1863                                                        (Nat.S (Nat.S (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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1869                                                | Bool.True ->
1870                                                  Types.Some (Types.Inl
1871                                                    SFR_TCON)
1872                                                | Bool.False ->
1873                                                  (match Nat.eqb address
1874                                                           (Nat.S (Nat.S
1875                                                           (Nat.S (Nat.S
1876                                                           (Nat.S (Nat.S
1877                                                           (Nat.S (Nat.S
1878                                                           (Nat.S (Nat.S
1879                                                           (Nat.S (Nat.S
1880                                                           (Nat.S (Nat.S
1881                                                           (Nat.S (Nat.S
1882                                                           (Nat.S (Nat.S
1883                                                           (Nat.S (Nat.S
1884                                                           (Nat.S (Nat.S
1885                                                           (Nat.S (Nat.S
1886                                                           (Nat.S (Nat.S
1887                                                           (Nat.S (Nat.S
1888                                                           (Nat.S (Nat.S
1889                                                           (Nat.S (Nat.S
1890                                                           (Nat.S (Nat.S
1891                                                           (Nat.S (Nat.S
1892                                                           (Nat.S (Nat.S
1893                                                           (Nat.S (Nat.S
1894                                                           (Nat.S (Nat.S
1895                                                           (Nat.S (Nat.S
1896                                                           (Nat.S (Nat.S
1897                                                           (Nat.S (Nat.S
1898                                                           (Nat.S (Nat.S
1899                                                           (Nat.S (Nat.S
1900                                                           (Nat.S (Nat.S
1901                                                           (Nat.S (Nat.S
1902                                                           (Nat.S (Nat.S
1903                                                           (Nat.S (Nat.S
1904                                                           (Nat.S (Nat.S
1905                                                           (Nat.S (Nat.S
1906                                                           (Nat.S (Nat.S
1907                                                           (Nat.S (Nat.S
1908                                                           (Nat.S (Nat.S
1909                                                           (Nat.S (Nat.S
1910                                                           (Nat.S (Nat.S
1911                                                           (Nat.S (Nat.S
1912                                                           (Nat.S (Nat.S
1913                                                           (Nat.S (Nat.S
1914                                                           (Nat.S (Nat.S
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
1943                                                           Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1944                                                   | Bool.True ->
1945                                                     Types.Some (Types.Inl
1946                                                       SFR_TMOD)
1947                                                   | Bool.False ->
1948                                                     (match Nat.eqb address
1949                                                              (Nat.S (Nat.S
1950                                                              (Nat.S (Nat.S
1951                                                              (Nat.S (Nat.S
1952                                                              (Nat.S (Nat.S
1953                                                              (Nat.S (Nat.S
1954                                                              (Nat.S (Nat.S
1955                                                              (Nat.S (Nat.S
1956                                                              (Nat.S (Nat.S
1957                                                              (Nat.S (Nat.S
1958                                                              (Nat.S (Nat.S
1959                                                              (Nat.S (Nat.S
1960                                                              (Nat.S (Nat.S
1961                                                              (Nat.S (Nat.S
1962                                                              (Nat.S (Nat.S
1963                                                              (Nat.S (Nat.S
1964                                                              (Nat.S (Nat.S
1965                                                              (Nat.S (Nat.S
1966                                                              (Nat.S (Nat.S
1967                                                              (Nat.S (Nat.S
1968                                                              (Nat.S (Nat.S
1969                                                              (Nat.S (Nat.S
1970                                                              (Nat.S (Nat.S
1971                                                              (Nat.S (Nat.S
1972                                                              (Nat.S (Nat.S
1973                                                              (Nat.S (Nat.S
1974                                                              (Nat.S (Nat.S
1975                                                              (Nat.S (Nat.S
1976                                                              (Nat.S (Nat.S
1977                                                              (Nat.S (Nat.S
1978                                                              (Nat.S (Nat.S
1979                                                              (Nat.S (Nat.S
1980                                                              (Nat.S (Nat.S
1981                                                              (Nat.S (Nat.S
1982                                                              (Nat.S (Nat.S
1983                                                              (Nat.S (Nat.S
1984                                                              (Nat.S (Nat.S
1985                                                              (Nat.S (Nat.S
1986                                                              (Nat.S (Nat.S
1987                                                              (Nat.S (Nat.S
1988                                                              (Nat.S (Nat.S
1989                                                              (Nat.S (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2026                                                      | Bool.True ->
2027                                                        Types.Some (Types.Inl
2028                                                          SFR_SCON)
2029                                                      | Bool.False ->
2030                                                        (match Nat.eqb
2031                                                                 address
2032                                                                 (Nat.S
2033                                                                 (Nat.S
2034                                                                 (Nat.S
2035                                                                 (Nat.S
2036                                                                 (Nat.S
2037                                                                 (Nat.S
2038                                                                 (Nat.S
2039                                                                 (Nat.S
2040                                                                 (Nat.S
2041                                                                 (Nat.S
2042                                                                 (Nat.S
2043                                                                 (Nat.S
2044                                                                 (Nat.S
2045                                                                 (Nat.S
2046                                                                 (Nat.S
2047                                                                 (Nat.S
2048                                                                 (Nat.S
2049                                                                 (Nat.S
2050                                                                 (Nat.S
2051                                                                 (Nat.S
2052                                                                 (Nat.S
2053                                                                 (Nat.S
2054                                                                 (Nat.S
2055                                                                 (Nat.S
2056                                                                 (Nat.S
2057                                                                 (Nat.S
2058                                                                 (Nat.S
2059                                                                 (Nat.S
2060                                                                 (Nat.S
2061                                                                 (Nat.S
2062                                                                 (Nat.S
2063                                                                 (Nat.S
2064                                                                 (Nat.S
2065                                                                 (Nat.S
2066                                                                 (Nat.S
2067                                                                 (Nat.S
2068                                                                 (Nat.S
2069                                                                 (Nat.S
2070                                                                 (Nat.S
2071                                                                 (Nat.S
2072                                                                 (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2201                                                         | Bool.True ->
2202                                                           Types.Some
2203                                                             (Types.Inl
2204                                                             SFR_IE)
2205                                                         | Bool.False ->
2206                                                           (match Nat.eqb
2207                                                                    address
2208                                                                    (Nat.S
2209                                                                    (Nat.S
2210                                                                    (Nat.S
2211                                                                    (Nat.S
2212                                                                    (Nat.S
2213                                                                    (Nat.S
2214                                                                    (Nat.S
2215                                                                    (Nat.S
2216                                                                    (Nat.S
2217                                                                    (Nat.S
2218                                                                    (Nat.S
2219                                                                    (Nat.S
2220                                                                    (Nat.S
2221                                                                    (Nat.S
2222                                                                    (Nat.S
2223                                                                    (Nat.S
2224                                                                    (Nat.S
2225                                                                    (Nat.S
2226                                                                    (Nat.S
2227                                                                    (Nat.S
2228                                                                    (Nat.S
2229                                                                    (Nat.S
2230                                                                    (Nat.S
2231                                                                    (Nat.S
2232                                                                    (Nat.S
2233                                                                    (Nat.S
2234                                                                    (Nat.S
2235                                                                    (Nat.S
2236                                                                    (Nat.S
2237                                                                    (Nat.S
2238                                                                    (Nat.S
2239                                                                    (Nat.S
2240                                                                    (Nat.S
2241                                                                    (Nat.S
2242                                                                    (Nat.S
2243                                                                    (Nat.S
2244                                                                    (Nat.S
2245                                                                    (Nat.S
2246                                                                    (Nat.S
2247                                                                    (Nat.S
2248                                                                    (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2393                                                            | Bool.True ->
2394                                                              Types.Some
2395                                                                (Types.Inl
2396                                                                SFR_IP)
2397                                                            | Bool.False ->
2398                                                              (match 
2399                                                               Nat.eqb
2400                                                                 address
2401                                                                 (Nat.S
2402                                                                 (Nat.S
2403                                                                 (Nat.S
2404                                                                 (Nat.S
2405                                                                 (Nat.S
2406                                                                 (Nat.S
2407                                                                 (Nat.S
2408                                                                 (Nat.S
2409                                                                 (Nat.S
2410                                                                 (Nat.S
2411                                                                 (Nat.S
2412                                                                 (Nat.S
2413                                                                 (Nat.S
2414                                                                 (Nat.S
2415                                                                 (Nat.S
2416                                                                 (Nat.S
2417                                                                 (Nat.S
2418                                                                 (Nat.S
2419                                                                 (Nat.S
2420                                                                 (Nat.S
2421                                                                 (Nat.S
2422                                                                 (Nat.S
2423                                                                 (Nat.S
2424                                                                 (Nat.S
2425                                                                 (Nat.S
2426                                                                 (Nat.S
2427                                                                 (Nat.S
2428                                                                 (Nat.S
2429                                                                 (Nat.S
2430                                                                 (Nat.S
2431                                                                 (Nat.S
2432                                                                 (Nat.S
2433                                                                 (Nat.S
2434                                                                 (Nat.S
2435                                                                 (Nat.S
2436                                                                 (Nat.S
2437                                                                 (Nat.S
2438                                                                 (Nat.S
2439                                                                 (Nat.S
2440                                                                 (Nat.S
2441                                                                 (Nat.S
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.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2531                                                               | Bool.True ->
2532                                                                 Types.Some
2533                                                                   (Types.Inl
2534                                                                   SFR_SP)
2535                                                               | Bool.False ->
2536                                                                 (match 
2537                                                                  Nat.eqb
2538                                                                    address
2539                                                                    (Nat.S
2540                                                                    (Nat.S
2541                                                                    (Nat.S
2542                                                                    (Nat.S
2543                                                                    (Nat.S
2544                                                                    (Nat.S
2545                                                                    (Nat.S
2546                                                                    (Nat.S
2547                                                                    (Nat.S
2548                                                                    (Nat.S
2549                                                                    (Nat.S
2550                                                                    (Nat.S
2551                                                                    (Nat.S
2552                                                                    (Nat.S
2553                                                                    (Nat.S
2554                                                                    (Nat.S
2555                                                                    (Nat.S
2556                                                                    (Nat.S
2557                                                                    (Nat.S
2558                                                                    (Nat.S
2559                                                                    (Nat.S
2560                                                                    (Nat.S
2561                                                                    (Nat.S
2562                                                                    (Nat.S
2563                                                                    (Nat.S
2564                                                                    (Nat.S
2565                                                                    (Nat.S
2566                                                                    (Nat.S
2567                                                                    (Nat.S
2568                                                                    (Nat.S
2569                                                                    (Nat.S
2570                                                                    (Nat.S
2571                                                                    (Nat.S
2572                                                                    (Nat.S
2573                                                                    (Nat.S
2574                                                                    (Nat.S
2575                                                                    (Nat.S
2576                                                                    (Nat.S
2577                                                                    (Nat.S
2578                                                                    (Nat.S
2579                                                                    (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2670                                                                  | Bool.True ->
2671                                                                    Types.Some
2672                                                                    (Types.Inl
2673                                                                    SFR_DPL)
2674                                                                  | Bool.False ->
2675                                                                    (match 
2676                                                                    Nat.eqb
2677                                                                    address
2678                                                                    (Nat.S
2679                                                                    (Nat.S
2680                                                                    (Nat.S
2681                                                                    (Nat.S
2682                                                                    (Nat.S
2683                                                                    (Nat.S
2684                                                                    (Nat.S
2685                                                                    (Nat.S
2686                                                                    (Nat.S
2687                                                                    (Nat.S
2688                                                                    (Nat.S
2689                                                                    (Nat.S
2690                                                                    (Nat.S
2691                                                                    (Nat.S
2692                                                                    (Nat.S
2693                                                                    (Nat.S
2694                                                                    (Nat.S
2695                                                                    (Nat.S
2696                                                                    (Nat.S
2697                                                                    (Nat.S
2698                                                                    (Nat.S
2699                                                                    (Nat.S
2700                                                                    (Nat.S
2701                                                                    (Nat.S
2702                                                                    (Nat.S
2703                                                                    (Nat.S
2704                                                                    (Nat.S
2705                                                                    (Nat.S
2706                                                                    (Nat.S
2707                                                                    (Nat.S
2708                                                                    (Nat.S
2709                                                                    (Nat.S
2710                                                                    (Nat.S
2711                                                                    (Nat.S
2712                                                                    (Nat.S
2713                                                                    (Nat.S
2714                                                                    (Nat.S
2715                                                                    (Nat.S
2716                                                                    (Nat.S
2717                                                                    (Nat.S
2718                                                                    (Nat.S
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.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2810                                                                    | Bool.True ->
2811                                                                    Types.Some
2812                                                                    (Types.Inl
2813                                                                    SFR_DPH)
2814                                                                    | Bool.False ->
2815                                                                    (match 
2816                                                                    Nat.eqb
2817                                                                    address
2818                                                                    (Nat.S
2819                                                                    (Nat.S
2820                                                                    (Nat.S
2821                                                                    (Nat.S
2822                                                                    (Nat.S
2823                                                                    (Nat.S
2824                                                                    (Nat.S
2825                                                                    (Nat.S
2826                                                                    (Nat.S
2827                                                                    (Nat.S
2828                                                                    (Nat.S
2829                                                                    (Nat.S
2830                                                                    (Nat.S
2831                                                                    (Nat.S
2832                                                                    (Nat.S
2833                                                                    (Nat.S
2834                                                                    (Nat.S
2835                                                                    (Nat.S
2836                                                                    (Nat.S
2837                                                                    (Nat.S
2838                                                                    (Nat.S
2839                                                                    (Nat.S
2840                                                                    (Nat.S
2841                                                                    (Nat.S
2842                                                                    (Nat.S
2843                                                                    (Nat.S
2844                                                                    (Nat.S
2845                                                                    (Nat.S
2846                                                                    (Nat.S
2847                                                                    (Nat.S
2848                                                                    (Nat.S
2849                                                                    (Nat.S
2850                                                                    (Nat.S
2851                                                                    (Nat.S
2852                                                                    (Nat.S
2853                                                                    (Nat.S
2854                                                                    (Nat.S
2855                                                                    (Nat.S
2856                                                                    (Nat.S
2857                                                                    (Nat.S
2858                                                                    (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3027                                                                    | Bool.True ->
3028                                                                    Types.Some
3029                                                                    (Types.Inl
3030                                                                    SFR_PSW)
3031                                                                    | Bool.False ->
3032                                                                    (match 
3033                                                                    Nat.eqb
3034                                                                    address
3035                                                                    (Nat.S
3036                                                                    (Nat.S
3037                                                                    (Nat.S
3038                                                                    (Nat.S
3039                                                                    (Nat.S
3040                                                                    (Nat.S
3041                                                                    (Nat.S
3042                                                                    (Nat.S
3043                                                                    (Nat.S
3044                                                                    (Nat.S
3045                                                                    (Nat.S
3046                                                                    (Nat.S
3047                                                                    (Nat.S
3048                                                                    (Nat.S
3049                                                                    (Nat.S
3050                                                                    (Nat.S
3051                                                                    (Nat.S
3052                                                                    (Nat.S
3053                                                                    (Nat.S
3054                                                                    (Nat.S
3055                                                                    (Nat.S
3056                                                                    (Nat.S
3057                                                                    (Nat.S
3058                                                                    (Nat.S
3059                                                                    (Nat.S
3060                                                                    (Nat.S
3061                                                                    (Nat.S
3062                                                                    (Nat.S
3063                                                                    (Nat.S
3064                                                                    (Nat.S
3065                                                                    (Nat.S
3066                                                                    (Nat.S
3067                                                                    (Nat.S
3068                                                                    (Nat.S
3069                                                                    (Nat.S
3070                                                                    (Nat.S
3071                                                                    (Nat.S
3072                                                                    (Nat.S
3073                                                                    (Nat.S
3074                                                                    (Nat.S
3075                                                                    (Nat.S
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.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3260                                                                    | Bool.True ->
3261                                                                    Types.Some
3262                                                                    (Types.Inl
3263                                                                    SFR_ACC_A)
3264                                                                    | Bool.False ->
3265                                                                    (match 
3266                                                                    Nat.eqb
3267                                                                    address
3268                                                                    (Nat.S
3269                                                                    (Nat.S
3270                                                                    (Nat.S
3271                                                                    (Nat.S
3272                                                                    (Nat.S
3273                                                                    (Nat.S
3274                                                                    (Nat.S
3275                                                                    (Nat.S
3276                                                                    (Nat.S
3277                                                                    (Nat.S
3278                                                                    (Nat.S
3279                                                                    (Nat.S
3280                                                                    (Nat.S
3281                                                                    (Nat.S
3282                                                                    (Nat.S
3283                                                                    (Nat.S
3284                                                                    (Nat.S
3285                                                                    (Nat.S
3286                                                                    (Nat.S
3287                                                                    (Nat.S
3288                                                                    (Nat.S
3289                                                                    (Nat.S
3290                                                                    (Nat.S
3291                                                                    (Nat.S
3292                                                                    (Nat.S
3293                                                                    (Nat.S
3294                                                                    (Nat.S
3295                                                                    (Nat.S
3296                                                                    (Nat.S
3297                                                                    (Nat.S
3298                                                                    (Nat.S
3299                                                                    (Nat.S
3300                                                                    (Nat.S
3301                                                                    (Nat.S
3302                                                                    (Nat.S
3303                                                                    (Nat.S
3304                                                                    (Nat.S
3305                                                                    (Nat.S
3306                                                                    (Nat.S
3307                                                                    (Nat.S
3308                                                                    (Nat.S
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                                                                    (Nat.S
3393                                                                    (Nat.S
3394                                                                    (Nat.S
3395                                                                    (Nat.S
3396                                                                    (Nat.S
3397                                                                    (Nat.S
3398                                                                    (Nat.S
3399                                                                    (Nat.S
3400                                                                    (Nat.S
3401                                                                    (Nat.S
3402                                                                    (Nat.S
3403                                                                    (Nat.S
3404                                                                    (Nat.S
3405                                                                    (Nat.S
3406                                                                    (Nat.S
3407                                                                    (Nat.S
3408                                                                    (Nat.S
3409                                                                    (Nat.S
3410                                                                    (Nat.S
3411                                                                    (Nat.S
3412                                                                    (Nat.S
3413                                                                    (Nat.S
3414                                                                    (Nat.S
3415                                                                    (Nat.S
3416                                                                    (Nat.S
3417                                                                    (Nat.S
3418                                                                    (Nat.S
3419                                                                    (Nat.S
3420                                                                    (Nat.S
3421                                                                    (Nat.S
3422                                                                    (Nat.S
3423                                                                    (Nat.S
3424                                                                    (Nat.S
3425                                                                    (Nat.S
3426                                                                    (Nat.S
3427                                                                    (Nat.S
3428                                                                    (Nat.S
3429                                                                    (Nat.S
3430                                                                    (Nat.S
3431                                                                    (Nat.S
3432                                                                    (Nat.S
3433                                                                    (Nat.S
3434                                                                    (Nat.S
3435                                                                    (Nat.S
3436                                                                    (Nat.S
3437                                                                    (Nat.S
3438                                                                    (Nat.S
3439                                                                    (Nat.S
3440                                                                    (Nat.S
3441                                                                    (Nat.S
3442                                                                    (Nat.S
3443                                                                    (Nat.S
3444                                                                    (Nat.S
3445                                                                    (Nat.S
3446                                                                    (Nat.S
3447                                                                    (Nat.S
3448                                                                    (Nat.S
3449                                                                    (Nat.S
3450                                                                    (Nat.S
3451                                                                    (Nat.S
3452                                                                    (Nat.S
3453                                                                    (Nat.S
3454                                                                    (Nat.S
3455                                                                    (Nat.S
3456                                                                    (Nat.S
3457                                                                    (Nat.S
3458                                                                    (Nat.S
3459                                                                    (Nat.S
3460                                                                    (Nat.S
3461                                                                    (Nat.S
3462                                                                    (Nat.S
3463                                                                    (Nat.S
3464                                                                    (Nat.S
3465                                                                    (Nat.S
3466                                                                    (Nat.S
3467                                                                    (Nat.S
3468                                                                    (Nat.S
3469                                                                    (Nat.S
3470                                                                    (Nat.S
3471                                                                    (Nat.S
3472                                                                    (Nat.S
3473                                                                    (Nat.S
3474                                                                    (Nat.S
3475                                                                    (Nat.S
3476                                                                    (Nat.S
3477                                                                    (Nat.S
3478                                                                    (Nat.S
3479                                                                    (Nat.S
3480                                                                    (Nat.S
3481                                                                    (Nat.S
3482                                                                    (Nat.S
3483