1 import Base 2 import ./f64light.bend as FL 3 import ../../../spec/lib/common.bend as C 4 import ../../../spec/math/f64.bend as SF 5 import ../../../spec/math/w64.bend as SW 6 import ../../../src/math/f64.bend as F 7 import ../../../src/math/w64.bend as X 8 import ../../../src/math/u64.bend as WU 9 import ../../../src/math/natural.bend as M 10 import ../../lib/nat.bend as N 11 import ../../lib/logic.bend as L 12 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 13 import ../natural/arith.bend as NR 14 import ./width.bend as WW 15 import ./w64add.bend as WA 16 import ./w64sh.bend as SH 17 import ./f64round.bend as FR 18 import ./f64rtools.bend as RT 19 import ./f64mulp.bend as MP 20 import ./f64adda.bend as AA 21 import ./f64divd.bend as DD 22 import ./w64mm.bend as MM 23 import ./w64est.bend as W64E 24 import ./f64divn.bend as DN 25 import ./f64divq.bend as DQ 26 27 # SoftFloat's f64_div quotient step (div_q) is the spec's division, rounded 28 # once: its two 32-bit quotient digits and sticky bit are the spec's 29 # 2 * floor(MX * 2^200 / MY) + [remainder != 0] cut at the rounding scale. 30 31 def v(+x: U32) -> Nat: 32 U32.to_nat(x) 33 34 def e0(+rl: U32, +rh: U32, +ml: U32, +mh: U32, +t: Nat) -> U32: 35 X.q_est(WU.U64{0, rl}, rh, WU.U64{ml, mh}, t) 36 37 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}: 38 match r b: 39 case WU.U64{+rl, +rh} WU.U64{+ml, +mh}: 40 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)) 41 42 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}: 43 match r b: 44 case WU.U64{+rl, +rh} WU.U64{+ml, +mh}: 45 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)) 46 47 def dm2(+l: Bool, +r: Bool) -> {Bool.or(Bool.not(r), Bool.not(l)) == Bool.not(Bool.and(l, r)) : Bool}: 48 FL.dm2(l, r) 49 50 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}: 51 FL.nfit_mono_c(a, b, x, hab, h, c, hc) 52 53 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}: 54 FL.nfit_mono(a, b, x, hab, h) 55 56 # the quotient step, for a in [b, 2b), a = MX * 2^u, b = MY * 2^w, 62 + u = w + P, P + dp = 200 57 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}: 58 sv = WA.sub_value(aw, bw, hle) 59 +eR = Equal.trans(Nat, SW.value(X.sub(aw, bw)), Nat.sub(SW.value(aw), SW.value(bw)), Nat.sub(SW.value(aw), SW.value(bw)), sv, {==}) 60 +hx1 = L.subst(Nat, z => {Nat.is_lt(z, SW.value(bw)) == True{} : Bool}, Nat.sub(SW.value(aw), SW.value(bw)), SW.value(X.sub(aw, bw)), Equal.sym(Nat, SW.value(X.sub(aw, bw)), Nat.sub(SW.value(aw), SW.value(bw)), eR), hRlt) 61 +q1 = dq96q(one, h1, X.sub(aw, bw), bw, X.bitlen(X.hi(bw)), hx1, hhi, {==}) 62 +r1 = dq96r(one, h1, X.sub(aw, bw), bw, X.bitlen(X.hi(bw)), hx1, hhi, {==}) 63 +hx2 = L.subst(Nat, z => {Nat.is_lt(SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), z) == True{} : Bool}, 1n+bp, SW.value(bw), Equal.sym(Nat, SW.value(bw), 1n+bp, hBp), L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), Equal.sym(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), Equal.trans(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), SW.value(bw)), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), r1, Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), z), SW.value(bw), 1n+bp, hBp))), NR.dm_lt(bp, C.shift(32n, SW.value(X.sub(aw, bw)))))) 64 +q2 = dq96q(one, h1, X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))), bw, X.bitlen(X.hi(bw)), hx2, hhi, {==}) 65 +r2 = dq96r(one, h1, X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))), bw, X.bitlen(X.hi(bw)), hx2, hhi, {==}) 66 +e1 = Equal.trans(Nat, v(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))), Nat.div(C.shift(32n, SW.value(X.sub(aw, bw))), SW.value(bw)), Nat.div(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), q1, Equal.cong(Nat, Nat, z => Nat.div(C.shift(32n, SW.value(X.sub(aw, bw))), z), SW.value(bw), 1n+bp, hBp)) 67 +f1 = Equal.trans(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), SW.value(bw)), Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), 1n+bp), r1, Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, SW.value(X.sub(aw, bw))), z), SW.value(bw), 1n+bp, hBp)) 68 +e2 = Equal.trans(Nat, v(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw)))), Nat.div(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), SW.value(bw)), Nat.div(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), 1n+bp), q2, Equal.cong(Nat, Nat, z => Nat.div(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), z), SW.value(bw), 1n+bp, hBp)) 69 +f2 = Equal.trans(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), SW.value(bw)), Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), 1n+bp), r2, Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), z), SW.value(bw), 1n+bp, hBp)) 70 +tw = DD.two(bp, SW.value(X.sub(aw, bw)), v(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))), SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), v(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw)))), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), e1, f1, e2, f2) 71 +hQ = Equal.trans(Nat, Nat.add(Nat.mul(SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}), 1n+bp), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw))))), Nat.add(Nat.mul(Nat.add(C.shift(32n, v(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))))), v(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))))), 1n+bp), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U 72 +hr2 = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), 1n+bp), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), Equal.sym(Nat, SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), Nat.mod(C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))), 1n+bp), f2), NR.dm_lt(bp, C.shift(32n, SW.value(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))))) 73 +iT = DQ.iq_T(one, h1, bp, SW.value(X.sub(aw, bw)), SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), hQ) 74 +eA = Equal.trans(Nat, Nat.add(SW.value(X.sub(aw, bw)), 1n+bp), Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), C.shift(u, MX), Equal.trans(Nat, Nat.add(SW.value(X.sub(aw, bw)), 1n+bp), Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), 1n+bp), Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), Equal.cong(Nat, Nat, z => Nat.add(z, 1n+bp), SW.value(X.sub(aw, bw)), Nat.sub(SW.value(aw), SW.value(bw)), eR), Equal.cong(Nat, Nat, z => Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), z), 1n+bp, SW.value(bw), Equal.sym(Nat, SW.value(bw), 1n+bp, hBp))), Equal.trans(Nat, Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), SW.value(aw), C.shift(u, MX), Equal.trans(Nat, Nat.add(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), Nat.add(SW.value(bw), Nat.sub(SW.value(aw), SW.value(bw))), SW.value(aw), NA.add_comm(Nat.sub(SW.value(aw), SW.value(bw)), SW.value(bw)), N.sub_add(SW.value(aw), SW.value(bw), hle)), ha)) 75 +hE = Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), 1n+bp), Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp))), C.shift(62n, Nat.add(SW.value(X.sub(aw, bw)), 1n+bp)), C.shift(62n, C.shift(u, MX)), iT, Equal.cong(Nat, Nat, z => C.shift(62n, z), Nat.add(SW.value(X.sub(aw, bw)), 1n+bp), C.shift(u, MX), eA)) 76 +he = DN.iq_lt(bp, SW.value(X.sub(aw, bw)), SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), hQ, hr2) 77 +hBw = Equal.trans(Nat, C.shift(w, 1n+yp), SW.value(bw), 1n+bp, Equal.sym(Nat, SW.value(bw), C.shift(w, 1n+yp), hb), hBp) 78 +jq = DN.jn_q(MX, yp, u, w, P, hP, bp, hBw, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp)), hE, he) 79 +jz = DN.jn_z(MX, yp, u, w, P, hP, bp, hBw, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Nat.sub(C.shift(62n, SW.value(X.sub(aw, bw))), Nat.mul(C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 1n+bp)), hE, he) 80 +iz = DN.iq_z(bp, SW.value(X.sub(aw, bw)), SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}), SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), hQ) 81 +est = Equal.trans(Bool, Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))), Bool.not(Bool.and(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n), Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X. 82 +im1 = DQ.dq_round(one, h1, s, e, x, hx, X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw))), 1073741824, {==}) 83 +im2 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.jam(z, SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))))), x), Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Nat.div(C.shift(P, MX), 1n+yp), jq) 84 +im3 = Equal.cong(Bool, F.F64, t => SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(t)), x), Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))), Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)), est) 85 +imp = Equal.trans(F.F64, F.div_q(s, e, aw, bw), SF.round(s, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), SF.b2n(Bool.or(Bool.not(Nat.is_eq(SW.value(X.sub(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), bw)))), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})), 0n))))), x), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), im1, Equal.trans(F.F64, SF.round(s, SW.jam(Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.h 86 +sA = DN.specA(MX, yp, P, dp, hdp) 87 +fL = DN.specA_fit(MX, yp, P, dp) 88 +zL = DN.specA_z(MX, yp, P, dp) 89 +eH = Equal.trans(Nat, C.high(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), C.high(1n+dp, Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)))), Nat.div(C.shift(P, MX), 1n+yp), Equal.cong(Nat, Nat, z => C.high(1n+dp, z), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Equal.sym(Nat, Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), sA)), WW.high_u(1n+dp, Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.div(C.shift(P, MX), 1n+yp), fL)) 90 +eL = Equal.trans(Nat, C.low(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), C.low(1n+dp, Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)))), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Equal.cong(Nat, Nat, z => C.low(1n+dp, z), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Equal.sym(Nat, Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), sA)), WW.low_u(1n+dp, Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.div(C.shift(P, MX), 1n+yp), fL)) 91 +q62 = Equal.trans(Bool, C.fits(62n, Nat.div(C.shift(P, MX), 1n+yp)), C.fits(62n, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))})))), False{}, Equal.cong(Nat, Bool, z => C.fits(62n, z), Nat.div(C.shift(P, MX), 1n+yp), Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Equal.sym(Nat, Nat.add(C.shift(62n, one), C.high(2n, SW.value(WU.U64{X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw)))), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw)))}))), Nat.div(C.shift(P, MX), 1n+yp), jq)), DQ.t62(one, h1, X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), X.q96(WU.U64{0, X.lo(X.sub(WU.U64{0, X.lo(X.sub(aw, bw))}, X.fst_q(X.mul_32_64(X.q96(WU.U64{0, X.lo(X.sub(aw, bw))}, X.hi(X.sub(aw, bw)), bw, X.bitlen(X.hi(bw))), bw))))}, X.hi(X.sub(WU.U64{0, X.l 92 +q54 = nfit_mono(54n, 62n, Nat.div(C.shift(P, MX), 1n+yp), {==}, q62) 93 +f54 = Equal.trans(Bool, C.fits(Nat.add(1n+dp, 54n), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), C.fits(54n, Nat.div(C.shift(P, MX), 1n+yp)), False{}, RT.fits_sh(1n+dp, 54n, Nat.div(C.shift(P, MX), 1n+yp)), q54) 94 +hle2 = L.subst(Nat, z => {Nat.is_le(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), z) == True{} : Bool}, Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Equal.trans(Nat, Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), NA.add_comm(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), sA), N.le_add_right(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))))) 95 +fM = FR.nfit(Nat.add(1n+dp, 54n), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), hle2, f54) 96 +bl1 = AA.nfit_bl(Nat.add(1n+dp, 54n), Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), fM) 97 +hbl = L.subst(Nat, z => {Nat.is_le(1n+z, M.bit_length(Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)))) == True{} : Bool}, 1n+Nat.add(dp, 54n), Nat.add(dp, 55n), Equal.sym(Nat, Nat.add(dp, 55n), 1n+Nat.add(dp, 54n), N.add_succ(dp, 54n)), bl1) 98 +sp1 = RT.round_jam(s, 1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), E, hbl) 99 +sp2 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.jam(z, C.low(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)))), Nat.add(E, 1n+dp)), C.high(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), Nat.div(C.shift(P, MX), 1n+yp), eH) 100 +sp3 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), z), Nat.add(E, 1n+dp)), C.low(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), eL) 101 +sp4 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.add(E, 1n+dp)), SW.jam(Nat.div(C.shift(P, MX), 1n+yp), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), 0n)))), Equal.sym(Nat, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), 0n)))), SW.jam(Nat.div(C.shift(P, MX), 1n+yp), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), MP.jmin(Nat.div(C.shift(P, MX), 1n+yp), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))))) 102 +sp5 = Equal.cong(Bool, F.F64, t => SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(t))), Nat.add(E, 1n+dp)), Nat.is_eq(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), zL) 103 +sp6 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), z), Nat.add(E, 1n+dp), x, hEx) 104 +spc = Equal.trans(F.F64, SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), E), SF.round(s, SW.jam(C.high(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), C.low(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)))), Nat.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), sp1, Equal.trans(F.F64, SF.round(s, SW.jam(C.high(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n))), C.low(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)))), Nat.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), C.low(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)))), Nat.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), sp2, Equal.trans(F.F64, SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), C.low(1n+dp, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)))), Nat.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), Nat.add(E, 1n+dp)), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), sp3, Equal.trans(F.F64, SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), Nat.add(E, 1n+dp)), SF.round(s, SW.jam(N 105 Equal.trans(F.F64, F.div_q(s, e, aw, bw), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), E), imp, Equal.sym(F.F64, SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), E), SF.round(s, SW.jam(Nat.div(C.shift(P, MX), 1n+yp), SF.b2n(Bool.not(Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n)))), x), spc))