def two

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divd.bend:58

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/logic.bend as L
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/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

58# two digits: r * 2^64 = (q1 * 2^32 + q2) * b + r2
59def two(+bp: Nat, +R: Nat, +q1: Nat, +r1: Nat, +q2: Nat, +r2: Nat, +e1: {q1 == Nat.div(C.shift(32n, R), 1n+bp) : Nat}, +f1: {r1 == Nat.mod(C.shift(32n, R), 1n+bp) : Nat}, +e2: {q2 == Nat.div(C.shift(32n, r1), 1n+bp) : Nat}, +f2: {r2 == Nat.mod(C.shift(32n, r1), 1n+bp) : Nat}) -> {Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2) == C.shift(64n, R) : Nat}:
60  +E1 = L.subst(Nat, w => {C.shift(32n, R) == Nat.add(Nat.mul(q1, 1n+bp), w) : Nat}, Nat.mod(C.shift(32n, R), 1n+bp), r1, Equal.sym(Nat, r1, Nat.mod(C.shift(32n, R), 1n+bp), f1), L.subst(Nat, w => {C.shift(32n, R) == Nat.add(Nat.mul(w, 1n+bp), Nat.mod(C.shift(32n, R), 1n+bp)) : Nat}, Nat.div(C.shift(32n, R), 1n+bp), q1, Equal.sym(Nat, q1, Nat.div(C.shift(32n, R), 1n+bp), e1), NR.dm_eq(bp, C.shift(32n, R))))
61  +E2 = L.subst(Nat, w => {C.shift(32n, r1) == Nat.add(Nat.mul(q2, 1n+bp), w) : Nat}, Nat.mod(C.shift(32n, r1), 1n+bp), r2, Equal.sym(Nat, r2, Nat.mod(C.shift(32n, r1), 1n+bp), f2), L.subst(Nat, w => {C.shift(32n, r1) == Nat.add(Nat.mul(w, 1n+bp), Nat.mod(C.shift(32n, r1), 1n+bp)) : Nat}, Nat.div(C.shift(32n, r1), 1n+bp), q2, Equal.sym(Nat, q2, Nat.div(C.shift(32n, r1), 1n+bp), e2), NR.dm_eq(bp, C.shift(32n, r1))))
62  +s1 = WW.shift_comp(32n, 32n, R)
63  +s2 = Equal.cong(Nat, Nat, w => C.shift(32n, w), C.shift(32n, R), Nat.add(Nat.mul(q1, 1n+bp), r1), E1)
64  +s3 = WW.shift_add(32n, Nat.mul(q1, 1n+bp), r1)
65  +s4 = Equal.cong(Nat, Nat, w => Nat.add(w, C.shift(32n, r1)), C.shift(32n, Nat.mul(q1, 1n+bp)), Nat.mul(C.shift(32n, q1), 1n+bp), sh_mul(32n, q1, 1n+bp))
66  +s5 = Equal.cong(Nat, Nat, w => Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), w), C.shift(32n, r1), Nat.add(Nat.mul(q2, 1n+bp), r2), E2)
67  +s6 = Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp)), r2), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.add(Nat.mul(q2, 1n+bp), r2)), NA.add_assoc(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp), r2))
68  +s7 = Equal.cong(Nat, Nat, w => Nat.add(w, r2), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp)), Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), Equal.sym(Nat, Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp)), NA.mul_add_right(C.shift(32n, q1), q2, 1n+bp)))
69  +ch = Equal.trans(Nat, C.shift(64n, R), C.shift(32n, C.shift(32n, R)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s1, Equal.trans(Nat, C.shift(32n, C.shift(32n, R)), C.shift(32n, Nat.add(Nat.mul(q1, 1n+bp), r1)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s2, Equal.trans(Nat, C.shift(32n, Nat.add(Nat.mul(q1, 1n+bp), r1)), Nat.add(C.shift(32n, Nat.mul(q1, 1n+bp)), C.shift(32n, r1)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s3, Equal.trans(Nat, Nat.add(C.shift(32n, Nat.mul(q1, 1n+bp)), C.shift(32n, r1)), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), C.shift(32n, r1)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s4, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), C.shift(32n, r1)), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.add(Nat.mul(q2, 1n+bp), r2)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s5, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.add(Nat.mul(q2, 1n+bp), r2)), Nat.add(Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp)), r2), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s6, s7))))))
70  Equal.sym(Nat, C.shift(64n, R), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), ch)