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