def step

bend-collections-laws-math@1.0.0.0 · proofs/lib/arith.bend:96

import Base
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/u32alg.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

96# one long-division step: if x == q d + r and 2^k r + y == q2 d + r2 then
97# 2^k x + y == (2^k q + q2) d + r2
98def step(+k: Nat, +q: Nat, +r: Nat, +d: Nat, +y: Nat, +q2: Nat, +r2: Nat, +x: Nat, +hx: {x == Nat.add(Nat.mul(q, d), r) : Nat}, +h2: {Nat.add(sc(k, r), y) == Nat.add(Nat.mul(q2, d), r2) : Nat}) -> {Nat.add(sc(k, x), y) == Nat.add(Nat.mul(Nat.add(sc(k, q), q2), d), r2) : Nat}:
99  +rhs = Nat.add(Nat.mul(Nat.add(sc(k, q), q2), d), r2)
100  %Equal.sym(Nat, x, Nat.add(Nat.mul(q, d), r), hx) : {Nat.add(sc(k, _), y) == rhs : Nat}
101  %A.sc_add(k, Nat.mul(q, d), r) : {Nat.add(_, y) == rhs : Nat}
102  %Equal.sym(Nat, Nat.add(Nat.add(sc(k, Nat.mul(q, d)), sc(k, r)), y), Nat.add(sc(k, Nat.mul(q, d)), Nat.add(sc(k, r), y)), N.add_assoc(sc(k, Nat.mul(q, d)), sc(k, r), y)) : {_ == rhs : Nat}
103  %Equal.sym(Nat, Nat.add(sc(k, r), y), Nat.add(Nat.mul(q2, d), r2), h2) : {Nat.add(sc(k, Nat.mul(q, d)), _) == rhs : Nat}
104  %Equal.sym(Nat, sc(k, Nat.mul(q, d)), Nat.mul(sc(k, q), d), sc_mul(k, q, d)) : {Nat.add(_, Nat.add(Nat.mul(q2, d), r2)) == rhs : Nat}
105  %Equal.sym(Nat, Nat.mul(Nat.add(sc(k, q), q2), d), Nat.add(Nat.mul(sc(k, q), d), Nat.mul(q2, d)), NA.mul_add_right(sc(k, q), q2, d)) : {Nat.add(Nat.mul(sc(k, q), d), Nat.add(Nat.mul(q2, d), r2)) == Nat.add(_, r2) : Nat}
106  Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(sc(k, q), d), Nat.mul(q2, d)), r2), Nat.add(Nat.mul(sc(k, q), d), Nat.add(Nat.mul(q2, d), r2)), N.add_assoc(Nat.mul(sc(k, q), d), Nat.mul(q2, d), r2))