F64divf.dgen: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend as F64divf Lines 56-105 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend&start_line=56&end_line=105 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 # the quotient step, for a in [b, 2b), a = MX * 2^u, b = MY * 2^w, 62 + u = w + P, P + dp = 200 def 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}: sv = WA.sub_value(aw, bw, hle) +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, {==}) +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) +q1 = dq96q(one, h1, X.sub(aw, bw), bw, X.bitlen(X.hi(bw)), hx1, hhi, {==}) +r1 = dq96r(one, h1, X.sub(aw, bw), bw, X.bitlen(X.hi(bw)), hx1, hhi, {==}) +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)))))) +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, {==}) +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, {==}) +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)) +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)) +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)) +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)) +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) +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) +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))))))) +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) +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)) +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)) +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) +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) +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) +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) +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) +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))) +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, {==}) +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) +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) +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)) +sA = DN.specA(MX, yp, P, dp, hdp) +fL = DN.specA_fit(MX, yp, P, dp) +zL = DN.specA_z(MX, yp, P, dp) +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)) +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)) +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))))) +q54 = nfit_mono(54n, 62n, Nat.div(C.shift(P, MX), 1n+yp), {==}, q62) +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) +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))))) +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) +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) +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) +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) +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) +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) +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)))))) +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) +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) +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))))) 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)) Uses (68): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.min https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_succ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_right https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=dm_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&name=nfit_bl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divd.bend&name=two https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend&name=dm2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend&name=dq96q https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend&name=dq96r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend&name=nfit_mono https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend&name=iq_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend&name=iq_z https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend&name=jn_q https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend&name=jn_z https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend&name=specA https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend&name=specA_fit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend&name=specA_z https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend&name=dq_round https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend&name=iq_T https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend&name=t62 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulp.bend&name=jmin https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=nfit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=fits_sh https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=round_jam https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=sub_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_u https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_u https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=b2n https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=round https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=jam https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=div_q https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=bit_length https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=bitlen https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=fst_q https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=hi https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=lo https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=mul_32_64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=q96 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=sub