def shift_nest

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqf.bend:31

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

31def shift_nest(+j: Nat, +sc: Nat, +MX: Nat) -> {C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(sc, MX))))) == C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX) : Nat}:
32  +e1 = Equal.sym(Nat, C.shift(Nat.add(8n, sc), MX), C.shift(8n, C.shift(sc, MX)), WW.shift_comp(8n, sc, MX))
33  +e2 = Equal.sym(Nat, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX), C.shift(64n, C.shift(Nat.add(8n, sc), MX)), WW.shift_comp(64n, Nat.add(8n, sc), MX))
34  +e3 = Equal.sym(Nat, C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX), C.shift(j, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX)), WW.shift_comp(j, Nat.add(64n, Nat.add(8n, sc)), MX))
35  +e4 = Equal.sym(Nat, C.shift(Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), MX), C.shift(j, C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX)), WW.shift_comp(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX))
36  +e5 = Equal.cong(Nat, Nat, z => C.shift(z, MX), Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Equal.trans(Nat, Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Equal.trans(Nat, Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(Nat.add(j, 0n), Nat.add(j, Nat.add(sc, 72n))), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), Equal.trans(Nat, Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(Nat.add(j, 0n), Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(Nat.add(j, 0n), Nat.add(j, Nat.add(sc, 72n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, 0n), z), Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), Nat.add(j, Nat.add(sc, 72n)), Equal.trans(Nat, Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Nat.add(j, Nat.add(sc, 72n)), Equal.trans(Nat, Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), Nat.add(Nat.add(j, 0n), Nat.add(64n, Nat.add(8n, sc))), Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(64n, Nat.add(8n, sc))), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, 0n), z), Nat.add(64n, Nat.add(8n, sc)), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(64n, Nat.add(8n, sc)), Nat.add(64n, Nat.add(sc, 8n)), Nat.add(sc, 72n), Equal.cong(Nat, Nat, z => Nat.add(64n, z), Nat.add(8n, sc), Nat.add(sc, 8n), Equal.trans(Nat, Nat.add(8n, sc), Nat.add(8n, Nat.add(sc, 0n)), Nat.add(sc, 8n), Equal.cong(Nat, Nat, z => Nat.add(8n, z), sc, Nat.add(sc, 0n), Equal.sym(Nat, Nat.add(sc, 0n), sc, N.add_zero(sc))), Equal.trans(Nat, Nat.add(8n, Nat.add(sc, 0n)), Nat.add(sc, Nat.add(8n, 0n)), Nat.add(sc, 8n), NA.add_swap(8n, sc, 0n), {==}))), Equal.trans(Nat, Nat.add(64n, Nat.add(sc, 8n)), Nat.add(sc, Nat.add(64n, 8n)), Nat.add(sc, 72n), NA.add_swap(64n, sc, 8n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Nat.add(j, Nat.add(0n, Nat.add(sc, 72n))), Nat.add(j, Nat.add(sc, 72n)), NA.add_assoc(j, 0n, Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, Nat.add(0n, 72n)), Nat.add(sc, 72n), NA.add_swap(0n, sc, 72n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(j, Nat.add(sc, 72n))), Nat.add(j, Nat.add(0n, Nat.add(j, Nat.add(sc, 72n)))), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), NA.add_assoc(j, 0n, Nat.add(j, Nat.add(sc, 72n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(j, Nat.add(sc, 72n))), Nat.add(j, Nat.add(sc, 72n)), Equal.trans(Nat, Nat.add(0n, Nat.add(j, Nat.add(sc, 72n))), Nat.add(j, Nat.add(0n, Nat.add(sc, 72n))), Nat.add(j, Nat.add(sc, 72n)), NA.add_swap(0n, j, Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, Nat.add(0n, 72n)), Nat.add(sc, 72n), NA.add_swap(0n, sc, 72n), {==})))))), Equal.sym(Nat, Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), Equal.trans(Nat, Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(sc, 72n)), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), Equal.trans(Nat, Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(72n, sc)), Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(72n, sc)), Nat.add(j, j), Nat.add(j, Nat.add(j, 0n)), Equal.trans(Nat, Nat.add(j, j), Nat.add(Nat.add(j, 0n), Nat.add(j, 0n)), Nat.add(j, Nat.add(j, 0n)), Equal.trans(Nat, Nat.add(j, j), Nat.add(Nat.add(j, 0n), j), Nat.add(Nat.add(j, 0n), Nat.add(j, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, j), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, 0n), z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)))), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(j, 0n)), Nat.add(j, Nat.add(0n, Nat.add(j, 0n))), Nat.add(j, Nat.add(j, 0n)), NA.add_assoc(j, 0n, Nat.add(j, 0n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(j, 0n)), Nat.add(j, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(j, 0n)), Nat.add(j, Nat.add(0n, 0n)), Nat.add(j, 0n), NA.add_swap(0n, j, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(j, 0n)), z), Nat.add(72n, sc), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(72n, sc), Nat.add(72n, Nat.add(sc, 0n)), Nat.add(sc, 72n), Equal.cong(Nat, Nat, z => Nat.add(72n, z), sc, Nat.add(sc, 0n), Equal.sym(Nat, Nat.add(sc, 0n), sc, N.add_zero(sc))), Equal.trans(Nat, Nat.add(72n, Nat.add(sc, 0n)), Nat.add(sc, Nat.add(72n, 0n)), Nat.add(sc, 72n), NA.add_swap(72n, sc, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(sc, 72n)), Nat.add(j, Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n))), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), NA.add_assoc(j, Nat.add(j, 0n), Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Nat.add(j, Nat.add(sc, 72n)), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Nat.add(j, Nat.add(0n, Nat.add(sc, 72n))), Nat.add(j, Nat.add(sc, 72n)), NA.add_assoc(j, 0n, Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, Nat.add(0n, 72n)), Nat.add(sc, 72n), NA.add_swap(0n, sc, 72n), {==})))))))))
37  +c1 = Equal.cong(Nat, Nat, z => C.shift(j, C.shift(j, C.shift(64n, z))), C.shift(8n, C.shift(sc, MX)), C.shift(Nat.add(8n, sc), MX), e1)
38  +c2 = Equal.cong(Nat, Nat, z => C.shift(j, C.shift(j, z)), C.shift(64n, C.shift(Nat.add(8n, sc), MX)), C.shift(Nat.add(64n, Nat.add(8n, sc)), MX), e2)
39  +c3 = Equal.cong(Nat, Nat, z => C.shift(j, z), C.shift(j, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX)), C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX), e3)
40  Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(sc, MX))))), C.shift(j, C.shift(j, C.shift(64n, C.shift(Nat.add(8n, sc), MX)))), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX), c1, Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, C.shift(Nat.add(8n, sc), MX)))), C.shift(j, C.shift(j, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX))), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX), c2, Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX))), C.shift(j, C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX)), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX), c3, Equal.trans(Nat, C.shift(j, C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX)), C.shift(Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), MX), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX), e4, e5))))