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