import Base
import ./f64light.bend as FL
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./width.bend as WW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64mulp.bend as MP
import ./f64adda.bend as AA
import ./f64divd.bend as DD
import ./w64mm.bend as MM
import ./w64est.bend as W64E
import ./f64divn.bend as DN
import ./f64divq.bend as DQ

# SoftFloat's f64_div quotient step (div_q) is the spec's division, rounded
# once: its two 32-bit quotient digits and sticky bit are the spec's
# 2 * floor(MX * 2^200 / MY) + [remainder != 0] cut at the rounding scale.

def v(+x: U32) -> Nat:
  U32.to_nat(x)

def e0(+rl: U32, +rh: U32, +ml: U32, +mh: U32, +t: Nat) -> U32:
  X.q_est(WU.U64{0, rl}, rh, WU.U64{ml, mh}, t)

def dq96q(+one: Nat, +h1: {one == 1n : Nat}, +r: WU.U64, +b: WU.U64, +t: Nat, +hx: {Nat.is_lt(SW.value(r), SW.value(b)) == True{} : Bool}, +hz: {U32.is_zero(X.hi(b)) == False{} : Bool}, +ht: {X.bitlen(X.hi(b)) == t : Nat}) -> {v(X.q96(WU.U64{0, X.lo(r)}, X.hi(r), b, t)) == Nat.div(C.shift(32n, SW.value(r)), SW.value(b)) : Nat}:
  match r b:
    case WU.U64{+rl, +rh} WU.U64{+ml, +mh}:
      DD.dig_q(one, h1, rl, rh, ml, mh, e0(rl, rh, ml, mh, t), hx, hz, W64E.est_t(one, h1, WU.U64{0, rl}, rh, ml, mh, hz, MM.red_hx(one, h1, 0, rl, rh, ml, mh, hx), t, ht))

def dq96r(+one: Nat, +h1: {one == 1n : Nat}, +r: WU.U64, +b: WU.U64, +t: Nat, +hx: {Nat.is_lt(SW.value(r), SW.value(b)) == True{} : Bool}, +hz: {U32.is_zero(X.hi(b)) == False{} : Bool}, +ht: {X.bitlen(X.hi(b)) == t : Nat}) -> {SW.value(X.sub(WU.U64{0, X.lo(r)}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(r)}, X.hi(r), b, t), b)))) == Nat.mod(C.shift(32n, SW.value(r)), SW.value(b)) : Nat}:
  match r b:
    case WU.U64{+rl, +rh} WU.U64{+ml, +mh}:
      DD.dig_r(one, h1, rl, rh, ml, mh, e0(rl, rh, ml, mh, t), hx, hz, W64E.est_t(one, h1, WU.U64{0, rl}, rh, ml, mh, hz, MM.red_hx(one, h1, 0, rl, rh, ml, mh, hx), t, ht))

def dm2(+l: Bool, +r: Bool) -> {Bool.or(Bool.not(r), Bool.not(l)) == Bool.not(Bool.and(l, r)) : Bool}:
  FL.dm2(l, r)

def nfit_mono_c(+a: Nat, +b: Nat, +x: Nat, +hab: {Nat.is_le(a, b) == True{} : Bool}, +h: {C.fits(b, x) == False{} : Bool}, +c: Bool, +hc: {C.fits(a, x) == c : Bool}) -> {c == False{} : Bool}:
  FL.nfit_mono_c(a, b, x, hab, h, c, hc)

def nfit_mono(+a: Nat, +b: Nat, +x: Nat, +hab: {Nat.is_le(a, b) == True{} : Bool}, +h: {C.fits(b, x) == False{} : Bool}) -> {C.fits(a, x) == False{} : Bool}:
  FL.nfit_mono(a, b, x, hab, h)

# 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))