def m128_alg

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64m128.bend:69

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/proofs/lib/nat.bend as N
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/w64mul.bend as W64M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

69def m128_alg(+A: Nat, +t1: Nat, +t2: Nat, +hh: Nat, +lo00: Nat, +hi00: Nat, +vm: Nat, +lomid: Nat, +himid: Nat, +c1v: Nat, +s: Nat, +c2v: Nat, +ea: {A == Nat.add(lo00, C.shift(32n, hi00)) : Nat}, +et: {Nat.add(t1, t2) == Nat.add(vm, C.shift(32n, C.shift(32n, c1v))) : Nat}, +em: {vm == Nat.add(lomid, C.shift(32n, himid)) : Nat}, +es: {Nat.add(s, C.shift(32n, c2v)) == Nat.add(hi00, lomid) : Nat}) -> {Nat.add(Nat.add(A, C.shift(32n, t1)), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))) == Nat.add(Nat.add(lo00, C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)))) : Nat}:
70  Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(32n, t1)), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)))), Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(32n, t1)), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), NA.add_assoc(A, C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh))))), Nat.add(A, Nat.add(Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, z), Nat.add(C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, C.shift(32n, hh))), Equal.sym(Nat, Nat.add(Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, C.shift(32n, hh))), Nat.add(C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), NA.add_assoc(C.shift(32n, t1), C.shift(32n, t2), C.shift(32n, C.shift(32n, hh))))), Equal.trans(Nat, Nat.add(A, Nat.add(Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(C.shift(32n, Nat.add(t1, t2)), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(z, C.shift(32n, C.shift(32n, hh)))), Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, Nat.add(t1, t2)), Equal.sym(Nat, C.shift(32n, Nat.add(t1, t2)), Nat.add(C.shift(32n, t1), C.shift(32n, t2)), WW.shift_add(32n, t1, t2))), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, Nat.add(t1, t2)), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(C.shift(32n, Nat.add(vm, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(C.shift(32n, z), C.shift(32n, C.shift(32n, hh)))), Nat.add(t1, t2), Nat.add(vm, C.shift(32n, C.shift(32n, c1v))), et), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, Nat.add(vm, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(Nat.add(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(z, C.shift(32n, C.shift(32n, hh)))), C.shift(32n, Nat.add(vm, C.shift(32n, C.shift(32n, c1v)))), Nat.add(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), WW.shift_add(32n, vm, C.shift(32n, C.shift(32n, c1v)))), Equal.trans(Nat, Nat.add(A, Nat.add(Nat.add(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(C.shift(32n, vm), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, z), Nat.add(Nat.add(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh))), Nat.add(C.shift(32n, vm), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))), NA.add_assoc(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, vm), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(A, Nat.add(C.shift(32n, Nat.add(lomid, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(C.shift(32n, z), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), vm, Nat.add(lomid, C.shift(32n, himid)), em), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, Nat.add(lomid, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(A, Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(z, Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), C.shift(32n, Nat.add(lomid, C.shift(32n, himid))), Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), WW.shift_add(32n, lomid, C.shift(32n, himid))), Equal.trans(Nat, Nat.add(A, Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), A, Nat.add(lo00, C.shift(32n, hi00)), ea), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, C.shift(32n, hi00)), z), Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))), Nat.add(C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), NA.add_assoc(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))))), Nat.add(Nat.add(Nat.add(lo00, C.shift(32n, hi00)), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(lo00, C.shift(32n, hi00)), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))))), NA.add_assoc(Nat.add(lo00, C.shift(32n, hi00)), C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, hi00)), C.shift(32n, lomid)), Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), NA.add_assoc(lo00, C.shift(32n, hi00), C.shift(32n, lomid)))))))))))))), Equal.sym(Nat, Nat.add(Nat.add(lo00, C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)))), Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, C.shift(32n, s)), z), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v))), Nat.add(C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v))), Equal.trans(Nat, C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v))), C.shift(32n, Nat.add(C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v)))), C.shift(32n, c2v))), Nat.add(C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v))), Equal.cong(Nat, Nat, z => C.shift(32n, z), C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)), Nat.add(C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v)))), C.shift(32n, c2v)), WW.shift_add(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)), WW.shift_add(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v)))), C.shift(32n, c2v)))), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(z, C.shift(32n, C.shift(32n, c2v)))), C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Equal.trans(Nat, C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, Nat.add(C.shift(32n, hh), C.shift(32n, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Equal.cong(Nat, Nat, z => C.shift(32n, z), C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v)))), Nat.add(C.shift(32n, hh), C.shift(32n, Nat.add(himid, C.shift(32n, c1v)))), WW.shift_add(32n, hh, Nat.add(himid, C.shift(32n, c1v)))), Equal.trans(Nat, C.shift(32n, Nat.add(C.shift(32n, hh), C.shift(32n, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), C.shift(32n, C.shift(32n, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), WW.shift_add(32n, C.shift(32n, hh), C.shift(32n, Nat.add(himid, C.shift(32n, c1v)))), Equal.trans(Nat, Nat.add(C.shift(32n, C.shift(32n, hh)), C.shift(32n, C.shift(32n, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), C.shift(32n, Nat.add(C.shift(32n, himid), C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Equal.cong(Nat, Nat, z => Nat.add(C.shift(32n, C.shift(32n, hh)), C.shift(32n, z)), C.shift(32n, Nat.add(himid, C.shift(32n, c1v))), Nat.add(C.shift(32n, himid), C.shift(32n, C.shift(32n, c1v))), WW.shift_add(32n, himid, C.shift(32n, c1v))), Equal.cong(Nat, Nat, z => Nat.add(C.shift(32n, C.shift(32n, hh)), z), C.shift(32n, Nat.add(C.shift(32n, himid), C.shift(32n, C.shift(32n, c1v)))), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), WW.shift_add(32n, C.shift(32n, himid), C.shift(32n, C.shift(32n, c1v)))))))), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), W64M.add4(lo00, C.shift(32n, s), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v))), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, Nat.add(s, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), z), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2v))), C.shift(32n, Nat.add(s, C.shift(32n, c2v))), Equal.sym(Nat, C.shift(32n, Nat.add(s, C.shift(32n, c2v))), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2v))), WW.shift_add(32n, s, C.shift(32n, c2v)))), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, Nat.add(s, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, Nat.add(hi00, lomid))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, z)), Nat.add(s, C.shift(32n, c2v)), Nat.add(hi00, lomid), es), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, Nat.add(hi00, lomid))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), z), C.shift(32n, Nat.add(hi00, lomid)), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), WW.shift_add(32n, hi00, lomid)), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), NA.add_assoc(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Equal.trans(Nat, Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)))), Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(lo00, z), Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), N.add_comm(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)))), Equal.trans(Nat, Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.sym(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))))), NA.add_assoc(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))))), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), z), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh))), N.add_comm(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), z), Nat.add(Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))), NA.add_assoc(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))))))))))))))