def mo_alg

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:376

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

376def mo_alg(+k: Nat, +A: Nat, +t1: Nat, +t2: Nat, +hh: Nat, +pl: Nat, +ph: Nat, +cl: Nat, +ch: Nat, +s: Nat, +cr: Nat, +ea: {A == Nat.add(pl, C.shift(k, ph)) : Nat}, +ec: {Nat.add(t2, t1) == Nat.add(cl, C.shift(k, ch)) : Nat}, +es: {Nat.add(s, C.shift(k, cr)) == Nat.add(ph, cl) : Nat}, +eh: {hh == 0n : Nat}) -> {Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, hh)))) == Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))) : Nat}:
377  Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, hh)))), Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, 0n)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, z)))), hh, 0n, eh), Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, 0n)))), Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), 0n)), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), z)), C.shift(k, C.shift(k, 0n)), 0n, Equal.trans(Nat, C.shift(k, C.shift(k, 0n)), C.shift(k, 0n), 0n, Equal.cong(Nat, Nat, z => C.shift(k, z), C.shift(k, 0n), 0n, WW.shift_zero(k)), WW.shift_zero(k))), Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), 0n)), Nat.add(Nat.add(A, C.shift(k, t1)), C.shift(k, t2)), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(A, C.shift(k, t1)), z), Nat.add(C.shift(k, t2), 0n), C.shift(k, t2), N.add_zero(C.shift(k, t2))), Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(k, t1)), C.shift(k, t2)), Nat.add(A, Nat.add(C.shift(k, t1), C.shift(k, t2))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), NA.add_assoc(A, C.shift(k, t1), C.shift(k, t2)), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(k, t1), C.shift(k, t2))), Nat.add(A, Nat.add(C.shift(k, t2), C.shift(k, t1))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(A, z), Nat.add(C.shift(k, t1), C.shift(k, t2)), Nat.add(C.shift(k, t2), C.shift(k, t1)), N.add_comm(C.shift(k, t1), C.shift(k, t2))), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(k, t2), C.shift(k, t1))), Nat.add(A, C.shift(k, Nat.add(t2, t1))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(A, z), Nat.add(C.shift(k, t2), C.shift(k, t1)), C.shift(k, Nat.add(t2, t1)), Equal.sym(Nat, C.shift(k, Nat.add(t2, t1)), Nat.add(C.shift(k, t2), C.shift(k, t1)), WW.shift_add(k, t2, t1))), Equal.trans(Nat, Nat.add(A, C.shift(k, Nat.add(t2, t1))), Nat.add(A, C.shift(k, Nat.add(cl, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(A, C.shift(k, z)), Nat.add(t2, t1), Nat.add(cl, C.shift(k, ch)), ec), Equal.trans(Nat, Nat.add(A, C.shift(k, Nat.add(cl, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, ph)), C.shift(k, Nat.add(cl, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(k, Nat.add(cl, C.shift(k, ch)))), A, Nat.add(pl, C.shift(k, ph)), ea), Equal.trans(Nat, Nat.add(Nat.add(pl, C.shift(k, ph)), C.shift(k, Nat.add(cl, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, ph)), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(pl, C.shift(k, ph)), z), C.shift(k, Nat.add(cl, C.shift(k, ch))), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch))), WW.shift_add(k, cl, C.shift(k, ch))), Equal.trans(Nat, Nat.add(Nat.add(pl, C.shift(k, ph)), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch))))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), NA.add_assoc(pl, C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch))))), Nat.add(pl, Nat.add(Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, z), Nat.add(C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, C.shift(k, ch))), Equal.sym(Nat, Nat.add(Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, C.shift(k, ch))), Nat.add(C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), NA.add_assoc(C.shift(k, ph), C.shift(k, cl), C.shift(k, C.shift(k, ch))))), Equal.trans(Nat, Nat.add(pl, Nat.add(Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(C.shift(k, Nat.add(ph, cl)), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(z, C.shift(k, C.shift(k, ch)))), Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, Nat.add(ph, cl)), Equal.sym(Nat, C.shift(k, Nat.add(ph, cl)), Nat.add(C.shift(k, ph), C.shift(k, cl)), WW.shift_add(k, ph, cl))), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, Nat.add(ph, cl)), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(C.shift(k, Nat.add(s, C.shift(k, cr))), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(C.shift(k, z), C.shift(k, C.shift(k, ch)))), Nat.add(ph, cl), Nat.add(s, C.shift(k, cr)), Equal.sym(Nat, Nat.add(s, C.shift(k, cr)), Nat.add(ph, cl), es)), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, Nat.add(s, C.shift(k, cr))), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(Nat.add(C.shift(k, s), C.shift(k, C.shift(k, cr))), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(z, C.shift(k, C.shift(k, ch)))), C.shift(k, Nat.add(s, C.shift(k, cr))), Nat.add(C.shift(k, s), C.shift(k, C.shift(k, cr))), WW.shift_add(k, s, C.shift(k, cr))), Equal.trans(Nat, Nat.add(pl, Nat.add(Nat.add(C.shift(k, s), C.shift(k, C.shift(k, cr))), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(C.shift(k, s), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch))))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, z), Nat.add(Nat.add(C.shift(k, s), C.shift(k, C.shift(k, cr))), C.shift(k, C.shift(k, ch))), Nat.add(C.shift(k, s), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch)))), NA.add_assoc(C.shift(k, s), C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch)))), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, s), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch))))), Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, Nat.add(C.shift(k, cr), C.shift(k, ch))))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(C.shift(k, s), z)), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch))), C.shift(k, Nat.add(C.shift(k, cr), C.shift(k, ch))), Equal.sym(Nat, C.shift(k, Nat.add(C.shift(k, cr), C.shift(k, ch))), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch))), WW.shift_add(k, C.shift(k, cr), C.shift(k, ch)))), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, Nat.add(C.shift(k, cr), C.shift(k, ch))))), Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, C.shift(k, Nat.add(cr, ch))))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, z))), Nat.add(C.shift(k, cr), C.shift(k, ch)), C.shift(k, Nat.add(cr, ch)), Equal.sym(Nat, C.shift(k, Nat.add(cr, ch)), Nat.add(C.shift(k, cr), C.shift(k, ch)), WW.shift_add(k, cr, ch))), Equal.sym(Nat, Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, C.shift(k, Nat.add(cr, ch))))), NA.add_assoc(pl, C.shift(k, s), C.shift(k, C.shift(k, Nat.add(cr, ch))))))))))))))))))))))