def zeros13

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fieldpow.bend:104

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

104def zeros13(+one: Nat) -> {FS.digits(one, [0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]) == 0n : Nat}:
105  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
106  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
107  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
108  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
109  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
110  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
111  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
112  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
113  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
114  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
115  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
116  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
117  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, 0n)))))))))))))))))))))))))) == 0n : Nat}
118  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))))))))))))))) == 0n : Nat}
119  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))))))))))))))) == 0n : Nat}
120  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))))))))))))) == 0n : Nat}
121  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))))))))))))) == 0n : Nat}
122  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))))))))))) == 0n : Nat}
123  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))))))))))) == 0n : Nat}
124  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))))))))) == 0n : Nat}
125  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))))))))) == 0n : Nat}
126  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))))))) == 0n : Nat}
127  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))))))) == 0n : Nat}
128  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))))) == 0n : Nat}
129  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))))) == 0n : Nat}
130  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))) == 0n : Nat}
131  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))) == 0n : Nat}
132  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))) == 0n : Nat}
133  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))) == 0n : Nat}
134  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))) == 0n : Nat}
135  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))) == 0n : Nat}
136  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))) == 0n : Nat}
137  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))) == 0n : Nat}
138  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))) == 0n : Nat}
139  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))) == 0n : Nat}
140  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, _))) == 0n : Nat}
141  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, _)) == 0n : Nat}
142  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, _) == 0n : Nat}
143  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {_ == 0n : Nat}
144  {==}