proofs/crypto/blake/blake2b/compress.bend

bend-collections-laws-crypto@1.0.0.0 · 894 lines · 43 definitions

1# Generated by tools/generators/blake2b_gen.py; do not edit by hand.
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/compress.bend as I
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as S
6
7law column0_correct:
8  for +v: T.State
9  for +x0: T.Lane
10  for +x1: T.Lane
11  for +x2: T.Lane
12  for +x3: T.Lane
13  for +x4: T.Lane
14  for +x5: T.Lane
15  for +x6: T.Lane
16  for +x7: T.Lane
17  {I.column0(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
18
19def column0_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
20  match v x0 x1 x2 x3 x4 x5 x6 x7:
21    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
22
23law diagonal0_correct:
24  for +v: T.State
25  for +x0: T.Lane
26  for +x1: T.Lane
27  for +x2: T.Lane
28  for +x3: T.Lane
29  for +x4: T.Lane
30  for +x5: T.Lane
31  for +x6: T.Lane
32  for +x7: T.Lane
33  {I.diagonal0(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
34
35def diagonal0_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
36  match v x0 x1 x2 x3 x4 x5 x6 x7:
37    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
38
39law round0_correct:
40  for +v: T.State
41  for +m0: T.Lane
42  for +m1: T.Lane
43  for +m2: T.Lane
44  for +m3: T.Lane
45  for +m4: T.Lane
46  for +m5: T.Lane
47  for +m6: T.Lane
48  for +m7: T.Lane
49  for +m8: T.Lane
50  for +m9: T.Lane
51  for +m10: T.Lane
52  for +m11: T.Lane
53  for +m12: T.Lane
54  for +m13: T.Lane
55  for +m14: T.Lane
56  for +m15: T.Lane
57  {I.round0(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)) : T.State}
58
59def round0_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
60  Equal.trans(T.State,
61    I.diagonal0(I.column0(v,m0,m1,m2,m3,m4,m5,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15),
62    I.diagonal0(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m0,m1),1n,5n,9n,13n,m2,m3),2n,6n,10n,14n,m4,m5),3n,7n,11n,15n,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15),
63    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m0,m1),1n,5n,9n,13n,m2,m3),2n,6n,10n,14n,m4,m5),3n,7n,11n,15n,m6,m7),0n,5n,10n,15n,m8,m9),1n,6n,11n,12n,m10,m11),2n,7n,8n,13n,m12,m13),3n,4n,9n,14n,m14,m15),
64    Equal.cong(T.State,T.State,t => I.diagonal0(t,m8,m9,m10,m11,m12,m13,m14,m15),I.column0(v,m0,m1,m2,m3,m4,m5,m6,m7),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m0,m1),1n,5n,9n,13n,m2,m3),2n,6n,10n,14n,m4,m5),3n,7n,11n,15n,m6,m7),column0_correct(v,m0,m1,m2,m3,m4,m5,m6,m7)),
65    diagonal0_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m0,m1),1n,5n,9n,13n,m2,m3),2n,6n,10n,14n,m4,m5),3n,7n,11n,15n,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15))
66
67law column1_correct:
68  for +v: T.State
69  for +x0: T.Lane
70  for +x1: T.Lane
71  for +x2: T.Lane
72  for +x3: T.Lane
73  for +x4: T.Lane
74  for +x5: T.Lane
75  for +x6: T.Lane
76  for +x7: T.Lane
77  {I.column1(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
78
79def column1_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
80  match v x0 x1 x2 x3 x4 x5 x6 x7:
81    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
82
83law diagonal1_correct:
84  for +v: T.State
85  for +x0: T.Lane
86  for +x1: T.Lane
87  for +x2: T.Lane
88  for +x3: T.Lane
89  for +x4: T.Lane
90  for +x5: T.Lane
91  for +x6: T.Lane
92  for +x7: T.Lane
93  {I.diagonal1(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
94
95def diagonal1_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
96  match v x0 x1 x2 x3 x4 x5 x6 x7:
97    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
98
99law round1_correct:
100  for +v: T.State
101  for +m0: T.Lane
102  for +m1: T.Lane
103  for +m2: T.Lane
104  for +m3: T.Lane
105  for +m4: T.Lane
106  for +m5: T.Lane
107  for +m6: T.Lane
108  for +m7: T.Lane
109  for +m8: T.Lane
110  for +m9: T.Lane
111  for +m10: T.Lane
112  for +m11: T.Lane
113  for +m12: T.Lane
114  for +m13: T.Lane
115  for +m14: T.Lane
116  for +m15: T.Lane
117  {I.round1(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)) : T.State}
118
119def round1_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
120  Equal.trans(T.State,
121    I.diagonal1(I.column1(v,m14,m10,m4,m8,m9,m15,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3),
122    I.diagonal1(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m14,m10),1n,5n,9n,13n,m4,m8),2n,6n,10n,14n,m9,m15),3n,7n,11n,15n,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3),
123    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m14,m10),1n,5n,9n,13n,m4,m8),2n,6n,10n,14n,m9,m15),3n,7n,11n,15n,m13,m6),0n,5n,10n,15n,m1,m12),1n,6n,11n,12n,m0,m2),2n,7n,8n,13n,m11,m7),3n,4n,9n,14n,m5,m3),
124    Equal.cong(T.State,T.State,t => I.diagonal1(t,m1,m12,m0,m2,m11,m7,m5,m3),I.column1(v,m14,m10,m4,m8,m9,m15,m13,m6),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m14,m10),1n,5n,9n,13n,m4,m8),2n,6n,10n,14n,m9,m15),3n,7n,11n,15n,m13,m6),column1_correct(v,m14,m10,m4,m8,m9,m15,m13,m6)),
125    diagonal1_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m14,m10),1n,5n,9n,13n,m4,m8),2n,6n,10n,14n,m9,m15),3n,7n,11n,15n,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3))
126
127law column2_correct:
128  for +v: T.State
129  for +x0: T.Lane
130  for +x1: T.Lane
131  for +x2: T.Lane
132  for +x3: T.Lane
133  for +x4: T.Lane
134  for +x5: T.Lane
135  for +x6: T.Lane
136  for +x7: T.Lane
137  {I.column2(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
138
139def column2_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
140  match v x0 x1 x2 x3 x4 x5 x6 x7:
141    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
142
143law diagonal2_correct:
144  for +v: T.State
145  for +x0: T.Lane
146  for +x1: T.Lane
147  for +x2: T.Lane
148  for +x3: T.Lane
149  for +x4: T.Lane
150  for +x5: T.Lane
151  for +x6: T.Lane
152  for +x7: T.Lane
153  {I.diagonal2(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
154
155def diagonal2_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
156  match v x0 x1 x2 x3 x4 x5 x6 x7:
157    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
158
159law round2_correct:
160  for +v: T.State
161  for +m0: T.Lane
162  for +m1: T.Lane
163  for +m2: T.Lane
164  for +m3: T.Lane
165  for +m4: T.Lane
166  for +m5: T.Lane
167  for +m6: T.Lane
168  for +m7: T.Lane
169  for +m8: T.Lane
170  for +m9: T.Lane
171  for +m10: T.Lane
172  for +m11: T.Lane
173  for +m12: T.Lane
174  for +m13: T.Lane
175  for +m14: T.Lane
176  for +m15: T.Lane
177  {I.round2(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)) : T.State}
178
179def round2_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
180  Equal.trans(T.State,
181    I.diagonal2(I.column2(v,m11,m8,m12,m0,m5,m2,m15,m13),m10,m14,m3,m6,m7,m1,m9,m4),
182    I.diagonal2(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m11,m8),1n,5n,9n,13n,m12,m0),2n,6n,10n,14n,m5,m2),3n,7n,11n,15n,m15,m13),m10,m14,m3,m6,m7,m1,m9,m4),
183    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m11,m8),1n,5n,9n,13n,m12,m0),2n,6n,10n,14n,m5,m2),3n,7n,11n,15n,m15,m13),0n,5n,10n,15n,m10,m14),1n,6n,11n,12n,m3,m6),2n,7n,8n,13n,m7,m1),3n,4n,9n,14n,m9,m4),
184    Equal.cong(T.State,T.State,t => I.diagonal2(t,m10,m14,m3,m6,m7,m1,m9,m4),I.column2(v,m11,m8,m12,m0,m5,m2,m15,m13),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m11,m8),1n,5n,9n,13n,m12,m0),2n,6n,10n,14n,m5,m2),3n,7n,11n,15n,m15,m13),column2_correct(v,m11,m8,m12,m0,m5,m2,m15,m13)),
185    diagonal2_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m11,m8),1n,5n,9n,13n,m12,m0),2n,6n,10n,14n,m5,m2),3n,7n,11n,15n,m15,m13),m10,m14,m3,m6,m7,m1,m9,m4))
186
187law column3_correct:
188  for +v: T.State
189  for +x0: T.Lane
190  for +x1: T.Lane
191  for +x2: T.Lane
192  for +x3: T.Lane
193  for +x4: T.Lane
194  for +x5: T.Lane
195  for +x6: T.Lane
196  for +x7: T.Lane
197  {I.column3(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
198
199def column3_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
200  match v x0 x1 x2 x3 x4 x5 x6 x7:
201    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
202
203law diagonal3_correct:
204  for +v: T.State
205  for +x0: T.Lane
206  for +x1: T.Lane
207  for +x2: T.Lane
208  for +x3: T.Lane
209  for +x4: T.Lane
210  for +x5: T.Lane
211  for +x6: T.Lane
212  for +x7: T.Lane
213  {I.diagonal3(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
214
215def diagonal3_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
216  match v x0 x1 x2 x3 x4 x5 x6 x7:
217    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
218
219law round3_correct:
220  for +v: T.State
221  for +m0: T.Lane
222  for +m1: T.Lane
223  for +m2: T.Lane
224  for +m3: T.Lane
225  for +m4: T.Lane
226  for +m5: T.Lane
227  for +m6: T.Lane
228  for +m7: T.Lane
229  for +m8: T.Lane
230  for +m9: T.Lane
231  for +m10: T.Lane
232  for +m11: T.Lane
233  for +m12: T.Lane
234  for +m13: T.Lane
235  for +m14: T.Lane
236  for +m15: T.Lane
237  {I.round3(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)) : T.State}
238
239def round3_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
240  Equal.trans(T.State,
241    I.diagonal3(I.column3(v,m7,m9,m3,m1,m13,m12,m11,m14),m2,m6,m5,m10,m4,m0,m15,m8),
242    I.diagonal3(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m7,m9),1n,5n,9n,13n,m3,m1),2n,6n,10n,14n,m13,m12),3n,7n,11n,15n,m11,m14),m2,m6,m5,m10,m4,m0,m15,m8),
243    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m7,m9),1n,5n,9n,13n,m3,m1),2n,6n,10n,14n,m13,m12),3n,7n,11n,15n,m11,m14),0n,5n,10n,15n,m2,m6),1n,6n,11n,12n,m5,m10),2n,7n,8n,13n,m4,m0),3n,4n,9n,14n,m15,m8),
244    Equal.cong(T.State,T.State,t => I.diagonal3(t,m2,m6,m5,m10,m4,m0,m15,m8),I.column3(v,m7,m9,m3,m1,m13,m12,m11,m14),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m7,m9),1n,5n,9n,13n,m3,m1),2n,6n,10n,14n,m13,m12),3n,7n,11n,15n,m11,m14),column3_correct(v,m7,m9,m3,m1,m13,m12,m11,m14)),
245    diagonal3_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m7,m9),1n,5n,9n,13n,m3,m1),2n,6n,10n,14n,m13,m12),3n,7n,11n,15n,m11,m14),m2,m6,m5,m10,m4,m0,m15,m8))
246
247law column4_correct:
248  for +v: T.State
249  for +x0: T.Lane
250  for +x1: T.Lane
251  for +x2: T.Lane
252  for +x3: T.Lane
253  for +x4: T.Lane
254  for +x5: T.Lane
255  for +x6: T.Lane
256  for +x7: T.Lane
257  {I.column4(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
258
259def column4_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
260  match v x0 x1 x2 x3 x4 x5 x6 x7:
261    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
262
263law diagonal4_correct:
264  for +v: T.State
265  for +x0: T.Lane
266  for +x1: T.Lane
267  for +x2: T.Lane
268  for +x3: T.Lane
269  for +x4: T.Lane
270  for +x5: T.Lane
271  for +x6: T.Lane
272  for +x7: T.Lane
273  {I.diagonal4(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
274
275def diagonal4_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
276  match v x0 x1 x2 x3 x4 x5 x6 x7:
277    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
278
279law round4_correct:
280  for +v: T.State
281  for +m0: T.Lane
282  for +m1: T.Lane
283  for +m2: T.Lane
284  for +m3: T.Lane
285  for +m4: T.Lane
286  for +m5: T.Lane
287  for +m6: T.Lane
288  for +m7: T.Lane
289  for +m8: T.Lane
290  for +m9: T.Lane
291  for +m10: T.Lane
292  for +m11: T.Lane
293  for +m12: T.Lane
294  for +m13: T.Lane
295  for +m14: T.Lane
296  for +m15: T.Lane
297  {I.round4(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)) : T.State}
298
299def round4_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
300  Equal.trans(T.State,
301    I.diagonal4(I.column4(v,m9,m0,m5,m7,m2,m4,m10,m15),m14,m1,m11,m12,m6,m8,m3,m13),
302    I.diagonal4(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m9,m0),1n,5n,9n,13n,m5,m7),2n,6n,10n,14n,m2,m4),3n,7n,11n,15n,m10,m15),m14,m1,m11,m12,m6,m8,m3,m13),
303    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m9,m0),1n,5n,9n,13n,m5,m7),2n,6n,10n,14n,m2,m4),3n,7n,11n,15n,m10,m15),0n,5n,10n,15n,m14,m1),1n,6n,11n,12n,m11,m12),2n,7n,8n,13n,m6,m8),3n,4n,9n,14n,m3,m13),
304    Equal.cong(T.State,T.State,t => I.diagonal4(t,m14,m1,m11,m12,m6,m8,m3,m13),I.column4(v,m9,m0,m5,m7,m2,m4,m10,m15),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m9,m0),1n,5n,9n,13n,m5,m7),2n,6n,10n,14n,m2,m4),3n,7n,11n,15n,m10,m15),column4_correct(v,m9,m0,m5,m7,m2,m4,m10,m15)),
305    diagonal4_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m9,m0),1n,5n,9n,13n,m5,m7),2n,6n,10n,14n,m2,m4),3n,7n,11n,15n,m10,m15),m14,m1,m11,m12,m6,m8,m3,m13))
306
307law column5_correct:
308  for +v: T.State
309  for +x0: T.Lane
310  for +x1: T.Lane
311  for +x2: T.Lane
312  for +x3: T.Lane
313  for +x4: T.Lane
314  for +x5: T.Lane
315  for +x6: T.Lane
316  for +x7: T.Lane
317  {I.column5(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
318
319def column5_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
320  match v x0 x1 x2 x3 x4 x5 x6 x7:
321    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
322
323law diagonal5_correct:
324  for +v: T.State
325  for +x0: T.Lane
326  for +x1: T.Lane
327  for +x2: T.Lane
328  for +x3: T.Lane
329  for +x4: T.Lane
330  for +x5: T.Lane
331  for +x6: T.Lane
332  for +x7: T.Lane
333  {I.diagonal5(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
334
335def diagonal5_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
336  match v x0 x1 x2 x3 x4 x5 x6 x7:
337    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
338
339law round5_correct:
340  for +v: T.State
341  for +m0: T.Lane
342  for +m1: T.Lane
343  for +m2: T.Lane
344  for +m3: T.Lane
345  for +m4: T.Lane
346  for +m5: T.Lane
347  for +m6: T.Lane
348  for +m7: T.Lane
349  for +m8: T.Lane
350  for +m9: T.Lane
351  for +m10: T.Lane
352  for +m11: T.Lane
353  for +m12: T.Lane
354  for +m13: T.Lane
355  for +m14: T.Lane
356  for +m15: T.Lane
357  {I.round5(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)) : T.State}
358
359def round5_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
360  Equal.trans(T.State,
361    I.diagonal5(I.column5(v,m2,m12,m6,m10,m0,m11,m8,m3),m4,m13,m7,m5,m15,m14,m1,m9),
362    I.diagonal5(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m2,m12),1n,5n,9n,13n,m6,m10),2n,6n,10n,14n,m0,m11),3n,7n,11n,15n,m8,m3),m4,m13,m7,m5,m15,m14,m1,m9),
363    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m2,m12),1n,5n,9n,13n,m6,m10),2n,6n,10n,14n,m0,m11),3n,7n,11n,15n,m8,m3),0n,5n,10n,15n,m4,m13),1n,6n,11n,12n,m7,m5),2n,7n,8n,13n,m15,m14),3n,4n,9n,14n,m1,m9),
364    Equal.cong(T.State,T.State,t => I.diagonal5(t,m4,m13,m7,m5,m15,m14,m1,m9),I.column5(v,m2,m12,m6,m10,m0,m11,m8,m3),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m2,m12),1n,5n,9n,13n,m6,m10),2n,6n,10n,14n,m0,m11),3n,7n,11n,15n,m8,m3),column5_correct(v,m2,m12,m6,m10,m0,m11,m8,m3)),
365    diagonal5_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m2,m12),1n,5n,9n,13n,m6,m10),2n,6n,10n,14n,m0,m11),3n,7n,11n,15n,m8,m3),m4,m13,m7,m5,m15,m14,m1,m9))
366
367law column6_correct:
368  for +v: T.State
369  for +x0: T.Lane
370  for +x1: T.Lane
371  for +x2: T.Lane
372  for +x3: T.Lane
373  for +x4: T.Lane
374  for +x5: T.Lane
375  for +x6: T.Lane
376  for +x7: T.Lane
377  {I.column6(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
378
379def column6_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
380  match v x0 x1 x2 x3 x4 x5 x6 x7:
381    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
382
383law diagonal6_correct:
384  for +v: T.State
385  for +x0: T.Lane
386  for +x1: T.Lane
387  for +x2: T.Lane
388  for +x3: T.Lane
389  for +x4: T.Lane
390  for +x5: T.Lane
391  for +x6: T.Lane
392  for +x7: T.Lane
393  {I.diagonal6(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
394
395def diagonal6_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
396  match v x0 x1 x2 x3 x4 x5 x6 x7:
397    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
398
399law round6_correct:
400  for +v: T.State
401  for +m0: T.Lane
402  for +m1: T.Lane
403  for +m2: T.Lane
404  for +m3: T.Lane
405  for +m4: T.Lane
406  for +m5: T.Lane
407  for +m6: T.Lane
408  for +m7: T.Lane
409  for +m8: T.Lane
410  for +m9: T.Lane
411  for +m10: T.Lane
412  for +m11: T.Lane
413  for +m12: T.Lane
414  for +m13: T.Lane
415  for +m14: T.Lane
416  for +m15: T.Lane
417  {I.round6(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)) : T.State}
418
419def round6_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
420  Equal.trans(T.State,
421    I.diagonal6(I.column6(v,m12,m5,m1,m15,m14,m13,m4,m10),m0,m7,m6,m3,m9,m2,m8,m11),
422    I.diagonal6(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m12,m5),1n,5n,9n,13n,m1,m15),2n,6n,10n,14n,m14,m13),3n,7n,11n,15n,m4,m10),m0,m7,m6,m3,m9,m2,m8,m11),
423    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m12,m5),1n,5n,9n,13n,m1,m15),2n,6n,10n,14n,m14,m13),3n,7n,11n,15n,m4,m10),0n,5n,10n,15n,m0,m7),1n,6n,11n,12n,m6,m3),2n,7n,8n,13n,m9,m2),3n,4n,9n,14n,m8,m11),
424    Equal.cong(T.State,T.State,t => I.diagonal6(t,m0,m7,m6,m3,m9,m2,m8,m11),I.column6(v,m12,m5,m1,m15,m14,m13,m4,m10),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m12,m5),1n,5n,9n,13n,m1,m15),2n,6n,10n,14n,m14,m13),3n,7n,11n,15n,m4,m10),column6_correct(v,m12,m5,m1,m15,m14,m13,m4,m10)),
425    diagonal6_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m12,m5),1n,5n,9n,13n,m1,m15),2n,6n,10n,14n,m14,m13),3n,7n,11n,15n,m4,m10),m0,m7,m6,m3,m9,m2,m8,m11))
426
427law column7_correct:
428  for +v: T.State
429  for +x0: T.Lane
430  for +x1: T.Lane
431  for +x2: T.Lane
432  for +x3: T.Lane
433  for +x4: T.Lane
434  for +x5: T.Lane
435  for +x6: T.Lane
436  for +x7: T.Lane
437  {I.column7(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
438
439def column7_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
440  match v x0 x1 x2 x3 x4 x5 x6 x7:
441    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
442
443law diagonal7_correct:
444  for +v: T.State
445  for +x0: T.Lane
446  for +x1: T.Lane
447  for +x2: T.Lane
448  for +x3: T.Lane
449  for +x4: T.Lane
450  for +x5: T.Lane
451  for +x6: T.Lane
452  for +x7: T.Lane
453  {I.diagonal7(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
454
455def diagonal7_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
456  match v x0 x1 x2 x3 x4 x5 x6 x7:
457    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
458
459law round7_correct:
460  for +v: T.State
461  for +m0: T.Lane
462  for +m1: T.Lane
463  for +m2: T.Lane
464  for +m3: T.Lane
465  for +m4: T.Lane
466  for +m5: T.Lane
467  for +m6: T.Lane
468  for +m7: T.Lane
469  for +m8: T.Lane
470  for +m9: T.Lane
471  for +m10: T.Lane
472  for +m11: T.Lane
473  for +m12: T.Lane
474  for +m13: T.Lane
475  for +m14: T.Lane
476  for +m15: T.Lane
477  {I.round7(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)) : T.State}
478
479def round7_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
480  Equal.trans(T.State,
481    I.diagonal7(I.column7(v,m13,m11,m7,m14,m12,m1,m3,m9),m5,m0,m15,m4,m8,m6,m2,m10),
482    I.diagonal7(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m13,m11),1n,5n,9n,13n,m7,m14),2n,6n,10n,14n,m12,m1),3n,7n,11n,15n,m3,m9),m5,m0,m15,m4,m8,m6,m2,m10),
483    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m13,m11),1n,5n,9n,13n,m7,m14),2n,6n,10n,14n,m12,m1),3n,7n,11n,15n,m3,m9),0n,5n,10n,15n,m5,m0),1n,6n,11n,12n,m15,m4),2n,7n,8n,13n,m8,m6),3n,4n,9n,14n,m2,m10),
484    Equal.cong(T.State,T.State,t => I.diagonal7(t,m5,m0,m15,m4,m8,m6,m2,m10),I.column7(v,m13,m11,m7,m14,m12,m1,m3,m9),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m13,m11),1n,5n,9n,13n,m7,m14),2n,6n,10n,14n,m12,m1),3n,7n,11n,15n,m3,m9),column7_correct(v,m13,m11,m7,m14,m12,m1,m3,m9)),
485    diagonal7_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m13,m11),1n,5n,9n,13n,m7,m14),2n,6n,10n,14n,m12,m1),3n,7n,11n,15n,m3,m9),m5,m0,m15,m4,m8,m6,m2,m10))
486
487law column8_correct:
488  for +v: T.State
489  for +x0: T.Lane
490  for +x1: T.Lane
491  for +x2: T.Lane
492  for +x3: T.Lane
493  for +x4: T.Lane
494  for +x5: T.Lane
495  for +x6: T.Lane
496  for +x7: T.Lane
497  {I.column8(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
498
499def column8_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
500  match v x0 x1 x2 x3 x4 x5 x6 x7:
501    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
502
503law diagonal8_correct:
504  for +v: T.State
505  for +x0: T.Lane
506  for +x1: T.Lane
507  for +x2: T.Lane
508  for +x3: T.Lane
509  for +x4: T.Lane
510  for +x5: T.Lane
511  for +x6: T.Lane
512  for +x7: T.Lane
513  {I.diagonal8(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
514
515def diagonal8_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
516  match v x0 x1 x2 x3 x4 x5 x6 x7:
517    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
518
519law round8_correct:
520  for +v: T.State
521  for +m0: T.Lane
522  for +m1: T.Lane
523  for +m2: T.Lane
524  for +m3: T.Lane
525  for +m4: T.Lane
526  for +m5: T.Lane
527  for +m6: T.Lane
528  for +m7: T.Lane
529  for +m8: T.Lane
530  for +m9: T.Lane
531  for +m10: T.Lane
532  for +m11: T.Lane
533  for +m12: T.Lane
534  for +m13: T.Lane
535  for +m14: T.Lane
536  for +m15: T.Lane
537  {I.round8(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)) : T.State}
538
539def round8_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
540  Equal.trans(T.State,
541    I.diagonal8(I.column8(v,m6,m15,m14,m9,m11,m3,m0,m8),m12,m2,m13,m7,m1,m4,m10,m5),
542    I.diagonal8(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m6,m15),1n,5n,9n,13n,m14,m9),2n,6n,10n,14n,m11,m3),3n,7n,11n,15n,m0,m8),m12,m2,m13,m7,m1,m4,m10,m5),
543    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m6,m15),1n,5n,9n,13n,m14,m9),2n,6n,10n,14n,m11,m3),3n,7n,11n,15n,m0,m8),0n,5n,10n,15n,m12,m2),1n,6n,11n,12n,m13,m7),2n,7n,8n,13n,m1,m4),3n,4n,9n,14n,m10,m5),
544    Equal.cong(T.State,T.State,t => I.diagonal8(t,m12,m2,m13,m7,m1,m4,m10,m5),I.column8(v,m6,m15,m14,m9,m11,m3,m0,m8),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m6,m15),1n,5n,9n,13n,m14,m9),2n,6n,10n,14n,m11,m3),3n,7n,11n,15n,m0,m8),column8_correct(v,m6,m15,m14,m9,m11,m3,m0,m8)),
545    diagonal8_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m6,m15),1n,5n,9n,13n,m14,m9),2n,6n,10n,14n,m11,m3),3n,7n,11n,15n,m0,m8),m12,m2,m13,m7,m1,m4,m10,m5))
546
547law column9_correct:
548  for +v: T.State
549  for +x0: T.Lane
550  for +x1: T.Lane
551  for +x2: T.Lane
552  for +x3: T.Lane
553  for +x4: T.Lane
554  for +x5: T.Lane
555  for +x6: T.Lane
556  for +x7: T.Lane
557  {I.column9(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
558
559def column9_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
560  match v x0 x1 x2 x3 x4 x5 x6 x7:
561    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
562
563law diagonal9_correct:
564  for +v: T.State
565  for +x0: T.Lane
566  for +x1: T.Lane
567  for +x2: T.Lane
568  for +x3: T.Lane
569  for +x4: T.Lane
570  for +x5: T.Lane
571  for +x6: T.Lane
572  for +x7: T.Lane
573  {I.diagonal9(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
574
575def diagonal9_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
576  match v x0 x1 x2 x3 x4 x5 x6 x7:
577    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
578
579law round9_correct:
580  for +v: T.State
581  for +m0: T.Lane
582  for +m1: T.Lane
583  for +m2: T.Lane
584  for +m3: T.Lane
585  for +m4: T.Lane
586  for +m5: T.Lane
587  for +m6: T.Lane
588  for +m7: T.Lane
589  for +m8: T.Lane
590  for +m9: T.Lane
591  for +m10: T.Lane
592  for +m11: T.Lane
593  for +m12: T.Lane
594  for +m13: T.Lane
595  for +m14: T.Lane
596  for +m15: T.Lane
597  {I.round9(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)) : T.State}
598
599def round9_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
600  Equal.trans(T.State,
601    I.diagonal9(I.column9(v,m10,m2,m8,m4,m7,m6,m1,m5),m15,m11,m9,m14,m3,m12,m13,m0),
602    I.diagonal9(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m10,m2),1n,5n,9n,13n,m8,m4),2n,6n,10n,14n,m7,m6),3n,7n,11n,15n,m1,m5),m15,m11,m9,m14,m3,m12,m13,m0),
603    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m10,m2),1n,5n,9n,13n,m8,m4),2n,6n,10n,14n,m7,m6),3n,7n,11n,15n,m1,m5),0n,5n,10n,15n,m15,m11),1n,6n,11n,12n,m9,m14),2n,7n,8n,13n,m3,m12),3n,4n,9n,14n,m13,m0),
604    Equal.cong(T.State,T.State,t => I.diagonal9(t,m15,m11,m9,m14,m3,m12,m13,m0),I.column9(v,m10,m2,m8,m4,m7,m6,m1,m5),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m10,m2),1n,5n,9n,13n,m8,m4),2n,6n,10n,14n,m7,m6),3n,7n,11n,15n,m1,m5),column9_correct(v,m10,m2,m8,m4,m7,m6,m1,m5)),
605    diagonal9_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m10,m2),1n,5n,9n,13n,m8,m4),2n,6n,10n,14n,m7,m6),3n,7n,11n,15n,m1,m5),m15,m11,m9,m14,m3,m12,m13,m0))
606
607law column10_correct:
608  for +v: T.State
609  for +x0: T.Lane
610  for +x1: T.Lane
611  for +x2: T.Lane
612  for +x3: T.Lane
613  for +x4: T.Lane
614  for +x5: T.Lane
615  for +x6: T.Lane
616  for +x7: T.Lane
617  {I.column10(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
618
619def column10_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
620  match v x0 x1 x2 x3 x4 x5 x6 x7:
621    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
622
623law diagonal10_correct:
624  for +v: T.State
625  for +x0: T.Lane
626  for +x1: T.Lane
627  for +x2: T.Lane
628  for +x3: T.Lane
629  for +x4: T.Lane
630  for +x5: T.Lane
631  for +x6: T.Lane
632  for +x7: T.Lane
633  {I.diagonal10(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
634
635def diagonal10_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
636  match v x0 x1 x2 x3 x4 x5 x6 x7:
637    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
638
639law round10_correct:
640  for +v: T.State
641  for +m0: T.Lane
642  for +m1: T.Lane
643  for +m2: T.Lane
644  for +m3: T.Lane
645  for +m4: T.Lane
646  for +m5: T.Lane
647  for +m6: T.Lane
648  for +m7: T.Lane
649  for +m8: T.Lane
650  for +m9: T.Lane
651  for +m10: T.Lane
652  for +m11: T.Lane
653  for +m12: T.Lane
654  for +m13: T.Lane
655  for +m14: T.Lane
656  for +m15: T.Lane
657  {I.round10(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)) : T.State}
658
659def round10_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
660  Equal.trans(T.State,
661    I.diagonal10(I.column10(v,m0,m1,m2,m3,m4,m5,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15),
662    I.diagonal10(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m0,m1),1n,5n,9n,13n,m2,m3),2n,6n,10n,14n,m4,m5),3n,7n,11n,15n,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15),
663    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m0,m1),1n,5n,9n,13n,m2,m3),2n,6n,10n,14n,m4,m5),3n,7n,11n,15n,m6,m7),0n,5n,10n,15n,m8,m9),1n,6n,11n,12n,m10,m11),2n,7n,8n,13n,m12,m13),3n,4n,9n,14n,m14,m15),
664    Equal.cong(T.State,T.State,t => I.diagonal10(t,m8,m9,m10,m11,m12,m13,m14,m15),I.column10(v,m0,m1,m2,m3,m4,m5,m6,m7),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m0,m1),1n,5n,9n,13n,m2,m3),2n,6n,10n,14n,m4,m5),3n,7n,11n,15n,m6,m7),column10_correct(v,m0,m1,m2,m3,m4,m5,m6,m7)),
665    diagonal10_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m0,m1),1n,5n,9n,13n,m2,m3),2n,6n,10n,14n,m4,m5),3n,7n,11n,15n,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15))
666
667law column11_correct:
668  for +v: T.State
669  for +x0: T.Lane
670  for +x1: T.Lane
671  for +x2: T.Lane
672  for +x3: T.Lane
673  for +x4: T.Lane
674  for +x5: T.Lane
675  for +x6: T.Lane
676  for +x7: T.Lane
677  {I.column11(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}
678
679def column11_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
680  match v x0 x1 x2 x3 x4 x5 x6 x7:
681    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
682
683law diagonal11_correct:
684  for +v: T.State
685  for +x0: T.Lane
686  for +x1: T.Lane
687  for +x2: T.Lane
688  for +x3: T.Lane
689  for +x4: T.Lane
690  for +x5: T.Lane
691  for +x6: T.Lane
692  for +x7: T.Lane
693  {I.diagonal11(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}
694
695def diagonal11_correct(v,x0,x1,x2,x3,x4,x5,x6,x7):
696  match v x0 x1 x2 x3 x4 x5 x6 x7:
697    case T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}} T.W{p0,q0} T.W{p1,q1} T.W{p2,q2} T.W{p3,q3} T.W{p4,q4} T.W{p5,q5} T.W{p6,q6} T.W{p7,q7}: {==}
698
699law round11_correct:
700  for +v: T.State
701  for +m0: T.Lane
702  for +m1: T.Lane
703  for +m2: T.Lane
704  for +m3: T.Lane
705  for +m4: T.Lane
706  for +m5: T.Lane
707  for +m6: T.Lane
708  for +m7: T.Lane
709  for +m8: T.Lane
710  for +m9: T.Lane
711  for +m10: T.Lane
712  for +m11: T.Lane
713  for +m12: T.Lane
714  for +m13: T.Lane
715  for +m14: T.Lane
716  for +m15: T.Lane
717  {I.round11(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)) : T.State}
718
719def round11_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
720  Equal.trans(T.State,
721    I.diagonal11(I.column11(v,m14,m10,m4,m8,m9,m15,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3),
722    I.diagonal11(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m14,m10),1n,5n,9n,13n,m4,m8),2n,6n,10n,14n,m9,m15),3n,7n,11n,15n,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3),
723    S.G(S.G(S.G(S.G(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m14,m10),1n,5n,9n,13n,m4,m8),2n,6n,10n,14n,m9,m15),3n,7n,11n,15n,m13,m6),0n,5n,10n,15n,m1,m12),1n,6n,11n,12n,m0,m2),2n,7n,8n,13n,m11,m7),3n,4n,9n,14n,m5,m3),
724    Equal.cong(T.State,T.State,t => I.diagonal11(t,m1,m12,m0,m2,m11,m7,m5,m3),I.column11(v,m14,m10,m4,m8,m9,m15,m13,m6),S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m14,m10),1n,5n,9n,13n,m4,m8),2n,6n,10n,14n,m9,m15),3n,7n,11n,15n,m13,m6),column11_correct(v,m14,m10,m4,m8,m9,m15,m13,m6)),
725    diagonal11_correct(S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,m14,m10),1n,5n,9n,13n,m4,m8),2n,6n,10n,14n,m9,m15),3n,7n,11n,15n,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3))
726
727law rounds_correct:
728  for +v: T.State
729  for +m0: T.Lane
730  for +m1: T.Lane
731  for +m2: T.Lane
732  for +m3: T.Lane
733  for +m4: T.Lane
734  for +m5: T.Lane
735  for +m6: T.Lane
736  for +m7: T.Lane
737  for +m8: T.Lane
738  for +m9: T.Lane
739  for +m10: T.Lane
740  for +m11: T.Lane
741  for +m12: T.Lane
742  for +m13: T.Lane
743  for +m14: T.Lane
744  for +m15: T.Lane
745  {I.rounds(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.rounds(12n,0n,v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : T.State}
746
747def rounds_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15):
748  Equal.trans(T.State,I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(I.round2(I.round1(I.round0(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(I.round2(I.round1(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
749    Equal.cong(T.State,T.State,x => I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(I.round2(I.round1(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round0(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),round0_correct(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
750    Equal.trans(T.State,I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(I.round2(I.round1(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(I.round2(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
751    Equal.cong(T.State,T.State,x => I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(I.round2(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round1(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),round1_correct(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
752    Equal.trans(T.State,I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(I.round2(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
753    Equal.cong(T.State,T.State,x => I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round2(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),round2_correct(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
754    Equal.trans(T.State,I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(I.round3(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
755    Equal.cong(T.State,T.State,x => I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round3(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),round3_correct(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
756    Equal.trans(T.State,I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(I.round4(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
757    Equal.cong(T.State,T.State,x => I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round4(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),round4_correct(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
758    Equal.trans(T.State,I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(I.round5(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
759    Equal.cong(T.State,T.State,x => I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round5(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),round5_correct(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
760    Equal.trans(T.State,I.round11(I.round10(I.round9(I.round8(I.round7(I.round6(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(I.round9(I.round8(I.round7(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
761    Equal.cong(T.State,T.State,x => I.round11(I.round10(I.round9(I.round8(I.round7(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round6(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),round6_correct(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
762    Equal.trans(T.State,I.round11(I.round10(I.round9(I.round8(I.round7(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(I.round9(I.round8(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
763    Equal.cong(T.State,T.State,x => I.round11(I.round10(I.round9(I.round8(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round7(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),round7_correct(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
764    Equal.trans(T.State,I.round11(I.round10(I.round9(I.round8(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(I.round9(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
765    Equal.cong(T.State,T.State,x => I.round11(I.round10(I.round9(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round8(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),round8_correct(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
766    Equal.trans(T.State,I.round11(I.round10(I.round9(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(I.round10(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
767    Equal.cong(T.State,T.State,x => I.round11(I.round10(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round9(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),round9_correct(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
768    Equal.trans(T.State,I.round11(I.round10(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round11(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),
769    Equal.cong(T.State,T.State,x => I.round11(x,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),I.round10(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),round10_correct(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)),
770    round11_correct(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(1n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(2n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(3n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(4n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(5n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(6n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(8n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(9n)),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(0n)),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15))))))))))))
771
772law start_correct:
773  for +h: T.Chain
774  for +t: T.Counter
775  {I.start(h,t) == S.start(h,t,False{}) : T.State}
776
777def start_correct(h,t):
778  match h t:
779    case T.H{T.W{g0,e0},T.W{g1,e1},T.W{g2,e2},T.W{g3,e3},T.W{g4,e4},T.W{g5,e5},T.W{g6,e6},T.W{g7,e7}} T.C{t0,t1,t2,t3}: {==}
780
781law start_last_correct:
782  for +h: T.Chain
783  for +t: T.Counter
784  {I.start_last(h,t) == S.start(h,t,True{}) : T.State}
785
786def start_last_correct(h,t):
787  match h t:
788    case T.H{T.W{g0,e0},T.W{g1,e1},T.W{g2,e2},T.W{g3,e3},T.W{g4,e4},T.W{g5,e5},T.W{g6,e6},T.W{g7,e7}} T.C{t0,t1,t2,t3}: {==}
789
790law finish_correct:
791  for +h: T.Chain
792  for +v: T.State
793  {I.finish(h,v) == S.finish(h,v) : T.Chain}
794
795def finish_correct(h,v):
796  match h v:
797    case T.H{T.W{g0,e0},T.W{g1,e1},T.W{g2,e2},T.W{g3,e3},T.W{g4,e4},T.W{g5,e5},T.W{g6,e6},T.W{g7,e7}} T.V{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7},T.W{l8,u8},T.W{l9,u9},T.W{l10,u10},T.W{l11,u11},T.W{l12,u12},T.W{l13,u13},T.W{l14,u14},T.W{l15,u15}}: {==}
798
799law compress_correct:
800  for +h: T.Chain
801  for +t: T.Counter
802  for +w0: U32
803  for +w1: U32
804  for +w2: U32
805  for +w3: U32
806  for +w4: U32
807  for +w5: U32
808  for +w6: U32
809  for +w7: U32
810  for +w8: U32
811  for +w9: U32
812  for +w10: U32
813  for +w11: U32
814  for +w12: U32
815  for +w13: U32
816  for +w14: U32
817  for +w15: U32
818  for +w16: U32
819  for +w17: U32
820  for +w18: U32
821  for +w19: U32
822  for +w20: U32
823  for +w21: U32
824  for +w22: U32
825  for +w23: U32
826  for +w24: U32
827  for +w25: U32
828  for +w26: U32
829  for +w27: U32
830  for +w28: U32
831  for +w29: U32
832  for +w30: U32
833  for +w31: U32
834  {I.compress(h,t,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31) == S.compress(h,[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}],t,False{}) : T.Chain}
835
836def compress_correct(h,t,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31):
837  Equal.trans(T.Chain,I.finish(h,I.rounds(I.start(h,t),T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31})),I.finish(h,S.rounds(12n,0n,I.start(h,t),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),S.finish(h,S.rounds(12n,0n,S.start(h,t,False{}),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),
838    Equal.cong(T.State,T.Chain,x => I.finish(h,x),I.rounds(I.start(h,t),T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}),S.rounds(12n,0n,I.start(h,t),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}]),rounds_correct(I.start(h,t),T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31})),
839    Equal.trans(T.Chain,I.finish(h,S.rounds(12n,0n,I.start(h,t),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),I.finish(h,S.rounds(12n,0n,S.start(h,t,False{}),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),S.finish(h,S.rounds(12n,0n,S.start(h,t,False{}),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),
840      Equal.cong(T.State,T.Chain,x => I.finish(h,S.rounds(12n,0n,x,[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),I.start(h,t),S.start(h,t,False{}),start_correct(h,t)),
841      finish_correct(h,S.rounds(12n,0n,S.start(h,t,False{}),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}]))))
842
843law compress_last_correct:
844  for +h: T.Chain
845  for +t: T.Counter
846  for +w0: U32
847  for +w1: U32
848  for +w2: U32
849  for +w3: U32
850  for +w4: U32
851  for +w5: U32
852  for +w6: U32
853  for +w7: U32
854  for +w8: U32
855  for +w9: U32
856  for +w10: U32
857  for +w11: U32
858  for +w12: U32
859  for +w13: U32
860  for +w14: U32
861  for +w15: U32
862  for +w16: U32
863  for +w17: U32
864  for +w18: U32
865  for +w19: U32
866  for +w20: U32
867  for +w21: U32
868  for +w22: U32
869  for +w23: U32
870  for +w24: U32
871  for +w25: U32
872  for +w26: U32
873  for +w27: U32
874  for +w28: U32
875  for +w29: U32
876  for +w30: U32
877  for +w31: U32
878  {I.compress_last(h,t,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31) == S.compress(h,[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}],t,True{}) : T.Chain}
879
880def compress_last_correct(h,t,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31):
881  Equal.trans(T.Chain,I.finish(h,I.rounds(I.start_last(h,t),T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31})),I.finish(h,S.rounds(12n,0n,I.start_last(h,t),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),S.finish(h,S.rounds(12n,0n,S.start(h,t,True{}),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),
882    Equal.cong(T.State,T.Chain,x => I.finish(h,x),I.rounds(I.start_last(h,t),T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}),S.rounds(12n,0n,I.start_last(h,t),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}]),rounds_correct(I.start_last(h,t),T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31})),
883    Equal.trans(T.Chain,I.finish(h,S.rounds(12n,0n,I.start_last(h,t),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),I.finish(h,S.rounds(12n,0n,S.start(h,t,True{}),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),S.finish(h,S.rounds(12n,0n,S.start(h,t,True{}),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),
884      Equal.cong(T.State,T.Chain,x => I.finish(h,S.rounds(12n,0n,x,[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}])),I.start_last(h,t),S.start(h,t,True{}),start_last_correct(h,t)),
885      finish_correct(h,S.rounds(12n,0n,S.start(h,t,True{}),[T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}]))))
886
887law bump_correct:
888  for +c: T.Counter
889  for +x: U32
890  {I.bump(c,x) == S.advance(c,x) : T.Counter}
891
892def bump_correct(c,x):
893  match c:
894    case T.C{c0,c1,c2,c3}: {==}