def dgen

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divf.bend:56

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/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
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/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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulp.bend as MP
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as AA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divd.bend as DD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend as DN
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend as DQ

56# the quotient step, for a in [b, 2b), a = MX * 2^u, b = MY * 2^w, 62 + u = w + P, P + dp = 200
57def dgen(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +aw: WU.U64, +bw: WU.U64, +bp: Nat, +hBp: {SW.value(bw) == 1n+bp : Nat}, +MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +dp: Nat, +ha: {SW.value(aw) == C.shift(u, MX) : Nat}, +hb: {SW.value(bw) == C.shift(w, 1n+yp) : Nat}, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +hdp: {Nat.add(dp, P) == 200n : Nat}, +hle: {Nat.is_le(SW.value(bw), SW.value(aw)) == True{} : Bool}, +hRlt: {Nat.is_lt(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)) == True{} : Bool}, +hhi: {U32.is_zero(X.hi(bw)) == False{} : Bool}, +E: Nat, +hEx: {Nat.add(E, 1n+dp) == x : Nat}) -> {F.div_q(s, e, aw, bw) == SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), E) : F.F64}:
58  sv = WA.sub_value(aw, bw, hle)
59  +eR = Equal.trans(Nat, SW.value(X.sub(aw, bw)), Nat.sub(SW.value(aw), SW.value(bw)), Nat.sub(SW.value(aw), SW.value(bw)), sv, {==})
60  +hx1 = L.subst(Nat, z => {Nat.is_lt(z, SW.value(bw)) == True{} : Bool}, Nat.sub(SW.value(aw), SW.value(bw)), SW.value(X.sub(aw, bw)), Equal.sym(Nat, SW.value(X.sub(aw, bw)), Nat.sub(SW.value(aw), SW.value(bw)), eR), hRlt)
61  +q1 = dq96q(one, h1, X.sub(aw, bw), bw, X.bitlen(X.hi(bw)), hx1, hhi, {==})
62  +r1 = dq96r(one, h1, X.sub(aw, bw), bw, X.bitlen(X.hi(bw)), hx1, hhi, {==})
63  +hx2 = L.subst(Nat, z => {Nat.is_lt(SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), z) == True{} : Bool}, 1n+bp, SW.value(bw), Equal.sym(Nat, SW.value(bw), 1n+bp, hBp), L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), Equal.sym(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), Equal.trans(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), SW.value(bw)), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), r1, Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), z), SW.value(bw), 1n+bp, hBp))), NR.dm_lt(bp, C.shift(32n, SW.value(X.sub(aw, bw))))))
64  +q2 = dq96q(one, h1, X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))), bw, X.bitlen(X.hi(bw)), hx2, hhi, {==})
65  +r2 = dq96r(one, h1, X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))), bw, X.bitlen(X.hi(bw)), hx2, hhi, {==})
66  +e1 = Equal.trans(Nat, v(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))), Nat.div(C.shift(32n, SW.value(X.sub(aw, bw))), SW.value(bw)), Nat.div(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), q1, Equal.cong(Nat, Nat, z => Nat.div(C.shift(32n, SW.value(X.sub(aw, bw))), z), SW.value(bw), 1n+bp, hBp))
67  +f1 = Equal.trans(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), SW.value(bw)), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), r1, Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), z), SW.value(bw), 1n+bp, hBp))
68  +e2 = Equal.trans(Nat, v(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw)))), Nat.div(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), SW.value(bw)), Nat.div(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), 1n+bp), q2, Equal.cong(Nat, Nat, z => Nat.div(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), z), SW.value(bw), 1n+bp, hBp))
69  +f2 = Equal.trans(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), SW.value(bw)), Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), 1n+bp), r2, Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), z), SW.value(bw), 1n+bp, hBp))
70  +tw = DD.two(bp, SW.value(X.sub(aw, bw)), v(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))), SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), v(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw)))), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), e1, f1, e2, f2)
71  +hQ = Equal.trans(Nat, Nat.add(Nat.mul(SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}), 1n+bp), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw))))), Nat.add(Nat.mul(Nat.add(C.shift(32n, v(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))))), v(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))))), 1n+bp), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw))))), C.shift(64n, SW.value(X.sub(aw, bw))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, 1n+bp), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw))))), SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}), Nat.add(C.shift(32n, v(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))))), v(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))))), NA.add_comm(v(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw)))), C.shift(32n, v(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))))))), tw)
72  +hr2 = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), 1n+bp), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), Equal.sym(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), 1n+bp), f2), NR.dm_lt(bp, C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))))))
73  +iT = DQ.iq_T(one, h1, bp, SW.value(X.sub(aw, bw)), SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), hQ)
74  +eA = Equal.trans(Nat, Nat.add(SW.value(X.sub(aw, bw)), 1n+bp), Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), C.shift(u, MX), Equal.trans(Nat, Nat.add(SW.value(X.sub(aw, bw)), 1n+bp), Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), 1n+bp), Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), Equal.cong(Nat, Nat, z => Nat.add(z, 1n+bp), SW.value(X.sub(aw, bw)), Nat.sub(SW.value(aw), SW.value(bw)), eR), Equal.cong(Nat, Nat, z => Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), z), 1n+bp, SW.value(bw), Equal.sym(Nat, SW.value(bw), 1n+bp, hBp))), Equal.trans(Nat, Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), SW.value(aw), C.shift(u, MX), Equal.trans(Nat, Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), Nat.add(SW.value(bw), Nat.sub(SW.value(aw), SW.value(bw))), SW.value(aw), NA.add_comm(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), N.sub_add(SW.value(aw), SW.value(bw), hle)), ha))
75  +hE = Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), 1n+bp), Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp))), C.shift(62n, Nat.add(SW.value(X.sub(aw, bw)), 1n+bp)), C.shift(62n, C.shift(u, MX)), iT, Equal.cong(Nat, Nat, z => C.shift(62n, z), Nat.add(SW.value(X.sub(aw, bw)), 1n+bp), C.shift(u, MX), eA))
76  +he = DN.iq_lt(bp, SW.value(X.sub(aw, bw)), SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), hQ, hr2)
77  +hBw = Equal.trans(Nat, C.shift(w, 1n+yp), SW.value(bw), 1n+bp, Equal.sym(Nat, SW.value(bw), C.shift(w, 1n+yp), hb), hBp)
78  +jq = DN.jn_q(MX, yp, u, w, P, hP, bp, hBw, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp)), hE, he)
79  +jz = DN.jn_z(MX, yp, u, w, P, hP, bp, hBw, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp)), hE, he)
80  +iz = DN.iq_z(bp, SW.value(X.sub(aw, bw)), SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), hQ)
81  +est = Equal.trans(Bool, Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))), Bool.not(Bool.and(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n), Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n))), Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)), dm2(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n), Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Equal.trans(Bool, Bool.not(Bool.and(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n), Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n))), Bool.not(Nat.is_eq(Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp)), 0n)), Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)), Equal.cong(Bool, Bool, t => Bool.not(t), Bool.and(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n), Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Nat.is_eq(Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp)), 0n), Equal.sym(Bool, Nat.is_eq(Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp)), 0n), Bool.and(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n), Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), iz)), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_eq(Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), jz)))
82  +im1 = DQ.dq_round(one, h1, s, e, x, hx, X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw))), 1073741824, {==})
83  +im2 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.jam(z, SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))))), x), Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Nat.div(C.shift(P, MX), 1n+yp), jq)
84  +im3 = Equal.cong(Bool, F.F64, t => SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(t)), x), Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))), Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)), est)
85  +imp = Equal.trans(F.F64, F.div_q(s, e, aw, bw), SF.round(s, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))))), x), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), im1, Equal.trans(F.F64, SF.round(s, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))))), x), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))))), x), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), im2, im3))
86  +sA = DN.specA(MX, yp, P, dp, hdp)
87  +fL = DN.specA_fit(MX, yp, P, dp)
88  +zL = DN.specA_z(MX, yp, P, dp)
89  +eH = Equal.trans(Nat, C.high(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), C.high(1n+dp, 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.div(C.shift(P, MX), 1n+yp), Equal.cong(Nat, Nat, z => C.high(1n+dp, z), 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))), Equal.sym(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)), sA)), WW.high_u(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))), Nat.div(C.shift(P, MX), 1n+yp), fL))
90  +eL = Equal.trans(Nat, C.low(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), C.low(1n+dp, 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.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))), Equal.cong(Nat, Nat, z => C.low(1n+dp, z), 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))), Equal.sym(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)), sA)), WW.low_u(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))), Nat.div(C.shift(P, MX), 1n+yp), fL))
91  +q62 = Equal.trans(Bool, C.fits(62n, Nat.div(C.shift(P, MX), 1n+yp)), C.fits(62n, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})))), False{}, Equal.cong(Nat, Bool, z => C.fits(62n, z), Nat.div(C.shift(P, MX), 1n+yp), Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Equal.sym(Nat, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Nat.div(C.shift(P, MX), 1n+yp), jq)), DQ.t62(one, h1, X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw)))))
92  +q54 = nfit_mono(54n, 62n, Nat.div(C.shift(P, MX), 1n+yp), {==}, q62)
93  +f54 = Equal.trans(Bool, C.fits(Nat.add(1n+dp, 54n), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), C.fits(54n, Nat.div(C.shift(P, MX), 1n+yp)), False{}, RT.fits_sh(1n+dp, 54n, Nat.div(C.shift(P, MX), 1n+yp)), q54)
94  +hle2 = L.subst(Nat, z => {Nat.is_le(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), z) == True{} : Bool}, Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), 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)))), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Equal.trans(Nat, Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), 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)))), 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)), NA.add_comm(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), 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)))), sA), N.le_add_right(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), 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)))))
95  +fM = FR.nfit(Nat.add(1n+dp, 54n), 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)), hle2, f54)
96  +bl1 = AA.nfit_bl(Nat.add(1n+dp, 54n), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), fM)
97  +hbl = L.subst(Nat, z => {Nat.is_le(1n+z, M.bit_length(Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)))) == True{} : Bool}, 1n+Nat.add(dp, 54n), Nat.add(dp, 55n), Equal.sym(Nat, Nat.add(dp, 55n), 1n+Nat.add(dp, 54n), N.add_succ(dp, 54n)), bl1)
98  +sp1 = RT.round_jam(s, 1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), E, hbl)
99  +sp2 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.jam(z, C.low(1n+dp, 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(E, 1n+dp)), C.high(1n+dp, 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.div(C.shift(P, MX), 1n+yp), eH)
100  +sp3 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), z), Nat.add(E, 1n+dp)), C.low(1n+dp, 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.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))), eL)
101  +sp4 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.add(E, 1n+dp)), SW.jam(Nat.div(C.shift(P, MX), 1n+yp), 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)))), SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(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)))), Equal.sym(Nat, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(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)))), SW.jam(Nat.div(C.shift(P, MX), 1n+yp), 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)))), MP.jmin(Nat.div(C.shift(P, MX), 1n+yp), 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))))))
102  +sp5 = Equal.cong(Bool, F.F64, t => SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(t))), Nat.add(E, 1n+dp)), 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), zL)
103  +sp6 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), z), Nat.add(E, 1n+dp), x, hEx)
104  +spc = Equal.trans(F.F64, SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), E), SF.round(s, SW.jam(C.high(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), C.low(1n+dp, 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(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), sp1, Equal.trans(F.F64, SF.round(s, SW.jam(C.high(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), C.low(1n+dp, 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(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), C.low(1n+dp, 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(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), sp2, Equal.trans(F.F64, SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), C.low(1n+dp, 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(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), 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)))), Nat.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), sp3, Equal.trans(F.F64, SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), 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)))), Nat.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(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.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), sp4, Equal.trans(F.F64, SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(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.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), Nat.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), sp5, sp6)))))
105  Equal.trans(F.F64, F.div_q(s, e, aw, bw), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), E), imp, Equal.sym(F.F64, SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), E), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), spc))