def red_alg

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mm.bend:24

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

24def red_alg(+vs: Nat, +vf: Nat, +vxl: Nat, +y1: Nat, +qs: Nat, +t: Nat, +mq: Nat, +r: Nat, +es: {Nat.add(vs, vf) == Nat.add(vxl, C.shift(64n, qs)) : Nat}, +e1: {Nat.add(vf, C.shift(64n, t)) == mq : Nat}, +er: {Nat.add(mq, r) == Nat.add(vxl, C.shift(64n, y1)) : Nat}) -> {Nat.add(vf, Nat.add(vs, C.shift(64n, y1))) == Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))) : Nat}:
25  Equal.trans(Nat, Nat.add(vf, Nat.add(vs, C.shift(64n, y1))), Nat.add(Nat.add(vf, vs), C.shift(64n, y1)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.sym(Nat, Nat.add(Nat.add(vf, vs), C.shift(64n, y1)), Nat.add(vf, Nat.add(vs, C.shift(64n, y1))), NA.add_assoc(vf, vs, C.shift(64n, y1))), Equal.trans(Nat, Nat.add(Nat.add(vf, vs), C.shift(64n, y1)), Nat.add(Nat.add(vs, vf), C.shift(64n, y1)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, y1)), Nat.add(vf, vs), Nat.add(vs, vf), N.add_comm(vf, vs)), Equal.trans(Nat, Nat.add(Nat.add(vs, vf), C.shift(64n, y1)), Nat.add(Nat.add(vxl, C.shift(64n, qs)), C.shift(64n, y1)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, y1)), Nat.add(vs, vf), Nat.add(vxl, C.shift(64n, qs)), es), Equal.trans(Nat, Nat.add(Nat.add(vxl, C.shift(64n, qs)), C.shift(64n, y1)), Nat.add(vxl, Nat.add(C.shift(64n, qs), C.shift(64n, y1))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), NA.add_assoc(vxl, C.shift(64n, qs), C.shift(64n, y1)), Equal.trans(Nat, Nat.add(vxl, Nat.add(C.shift(64n, qs), C.shift(64n, y1))), Nat.add(vxl, Nat.add(C.shift(64n, y1), C.shift(64n, qs))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(vxl, z), Nat.add(C.shift(64n, qs), C.shift(64n, y1)), Nat.add(C.shift(64n, y1), C.shift(64n, qs)), N.add_comm(C.shift(64n, qs), C.shift(64n, y1))), Equal.trans(Nat, Nat.add(vxl, Nat.add(C.shift(64n, y1), C.shift(64n, qs))), Nat.add(Nat.add(vxl, C.shift(64n, y1)), C.shift(64n, qs)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.sym(Nat, Nat.add(Nat.add(vxl, C.shift(64n, y1)), C.shift(64n, qs)), Nat.add(vxl, Nat.add(C.shift(64n, y1), C.shift(64n, qs))), NA.add_assoc(vxl, C.shift(64n, y1), C.shift(64n, qs))), Equal.trans(Nat, Nat.add(Nat.add(vxl, C.shift(64n, y1)), C.shift(64n, qs)), Nat.add(Nat.add(mq, r), C.shift(64n, qs)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, qs)), Nat.add(vxl, C.shift(64n, y1)), Nat.add(mq, r), Equal.sym(Nat, Nat.add(mq, r), Nat.add(vxl, C.shift(64n, y1)), er)), Equal.trans(Nat, Nat.add(Nat.add(mq, r), C.shift(64n, qs)), Nat.add(Nat.add(Nat.add(vf, C.shift(64n, t)), r), C.shift(64n, qs)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, r), C.shift(64n, qs)), mq, Nat.add(vf, C.shift(64n, t)), Equal.sym(Nat, Nat.add(vf, C.shift(64n, t)), mq, e1)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(vf, C.shift(64n, t)), r), C.shift(64n, qs)), Nat.add(Nat.add(vf, Nat.add(C.shift(64n, t), r)), C.shift(64n, qs)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, qs)), Nat.add(Nat.add(vf, C.shift(64n, t)), r), Nat.add(vf, Nat.add(C.shift(64n, t), r)), NA.add_assoc(vf, C.shift(64n, t), r)), Equal.trans(Nat, Nat.add(Nat.add(vf, Nat.add(C.shift(64n, t), r)), C.shift(64n, qs)), Nat.add(vf, Nat.add(Nat.add(C.shift(64n, t), r), C.shift(64n, qs))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), NA.add_assoc(vf, Nat.add(C.shift(64n, t), r), C.shift(64n, qs)), Equal.trans(Nat, Nat.add(vf, Nat.add(Nat.add(C.shift(64n, t), r), C.shift(64n, qs))), Nat.add(vf, Nat.add(Nat.add(r, C.shift(64n, t)), C.shift(64n, qs))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(vf, Nat.add(z, C.shift(64n, qs))), Nat.add(C.shift(64n, t), r), Nat.add(r, C.shift(64n, t)), N.add_comm(C.shift(64n, t), r)), Equal.trans(Nat, Nat.add(vf, Nat.add(Nat.add(r, C.shift(64n, t)), C.shift(64n, qs))), Nat.add(vf, Nat.add(r, Nat.add(C.shift(64n, t), C.shift(64n, qs)))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(vf, z), Nat.add(Nat.add(r, C.shift(64n, t)), C.shift(64n, qs)), Nat.add(r, Nat.add(C.shift(64n, t), C.shift(64n, qs))), NA.add_assoc(r, C.shift(64n, t), C.shift(64n, qs))), Equal.cong(Nat, Nat, z => Nat.add(vf, Nat.add(r, z)), Nat.add(C.shift(64n, t), C.shift(64n, qs)), C.shift(64n, Nat.add(t, qs)), Equal.sym(Nat, C.shift(64n, Nat.add(t, qs)), Nat.add(C.shift(64n, t), C.shift(64n, qs)), WW.shift_add(64n, t, qs)))))))))))))))