law bits32

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake2s/bytes.bend:10

import Base

10# Two words are equal when their digits are.
11law bits32:
12  for -y0: Bool
13  for -y1: Bool
14  for -y2: Bool
15  for -y3: Bool
16  for -y4: Bool
17  for -y5: Bool
18  for -y6: Bool
19  for -y7: Bool
20  for -y8: Bool
21  for -y9: Bool
22  for -y10: Bool
23  for -y11: Bool
24  for -y12: Bool
25  for -y13: Bool
26  for -y14: Bool
27  for -y15: Bool
28  for -y16: Bool
29  for -y17: Bool
30  for -y18: Bool
31  for -y19: Bool
32  for -y20: Bool
33  for -y21: Bool
34  for -y22: Bool
35  for -y23: Bool
36  for -y24: Bool
37  for -y25: Bool
38  for -y26: Bool
39  for -y27: Bool
40  for -y28: Bool
41  for -y29: Bool
42  for -y30: Bool
43  for -y31: Bool
44  for -z0: Bool
45  for -z1: Bool
46  for -z2: Bool
47  for -z3: Bool
48  for -z4: Bool
49  for -z5: Bool
50  for -z6: Bool
51  for -z7: Bool
52  for -z8: Bool
53  for -z9: Bool
54  for -z10: Bool
55  for -z11: Bool
56  for -z12: Bool
57  for -z13: Bool
58  for -z14: Bool
59  for -z15: Bool
60  for -z16: Bool
61  for -z17: Bool
62  for -z18: Bool
63  for -z19: Bool
64  for -z20: Bool
65  for -z21: Bool
66  for -z22: Bool
67  for -z23: Bool
68  for -z24: Bool
69  for -z25: Bool
70  for -z26: Bool
71  for -z27: Bool
72  for -z28: Bool
73  for -z29: Bool
74  for -z30: Bool
75  for -z31: Bool
76  for e0: {y0 == z0 : Bool}
77  for e1: {y1 == z1 : Bool}
78  for e2: {y2 == z2 : Bool}
79  for e3: {y3 == z3 : Bool}
80  for e4: {y4 == z4 : Bool}
81  for e5: {y5 == z5 : Bool}
82  for e6: {y6 == z6 : Bool}
83  for e7: {y7 == z7 : Bool}
84  for e8: {y8 == z8 : Bool}
85  for e9: {y9 == z9 : Bool}
86  for e10: {y10 == z10 : Bool}
87  for e11: {y11 == z11 : Bool}
88  for e12: {y12 == z12 : Bool}
89  for e13: {y13 == z13 : Bool}
90  for e14: {y14 == z14 : Bool}
91  for e15: {y15 == z15 : Bool}
92  for e16: {y16 == z16 : Bool}
93  for e17: {y17 == z17 : Bool}
94  for e18: {y18 == z18 : Bool}
95  for e19: {y19 == z19 : Bool}
96  for e20: {y20 == z20 : Bool}
97  for e21: {y21 == z21 : Bool}
98  for e22: {y22 == z22 : Bool}
99  for e23: {y23 == z23 : Bool}
100  for e24: {y24 == z24 : Bool}
101  for e25: {y25 == z25 : Bool}
102  for e26: {y26 == z26 : Bool}
103  for e27: {y27 == z27 : Bool}
104  for e28: {y28 == z28 : Bool}
105  for e29: {y29 == z29 : Bool}
106  for e30: {y30 == z30 : Bool}
107  for e31: {y31 == z31 : Bool}
108  {U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{z0, WCon{z1, WCon{z2, WCon{z3, WCon{z4, WCon{z5, WCon{z6, WCon{z7, WCon{z8, WCon{z9, WCon{z10, WCon{z11, WCon{z12, WCon{z13, WCon{z14, WCon{z15, WCon{z16, WCon{z17, WCon{z18, WCon{z19, WCon{z20, WCon{z21, WCon{z22, WCon{z23, WCon{z24, WCon{z25, WCon{z26, WCon{z27, WCon{z28, WCon{z29, WCon{z30, WCon{z31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}