1 # Generated by tools/generators/blake2b_gen.py; do not edit by hand. 2 import Base 3 import ../../../../src/crypto/blake/blake2b/types.bend as T 4 import ../../../../src/crypto/blake/blake2b/compress.bend as I 5 import ../../../../spec/crypto/blake/blake2b.bend as S 6 7 law 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 19 def 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 23 law 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 35 def 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 39 law 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 59 def 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 67 law 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 79 def 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 83 law 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 95 def 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 99 law 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 119 def 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 127 law 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 139 def 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 143 law 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 155 def 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 159 law 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 179 def 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 187 law 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 199 def 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 203 law 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 215 def 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 219 law 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 239 def 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 247 law 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 259 def 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 263 law 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 275 def 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 279 law 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 299 def 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 307 law 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 319 def 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 323 law 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 335 def 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 339 law 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 359 def 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 367 law 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 379 def 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 383 law 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 395 def 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 399 law 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 419 def 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 427 law 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 439 def 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 443 law 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 455 def 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 459 law 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 479 def 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 487 law 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 499 def 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 503 law 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 515 def 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 519 law 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 539 def 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 547 law 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 559 def 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 563 law 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 575 def 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 579 law 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 599 def 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 607 law 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 619 def 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 623 law 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 635 def 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 639 law 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 659 def 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 667 law 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 679 def 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 683 law 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 695 def 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 699 law 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 719 def 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 727 law 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 747 def 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, 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, 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.sigm 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,m 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, 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,m1 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 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)),[ 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 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,m 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 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 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,m 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.sigm 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,m 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 772 law 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 777 def 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 781 law 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 786 def 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 790 law finish_correct: 791 for +h: T.Chain 792 for +v: T.State 793 {I.finish(h,v) == S.finish(h,v) : T.Chain} 794 795 def 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 799 law 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 836 def 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 843 law 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 880 def 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 887 law bump_correct: 888 for +c: T.Counter 889 for +x: U32 890 {I.bump(c,x) == S.advance(c,x) : T.Counter} 891 892 def bump_correct(c,x): 893 match c: 894 case T.C{c0,c1,c2,c3}: {==}