~/bend-docscommunity

proofs/math/typed/f64divn.bend source

proofs/math/typed/f64divn.bend on the hub · documented module

import Baseimport ./f64light.bend as FLimport ../../../spec/lib/common.bend as Cimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../natural/arith.bend as NRimport ./width.bend as WWimport ./natcmp.bend as NCimport ./f64rtools.bend as RTimport ./natfuel.bend as NF# The quotient and sticky bit of a division, at two scales: the spec's# 2 * floor(MX * 2^200 / MY) + [remainder != 0] cut at bit d is floor(MX *# 2^P / MY) with the same sticky bit (P + d = 201), and SoftFloat's two# 32-bit digits of (a - b) * 2^64 / b give floor(a * 2^62 / b) and its# sticky bit.def add_eq0(+a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:  FL.add_eq0(a, b)def mul_eq0(+a: Nat, +yp: Nat) -> {Nat.is_eq(Nat.mul(a, 1n+yp), 0n) == Nat.is_eq(a, 0n) : Bool}:  match a:    case 0n:      {==}    case 1n+ +ap:      {==}def min1_eq0(+b: Nat) -> {Nat.is_eq(Nat.min(b, 1n), 0n) == Nat.is_eq(b, 0n) : Bool}:  match b:    case 0n:      {==}    case 1n+ +bq:      {==}def min1_le(+b: Nat) -> {Nat.is_le(Nat.min(b, 1n), 1n) == True{} : Bool}:  match b:    case 0n:      {==}    case 1n+ +bq:      match bq:        case 0n:          {==}        case 1n+ +bz:          {==}def and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}:  match a b:    case True{} True{}:      {==}    case True{} False{}:      {==}    case False{} True{}:      {==}    case False{} False{}:      {==}def mul1(+y: Nat) -> {Nat.mul(1n, y) == y : Nat}:  Equal.trans(Nat, Nat.mul(1n, y), Nat.mul(y, 1n), y, NA.mul_comm(1n, y), NA.mul_one(y))# 2^k * y as a productdef sh_y(+k: Nat, +y: Nat) -> {Nat.mul(C.shift(k, 1n), y) == C.shift(k, y) : Nat}:  Equal.trans(Nat, Nat.mul(C.shift(k, 1n), y), C.shift(k, Nat.mul(1n, y)), C.shift(k, y), WW.shift_mul_l(k, 1n, y), Equal.cong(Nat, Nat, z => C.shift(k, z), Nat.mul(1n, y), y, mul1(y)))# le/lt under a common shiftdef le_sh(+k: Nat, +a: Nat, +b: Nat) -> {Nat.is_le(C.shift(k, a), C.shift(k, b)) == Nat.is_le(a, b) : Bool}:  Equal.cong(Cmp, Bool, c => Cmp.is_le(c), Nat.cmp(C.shift(k, a), C.shift(k, b)), Nat.cmp(a, b), NC.cmp_shift(k, a, b))def lt_sh(+k: Nat, +a: Nat, +b: Nat) -> {Nat.is_lt(C.shift(k, a), C.shift(k, b)) == Nat.is_lt(a, b) : Bool}:  Equal.cong(Cmp, Bool, c => Cmp.is_lt(c), Nat.cmp(C.shift(k, a), C.shift(k, b)), Nat.cmp(a, b), NC.cmp_shift(k, a, b))# the spec's significand cut at bit 1+dp, where P + dp = 200def specA(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat, +hP: {Nat.add(dp, P) == 200n : Nat}) -> {Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))) == Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)) : Nat}:  +e0 = NR.dm_eq(yp, C.shift(P, MX))  +e1 = Equal.trans(Nat, C.shift(200n, MX), C.shift(Nat.add(dp, P), MX), C.shift(dp, C.shift(P, MX)), Equal.cong(Nat, Nat, z => C.shift(z, MX), 200n, Nat.add(dp, P), Equal.sym(Nat, Nat.add(dp, P), 200n, hP)), WW.shift_comp(dp, P, MX))  +e2 = Equal.cong(Nat, Nat, z => C.shift(dp, z), C.shift(P, MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp)), e0)  +e3 = WW.shift_add(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))  +e4 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Equal.sym(Nat, Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), WW.shift_mul_l(dp, Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)))  +e5 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), z), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), NR.dm_eq(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))))  +e6 = Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.add_assoc(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))  +e7 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Equal.sym(Nat, Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), NA.mul_add_right(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)))  +eN = Equal.trans(Nat, C.shift(200n, MX), C.shift(dp, C.shift(P, MX)), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e1, Equal.trans(Nat, C.shift(dp, C.shift(P, MX)), C.shift(dp, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e2, Equal.trans(Nat, C.shift(dp, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e3, Equal.trans(Nat, Nat.add(C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e4, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e5, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e6, e7))))))  +hb = NR.dm_lt(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)))  +eD = Equal.trans(Nat, Nat.div(C.shift(200n, MX), 1n+yp), Nat.div(Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Equal.cong(Nat, Nat, z => Nat.div(z, 1n+yp), C.shift(200n, MX), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eN), NR.div_of(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), yp, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), hb))  +eR = Equal.trans(Nat, Nat.mod(C.shift(200n, MX), 1n+yp), Nat.mod(Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+yp), C.shift(200n, MX), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eN), NR.mod_of(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), yp, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), hb))  +m1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, z), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.div(C.shift(200n, MX), 1n+yp), Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eD)  +m2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(z, 1n)), Nat.mod(C.shift(200n, MX), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), eR)  +m3 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Equal.sym(Nat, Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.double_mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))))  +m4 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.double_add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))  +m5 = NA.add_assoc(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))  +m6 = NA.add_comm(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)))  +m7 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.add_comm(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)))  +ch = Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m1, Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m2, Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m3, Equal.trans(Nat, Nat.add(Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m4, Equal.trans(Nat, Nat.add(Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m5, Equal.trans(Nat, Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))), Nat.add(Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m6, m7))))))  Equal.sym(Nat, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), ch)# the low part fits 1+dp bitsdef specA_fit(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat) -> {C.fits(1n+dp, Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))) == True{} : Bool}:  +l1 = Equal.trans(Bool, Nat.is_le(C.shift(dp, 1n), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.is_le(Nat.mul(C.shift(dp, 1n), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), False{}, NR.le_div(yp, C.shift(dp, 1n), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Equal.trans(Bool, Nat.is_le(Nat.mul(C.shift(dp, 1n), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.is_le(C.shift(dp, 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.mul(C.shift(dp, 1n), 1n+yp), C.shift(dp, 1n+yp), sh_y(dp, 1n+yp)), Equal.trans(Bool, Nat.is_le(C.shift(dp, 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.is_le(1n+yp, Nat.mod(C.shift(P, MX), 1n+yp)), False{}, le_sh(dp, 1n+yp, Nat.mod(C.shift(P, MX), 1n+yp)), N.lt_not_le(Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp, NR.dm_lt(yp, C.shift(P, MX))))))  +l2 = N.not_le_lt(C.shift(dp, 1n), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), l1)  +fa = WW.fits_one(dp, 1n, {==}, Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), l2)  Equal.trans(Bool, C.fits(1n+dp, Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), C.fits(dp, Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), True{}, RT.fit_td(dp, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), min1_le(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), fa)# the low part is zero exactly when MX * 2^P is a multiple of MYdef specA_z(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat) -> {Nat.is_eq(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), 0n) == Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n) : Bool}:  +z1 = add_eq0(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))  +z2 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), min1_eq0(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))  +z3 = Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), t), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), WW.dbl_eq0(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))  +z4 = and_comm(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n))  +z5 = Equal.sym(Bool, Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), mul_eq0(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), yp))  +z6 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), z5)  +z7 = Equal.sym(Bool, Nat.is_eq(Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), add_eq0(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))  +z8 = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.sym(Nat, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), NR.dm_eq(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)))))  +z9 = WW.shift_eq0(dp, Nat.mod(C.shift(P, MX), 1n+yp))  Equal.trans(Bool, Nat.is_eq(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), 0n), Bool.and(Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z1, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z2, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z3, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Bool.and(Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z4, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z6, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z7, Equal.trans(Bool, Nat.is_eq(Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z8, z9)))))))# SoftFloat's quotient: (a - b) * 2^64 = Q * b + r2 with r2 < b gives# a * 2^62 = T * b + e with T = 2^62 + floor(Q / 4) and e < bdef iq_parts(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)) == C.shift(2n, C.shift(62n, R)) : Nat}:  +q1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, B), r2), Q, Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), WW.low_high(2n, Q))  +q2 = Equal.cong(Nat, Nat, z => Nat.add(z, r2), Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), NA.mul_add_right(C.low(2n, Q), C.shift(2n, C.high(2n, Q)), B))  +q3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), z), r2), Nat.mul(C.shift(2n, C.high(2n, Q)), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), WW.shift_mul_l(2n, C.high(2n, Q), B))  +q4 = NA.add_assoc(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)  +q5 = NA.add_swap(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)  +q7 = Equal.trans(Nat, C.shift(64n, R), C.shift(Nat.add(2n, 62n), R), C.shift(2n, C.shift(62n, R)), {==}, WW.shift_comp(2n, 62n, R))  +x1 = Equal.trans(Nat, Nat.add(Nat.mul(Q, B), r2), Nat.add(Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q1, Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), r2), Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q2, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), r2), Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B))), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q3, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B))), r2), Nat.add(Nat.mul(C.low(2n, Q), B), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q4, q5))))  Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), Nat.add(Nat.mul(Q, B), r2), C.shift(2n, C.shift(62n, R)), Equal.sym(Nat, Nat.add(Nat.mul(Q, B), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), x1), Equal.trans(Nat, Nat.add(Nat.mul(Q, B), r2), C.shift(64n, R), C.shift(2n, C.shift(62n, R)), hQ, q7))# h * b <= (a - b) * 2^62def iq_le(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)) == True{} : Bool}:  +p = iq_parts(B, R, Q, r2, hQ)  +l = L.subst(Nat, z => {Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), z) == True{} : Bool}, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), C.shift(2n, C.shift(62n, R)), p, N.le_add_right(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)))  Equal.trans(Bool, Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)), Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, C.shift(62n, R))), True{}, Equal.sym(Bool, Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, C.shift(62n, R))), Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)), le_sh(2n, Nat.mul(C.high(2n, Q), B), C.shift(62n, R))), l)# the remainder e = (a - b) * 2^62 - h * b, and 4 e = low2(Q) * b + r2def iq_eps(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))) == Nat.add(Nat.mul(C.low(2n, Q), B), r2) : Nat}:  +p = iq_parts(B, R, Q, r2, hQ)  +e1 = N.sub_add(C.shift(62n, R), Nat.mul(C.high(2n, Q), B), iq_le(B, R, Q, r2, hQ))  +e2 = Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, C.shift(62n, R)), Equal.sym(Nat, C.shift(2n, Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), WW.shift_add(2n, Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), Equal.cong(Nat, Nat, z => C.shift(2n, z), Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))), C.shift(62n, R), e1))  NR.add_cancel(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))), Nat.add(Nat.mul(C.low(2n, Q), B), r2), Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, C.shift(62n, R)), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), e2, Equal.sym(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), C.shift(2n, C.shift(62n, R)), p)))def low2_le(+Q: Nat, +bp: Nat) -> {Nat.is_le(Nat.mul(1n+C.low(2n, Q), 1n+bp), C.shift(2n, 1n+bp)) == True{} : Bool}:  +l = N.lt_succ_le_succ(C.low(2n, Q), 4n, WW.low_lt(2n, Q))  +m = NF.mul_le_r(1n+bp, 1n+C.low(2n, Q), 4n, l)  +e = Equal.trans(Nat, Nat.mul(1n+bp, 4n), Nat.mul(4n, 1n+bp), C.shift(2n, 1n+bp), NA.mul_comm(1n+bp, 4n), sh_y(2n, 1n+bp))  L.subst(Nat, z => {Nat.is_le(Nat.mul(1n+C.low(2n, Q), 1n+bp), z) == True{} : Bool}, Nat.mul(1n+bp, 4n), C.shift(2n, 1n+bp), e, L.subst(Nat, z => {Nat.is_le(z, Nat.mul(1n+bp, 4n)) == True{} : Bool}, Nat.mul(1n+bp, 1n+C.low(2n, Q)), Nat.mul(1n+C.low(2n, Q), 1n+bp), NA.mul_comm(1n+bp, 1n+C.low(2n, Q)), m))# e < bdef iq_lt(+bp: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, 1n+bp), r2) == C.shift(64n, R) : Nat}, +hr2: {Nat.is_lt(r2, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp) == True{} : Bool}:  +E = Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2)  +l1 = Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp)), Nat.is_lt(r2, 1n+bp), True{}, WW.lt_cancel_l(Nat.mul(C.low(2n, Q), 1n+bp), r2, 1n+bp), hr2)  +e1 = Equal.trans(Nat, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Nat.add(1n+bp, Nat.mul(C.low(2n, Q), 1n+bp)), Nat.mul(1n+C.low(2n, Q), 1n+bp), NA.add_comm(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), {==})  +l2 = N.lt_le_trans(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), C.shift(2n, 1n+bp), l1, L.subst(Nat, z => {Nat.is_le(z, C.shift(2n, 1n+bp)) == True{} : Bool}, Nat.mul(1n+C.low(2n, Q), 1n+bp), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Equal.sym(Nat, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Nat.mul(1n+C.low(2n, Q), 1n+bp), e1), low2_le(Q, bp)))  +l3 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(2n, 1n+bp)) == True{} : Bool}, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Equal.sym(Nat, C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), iq_eps(1n+bp, R, Q, r2, hQ)), l2)  Equal.trans(Bool, Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp), Nat.is_lt(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), C.shift(2n, 1n+bp)), True{}, Equal.sym(Bool, Nat.is_lt(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), C.shift(2n, 1n+bp)), Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp), lt_sh(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp)), l3)# e is zero exactly when the low two quotient bits and r2 aredef iq_z(+bp: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, 1n+bp), r2) == C.shift(64n, R) : Nat}) -> {Nat.is_eq(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 0n) == Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)) : Bool}:  +z1 = Equal.sym(Bool, Nat.is_eq(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), 0n), Nat.is_eq(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 0n), WW.shift_eq0(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))))  +z2 = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), iq_eps(1n+bp, R, Q, r2, hQ))  +z3 = add_eq0(Nat.mul(C.low(2n, Q), 1n+bp), r2)  +z4 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(r2, 0n)), Nat.is_eq(Nat.mul(C.low(2n, Q), 1n+bp), 0n), Nat.is_eq(C.low(2n, Q), 0n), mul_eq0(C.low(2n, Q), bp))  Equal.trans(Bool, Nat.is_eq(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 0n), Nat.is_eq(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), 0n), Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)), z1, Equal.trans(Bool, Nat.is_eq(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), 0n), Nat.is_eq(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), 0n), Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)), z2, Equal.trans(Bool, Nat.is_eq(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), 0n), Bool.and(Nat.is_eq(Nat.mul(C.low(2n, Q), 1n+bp), 0n), Nat.is_eq(r2, 0n)), Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)), z3, z4)))# the two scales agree: a * 2^62 = T * b + e with e < b, a = MX * 2^u and# b = MY * 2^w give T = floor(MX * 2^P / MY) and e = 0 iff MY | MX * 2^Pdef jn_eq(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}) -> {C.shift(62n, C.shift(u, MX)) == Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))) : Nat}:  +j1 = Equal.sym(Nat, C.shift(Nat.add(62n, u), MX), C.shift(62n, C.shift(u, MX)), WW.shift_comp(62n, u, MX))  +j2 = Equal.cong(Nat, Nat, z => C.shift(z, MX), Nat.add(62n, u), Nat.add(w, P), hP)  +j3 = WW.shift_comp(w, P, MX)  +j4 = Equal.cong(Nat, Nat, z => C.shift(w, z), C.shift(P, MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp)), NR.dm_eq(yp, C.shift(P, MX)))  +j5 = WW.shift_add(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))  +j6 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), C.shift(w, 1n+yp)), Equal.sym(Nat, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), C.shift(w, 1n+yp)), C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), WW.shift_mul_r(w, Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)))  +j7 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), z), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(w, 1n+yp), 1n+bp, hB)  Equal.trans(Nat, C.shift(62n, C.shift(u, MX)), C.shift(Nat.add(62n, u), MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j1, Equal.trans(Nat, C.shift(Nat.add(62n, u), MX), C.shift(Nat.add(w, P), MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j2, Equal.trans(Nat, C.shift(Nat.add(w, P), MX), C.shift(w, C.shift(P, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j3, Equal.trans(Nat, C.shift(w, C.shift(P, MX)), C.shift(w, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j4, Equal.trans(Nat, C.shift(w, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j5, Equal.trans(Nat, Nat.add(C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), C.shift(w, 1n+yp)), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j6, j7))))))def jn_lt(+MX: Nat, +yp: Nat, +w: Nat, +P: Nat, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}) -> {Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+bp) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), z) == True{} : Bool}, C.shift(w, 1n+yp), 1n+bp, hB, Equal.trans(Bool, Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), C.shift(w, 1n+yp)), Nat.is_lt(Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp), True{}, lt_sh(w, Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp), NR.dm_lt(yp, C.shift(P, MX))))def jn_q(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}, +T: Nat, +e: Nat, +hE: {Nat.add(Nat.mul(T, 1n+bp), e) == C.shift(62n, C.shift(u, MX)) : Nat}, +he: {Nat.is_lt(e, 1n+bp) == True{} : Bool}) -> {T == Nat.div(C.shift(P, MX), 1n+yp) : Nat}:  +eq = Equal.trans(Nat, Nat.add(Nat.mul(T, 1n+bp), e), C.shift(62n, C.shift(u, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), hE, jn_eq(MX, yp, u, w, P, hP, bp, hB))  +dT = NR.div_of(T, bp, e, he)  +dQ = NR.div_of(Nat.div(C.shift(P, MX), 1n+yp), bp, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), jn_lt(MX, yp, w, P, bp, hB))  Equal.trans(Nat, T, Nat.div(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.div(C.shift(P, MX), 1n+yp), Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), T, dT), Equal.trans(Nat, Nat.div(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.div(Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), 1n+bp), Nat.div(C.shift(P, MX), 1n+yp), Equal.cong(Nat, Nat, z => Nat.div(z, 1n+bp), Nat.add(Nat.mul(T, 1n+bp), e), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), eq), dQ))def jn_z(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}, +T: Nat, +e: Nat, +hE: {Nat.add(Nat.mul(T, 1n+bp), e) == C.shift(62n, C.shift(u, MX)) : Nat}, +he: {Nat.is_lt(e, 1n+bp) == True{} : Bool}) -> {Nat.is_eq(e, 0n) == Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n) : Bool}:  +eq = Equal.trans(Nat, Nat.add(Nat.mul(T, 1n+bp), e), C.shift(62n, C.shift(u, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), hE, jn_eq(MX, yp, u, w, P, hP, bp, hB))  +mT = NR.mod_of(T, bp, e, he)  +mQ = NR.mod_of(Nat.div(C.shift(P, MX), 1n+yp), bp, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), jn_lt(MX, yp, w, P, bp, hB))  +ee = Equal.trans(Nat, e, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), e, mT), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.mod(Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(Nat.mul(T, 1n+bp), e), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), eq), mQ))  Equal.trans(Bool, Nat.is_eq(e, 0n), Nat.is_eq(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), e, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), ee), WW.shift_eq0(w, Nat.mod(C.shift(P, MX), 1n+yp)))