1	import Base
2	import bend-osdev-word64@0.1.1.0/word64.bend as W
3	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
4	import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
5	import bend-osdev-bytes@0.1.1.0/PROOF.bend as BP
6	import ./error.bend as E
7	import ./aml_pkglength.bend as K
8	import ./aml_name.bend as N
9	import ./header.bend as H
10	import ./checksum.bend as C
11	import ./fields.bend as F
12	import ./rsdp.bend as P
13	import ./registry.bend as R
14	import ./aml_value.bend as V
15	import ./aml_host.bend as Hs
16	import ./aml_interp.bend as I
17	import ./aml.bend as A
18	import ./aml_term.bend as T
19	import ./aml_device.bend as Dv
20	import ./mcfg.bend as Mc
21	import ./example.bend as X
22	import ./LAWS.bend as Laws
23	import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
24	import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
25	
26	# The proofs reach Octets only through bytes' interface laws (octets_to_of,
27	# octets_of_to, octets_append_list, octets_len_list, octets_split_at_append,
28	# octets_le32_round_trip) and its list layer (B.append, B.mask, B.byte),
29	# and W64 only through word64's public defs. The PkgLength proof and the
30	# field lengths compute through B.mask and B.le32 on words split into their
31	# bits, as bytes' own proofs do.
32	
33	# Contradictions
34	
35	def bdisc(+b: Bool) -> Type:
36	  match b:
37	    case True{}:
38	      Empty
39	    case False{}:
40	      Unit
41	
42	def ft_absurd(+e: {False{} == True{} : Bool}) -> Empty:
43	  %e : bdisc(_)
44	  Unit{}
45	
46	# PkgLength: with the value split into its 32 bits, and the bits above the
47	# highest one set taken one by one from the top, the encoder's choice of
48	# form and the decoder's reading compute; values of 2^28 and up are refused
49	# by the hypothesis
50	
51	def pk_abs(+v: U32, +r: List<&2, U32>, e: Empty) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), r))) == Done{K.AmlPkgLen{v, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}:
52	  Empty.absurd({K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), r))) == Done{K.AmlPkgLen{v, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}, e)
53	
54	# the bits from the top down, so that they are matched in binder order
55	def pk_bits(+b31: Bool, +b30: Bool, +b29: Bool, +b28: Bool, +b27: Bool, +b26: Bool, +b25: Bool, +b24: Bool, +b23: Bool, +b22: Bool, +b21: Bool, +b20: Bool, +b19: Bool, +b18: Bool, +b17: Bool, +b16: Bool, +b15: Bool, +b14: Bool, +b13: Bool, +b12: Bool, +b11: Bool, +b10: Bool, +b9: Bool, +b8: Bool, +b7: Bool, +b6: Bool, +b5: Bool, +b4: Bool, +b3: Bool, +b2: Bool, +b1: Bool, +b0: Bool, +r: List<&2, U32>, +fits: {K.AmlPkgLength.fits(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == True{} : Bool}) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})), r))) == Done{K.AmlPkgLen{U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}:
56	  match b31:
57	    case True{}:
58	      pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{True{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
59	    case False{}:
60	      match b30:
61	        case True{}:
62	          pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
63	        case False{}:
64	          match b29:
65	            case True{}:
66	              pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
67	            case False{}:
68	              match b28:
69	                case True{}:
70	                  pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
71	                case False{}:
72	                  match b27:
73	                    case True{}:
74	                      {==}
75	                    case False{}:
76	                      match b26:
77	                        case True{}:
78	                          {==}
79	                        case False{}:
80	                          match b25:
81	                            case True{}:
82	                              {==}
83	                            case False{}:
84	                              match b24:
85	                                case True{}:
86	                                  {==}
87	                                case False{}:
88	                                  match b23:
89	                                    case True{}:
90	                                      {==}
91	                                    case False{}:
92	                                      match b22:
93	                                        case True{}:
94	                                          {==}
95	                                        case False{}:
96	                                          match b21:
97	                                            case True{}:
98	                                              {==}
99	                                            case False{}:
100	                                              match b20:
101	                                                case True{}:
102	                                                  {==}
103	                                                case False{}:
104	                                                  match b19:
105	                                                    case True{}:
106	                                                      {==}
107	                                                    case False{}:
108	                                                      match b18:
109	                                                        case True{}:
110	                                                          {==}
111	                                                        case False{}:
112	                                                          match b17:
113	                                                            case True{}:
114	                                                              {==}
115	                                                            case False{}:
116	                                                              match b16:
117	                                                                case True{}:
118	                                                                  {==}
119	                                                                case False{}:
120	                                                                  match b15:
121	                                                                    case True{}:
122	                                                                      {==}
123	                                                                    case False{}:
124	                                                                      match b14:
125	                                                                        case True{}:
126	                                                                          {==}
127	                                                                        case False{}:
128	                                                                          match b13:
129	                                                                            case True{}:
130	                                                                              {==}
131	                                                                            case False{}:
132	                                                                              match b12:
133	                                                                                case True{}:
134	                                                                                  {==}
135	                                                                                case False{}:
136	                                                                                  match b11:
137	                                                                                    case True{}:
138	                                                                                      {==}
139	                                                                                    case False{}:
140	                                                                                      match b10:
141	                                                                                        case True{}:
142	                                                                                          {==}
143	                                                                                        case False{}:
144	                                                                                          match b9:
145	                                                                                            case True{}:
146	                                                                                              {==}
147	                                                                                            case False{}:
148	                                                                                              match b8:
149	                                                                                                case True{}:
150	                                                                                                  {==}
151	                                                                                                case False{}:
152	                                                                                                  match b7:
153	                                                                                                    case True{}:
154	                                                                                                      {==}
155	                                                                                                    case False{}:
156	                                                                                                      match b6:
157	                                                                                                        case True{}:
158	                                                                                                          {==}
159	                                                                                                        case False{}:
160	                                                                                                          {==}
161	
162	def pk_rt(+v: U32, +r: List<&2, U32>, +fits: {K.AmlPkgLength.fits(v) == True{} : Bool}) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), r))) == Done{K.AmlPkgLen{v, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}:
163	  match v:
164	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
165	      pk_bits(b31, b30, b29, b28, b27, b26, b25, b24, b23, b22, b21, b20, b19, b18, b17, b16, b15, b14, b13, b12, b11, b10, b9, b8, b7, b6, b5, b4, b3, b2, b1, b0, r, fits)
166	
167	# The SegCount of a MultiNamePath: a count below 256 survives being written
168	# as a byte, by a chain of lemmas cnt.d (for k + d, d from 0 to 256), each a
169	# closed computation or a step to the next
170	
171	def cnt_abs(+k: Nat, e: Empty) -> {U32.to_nat(B.byte(U32.from_nat(k))) == k : Nat}:
172	  Empty.absurd({U32.to_nat(B.byte(U32.from_nat(k))) == k : Nat}, e)
173	
174	def cnt.d256(+k: Nat, +lt: {Nat.is_lt(Nat.add(256n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(256n, k)))) == Nat.add(256n, k) : Nat}:
175	  match k:
176	    case 0n:
177	      cnt_abs(Nat.add(256n, 0n), ft_absurd(lt))
178	    case 1n+p:
179	      cnt_abs(Nat.add(256n, 1n+p), ft_absurd(lt))
180	
181	def cnt.d255(+k: Nat, +lt: {Nat.is_lt(Nat.add(255n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(255n, k)))) == Nat.add(255n, k) : Nat}:
182	  match k:
183	    case 0n:
184	      {==}
185	    case 1n+p:
186	      cnt.d256(p, lt)
187	
188	def cnt.d254(+k: Nat, +lt: {Nat.is_lt(Nat.add(254n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(254n, k)))) == Nat.add(254n, k) : Nat}:
189	  match k:
190	    case 0n:
191	      {==}
192	    case 1n+p:
193	      cnt.d255(p, lt)
194	
195	def cnt.d253(+k: Nat, +lt: {Nat.is_lt(Nat.add(253n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(253n, k)))) == Nat.add(253n, k) : Nat}:
196	  match k:
197	    case 0n:
198	      {==}
199	    case 1n+p:
200	      cnt.d254(p, lt)
201	
202	def cnt.d252(+k: Nat, +lt: {Nat.is_lt(Nat.add(252n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(252n, k)))) == Nat.add(252n, k) : Nat}:
203	  match k:
204	    case 0n:
205	      {==}
206	    case 1n+p:
207	      cnt.d253(p, lt)
208	
209	def cnt.d251(+k: Nat, +lt: {Nat.is_lt(Nat.add(251n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(251n, k)))) == Nat.add(251n, k) : Nat}:
210	  match k:
211	    case 0n:
212	      {==}
213	    case 1n+p:
214	      cnt.d252(p, lt)
215	
216	def cnt.d250(+k: Nat, +lt: {Nat.is_lt(Nat.add(250n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(250n, k)))) == Nat.add(250n, k) : Nat}:
217	  match k:
218	    case 0n:
219	      {==}
220	    case 1n+p:
221	      cnt.d251(p, lt)
222	
223	def cnt.d249(+k: Nat, +lt: {Nat.is_lt(Nat.add(249n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(249n, k)))) == Nat.add(249n, k) : Nat}:
224	  match k:
225	    case 0n:
226	      {==}
227	    case 1n+p:
228	      cnt.d250(p, lt)
229	
230	def cnt.d248(+k: Nat, +lt: {Nat.is_lt(Nat.add(248n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(248n, k)))) == Nat.add(248n, k) : Nat}:
231	  match k:
232	    case 0n:
233	      {==}
234	    case 1n+p:
235	      cnt.d249(p, lt)
236	
237	def cnt.d247(+k: Nat, +lt: {Nat.is_lt(Nat.add(247n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(247n, k)))) == Nat.add(247n, k) : Nat}:
238	  match k:
239	    case 0n:
240	      {==}
241	    case 1n+p:
242	      cnt.d248(p, lt)
243	
244	def cnt.d246(+k: Nat, +lt: {Nat.is_lt(Nat.add(246n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(246n, k)))) == Nat.add(246n, k) : Nat}:
245	  match k:
246	    case 0n:
247	      {==}
248	    case 1n+p:
249	      cnt.d247(p, lt)
250	
251	def cnt.d245(+k: Nat, +lt: {Nat.is_lt(Nat.add(245n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(245n, k)))) == Nat.add(245n, k) : Nat}:
252	  match k:
253	    case 0n:
254	      {==}
255	    case 1n+p:
256	      cnt.d246(p, lt)
257	
258	def cnt.d244(+k: Nat, +lt: {Nat.is_lt(Nat.add(244n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(244n, k)))) == Nat.add(244n, k) : Nat}:
259	  match k:
260	    case 0n:
261	      {==}
262	    case 1n+p:
263	      cnt.d245(p, lt)
264	
265	def cnt.d243(+k: Nat, +lt: {Nat.is_lt(Nat.add(243n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(243n, k)))) == Nat.add(243n, k) : Nat}:
266	  match k:
267	    case 0n:
268	      {==}
269	    case 1n+p:
270	      cnt.d244(p, lt)
271	
272	def cnt.d242(+k: Nat, +lt: {Nat.is_lt(Nat.add(242n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(242n, k)))) == Nat.add(242n, k) : Nat}:
273	  match k:
274	    case 0n:
275	      {==}
276	    case 1n+p:
277	      cnt.d243(p, lt)
278	
279	def cnt.d241(+k: Nat, +lt: {Nat.is_lt(Nat.add(241n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(241n, k)))) == Nat.add(241n, k) : Nat}:
280	  match k:
281	    case 0n:
282	      {==}
283	    case 1n+p:
284	      cnt.d242(p, lt)
285	
286	def cnt.d240(+k: Nat, +lt: {Nat.is_lt(Nat.add(240n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(240n, k)))) == Nat.add(240n, k) : Nat}:
287	  match k:
288	    case 0n:
289	      {==}
290	    case 1n+p:
291	      cnt.d241(p, lt)
292	
293	def cnt.d239(+k: Nat, +lt: {Nat.is_lt(Nat.add(239n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(239n, k)))) == Nat.add(239n, k) : Nat}:
294	  match k:
295	    case 0n:
296	      {==}
297	    case 1n+p:
298	      cnt.d240(p, lt)
299	
300	def cnt.d238(+k: Nat, +lt: {Nat.is_lt(Nat.add(238n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(238n, k)))) == Nat.add(238n, k) : Nat}:
301	  match k:
302	    case 0n:
303	      {==}
304	    case 1n+p:
305	      cnt.d239(p, lt)
306	
307	def cnt.d237(+k: Nat, +lt: {Nat.is_lt(Nat.add(237n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(237n, k)))) == Nat.add(237n, k) : Nat}:
308	  match k:
309	    case 0n:
310	      {==}
311	    case 1n+p:
312	      cnt.d238(p, lt)
313	
314	def cnt.d236(+k: Nat, +lt: {Nat.is_lt(Nat.add(236n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(236n, k)))) == Nat.add(236n, k) : Nat}:
315	  match k:
316	    case 0n:
317	      {==}
318	    case 1n+p:
319	      cnt.d237(p, lt)
320	
321	def cnt.d235(+k: Nat, +lt: {Nat.is_lt(Nat.add(235n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(235n, k)))) == Nat.add(235n, k) : Nat}:
322	  match k:
323	    case 0n:
324	      {==}
325	    case 1n+p:
326	      cnt.d236(p, lt)
327	
328	def cnt.d234(+k: Nat, +lt: {Nat.is_lt(Nat.add(234n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(234n, k)))) == Nat.add(234n, k) : Nat}:
329	  match k:
330	    case 0n:
331	      {==}
332	    case 1n+p:
333	      cnt.d235(p, lt)
334	
335	def cnt.d233(+k: Nat, +lt: {Nat.is_lt(Nat.add(233n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(233n, k)))) == Nat.add(233n, k) : Nat}:
336	  match k:
337	    case 0n:
338	      {==}
339	    case 1n+p:
340	      cnt.d234(p, lt)
341	
342	def cnt.d232(+k: Nat, +lt: {Nat.is_lt(Nat.add(232n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(232n, k)))) == Nat.add(232n, k) : Nat}:
343	  match k:
344	    case 0n:
345	      {==}
346	    case 1n+p:
347	      cnt.d233(p, lt)
348	
349	def cnt.d231(+k: Nat, +lt: {Nat.is_lt(Nat.add(231n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(231n, k)))) == Nat.add(231n, k) : Nat}:
350	  match k:
351	    case 0n:
352	      {==}
353	    case 1n+p:
354	      cnt.d232(p, lt)
355	
356	def cnt.d230(+k: Nat, +lt: {Nat.is_lt(Nat.add(230n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(230n, k)))) == Nat.add(230n, k) : Nat}:
357	  match k:
358	    case 0n:
359	      {==}
360	    case 1n+p:
361	      cnt.d231(p, lt)
362	
363	def cnt.d229(+k: Nat, +lt: {Nat.is_lt(Nat.add(229n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(229n, k)))) == Nat.add(229n, k) : Nat}:
364	  match k:
365	    case 0n:
366	      {==}
367	    case 1n+p:
368	      cnt.d230(p, lt)
369	
370	def cnt.d228(+k: Nat, +lt: {Nat.is_lt(Nat.add(228n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(228n, k)))) == Nat.add(228n, k) : Nat}:
371	  match k:
372	    case 0n:
373	      {==}
374	    case 1n+p:
375	      cnt.d229(p, lt)
376	
377	def cnt.d227(+k: Nat, +lt: {Nat.is_lt(Nat.add(227n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(227n, k)))) == Nat.add(227n, k) : Nat}:
378	  match k:
379	    case 0n:
380	      {==}
381	    case 1n+p:
382	      cnt.d228(p, lt)
383	
384	def cnt.d226(+k: Nat, +lt: {Nat.is_lt(Nat.add(226n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(226n, k)))) == Nat.add(226n, k) : Nat}:
385	  match k:
386	    case 0n:
387	      {==}
388	    case 1n+p:
389	      cnt.d227(p, lt)
390	
391	def cnt.d225(+k: Nat, +lt: {Nat.is_lt(Nat.add(225n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(225n, k)))) == Nat.add(225n, k) : Nat}:
392	  match k:
393	    case 0n:
394	      {==}
395	    case 1n+p:
396	      cnt.d226(p, lt)
397	
398	def cnt.d224(+k: Nat, +lt: {Nat.is_lt(Nat.add(224n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(224n, k)))) == Nat.add(224n, k) : Nat}:
399	  match k:
400	    case 0n:
401	      {==}
402	    case 1n+p:
403	      cnt.d225(p, lt)
404	
405	def cnt.d223(+k: Nat, +lt: {Nat.is_lt(Nat.add(223n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(223n, k)))) == Nat.add(223n, k) : Nat}:
406	  match k:
407	    case 0n:
408	      {==}
409	    case 1n+p:
410	      cnt.d224(p, lt)
411	
412	def cnt.d222(+k: Nat, +lt: {Nat.is_lt(Nat.add(222n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(222n, k)))) == Nat.add(222n, k) : Nat}:
413	  match k:
414	    case 0n:
415	      {==}
416	    case 1n+p:
417	      cnt.d223(p, lt)
418	
419	def cnt.d221(+k: Nat, +lt: {Nat.is_lt(Nat.add(221n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(221n, k)))) == Nat.add(221n, k) : Nat}:
420	  match k:
421	    case 0n:
422	      {==}
423	    case 1n+p:
424	      cnt.d222(p, lt)
425	
426	def cnt.d220(+k: Nat, +lt: {Nat.is_lt(Nat.add(220n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(220n, k)))) == Nat.add(220n, k) : Nat}:
427	  match k:
428	    case 0n:
429	      {==}
430	    case 1n+p:
431	      cnt.d221(p, lt)
432	
433	def cnt.d219(+k: Nat, +lt: {Nat.is_lt(Nat.add(219n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(219n, k)))) == Nat.add(219n, k) : Nat}:
434	  match k:
435	    case 0n:
436	      {==}
437	    case 1n+p:
438	      cnt.d220(p, lt)
439	
440	def cnt.d218(+k: Nat, +lt: {Nat.is_lt(Nat.add(218n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(218n, k)))) == Nat.add(218n, k) : Nat}:
441	  match k:
442	    case 0n:
443	      {==}
444	    case 1n+p:
445	      cnt.d219(p, lt)
446	
447	def cnt.d217(+k: Nat, +lt: {Nat.is_lt(Nat.add(217n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(217n, k)))) == Nat.add(217n, k) : Nat}:
448	  match k:
449	    case 0n:
450	      {==}
451	    case 1n+p:
452	      cnt.d218(p, lt)
453	
454	def cnt.d216(+k: Nat, +lt: {Nat.is_lt(Nat.add(216n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(216n, k)))) == Nat.add(216n, k) : Nat}:
455	  match k:
456	    case 0n:
457	      {==}
458	    case 1n+p:
459	      cnt.d217(p, lt)
460	
461	def cnt.d215(+k: Nat, +lt: {Nat.is_lt(Nat.add(215n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(215n, k)))) == Nat.add(215n, k) : Nat}:
462	  match k:
463	    case 0n:
464	      {==}
465	    case 1n+p:
466	      cnt.d216(p, lt)
467	
468	def cnt.d214(+k: Nat, +lt: {Nat.is_lt(Nat.add(214n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(214n, k)))) == Nat.add(214n, k) : Nat}:
469	  match k:
470	    case 0n:
471	      {==}
472	    case 1n+p:
473	      cnt.d215(p, lt)
474	
475	def cnt.d213(+k: Nat, +lt: {Nat.is_lt(Nat.add(213n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(213n, k)))) == Nat.add(213n, k) : Nat}:
476	  match k:
477	    case 0n:
478	      {==}
479	    case 1n+p:
480	      cnt.d214(p, lt)
481	
482	def cnt.d212(+k: Nat, +lt: {Nat.is_lt(Nat.add(212n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(212n, k)))) == Nat.add(212n, k) : Nat}:
483	  match k:
484	    case 0n:
485	      {==}
486	    case 1n+p:
487	      cnt.d213(p, lt)
488	
489	def cnt.d211(+k: Nat, +lt: {Nat.is_lt(Nat.add(211n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(211n, k)))) == Nat.add(211n, k) : Nat}:
490	  match k:
491	    case 0n:
492	      {==}
493	    case 1n+p:
494	      cnt.d212(p, lt)
495	
496	def cnt.d210(+k: Nat, +lt: {Nat.is_lt(Nat.add(210n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(210n, k)))) == Nat.add(210n, k) : Nat}:
497	  match k:
498	    case 0n:
499	      {==}
500	    case 1n+p:
501	      cnt.d211(p, lt)
502	
503	def cnt.d209(+k: Nat, +lt: {Nat.is_lt(Nat.add(209n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(209n, k)))) == Nat.add(209n, k) : Nat}:
504	  match k:
505	    case 0n:
506	      {==}
507	    case 1n+p:
508	      cnt.d210(p, lt)
509	
510	def cnt.d208(+k: Nat, +lt: {Nat.is_lt(Nat.add(208n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(208n, k)))) == Nat.add(208n, k) : Nat}:
511	  match k:
512	    case 0n:
513	      {==}
514	    case 1n+p:
515	      cnt.d209(p, lt)
516	
517	def cnt.d207(+k: Nat, +lt: {Nat.is_lt(Nat.add(207n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(207n, k)))) == Nat.add(207n, k) : Nat}:
518	  match k:
519	    case 0n:
520	      {==}
521	    case 1n+p:
522	      cnt.d208(p, lt)
523	
524	def cnt.d206(+k: Nat, +lt: {Nat.is_lt(Nat.add(206n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(206n, k)))) == Nat.add(206n, k) : Nat}:
525	  match k:
526	    case 0n:
527	      {==}
528	    case 1n+p:
529	      cnt.d207(p, lt)
530	
531	def cnt.d205(+k: Nat, +lt: {Nat.is_lt(Nat.add(205n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(205n, k)))) == Nat.add(205n, k) : Nat}:
532	  match k:
533	    case 0n:
534	      {==}
535	    case 1n+p:
536	      cnt.d206(p, lt)
537	
538	def cnt.d204(+k: Nat, +lt: {Nat.is_lt(Nat.add(204n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(204n, k)))) == Nat.add(204n, k) : Nat}:
539	  match k:
540	    case 0n:
541	      {==}
542	    case 1n+p:
543	      cnt.d205(p, lt)
544	
545	def cnt.d203(+k: Nat, +lt: {Nat.is_lt(Nat.add(203n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(203n, k)))) == Nat.add(203n, k) : Nat}:
546	  match k:
547	    case 0n:
548	      {==}
549	    case 1n+p:
550	      cnt.d204(p, lt)
551	
552	def cnt.d202(+k: Nat, +lt: {Nat.is_lt(Nat.add(202n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(202n, k)))) == Nat.add(202n, k) : Nat}:
553	  match k:
554	    case 0n:
555	      {==}
556	    case 1n+p:
557	      cnt.d203(p, lt)
558	
559	def cnt.d201(+k: Nat, +lt: {Nat.is_lt(Nat.add(201n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(201n, k)))) == Nat.add(201n, k) : Nat}:
560	  match k:
561	    case 0n:
562	      {==}
563	    case 1n+p:
564	      cnt.d202(p, lt)
565	
566	def cnt.d200(+k: Nat, +lt: {Nat.is_lt(Nat.add(200n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(200n, k)))) == Nat.add(200n, k) : Nat}:
567	  match k:
568	    case 0n:
569	      {==}
570	    case 1n+p:
571	      cnt.d201(p, lt)
572	
573	def cnt.d199(+k: Nat, +lt: {Nat.is_lt(Nat.add(199n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(199n, k)))) == Nat.add(199n, k) : Nat}:
574	  match k:
575	    case 0n:
576	      {==}
577	    case 1n+p:
578	      cnt.d200(p, lt)
579	
580	def cnt.d198(+k: Nat, +lt: {Nat.is_lt(Nat.add(198n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(198n, k)))) == Nat.add(198n, k) : Nat}:
581	  match k:
582	    case 0n:
583	      {==}
584	    case 1n+p:
585	      cnt.d199(p, lt)
586	
587	def cnt.d197(+k: Nat, +lt: {Nat.is_lt(Nat.add(197n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(197n, k)))) == Nat.add(197n, k) : Nat}:
588	  match k:
589	    case 0n:
590	      {==}
591	    case 1n+p:
592	      cnt.d198(p, lt)
593	
594	def cnt.d196(+k: Nat, +lt: {Nat.is_lt(Nat.add(196n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(196n, k)))) == Nat.add(196n, k) : Nat}:
595	  match k:
596	    case 0n:
597	      {==}
598	    case 1n+p:
599	      cnt.d197(p, lt)
600	
601	def cnt.d195(+k: Nat, +lt: {Nat.is_lt(Nat.add(195n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(195n, k)))) == Nat.add(195n, k) : Nat}:
602	  match k:
603	    case 0n:
604	      {==}
605	    case 1n+p:
606	      cnt.d196(p, lt)
607	
608	def cnt.d194(+k: Nat, +lt: {Nat.is_lt(Nat.add(194n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(194n, k)))) == Nat.add(194n, k) : Nat}:
609	  match k:
610	    case 0n:
611	      {==}
612	    case 1n+p:
613	      cnt.d195(p, lt)
614	
615	def cnt.d193(+k: Nat, +lt: {Nat.is_lt(Nat.add(193n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(193n, k)))) == Nat.add(193n, k) : Nat}:
616	  match k:
617	    case 0n:
618	      {==}
619	    case 1n+p:
620	      cnt.d194(p, lt)
621	
622	def cnt.d192(+k: Nat, +lt: {Nat.is_lt(Nat.add(192n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(192n, k)))) == Nat.add(192n, k) : Nat}:
623	  match k:
624	    case 0n:
625	      {==}
626	    case 1n+p:
627	      cnt.d193(p, lt)
628	
629	def cnt.d191(+k: Nat, +lt: {Nat.is_lt(Nat.add(191n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(191n, k)))) == Nat.add(191n, k) : Nat}:
630	  match k:
631	    case 0n:
632	      {==}
633	    case 1n+p:
634	      cnt.d192(p, lt)
635	
636	def cnt.d190(+k: Nat, +lt: {Nat.is_lt(Nat.add(190n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(190n, k)))) == Nat.add(190n, k) : Nat}:
637	  match k:
638	    case 0n:
639	      {==}
640	    case 1n+p:
641	      cnt.d191(p, lt)
642	
643	def cnt.d189(+k: Nat, +lt: {Nat.is_lt(Nat.add(189n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(189n, k)))) == Nat.add(189n, k) : Nat}:
644	  match k:
645	    case 0n:
646	      {==}
647	    case 1n+p:
648	      cnt.d190(p, lt)
649	
650	def cnt.d188(+k: Nat, +lt: {Nat.is_lt(Nat.add(188n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(188n, k)))) == Nat.add(188n, k) : Nat}:
651	  match k:
652	    case 0n:
653	      {==}
654	    case 1n+p:
655	      cnt.d189(p, lt)
656	
657	def cnt.d187(+k: Nat, +lt: {Nat.is_lt(Nat.add(187n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(187n, k)))) == Nat.add(187n, k) : Nat}:
658	  match k:
659	    case 0n:
660	      {==}
661	    case 1n+p:
662	      cnt.d188(p, lt)
663	
664	def cnt.d186(+k: Nat, +lt: {Nat.is_lt(Nat.add(186n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(186n, k)))) == Nat.add(186n, k) : Nat}:
665	  match k:
666	    case 0n:
667	      {==}
668	    case 1n+p:
669	      cnt.d187(p, lt)
670	
671	def cnt.d185(+k: Nat, +lt: {Nat.is_lt(Nat.add(185n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(185n, k)))) == Nat.add(185n, k) : Nat}:
672	  match k:
673	    case 0n:
674	      {==}
675	    case 1n+p:
676	      cnt.d186(p, lt)
677	
678	def cnt.d184(+k: Nat, +lt: {Nat.is_lt(Nat.add(184n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(184n, k)))) == Nat.add(184n, k) : Nat}:
679	  match k:
680	    case 0n:
681	      {==}
682	    case 1n+p:
683	      cnt.d185(p, lt)
684	
685	def cnt.d183(+k: Nat, +lt: {Nat.is_lt(Nat.add(183n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(183n, k)))) == Nat.add(183n, k) : Nat}:
686	  match k:
687	    case 0n:
688	      {==}
689	    case 1n+p:
690	      cnt.d184(p, lt)
691	
692	def cnt.d182(+k: Nat, +lt: {Nat.is_lt(Nat.add(182n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(182n, k)))) == Nat.add(182n, k) : Nat}:
693	  match k:
694	    case 0n:
695	      {==}
696	    case 1n+p:
697	      cnt.d183(p, lt)
698	
699	def cnt.d181(+k: Nat, +lt: {Nat.is_lt(Nat.add(181n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(181n, k)))) == Nat.add(181n, k) : Nat}:
700	  match k:
701	    case 0n:
702	      {==}
703	    case 1n+p:
704	      cnt.d182(p, lt)
705	
706	def cnt.d180(+k: Nat, +lt: {Nat.is_lt(Nat.add(180n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(180n, k)))) == Nat.add(180n, k) : Nat}:
707	  match k:
708	    case 0n:
709	      {==}
710	    case 1n+p:
711	      cnt.d181(p, lt)
712	
713	def cnt.d179(+k: Nat, +lt: {Nat.is_lt(Nat.add(179n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(179n, k)))) == Nat.add(179n, k) : Nat}:
714	  match k:
715	    case 0n:
716	      {==}
717	    case 1n+p:
718	      cnt.d180(p, lt)
719	
720	def cnt.d178(+k: Nat, +lt: {Nat.is_lt(Nat.add(178n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(178n, k)))) == Nat.add(178n, k) : Nat}:
721	  match k:
722	    case 0n:
723	      {==}
724	    case 1n+p:
725	      cnt.d179(p, lt)
726	
727	def cnt.d177(+k: Nat, +lt: {Nat.is_lt(Nat.add(177n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(177n, k)))) == Nat.add(177n, k) : Nat}:
728	  match k:
729	    case 0n:
730	      {==}
731	    case 1n+p:
732	      cnt.d178(p, lt)
733	
734	def cnt.d176(+k: Nat, +lt: {Nat.is_lt(Nat.add(176n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(176n, k)))) == Nat.add(176n, k) : Nat}:
735	  match k:
736	    case 0n:
737	      {==}
738	    case 1n+p:
739	      cnt.d177(p, lt)
740	
741	def cnt.d175(+k: Nat, +lt: {Nat.is_lt(Nat.add(175n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(175n, k)))) == Nat.add(175n, k) : Nat}:
742	  match k:
743	    case 0n:
744	      {==}
745	    case 1n+p:
746	      cnt.d176(p, lt)
747	
748	def cnt.d174(+k: Nat, +lt: {Nat.is_lt(Nat.add(174n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(174n, k)))) == Nat.add(174n, k) : Nat}:
749	  match k:
750	    case 0n:
751	      {==}
752	    case 1n+p:
753	      cnt.d175(p, lt)
754	
755	def cnt.d173(+k: Nat, +lt: {Nat.is_lt(Nat.add(173n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(173n, k)))) == Nat.add(173n, k) : Nat}:
756	  match k:
757	    case 0n:
758	      {==}
759	    case 1n+p:
760	      cnt.d174(p, lt)
761	
762	def cnt.d172(+k: Nat, +lt: {Nat.is_lt(Nat.add(172n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(172n, k)))) == Nat.add(172n, k) : Nat}:
763	  match k:
764	    case 0n:
765	      {==}
766	    case 1n+p:
767	      cnt.d173(p, lt)
768	
769	def cnt.d171(+k: Nat, +lt: {Nat.is_lt(Nat.add(171n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(171n, k)))) == Nat.add(171n, k) : Nat}:
770	  match k:
771	    case 0n:
772	      {==}
773	    case 1n+p:
774	      cnt.d172(p, lt)
775	
776	def cnt.d170(+k: Nat, +lt: {Nat.is_lt(Nat.add(170n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(170n, k)))) == Nat.add(170n, k) : Nat}:
777	  match k:
778	    case 0n:
779	      {==}
780	    case 1n+p:
781	      cnt.d171(p, lt)
782	
783	def cnt.d169(+k: Nat, +lt: {Nat.is_lt(Nat.add(169n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(169n, k)))) == Nat.add(169n, k) : Nat}:
784	  match k:
785	    case 0n:
786	      {==}
787	    case 1n+p:
788	      cnt.d170(p, lt)
789	
790	def cnt.d168(+k: Nat, +lt: {Nat.is_lt(Nat.add(168n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(168n, k)))) == Nat.add(168n, k) : Nat}:
791	  match k:
792	    case 0n:
793	      {==}
794	    case 1n+p:
795	      cnt.d169(p, lt)
796	
797	def cnt.d167(+k: Nat, +lt: {Nat.is_lt(Nat.add(167n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(167n, k)))) == Nat.add(167n, k) : Nat}:
798	  match k:
799	    case 0n:
800	      {==}
801	    case 1n+p:
802	      cnt.d168(p, lt)
803	
804	def cnt.d166(+k: Nat, +lt: {Nat.is_lt(Nat.add(166n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(166n, k)))) == Nat.add(166n, k) : Nat}:
805	  match k:
806	    case 0n:
807	      {==}
808	    case 1n+p:
809	      cnt.d167(p, lt)
810	
811	def cnt.d165(+k: Nat, +lt: {Nat.is_lt(Nat.add(165n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(165n, k)))) == Nat.add(165n, k) : Nat}:
812	  match k:
813	    case 0n:
814	      {==}
815	    case 1n+p:
816	      cnt.d166(p, lt)
817	
818	def cnt.d164(+k: Nat, +lt: {Nat.is_lt(Nat.add(164n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(164n, k)))) == Nat.add(164n, k) : Nat}:
819	  match k:
820	    case 0n:
821	      {==}
822	    case 1n+p:
823	      cnt.d165(p, lt)
824	
825	def cnt.d163(+k: Nat, +lt: {Nat.is_lt(Nat.add(163n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(163n, k)))) == Nat.add(163n, k) : Nat}:
826	  match k:
827	    case 0n:
828	      {==}
829	    case 1n+p:
830	      cnt.d164(p, lt)
831	
832	def cnt.d162(+k: Nat, +lt: {Nat.is_lt(Nat.add(162n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(162n, k)))) == Nat.add(162n, k) : Nat}:
833	  match k:
834	    case 0n:
835	      {==}
836	    case 1n+p:
837	      cnt.d163(p, lt)
838	
839	def cnt.d161(+k: Nat, +lt: {Nat.is_lt(Nat.add(161n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(161n, k)))) == Nat.add(161n, k) : Nat}:
840	  match k:
841	    case 0n:
842	      {==}
843	    case 1n+p:
844	      cnt.d162(p, lt)
845	
846	def cnt.d160(+k: Nat, +lt: {Nat.is_lt(Nat.add(160n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(160n, k)))) == Nat.add(160n, k) : Nat}:
847	  match k:
848	    case 0n:
849	      {==}
850	    case 1n+p:
851	      cnt.d161(p, lt)
852	
853	def cnt.d159(+k: Nat, +lt: {Nat.is_lt(Nat.add(159n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(159n, k)))) == Nat.add(159n, k) : Nat}:
854	  match k:
855	    case 0n:
856	      {==}
857	    case 1n+p:
858	      cnt.d160(p, lt)
859	
860	def cnt.d158(+k: Nat, +lt: {Nat.is_lt(Nat.add(158n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(158n, k)))) == Nat.add(158n, k) : Nat}:
861	  match k:
862	    case 0n:
863	      {==}
864	    case 1n+p:
865	      cnt.d159(p, lt)
866	
867	def cnt.d157(+k: Nat, +lt: {Nat.is_lt(Nat.add(157n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(157n, k)))) == Nat.add(157n, k) : Nat}:
868	  match k:
869	    case 0n:
870	      {==}
871	    case 1n+p:
872	      cnt.d158(p, lt)
873	
874	def cnt.d156(+k: Nat, +lt: {Nat.is_lt(Nat.add(156n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(156n, k)))) == Nat.add(156n, k) : Nat}:
875	  match k:
876	    case 0n:
877	      {==}
878	    case 1n+p:
879	      cnt.d157(p, lt)
880	
881	def cnt.d155(+k: Nat, +lt: {Nat.is_lt(Nat.add(155n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(155n, k)))) == Nat.add(155n, k) : Nat}:
882	  match k:
883	    case 0n:
884	      {==}
885	    case 1n+p:
886	      cnt.d156(p, lt)
887	
888	def cnt.d154(+k: Nat, +lt: {Nat.is_lt(Nat.add(154n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(154n, k)))) == Nat.add(154n, k) : Nat}:
889	  match k:
890	    case 0n:
891	      {==}
892	    case 1n+p:
893	      cnt.d155(p, lt)
894	
895	def cnt.d153(+k: Nat, +lt: {Nat.is_lt(Nat.add(153n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(153n, k)))) == Nat.add(153n, k) : Nat}:
896	  match k:
897	    case 0n:
898	      {==}
899	    case 1n+p:
900	      cnt.d154(p, lt)
901	
902	def cnt.d152(+k: Nat, +lt: {Nat.is_lt(Nat.add(152n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(152n, k)))) == Nat.add(152n, k) : Nat}:
903	  match k:
904	    case 0n:
905	      {==}
906	    case 1n+p:
907	      cnt.d153(p, lt)
908	
909	def cnt.d151(+k: Nat, +lt: {Nat.is_lt(Nat.add(151n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(151n, k)))) == Nat.add(151n, k) : Nat}:
910	  match k:
911	    case 0n:
912	      {==}
913	    case 1n+p:
914	      cnt.d152(p, lt)
915	
916	def cnt.d150(+k: Nat, +lt: {Nat.is_lt(Nat.add(150n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(150n, k)))) == Nat.add(150n, k) : Nat}:
917	  match k:
918	    case 0n:
919	      {==}
920	    case 1n+p:
921	      cnt.d151(p, lt)
922	
923	def cnt.d149(+k: Nat, +lt: {Nat.is_lt(Nat.add(149n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(149n, k)))) == Nat.add(149n, k) : Nat}:
924	  match k:
925	    case 0n:
926	      {==}
927	    case 1n+p:
928	      cnt.d150(p, lt)
929	
930	def cnt.d148(+k: Nat, +lt: {Nat.is_lt(Nat.add(148n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(148n, k)))) == Nat.add(148n, k) : Nat}:
931	  match k:
932	    case 0n:
933	      {==}
934	    case 1n+p:
935	      cnt.d149(p, lt)
936	
937	def cnt.d147(+k: Nat, +lt: {Nat.is_lt(Nat.add(147n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(147n, k)))) == Nat.add(147n, k) : Nat}:
938	  match k:
939	    case 0n:
940	      {==}
941	    case 1n+p:
942	      cnt.d148(p, lt)
943	
944	def cnt.d146(+k: Nat, +lt: {Nat.is_lt(Nat.add(146n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(146n, k)))) == Nat.add(146n, k) : Nat}:
945	  match k:
946	    case 0n:
947	      {==}
948	    case 1n+p:
949	      cnt.d147(p, lt)
950	
951	def cnt.d145(+k: Nat, +lt: {Nat.is_lt(Nat.add(145n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(145n, k)))) == Nat.add(145n, k) : Nat}:
952	  match k:
953	    case 0n:
954	      {==}
955	    case 1n+p:
956	      cnt.d146(p, lt)
957	
958	def cnt.d144(+k: Nat, +lt: {Nat.is_lt(Nat.add(144n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(144n, k)))) == Nat.add(144n, k) : Nat}:
959	  match k:
960	    case 0n:
961	      {==}
962	    case 1n+p:
963	      cnt.d145(p, lt)
964	
965	def cnt.d143(+k: Nat, +lt: {Nat.is_lt(Nat.add(143n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(143n, k)))) == Nat.add(143n, k) : Nat}:
966	  match k:
967	    case 0n:
968	      {==}
969	    case 1n+p:
970	      cnt.d144(p, lt)
971	
972	def cnt.d142(+k: Nat, +lt: {Nat.is_lt(Nat.add(142n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(142n, k)))) == Nat.add(142n, k) : Nat}:
973	  match k:
974	    case 0n:
975	      {==}
976	    case 1n+p:
977	      cnt.d143(p, lt)
978	
979	def cnt.d141(+k: Nat, +lt: {Nat.is_lt(Nat.add(141n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(141n, k)))) == Nat.add(141n, k) : Nat}:
980	  match k:
981	    case 0n:
982	      {==}
983	    case 1n+p:
984	      cnt.d142(p, lt)
985	
986	def cnt.d140(+k: Nat, +lt: {Nat.is_lt(Nat.add(140n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(140n, k)))) == Nat.add(140n, k) : Nat}:
987	  match k:
988	    case 0n:
989	      {==}
990	    case 1n+p:
991	      cnt.d141(p, lt)
992	
993	def cnt.d139(+k: Nat, +lt: {Nat.is_lt(Nat.add(139n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(139n, k)))) == Nat.add(139n, k) : Nat}:
994	  match k:
995	    case 0n:
996	      {==}
997	    case 1n+p:
998	      cnt.d140(p, lt)
999	
1000	def cnt.d138(+k: Nat, +lt: {Nat.is_lt(Nat.add(138n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(138n, k)))) == Nat.add(138n, k) : Nat}:
1001	  match k:
1002	    case 0n:
1003	      {==}
1004	    case 1n+p:
1005	      cnt.d139(p, lt)
1006	
1007	def cnt.d137(+k: Nat, +lt: {Nat.is_lt(Nat.add(137n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(137n, k)))) == Nat.add(137n, k) : Nat}:
1008	  match k:
1009	    case 0n:
1010	      {==}
1011	    case 1n+p:
1012	      cnt.d138(p, lt)
1013	
1014	def cnt.d136(+k: Nat, +lt: {Nat.is_lt(Nat.add(136n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(136n, k)))) == Nat.add(136n, k) : Nat}:
1015	  match k:
1016	    case 0n:
1017	      {==}
1018	    case 1n+p:
1019	      cnt.d137(p, lt)
1020	
1021	def cnt.d135(+k: Nat, +lt: {Nat.is_lt(Nat.add(135n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(135n, k)))) == Nat.add(135n, k) : Nat}:
1022	  match k:
1023	    case 0n:
1024	      {==}
1025	    case 1n+p:
1026	      cnt.d136(p, lt)
1027	
1028	def cnt.d134(+k: Nat, +lt: {Nat.is_lt(Nat.add(134n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(134n, k)))) == Nat.add(134n, k) : Nat}:
1029	  match k:
1030	    case 0n:
1031	      {==}
1032	    case 1n+p:
1033	      cnt.d135(p, lt)
1034	
1035	def cnt.d133(+k: Nat, +lt: {Nat.is_lt(Nat.add(133n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(133n, k)))) == Nat.add(133n, k) : Nat}:
1036	  match k:
1037	    case 0n:
1038	      {==}
1039	    case 1n+p:
1040	      cnt.d134(p, lt)
1041	
1042	def cnt.d132(+k: Nat, +lt: {Nat.is_lt(Nat.add(132n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(132n, k)))) == Nat.add(132n, k) : Nat}:
1043	  match k:
1044	    case 0n:
1045	      {==}
1046	    case 1n+p:
1047	      cnt.d133(p, lt)
1048	
1049	def cnt.d131(+k: Nat, +lt: {Nat.is_lt(Nat.add(131n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(131n, k)))) == Nat.add(131n, k) : Nat}:
1050	  match k:
1051	    case 0n:
1052	      {==}
1053	    case 1n+p:
1054	      cnt.d132(p, lt)
1055	
1056	def cnt.d130(+k: Nat, +lt: {Nat.is_lt(Nat.add(130n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(130n, k)))) == Nat.add(130n, k) : Nat}:
1057	  match k:
1058	    case 0n:
1059	      {==}
1060	    case 1n+p:
1061	      cnt.d131(p, lt)
1062	
1063	def cnt.d129(+k: Nat, +lt: {Nat.is_lt(Nat.add(129n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(129n, k)))) == Nat.add(129n, k) : Nat}:
1064	  match k:
1065	    case 0n:
1066	      {==}
1067	    case 1n+p:
1068	      cnt.d130(p, lt)
1069	
1070	def cnt.d128(+k: Nat, +lt: {Nat.is_lt(Nat.add(128n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(128n, k)))) == Nat.add(128n, k) : Nat}:
1071	  match k:
1072	    case 0n:
1073	      {==}
1074	    case 1n+p:
1075	      cnt.d129(p, lt)
1076	
1077	def cnt.d127(+k: Nat, +lt: {Nat.is_lt(Nat.add(127n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(127n, k)))) == Nat.add(127n, k) : Nat}:
1078	  match k:
1079	    case 0n:
1080	      {==}
1081	    case 1n+p:
1082	      cnt.d128(p, lt)
1083	
1084	def cnt.d126(+k: Nat, +lt: {Nat.is_lt(Nat.add(126n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(126n, k)))) == Nat.add(126n, k) : Nat}:
1085	  match k:
1086	    case 0n:
1087	      {==}
1088	    case 1n+p:
1089	      cnt.d127(p, lt)
1090	
1091	def cnt.d125(+k: Nat, +lt: {Nat.is_lt(Nat.add(125n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(125n, k)))) == Nat.add(125n, k) : Nat}:
1092	  match k:
1093	    case 0n:
1094	      {==}
1095	    case 1n+p:
1096	      cnt.d126(p, lt)
1097	
1098	def cnt.d124(+k: Nat, +lt: {Nat.is_lt(Nat.add(124n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(124n, k)))) == Nat.add(124n, k) : Nat}:
1099	  match k:
1100	    case 0n:
1101	      {==}
1102	    case 1n+p:
1103	      cnt.d125(p, lt)
1104	
1105	def cnt.d123(+k: Nat, +lt: {Nat.is_lt(Nat.add(123n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(123n, k)))) == Nat.add(123n, k) : Nat}:
1106	  match k:
1107	    case 0n:
1108	      {==}
1109	    case 1n+p:
1110	      cnt.d124(p, lt)
1111	
1112	def cnt.d122(+k: Nat, +lt: {Nat.is_lt(Nat.add(122n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(122n, k)))) == Nat.add(122n, k) : Nat}:
1113	  match k:
1114	    case 0n:
1115	      {==}
1116	    case 1n+p:
1117	      cnt.d123(p, lt)
1118	
1119	def cnt.d121(+k: Nat, +lt: {Nat.is_lt(Nat.add(121n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(121n, k)))) == Nat.add(121n, k) : Nat}:
1120	  match k:
1121	    case 0n:
1122	      {==}
1123	    case 1n+p:
1124	      cnt.d122(p, lt)
1125	
1126	def cnt.d120(+k: Nat, +lt: {Nat.is_lt(Nat.add(120n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(120n, k)))) == Nat.add(120n, k) : Nat}:
1127	  match k:
1128	    case 0n:
1129	      {==}
1130	    case 1n+p:
1131	      cnt.d121(p, lt)
1132	
1133	def cnt.d119(+k: Nat, +lt: {Nat.is_lt(Nat.add(119n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(119n, k)))) == Nat.add(119n, k) : Nat}:
1134	  match k:
1135	    case 0n:
1136	      {==}
1137	    case 1n+p:
1138	      cnt.d120(p, lt)
1139	
1140	def cnt.d118(+k: Nat, +lt: {Nat.is_lt(Nat.add(118n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(118n, k)))) == Nat.add(118n, k) : Nat}:
1141	  match k:
1142	    case 0n:
1143	      {==}
1144	    case 1n+p:
1145	      cnt.d119(p, lt)
1146	
1147	def cnt.d117(+k: Nat, +lt: {Nat.is_lt(Nat.add(117n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(117n, k)))) == Nat.add(117n, k) : Nat}:
1148	  match k:
1149	    case 0n:
1150	      {==}
1151	    case 1n+p:
1152	      cnt.d118(p, lt)
1153	
1154	def cnt.d116(+k: Nat, +lt: {Nat.is_lt(Nat.add(116n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(116n, k)))) == Nat.add(116n, k) : Nat}:
1155	  match k:
1156	    case 0n:
1157	      {==}
1158	    case 1n+p:
1159	      cnt.d117(p, lt)
1160	
1161	def cnt.d115(+k: Nat, +lt: {Nat.is_lt(Nat.add(115n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(115n, k)))) == Nat.add(115n, k) : Nat}:
1162	  match k:
1163	    case 0n:
1164	      {==}
1165	    case 1n+p:
1166	      cnt.d116(p, lt)
1167	
1168	def cnt.d114(+k: Nat, +lt: {Nat.is_lt(Nat.add(114n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(114n, k)))) == Nat.add(114n, k) : Nat}:
1169	  match k:
1170	    case 0n:
1171	      {==}
1172	    case 1n+p:
1173	      cnt.d115(p, lt)
1174	
1175	def cnt.d113(+k: Nat, +lt: {Nat.is_lt(Nat.add(113n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(113n, k)))) == Nat.add(113n, k) : Nat}:
1176	  match k:
1177	    case 0n:
1178	      {==}
1179	    case 1n+p:
1180	      cnt.d114(p, lt)
1181	
1182	def cnt.d112(+k: Nat, +lt: {Nat.is_lt(Nat.add(112n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(112n, k)))) == Nat.add(112n, k) : Nat}:
1183	  match k:
1184	    case 0n:
1185	      {==}
1186	    case 1n+p:
1187	      cnt.d113(p, lt)
1188	
1189	def cnt.d111(+k: Nat, +lt: {Nat.is_lt(Nat.add(111n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(111n, k)))) == Nat.add(111n, k) : Nat}:
1190	  match k:
1191	    case 0n:
1192	      {==}
1193	    case 1n+p:
1194	      cnt.d112(p, lt)
1195	
1196	def cnt.d110(+k: Nat, +lt: {Nat.is_lt(Nat.add(110n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(110n, k)))) == Nat.add(110n, k) : Nat}:
1197	  match k:
1198	    case 0n:
1199	      {==}
1200	    case 1n+p:
1201	      cnt.d111(p, lt)
1202	
1203	def cnt.d109(+k: Nat, +lt: {Nat.is_lt(Nat.add(109n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(109n, k)))) == Nat.add(109n, k) : Nat}:
1204	  match k:
1205	    case 0n:
1206	      {==}
1207	    case 1n+p:
1208	      cnt.d110(p, lt)
1209	
1210	def cnt.d108(+k: Nat, +lt: {Nat.is_lt(Nat.add(108n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(108n, k)))) == Nat.add(108n, k) : Nat}:
1211	  match k:
1212	    case 0n:
1213	      {==}
1214	    case 1n+p:
1215	      cnt.d109(p, lt)
1216	
1217	def cnt.d107(+k: Nat, +lt: {Nat.is_lt(Nat.add(107n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(107n, k)))) == Nat.add(107n, k) : Nat}:
1218	  match k:
1219	    case 0n:
1220	      {==}
1221	    case 1n+p:
1222	      cnt.d108(p, lt)
1223	
1224	def cnt.d106(+k: Nat, +lt: {Nat.is_lt(Nat.add(106n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(106n, k)))) == Nat.add(106n, k) : Nat}:
1225	  match k:
1226	    case 0n:
1227	      {==}
1228	    case 1n+p:
1229	      cnt.d107(p, lt)
1230	
1231	def cnt.d105(+k: Nat, +lt: {Nat.is_lt(Nat.add(105n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(105n, k)))) == Nat.add(105n, k) : Nat}:
1232	  match k:
1233	    case 0n:
1234	      {==}
1235	    case 1n+p:
1236	      cnt.d106(p, lt)
1237	
1238	def cnt.d104(+k: Nat, +lt: {Nat.is_lt(Nat.add(104n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(104n, k)))) == Nat.add(104n, k) : Nat}:
1239	  match k:
1240	    case 0n:
1241	      {==}
1242	    case 1n+p:
1243	      cnt.d105(p, lt)
1244	
1245	def cnt.d103(+k: Nat, +lt: {Nat.is_lt(Nat.add(103n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(103n, k)))) == Nat.add(103n, k) : Nat}:
1246	  match k:
1247	    case 0n:
1248	      {==}
1249	    case 1n+p:
1250	      cnt.d104(p, lt)
1251	
1252	def cnt.d102(+k: Nat, +lt: {Nat.is_lt(Nat.add(102n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(102n, k)))) == Nat.add(102n, k) : Nat}:
1253	  match k:
1254	    case 0n:
1255	      {==}
1256	    case 1n+p:
1257	      cnt.d103(p, lt)
1258	
1259	def cnt.d101(+k: Nat, +lt: {Nat.is_lt(Nat.add(101n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(101n, k)))) == Nat.add(101n, k) : Nat}:
1260	  match k:
1261	    case 0n:
1262	      {==}
1263	    case 1n+p:
1264	      cnt.d102(p, lt)
1265	
1266	def cnt.d100(+k: Nat, +lt: {Nat.is_lt(Nat.add(100n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(100n, k)))) == Nat.add(100n, k) : Nat}:
1267	  match k:
1268	    case 0n:
1269	      {==}
1270	    case 1n+p:
1271	      cnt.d101(p, lt)
1272	
1273	def cnt.d99(+k: Nat, +lt: {Nat.is_lt(Nat.add(99n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(99n, k)))) == Nat.add(99n, k) : Nat}:
1274	  match k:
1275	    case 0n:
1276	      {==}
1277	    case 1n+p:
1278	      cnt.d100(p, lt)
1279	
1280	def cnt.d98(+k: Nat, +lt: {Nat.is_lt(Nat.add(98n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(98n, k)))) == Nat.add(98n, k) : Nat}:
1281	  match k:
1282	    case 0n:
1283	      {==}
1284	    case 1n+p:
1285	      cnt.d99(p, lt)
1286	
1287	def cnt.d97(+k: Nat, +lt: {Nat.is_lt(Nat.add(97n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(97n, k)))) == Nat.add(97n, k) : Nat}:
1288	  match k:
1289	    case 0n:
1290	      {==}
1291	    case 1n+p:
1292	      cnt.d98(p, lt)
1293	
1294	def cnt.d96(+k: Nat, +lt: {Nat.is_lt(Nat.add(96n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(96n, k)))) == Nat.add(96n, k) : Nat}:
1295	  match k:
1296	    case 0n:
1297	      {==}
1298	    case 1n+p:
1299	      cnt.d97(p, lt)
1300	
1301	def cnt.d95(+k: Nat, +lt: {Nat.is_lt(Nat.add(95n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(95n, k)))) == Nat.add(95n, k) : Nat}:
1302	  match k:
1303	    case 0n:
1304	      {==}
1305	    case 1n+p:
1306	      cnt.d96(p, lt)
1307	
1308	def cnt.d94(+k: Nat, +lt: {Nat.is_lt(Nat.add(94n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(94n, k)))) == Nat.add(94n, k) : Nat}:
1309	  match k:
1310	    case 0n:
1311	      {==}
1312	    case 1n+p:
1313	      cnt.d95(p, lt)
1314	
1315	def cnt.d93(+k: Nat, +lt: {Nat.is_lt(Nat.add(93n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(93n, k)))) == Nat.add(93n, k) : Nat}:
1316	  match k:
1317	    case 0n:
1318	      {==}
1319	    case 1n+p:
1320	      cnt.d94(p, lt)
1321	
1322	def cnt.d92(+k: Nat, +lt: {Nat.is_lt(Nat.add(92n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(92n, k)))) == Nat.add(92n, k) : Nat}:
1323	  match k:
1324	    case 0n:
1325	      {==}
1326	    case 1n+p:
1327	      cnt.d93(p, lt)
1328	
1329	def cnt.d91(+k: Nat, +lt: {Nat.is_lt(Nat.add(91n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(91n, k)))) == Nat.add(91n, k) : Nat}:
1330	  match k:
1331	    case 0n:
1332	      {==}
1333	    case 1n+p:
1334	      cnt.d92(p, lt)
1335	
1336	def cnt.d90(+k: Nat, +lt: {Nat.is_lt(Nat.add(90n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(90n, k)))) == Nat.add(90n, k) : Nat}:
1337	  match k:
1338	    case 0n:
1339	      {==}
1340	    case 1n+p:
1341	      cnt.d91(p, lt)
1342	
1343	def cnt.d89(+k: Nat, +lt: {Nat.is_lt(Nat.add(89n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(89n, k)))) == Nat.add(89n, k) : Nat}:
1344	  match k:
1345	    case 0n:
1346	      {==}
1347	    case 1n+p:
1348	      cnt.d90(p, lt)
1349	
1350	def cnt.d88(+k: Nat, +lt: {Nat.is_lt(Nat.add(88n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(88n, k)))) == Nat.add(88n, k) : Nat}:
1351	  match k:
1352	    case 0n:
1353	      {==}
1354	    case 1n+p:
1355	      cnt.d89(p, lt)
1356	
1357	def cnt.d87(+k: Nat, +lt: {Nat.is_lt(Nat.add(87n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(87n, k)))) == Nat.add(87n, k) : Nat}:
1358	  match k:
1359	    case 0n:
1360	      {==}
1361	    case 1n+p:
1362	      cnt.d88(p, lt)
1363	
1364	def cnt.d86(+k: Nat, +lt: {Nat.is_lt(Nat.add(86n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(86n, k)))) == Nat.add(86n, k) : Nat}:
1365	  match k:
1366	    case 0n:
1367	      {==}
1368	    case 1n+p:
1369	      cnt.d87(p, lt)
1370	
1371	def cnt.d85(+k: Nat, +lt: {Nat.is_lt(Nat.add(85n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(85n, k)))) == Nat.add(85n, k) : Nat}:
1372	  match k:
1373	    case 0n:
1374	      {==}
1375	    case 1n+p:
1376	      cnt.d86(p, lt)
1377	
1378	def cnt.d84(+k: Nat, +lt: {Nat.is_lt(Nat.add(84n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(84n, k)))) == Nat.add(84n, k) : Nat}:
1379	  match k:
1380	    case 0n:
1381	      {==}
1382	    case 1n+p:
1383	      cnt.d85(p, lt)
1384	
1385	def cnt.d83(+k: Nat, +lt: {Nat.is_lt(Nat.add(83n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(83n, k)))) == Nat.add(83n, k) : Nat}:
1386	  match k:
1387	    case 0n:
1388	      {==}
1389	    case 1n+p:
1390	      cnt.d84(p, lt)
1391	
1392	def cnt.d82(+k: Nat, +lt: {Nat.is_lt(Nat.add(82n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(82n, k)))) == Nat.add(82n, k) : Nat}:
1393	  match k:
1394	    case 0n:
1395	      {==}
1396	    case 1n+p:
1397	      cnt.d83(p, lt)
1398	
1399	def cnt.d81(+k: Nat, +lt: {Nat.is_lt(Nat.add(81n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(81n, k)))) == Nat.add(81n, k) : Nat}:
1400	  match k:
1401	    case 0n:
1402	      {==}
1403	    case 1n+p:
1404	      cnt.d82(p, lt)
1405	
1406	def cnt.d80(+k: Nat, +lt: {Nat.is_lt(Nat.add(80n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(80n, k)))) == Nat.add(80n, k) : Nat}:
1407	  match k:
1408	    case 0n:
1409	      {==}
1410	    case 1n+p:
1411	      cnt.d81(p, lt)
1412	
1413	def cnt.d79(+k: Nat, +lt: {Nat.is_lt(Nat.add(79n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(79n, k)))) == Nat.add(79n, k) : Nat}:
1414	  match k:
1415	    case 0n:
1416	      {==}
1417	    case 1n+p:
1418	      cnt.d80(p, lt)
1419	
1420	def cnt.d78(+k: Nat, +lt: {Nat.is_lt(Nat.add(78n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(78n, k)))) == Nat.add(78n, k) : Nat}:
1421	  match k:
1422	    case 0n:
1423	      {==}
1424	    case 1n+p:
1425	      cnt.d79(p, lt)
1426	
1427	def cnt.d77(+k: Nat, +lt: {Nat.is_lt(Nat.add(77n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(77n, k)))) == Nat.add(77n, k) : Nat}:
1428	  match k:
1429	    case 0n:
1430	      {==}
1431	    case 1n+p:
1432	      cnt.d78(p, lt)
1433	
1434	def cnt.d76(+k: Nat, +lt: {Nat.is_lt(Nat.add(76n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(76n, k)))) == Nat.add(76n, k) : Nat}:
1435	  match k:
1436	    case 0n:
1437	      {==}
1438	    case 1n+p:
1439	      cnt.d77(p, lt)
1440	
1441	def cnt.d75(+k: Nat, +lt: {Nat.is_lt(Nat.add(75n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(75n, k)))) == Nat.add(75n, k) : Nat}:
1442	  match k:
1443	    case 0n:
1444	      {==}
1445	    case 1n+p:
1446	      cnt.d76(p, lt)
1447	
1448	def cnt.d74(+k: Nat, +lt: {Nat.is_lt(Nat.add(74n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(74n, k)))) == Nat.add(74n, k) : Nat}:
1449	  match k:
1450	    case 0n:
1451	      {==}
1452	    case 1n+p:
1453	      cnt.d75(p, lt)
1454	
1455	def cnt.d73(+k: Nat, +lt: {Nat.is_lt(Nat.add(73n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(73n, k)))) == Nat.add(73n, k) : Nat}:
1456	  match k:
1457	    case 0n:
1458	      {==}
1459	    case 1n+p:
1460	      cnt.d74(p, lt)
1461	
1462	def cnt.d72(+k: Nat, +lt: {Nat.is_lt(Nat.add(72n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(72n, k)))) == Nat.add(72n, k) : Nat}:
1463	  match k:
1464	    case 0n:
1465	      {==}
1466	    case 1n+p:
1467	      cnt.d73(p, lt)
1468	
1469	def cnt.d71(+k: Nat, +lt: {Nat.is_lt(Nat.add(71n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(71n, k)))) == Nat.add(71n, k) : Nat}:
1470	  match k:
1471	    case 0n:
1472	      {==}
1473	    case 1n+p:
1474	      cnt.d72(p, lt)
1475	
1476	def cnt.d70(+k: Nat, +lt: {Nat.is_lt(Nat.add(70n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(70n, k)))) == Nat.add(70n, k) : Nat}:
1477	  match k:
1478	    case 0n:
1479	      {==}
1480	    case 1n+p:
1481	      cnt.d71(p, lt)
1482	
1483	def cnt.d69(+k: Nat, +lt: {Nat.is_lt(Nat.add(69n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(69n, k)))) == Nat.add(69n, k) : Nat}:
1484	  match k:
1485	    case 0n:
1486	      {==}
1487	    case 1n+p:
1488	      cnt.d70(p, lt)
1489	
1490	def cnt.d68(+k: Nat, +lt: {Nat.is_lt(Nat.add(68n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(68n, k)))) == Nat.add(68n, k) : Nat}:
1491	  match k:
1492	    case 0n:
1493	      {==}
1494	    case 1n+p:
1495	      cnt.d69(p, lt)
1496	
1497	def cnt.d67(+k: Nat, +lt: {Nat.is_lt(Nat.add(67n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(67n, k)))) == Nat.add(67n, k) : Nat}:
1498	  match k:
1499	    case 0n:
1500	      {==}
1501	    case 1n+p:
1502	      cnt.d68(p, lt)
1503	
1504	def cnt.d66(+k: Nat, +lt: {Nat.is_lt(Nat.add(66n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(66n, k)))) == Nat.add(66n, k) : Nat}:
1505	  match k:
1506	    case 0n:
1507	      {==}
1508	    case 1n+p:
1509	      cnt.d67(p, lt)
1510	
1511	def cnt.d65(+k: Nat, +lt: {Nat.is_lt(Nat.add(65n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(65n, k)))) == Nat.add(65n, k) : Nat}:
1512	  match k:
1513	    case 0n:
1514	      {==}
1515	    case 1n+p:
1516	      cnt.d66(p, lt)
1517	
1518	def cnt.d64(+k: Nat, +lt: {Nat.is_lt(Nat.add(64n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(64n, k)))) == Nat.add(64n, k) : Nat}:
1519	  match k:
1520	    case 0n:
1521	      {==}
1522	    case 1n+p:
1523	      cnt.d65(p, lt)
1524	
1525	def cnt.d63(+k: Nat, +lt: {Nat.is_lt(Nat.add(63n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(63n, k)))) == Nat.add(63n, k) : Nat}:
1526	  match k:
1527	    case 0n:
1528	      {==}
1529	    case 1n+p:
1530	      cnt.d64(p, lt)
1531	
1532	def cnt.d62(+k: Nat, +lt: {Nat.is_lt(Nat.add(62n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(62n, k)))) == Nat.add(62n, k) : Nat}:
1533	  match k:
1534	    case 0n:
1535	      {==}
1536	    case 1n+p:
1537	      cnt.d63(p, lt)
1538	
1539	def cnt.d61(+k: Nat, +lt: {Nat.is_lt(Nat.add(61n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(61n, k)))) == Nat.add(61n, k) : Nat}:
1540	  match k:
1541	    case 0n:
1542	      {==}
1543	    case 1n+p:
1544	      cnt.d62(p, lt)
1545	
1546	def cnt.d60(+k: Nat, +lt: {Nat.is_lt(Nat.add(60n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(60n, k)))) == Nat.add(60n, k) : Nat}:
1547	  match k:
1548	    case 0n:
1549	      {==}
1550	    case 1n+p:
1551	      cnt.d61(p, lt)
1552	
1553	def cnt.d59(+k: Nat, +lt: {Nat.is_lt(Nat.add(59n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(59n, k)))) == Nat.add(59n, k) : Nat}:
1554	  match k:
1555	    case 0n:
1556	      {==}
1557	    case 1n+p:
1558	      cnt.d60(p, lt)
1559	
1560	def cnt.d58(+k: Nat, +lt: {Nat.is_lt(Nat.add(58n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(58n, k)))) == Nat.add(58n, k) : Nat}:
1561	  match k:
1562	    case 0n:
1563	      {==}
1564	    case 1n+p:
1565	      cnt.d59(p, lt)
1566	
1567	def cnt.d57(+k: Nat, +lt: {Nat.is_lt(Nat.add(57n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(57n, k)))) == Nat.add(57n, k) : Nat}:
1568	  match k:
1569	    case 0n:
1570	      {==}
1571	    case 1n+p:
1572	      cnt.d58(p, lt)
1573	
1574	def cnt.d56(+k: Nat, +lt: {Nat.is_lt(Nat.add(56n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(56n, k)))) == Nat.add(56n, k) : Nat}:
1575	  match k:
1576	    case 0n:
1577	      {==}
1578	    case 1n+p:
1579	      cnt.d57(p, lt)
1580	
1581	def cnt.d55(+k: Nat, +lt: {Nat.is_lt(Nat.add(55n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(55n, k)))) == Nat.add(55n, k) : Nat}:
1582	  match k:
1583	    case 0n:
1584	      {==}
1585	    case 1n+p:
1586	      cnt.d56(p, lt)
1587	
1588	def cnt.d54(+k: Nat, +lt: {Nat.is_lt(Nat.add(54n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(54n, k)))) == Nat.add(54n, k) : Nat}:
1589	  match k:
1590	    case 0n:
1591	      {==}
1592	    case 1n+p:
1593	      cnt.d55(p, lt)
1594	
1595	def cnt.d53(+k: Nat, +lt: {Nat.is_lt(Nat.add(53n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(53n, k)))) == Nat.add(53n, k) : Nat}:
1596	  match k:
1597	    case 0n:
1598	      {==}
1599	    case 1n+p:
1600	      cnt.d54(p, lt)
1601	
1602	def cnt.d52(+k: Nat, +lt: {Nat.is_lt(Nat.add(52n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(52n, k)))) == Nat.add(52n, k) : Nat}:
1603	  match k:
1604	    case 0n:
1605	      {==}
1606	    case 1n+p:
1607	      cnt.d53(p, lt)
1608	
1609	def cnt.d51(+k: Nat, +lt: {Nat.is_lt(Nat.add(51n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(51n, k)))) == Nat.add(51n, k) : Nat}:
1610	  match k:
1611	    case 0n:
1612	      {==}
1613	    case 1n+p:
1614	      cnt.d52(p, lt)
1615	
1616	def cnt.d50(+k: Nat, +lt: {Nat.is_lt(Nat.add(50n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(50n, k)))) == Nat.add(50n, k) : Nat}:
1617	  match k:
1618	    case 0n:
1619	      {==}
1620	    case 1n+p:
1621	      cnt.d51(p, lt)
1622	
1623	def cnt.d49(+k: Nat, +lt: {Nat.is_lt(Nat.add(49n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(49n, k)))) == Nat.add(49n, k) : Nat}:
1624	  match k:
1625	    case 0n:
1626	      {==}
1627	    case 1n+p:
1628	      cnt.d50(p, lt)
1629	
1630	def cnt.d48(+k: Nat, +lt: {Nat.is_lt(Nat.add(48n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(48n, k)))) == Nat.add(48n, k) : Nat}:
1631	  match k:
1632	    case 0n:
1633	      {==}
1634	    case 1n+p:
1635	      cnt.d49(p, lt)
1636	
1637	def cnt.d47(+k: Nat, +lt: {Nat.is_lt(Nat.add(47n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(47n, k)))) == Nat.add(47n, k) : Nat}:
1638	  match k:
1639	    case 0n:
1640	      {==}
1641	    case 1n+p:
1642	      cnt.d48(p, lt)
1643	
1644	def cnt.d46(+k: Nat, +lt: {Nat.is_lt(Nat.add(46n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(46n, k)))) == Nat.add(46n, k) : Nat}:
1645	  match k:
1646	    case 0n:
1647	      {==}
1648	    case 1n+p:
1649	      cnt.d47(p, lt)
1650	
1651	def cnt.d45(+k: Nat, +lt: {Nat.is_lt(Nat.add(45n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(45n, k)))) == Nat.add(45n, k) : Nat}:
1652	  match k:
1653	    case 0n:
1654	      {==}
1655	    case 1n+p:
1656	      cnt.d46(p, lt)
1657	
1658	def cnt.d44(+k: Nat, +lt: {Nat.is_lt(Nat.add(44n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(44n, k)))) == Nat.add(44n, k) : Nat}:
1659	  match k:
1660	    case 0n:
1661	      {==}
1662	    case 1n+p:
1663	      cnt.d45(p, lt)
1664	
1665	def cnt.d43(+k: Nat, +lt: {Nat.is_lt(Nat.add(43n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(43n, k)))) == Nat.add(43n, k) : Nat}:
1666	  match k:
1667	    case 0n:
1668	      {==}
1669	    case 1n+p:
1670	      cnt.d44(p, lt)
1671	
1672	def cnt.d42(+k: Nat, +lt: {Nat.is_lt(Nat.add(42n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(42n, k)))) == Nat.add(42n, k) : Nat}:
1673	  match k:
1674	    case 0n:
1675	      {==}
1676	    case 1n+p:
1677	      cnt.d43(p, lt)
1678	
1679	def cnt.d41(+k: Nat, +lt: {Nat.is_lt(Nat.add(41n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(41n, k)))) == Nat.add(41n, k) : Nat}:
1680	  match k:
1681	    case 0n:
1682	      {==}
1683	    case 1n+p:
1684	      cnt.d42(p, lt)
1685	
1686	def cnt.d40(+k: Nat, +lt: {Nat.is_lt(Nat.add(40n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(40n, k)))) == Nat.add(40n, k) : Nat}:
1687	  match k:
1688	    case 0n:
1689	      {==}
1690	    case 1n+p:
1691	      cnt.d41(p, lt)
1692	
1693	def cnt.d39(+k: Nat, +lt: {Nat.is_lt(Nat.add(39n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(39n, k)))) == Nat.add(39n, k) : Nat}:
1694	  match k:
1695	    case 0n:
1696	      {==}
1697	    case 1n+p:
1698	      cnt.d40(p, lt)
1699	
1700	def cnt.d38(+k: Nat, +lt: {Nat.is_lt(Nat.add(38n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(38n, k)))) == Nat.add(38n, k) : Nat}:
1701	  match k:
1702	    case 0n:
1703	      {==}
1704	    case 1n+p:
1705	      cnt.d39(p, lt)
1706	
1707	def cnt.d37(+k: Nat, +lt: {Nat.is_lt(Nat.add(37n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(37n, k)))) == Nat.add(37n, k) : Nat}:
1708	  match k:
1709	    case 0n:
1710	      {==}
1711	    case 1n+p:
1712	      cnt.d38(p, lt)
1713	
1714	def cnt.d36(+k: Nat, +lt: {Nat.is_lt(Nat.add(36n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(36n, k)))) == Nat.add(36n, k) : Nat}:
1715	  match k:
1716	    case 0n:
1717	      {==}
1718	    case 1n+p:
1719	      cnt.d37(p, lt)
1720	
1721	def cnt.d35(+k: Nat, +lt: {Nat.is_lt(Nat.add(35n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(35n, k)))) == Nat.add(35n, k) : Nat}:
1722	  match k:
1723	    case 0n:
1724	      {==}
1725	    case 1n+p:
1726	      cnt.d36(p, lt)
1727	
1728	def cnt.d34(+k: Nat, +lt: {Nat.is_lt(Nat.add(34n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(34n, k)))) == Nat.add(34n, k) : Nat}:
1729	  match k:
1730	    case 0n:
1731	      {==}
1732	    case 1n+p:
1733	      cnt.d35(p, lt)
1734	
1735	def cnt.d33(+k: Nat, +lt: {Nat.is_lt(Nat.add(33n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(33n, k)))) == Nat.add(33n, k) : Nat}:
1736	  match k:
1737	    case 0n:
1738	      {==}
1739	    case 1n+p:
1740	      cnt.d34(p, lt)
1741	
1742	def cnt.d32(+k: Nat, +lt: {Nat.is_lt(Nat.add(32n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(32n, k)))) == Nat.add(32n, k) : Nat}:
1743	  match k:
1744	    case 0n:
1745	      {==}
1746	    case 1n+p:
1747	      cnt.d33(p, lt)
1748	
1749	def cnt.d31(+k: Nat, +lt: {Nat.is_lt(Nat.add(31n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(31n, k)))) == Nat.add(31n, k) : Nat}:
1750	  match k:
1751	    case 0n:
1752	      {==}
1753	    case 1n+p:
1754	      cnt.d32(p, lt)
1755	
1756	def cnt.d30(+k: Nat, +lt: {Nat.is_lt(Nat.add(30n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(30n, k)))) == Nat.add(30n, k) : Nat}:
1757	  match k:
1758	    case 0n:
1759	      {==}
1760	    case 1n+p:
1761	      cnt.d31(p, lt)
1762	
1763	def cnt.d29(+k: Nat, +lt: {Nat.is_lt(Nat.add(29n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(29n, k)))) == Nat.add(29n, k) : Nat}:
1764	  match k:
1765	    case 0n:
1766	      {==}
1767	    case 1n+p:
1768	      cnt.d30(p, lt)
1769	
1770	def cnt.d28(+k: Nat, +lt: {Nat.is_lt(Nat.add(28n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(28n, k)))) == Nat.add(28n, k) : Nat}:
1771	  match k:
1772	    case 0n:
1773	      {==}
1774	    case 1n+p:
1775	      cnt.d29(p, lt)
1776	
1777	def cnt.d27(+k: Nat, +lt: {Nat.is_lt(Nat.add(27n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(27n, k)))) == Nat.add(27n, k) : Nat}:
1778	  match k:
1779	    case 0n:
1780	      {==}
1781	    case 1n+p:
1782	      cnt.d28(p, lt)
1783	
1784	def cnt.d26(+k: Nat, +lt: {Nat.is_lt(Nat.add(26n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(26n, k)))) == Nat.add(26n, k) : Nat}:
1785	  match k:
1786	    case 0n:
1787	      {==}
1788	    case 1n+p:
1789	      cnt.d27(p, lt)
1790	
1791	def cnt.d25(+k: Nat, +lt: {Nat.is_lt(Nat.add(25n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(25n, k)))) == Nat.add(25n, k) : Nat}:
1792	  match k:
1793	    case 0n:
1794	      {==}
1795	    case 1n+p:
1796	      cnt.d26(p, lt)
1797	
1798	def cnt.d24(+k: Nat, +lt: {Nat.is_lt(Nat.add(24n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(24n, k)))) == Nat.add(24n, k) : Nat}:
1799	  match k:
1800	    case 0n:
1801	      {==}
1802	    case 1n+p:
1803	      cnt.d25(p, lt)
1804	
1805	def cnt.d23(+k: Nat, +lt: {Nat.is_lt(Nat.add(23n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(23n, k)))) == Nat.add(23n, k) : Nat}:
1806	  match k:
1807	    case 0n:
1808	      {==}
1809	    case 1n+p:
1810	      cnt.d24(p, lt)
1811	
1812	def cnt.d22(+k: Nat, +lt: {Nat.is_lt(Nat.add(22n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(22n, k)))) == Nat.add(22n, k) : Nat}:
1813	  match k:
1814	    case 0n:
1815	      {==}
1816	    case 1n+p:
1817	      cnt.d23(p, lt)
1818	
1819	def cnt.d21(+k: Nat, +lt: {Nat.is_lt(Nat.add(21n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(21n, k)))) == Nat.add(21n, k) : Nat}:
1820	  match k:
1821	    case 0n:
1822	      {==}
1823	    case 1n+p:
1824	      cnt.d22(p, lt)
1825	
1826	def cnt.d20(+k: Nat, +lt: {Nat.is_lt(Nat.add(20n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(20n, k)))) == Nat.add(20n, k) : Nat}:
1827	  match k:
1828	    case 0n:
1829	      {==}
1830	    case 1n+p:
1831	      cnt.d21(p, lt)
1832	
1833	def cnt.d19(+k: Nat, +lt: {Nat.is_lt(Nat.add(19n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(19n, k)))) == Nat.add(19n, k) : Nat}:
1834	  match k:
1835	    case 0n:
1836	      {==}
1837	    case 1n+p:
1838	      cnt.d20(p, lt)
1839	
1840	def cnt.d18(+k: Nat, +lt: {Nat.is_lt(Nat.add(18n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(18n, k)))) == Nat.add(18n, k) : Nat}:
1841	  match k:
1842	    case 0n:
1843	      {==}
1844	    case 1n+p:
1845	      cnt.d19(p, lt)
1846	
1847	def cnt.d17(+k: Nat, +lt: {Nat.is_lt(Nat.add(17n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(17n, k)))) == Nat.add(17n, k) : Nat}:
1848	  match k:
1849	    case 0n:
1850	      {==}
1851	    case 1n+p:
1852	      cnt.d18(p, lt)
1853	
1854	def cnt.d16(+k: Nat, +lt: {Nat.is_lt(Nat.add(16n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(16n, k)))) == Nat.add(16n, k) : Nat}:
1855	  match k:
1856	    case 0n:
1857	      {==}
1858	    case 1n+p:
1859	      cnt.d17(p, lt)
1860	
1861	def cnt.d15(+k: Nat, +lt: {Nat.is_lt(Nat.add(15n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(15n, k)))) == Nat.add(15n, k) : Nat}:
1862	  match k:
1863	    case 0n:
1864	      {==}
1865	    case 1n+p:
1866	      cnt.d16(p, lt)
1867	
1868	def cnt.d14(+k: Nat, +lt: {Nat.is_lt(Nat.add(14n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(14n, k)))) == Nat.add(14n, k) : Nat}:
1869	  match k:
1870	    case 0n:
1871	      {==}
1872	    case 1n+p:
1873	      cnt.d15(p, lt)
1874	
1875	def cnt.d13(+k: Nat, +lt: {Nat.is_lt(Nat.add(13n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(13n, k)))) == Nat.add(13n, k) : Nat}:
1876	  match k:
1877	    case 0n:
1878	      {==}
1879	    case 1n+p:
1880	      cnt.d14(p, lt)
1881	
1882	def cnt.d12(+k: Nat, +lt: {Nat.is_lt(Nat.add(12n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(12n, k)))) == Nat.add(12n, k) : Nat}:
1883	  match k:
1884	    case 0n:
1885	      {==}
1886	    case 1n+p:
1887	      cnt.d13(p, lt)
1888	
1889	def cnt.d11(+k: Nat, +lt: {Nat.is_lt(Nat.add(11n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(11n, k)))) == Nat.add(11n, k) : Nat}:
1890	  match k:
1891	    case 0n:
1892	      {==}
1893	    case 1n+p:
1894	      cnt.d12(p, lt)
1895	
1896	def cnt.d10(+k: Nat, +lt: {Nat.is_lt(Nat.add(10n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(10n, k)))) == Nat.add(10n, k) : Nat}:
1897	  match k:
1898	    case 0n:
1899	      {==}
1900	    case 1n+p:
1901	      cnt.d11(p, lt)
1902	
1903	def cnt.d9(+k: Nat, +lt: {Nat.is_lt(Nat.add(9n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(9n, k)))) == Nat.add(9n, k) : Nat}:
1904	  match k:
1905	    case 0n:
1906	      {==}
1907	    case 1n+p:
1908	      cnt.d10(p, lt)
1909	
1910	def cnt.d8(+k: Nat, +lt: {Nat.is_lt(Nat.add(8n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(8n, k)))) == Nat.add(8n, k) : Nat}:
1911	  match k:
1912	    case 0n:
1913	      {==}
1914	    case 1n+p:
1915	      cnt.d9(p, lt)
1916	
1917	def cnt.d7(+k: Nat, +lt: {Nat.is_lt(Nat.add(7n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(7n, k)))) == Nat.add(7n, k) : Nat}:
1918	  match k:
1919	    case 0n:
1920	      {==}
1921	    case 1n+p:
1922	      cnt.d8(p, lt)
1923	
1924	def cnt.d6(+k: Nat, +lt: {Nat.is_lt(Nat.add(6n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(6n, k)))) == Nat.add(6n, k) : Nat}:
1925	  match k:
1926	    case 0n:
1927	      {==}
1928	    case 1n+p:
1929	      cnt.d7(p, lt)
1930	
1931	def cnt.d5(+k: Nat, +lt: {Nat.is_lt(Nat.add(5n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(5n, k)))) == Nat.add(5n, k) : Nat}:
1932	  match k:
1933	    case 0n:
1934	      {==}
1935	    case 1n+p:
1936	      cnt.d6(p, lt)
1937	
1938	def cnt.d4(+k: Nat, +lt: {Nat.is_lt(Nat.add(4n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(4n, k)))) == Nat.add(4n, k) : Nat}:
1939	  match k:
1940	    case 0n:
1941	      {==}
1942	    case 1n+p:
1943	      cnt.d5(p, lt)
1944	
1945	def cnt.d3(+k: Nat, +lt: {Nat.is_lt(Nat.add(3n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(3n, k)))) == Nat.add(3n, k) : Nat}:
1946	  match k:
1947	    case 0n:
1948	      {==}
1949	    case 1n+p:
1950	      cnt.d4(p, lt)
1951	
1952	def cnt.d2(+k: Nat, +lt: {Nat.is_lt(Nat.add(2n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(2n, k)))) == Nat.add(2n, k) : Nat}:
1953	  match k:
1954	    case 0n:
1955	      {==}
1956	    case 1n+p:
1957	      cnt.d3(p, lt)
1958	
1959	def cnt.d1(+k: Nat, +lt: {Nat.is_lt(Nat.add(1n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(1n, k)))) == Nat.add(1n, k) : Nat}:
1960	  match k:
1961	    case 0n:
1962	      {==}
1963	    case 1n+p:
1964	      cnt.d2(p, lt)
1965	
1966	def cnt.d0(+k: Nat, +lt: {Nat.is_lt(Nat.add(0n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(0n, k)))) == Nat.add(0n, k) : Nat}:
1967	  match k:
1968	    case 0n:
1969	      {==}
1970	    case 1n+p:
1971	      cnt.d1(p, lt)
1972	
1973	def cnt_rt(+k: Nat, +lt: {Nat.is_lt(k, 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(k))) == k : Nat}:
1974	  cnt.d0(k, lt)
1975	
1976	def Laws.pkglength_round_trip(v, rest, fits):
1977	  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(K.AmlPkgLength.encode(v), rest)), B.append(B.Octets.to_list(K.AmlPkgLength.encode(v)), B.Octets.to_list(rest)), BL.octets_append_list(K.AmlPkgLength.encode(v), rest)) : {K.pk.pub(K.pk.dec(_)) == Done{K.AmlPkgLen{v, rest}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}
1978	  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(K.pk.enc(v))), B.mask(K.pk.enc(v)), BL.octets_to_of(K.pk.enc(v))) : {K.pk.pub(K.pk.dec(B.append(_, B.Octets.to_list(rest)))) == Done{K.AmlPkgLen{v, rest}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}
1979	  %BL.octets_of_to(rest) : {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), B.Octets.to_list(rest)))) == Done{K.AmlPkgLen{v, _}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}
1980	  pk_rt(v, B.Octets.to_list(rest), fits)
1981	# Lists and masks
1982	
1983	def app_assoc(+a: List<&2, U32>, +b: List<&2, U32>, +c: List<&2, U32>) -> {B.append(a, B.append(b, c)) == B.append(B.append(a, b), c) : List<&2, U32>}:
1984	  match a:
1985	    case Nil{}:
1986	      {==}
1987	    case Con{h, t}:
1988	      %app_assoc(t, b, c) : {Con{h, B.append(t, B.append(b, c))} == Con{h, _} : List<&2, U32>}
1989	      {==}
1990	
1991	def mask_app(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.append(B.mask(a), B.mask(b)) == B.mask(B.append(a, b)) : List<&2, U32>}:
1992	  match a:
1993	    case Nil{}:
1994	      {==}
1995	    case Con{h, t}:
1996	      %mask_app(t, b) : {Con{B.byte(h), B.append(B.mask(t), B.mask(b))} == Con{B.byte(h), _} : List<&2, U32>}
1997	      {==}
1998	
1999	def mask_tl(+o: B.Octets) -> {B.Octets.to_list(o) == B.mask(B.Octets.to_list(o)) : List<&2, U32>}:
2000	  %BL.octets_to_of(B.Octets.to_list(o)) : {B.Octets.to_list(o) == _ : List<&2, U32>}
Lines 1-2000 of 2633. More: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&start_line=2001