def oct

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64div.bend:62

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

62# eight steps of a: L_i == i * a, so L8 == 2^3 * a
63def oct(+one: Nat, +e: Nat, +l1: Nat, +l2: Nat, +l3: Nat, +l4: Nat, +l5: Nat, +l6: Nat, +l7: Nat, +l8: Nat, +h1: {l1 == WD.sc(e, one) : Nat}, +h2: {Nat.add(l1, l1) == l2 : Nat}, +h3: {Nat.add(l1, l2) == l3 : Nat}, +h4: {Nat.add(l1, l3) == l4 : Nat}, +h5: {Nat.add(l1, l4) == l5 : Nat}, +h6: {Nat.add(l1, l5) == l6 : Nat}, +h7: {Nat.add(l1, l6) == l7 : Nat}, +h8: {Nat.add(l1, l7) == l8 : Nat}) -> {l8 == WD.sc(3n, WD.sc(e, one)) : Nat}:
64  +q4 = L.subst(Nat, z => {l4 == Nat.add(z, l2) : Nat}, Nat.add(l1, l1), l2, h2, add_twice(l1, l2, l3, l4, h3, h4))
65  +q6 = L.subst(Nat, z => {l6 == Nat.add(z, l4) : Nat}, Nat.add(l1, l1), l2, h2, add_twice(l1, l4, l5, l6, h5, h6))
66  +q8a = L.subst(Nat, z => {l8 == Nat.add(z, l6) : Nat}, Nat.add(l1, l1), l2, h2, add_twice(l1, l6, l7, l8, h7, h8))
67  +q8b = L.subst(Nat, z => {l8 == Nat.add(l2, z) : Nat}, l6, Nat.add(l2, l4), q6, q8a)
68  +q8c = Equal.trans(Nat, l8, Nat.add(l2, Nat.add(l2, l4)), Nat.add(Nat.add(l2, l2), l4), q8b, Equal.sym(Nat, Nat.add(Nat.add(l2, l2), l4), Nat.add(l2, Nat.add(l2, l4)), NA.add_assoc(l2, l2, l4)))
69  +q8 = L.subst(Nat, z => {l8 == Nat.add(z, l4) : Nat}, Nat.add(l2, l2), l4, Equal.sym(Nat, l4, Nat.add(l2, l2), q4), q8c)
70  +d2 = Equal.trans(Nat, l2, Nat.add(l1, l1), Nat.double(l1), Equal.sym(Nat, Nat.add(l1, l1), l2, h2), Equal.sym(Nat, Nat.double(l1), Nat.add(l1, l1), NA.double_self(l1)))
71  +d4 = Equal.trans(Nat, l4, Nat.add(l2, l2), Nat.double(l2), q4, Equal.sym(Nat, Nat.double(l2), Nat.add(l2, l2), NA.double_self(l2)))
72  +d8 = Equal.trans(Nat, l8, Nat.add(l4, l4), Nat.double(l4), q8, Equal.sym(Nat, Nat.double(l4), Nat.add(l4, l4), NA.double_self(l4)))
73  +r1 = L.subst(Nat, z => {l8 == Nat.double(z) : Nat}, l4, Nat.double(l2), d4, d8)
74  +r2 = L.subst(Nat, z => {l8 == Nat.double(Nat.double(z)) : Nat}, l2, Nat.double(l1), d2, r1)
75  L.subst(Nat, z => {l8 == Nat.double(Nat.double(Nat.double(z))) : Nat}, l1, WD.sc(e, one), h1, r2)