def dq_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divv.bend:85

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend as EX
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divf.bend as DF
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divx.bend as DX

85def dq_lt(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +EA: Nat, +A: WU.U64, +EB: Nat, +B: WU.U64, +MX: Nat, +yp: Nat, +sx: Nat, +sy: Nat, +XX: Nat, +XY: Nat, +hA: {SW.value(A) == C.shift(sx, MX) : Nat}, +hB: {SW.value(B) == C.shift(sy, 1n+yp) : Nat}, +a53: {C.fits(53n, SW.value(A)) == True{} : Bool}, +a52: {C.fits(52n, SW.value(A)) == False{} : Bool}, +b53: {C.fits(53n, SW.value(B)) == True{} : Bool}, +b52: {C.fits(52n, SW.value(B)) == False{} : Bool}, +hEAx: {Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat}, +hEBy: {Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat}, +hsx: {Nat.is_le(sx, 53n) == True{} : Bool}, +hsy: {Nat.is_le(sy, 53n) == True{} : Bool}, +hXX: {Nat.is_le(1926n, XX) == True{} : Bool}, +hXY: {Nat.is_le(XY, 3971n) == True{} : Bool}, +hlt0: {Nat.is_lt(SW.value(A), SW.value(B)) == True{} : Bool}) -> {F.div_q(s, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), X.add(A, A), B) == 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)), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))) : F.F64}:
86  +hlt = hlt0
87  +hu2 = N.le_trans(Nat.add(62n, 1n+sx), Nat.add(62n, 54n), 200n, N.le_add_left(1n+sx, 54n, 62n, hsx), {==})
88  +hva = Equal.trans(Nat, SW.value(X.add(A, A)), C.low(64n, Nat.add(SW.value(A), SW.value(A))), C.shift(1n+sx, MX), WA.add_value(A, A), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(A), SW.value(A))), Nat.add(SW.value(A), SW.value(A)), C.shift(1n+sx, MX), WW.low_fit(64n, Nat.add(SW.value(A), SW.value(A)), SH.fits_mono(54n, 64n, Nat.add(SW.value(A), SW.value(A)), {==}, FR.fits_add1(53n, SW.value(A), SW.value(A), a53, a53))), Equal.trans(Nat, Nat.add(SW.value(A), SW.value(A)), Nat.double(SW.value(A)), C.shift(1n+sx, MX), Equal.sym(Nat, Nat.double(SW.value(A)), Nat.add(SW.value(A), SW.value(A)), NA.double_self(SW.value(A))), Equal.cong(Nat, Nat, z => Nat.double(z), SW.value(A), C.shift(sx, MX), hA))))
89  +hle = L.subst(Nat, z => {Nat.is_le(SW.value(B), z) == True{} : Bool}, Nat.add(SW.value(A), SW.value(A)), SW.value(X.add(A, A)), Equal.sym(Nat, SW.value(X.add(A, A)), Nat.add(SW.value(A), SW.value(A)), Equal.trans(Nat, SW.value(X.add(A, A)), C.low(64n, Nat.add(SW.value(A), SW.value(A))), Nat.add(SW.value(A), SW.value(A)), WA.add_value(A, A), WW.low_fit(64n, Nat.add(SW.value(A), SW.value(A)), SH.fits_mono(54n, 64n, Nat.add(SW.value(A), SW.value(A)), {==}, FR.fits_add1(53n, SW.value(A), SW.value(A), a53, a53))))), N.lt_le(SW.value(B), Nat.add(SW.value(A), SW.value(A)), lt2x(one, h1, SW.value(B), SW.value(A), b53, a52)))
90  +hRlt = L.subst(Nat, z => {Nat.is_lt(Nat.sub(z, SW.value(B)), SW.value(B)) == True{} : Bool}, Nat.add(SW.value(A), SW.value(A)), SW.value(X.add(A, A)), Equal.sym(Nat, SW.value(X.add(A, A)), Nat.add(SW.value(A), SW.value(A)), Equal.trans(Nat, SW.value(X.add(A, A)), C.low(64n, Nat.add(SW.value(A), SW.value(A))), Nat.add(SW.value(A), SW.value(A)), WA.add_value(A, A), WW.low_fit(64n, Nat.add(SW.value(A), SW.value(A)), SH.fits_mono(54n, 64n, Nat.add(SW.value(A), SW.value(A)), {==}, FR.fits_add1(53n, SW.value(A), SW.value(A), a53, a53))))), sub_lt_of(Nat.add(SW.value(A), SW.value(A)), SW.value(B), N.lt_le(SW.value(B), Nat.add(SW.value(A), SW.value(A)), lt2x(one, h1, SW.value(B), SW.value(A), b53, a52)), add_lt2(SW.value(A), SW.value(B), hlt)))
91  +hf = Equal.trans(Nat, Nat.add(Nat.add(1n, sx), 1021n), Nat.add(sx, 1022n), Nat.add(sx, 1022n), Equal.trans(Nat, Nat.add(Nat.add(1n, sx), 1021n), Nat.add(Nat.add(sx, 1n), 1021n), Nat.add(sx, 1022n), Equal.cong(Nat, Nat, z => Nat.add(z, 1021n), Nat.add(1n, sx), Nat.add(sx, 1n), Equal.trans(Nat, Nat.add(1n, sx), Nat.add(1n, Nat.add(sx, 0n)), Nat.add(sx, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.trans(Nat, Nat.add(1n, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(1n, 0n)), Nat.add(sx, 1n), NA.add_swap(1n, sx, 0n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(sx, 1n), 1021n), Nat.add(sx, Nat.add(1n, 1021n)), Nat.add(sx, 1022n), NA.add_assoc(sx, 1n, 1021n), {==})), Equal.sym(Nat, Nat.add(sx, 1022n), Nat.add(sx, 1022n), Equal.trans(Nat, Nat.add(sx, 1022n), Nat.add(Nat.add(sx, 0n), 1022n), Nat.add(sx, 1022n), Equal.cong(Nat, Nat, z => Nat.add(z, 1022n), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), 1022n), Nat.add(sx, Nat.add(0n, 1022n)), Nat.add(sx, 1022n), NA.add_assoc(sx, 0n, 1022n), {==}))))
92  +hu = N.le_trans(sy, 62n, Nat.add(62n, 1n+sx), N.le_trans(sy, 53n, 62n, hsy, {==}), N.le_add_right(62n, 1n+sx))
93  +hP = Equal.sym(Nat, Nat.add(sy, Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.add(62n, 1n+sx), N.sub_add(Nat.add(62n, 1n+sx), sy, hu))
94  +hP200 = N.le_trans(Nat.sub(Nat.add(62n, 1n+sx), sy), Nat.add(62n, 1n+sx), 200n, sub_le0(Nat.add(62n, 1n+sx), sy), hu2)
95  +hdp = Equal.trans(Nat, Nat.add(Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.add(Nat.sub(Nat.add(62n, 1n+sx), sy), Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy))), 200n, NA.add_comm(Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.sub(Nat.add(62n, 1n+sx), sy)), N.sub_add(200n, Nat.sub(Nat.add(62n, 1n+sx), sy), hP200))
96  +bp = Nat.sub(SW.value(B), 1n)
97  +hBp = Equal.sym(Nat, 1n+Nat.sub(SW.value(B), 1n), SW.value(B), N.sub_add(SW.value(B), 1n, pos52(SW.value(B), b52)))
98  +hhi = hi_nz(B, DF.nfit_mono(32n, 52n, SW.value(B), {==}, b52))
99  +eEA = EX.eg(EA, sx, XX, hEAx, hsx, hXX)
100  +hEB = N.le_trans(EB, Nat.add(EB, sy), 6142n, N.le_add_right(EB, sy), L.subst(Nat, z => {Nat.is_le(z, 6142n) == True{} : Bool}, Nat.add(XY, 2171n), Nat.add(EB, sy), Equal.sym(Nat, Nat.add(EB, sy), Nat.add(XY, 2171n), hEBy), Equal.trans(Bool, Nat.is_le(Nat.add(XY, 2171n), Nat.add(3971n, 2171n)), Nat.is_le(XY, 3971n), True{}, FR.le_cancel_r(XY, 3971n, 2171n), hXY)))
101  +hEA2 = Equal.trans(Bool, Nat.is_le(Nat.add(4044n, Nat.add(F.off(), 1021n)), Nat.add(EA, Nat.add(F.off(), 1021n))), Nat.is_le(4044n, EA), True{}, FR.le_cancel_r(4044n, EA, Nat.add(F.off(), 1021n)), eEA)
102  +hle2 = N.le_trans(EB, 6142n, Nat.add(EA, Nat.add(F.off(), 1021n)), hEB, N.le_trans(6142n, Nat.add(4044n, Nat.add(F.off(), 1021n)), Nat.add(EA, Nat.add(F.off(), 1021n)), {==}, hEA2))
103  +hd = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), Nat.add(EB, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB)), Nat.add(EA, Nat.add(F.off(), 1021n)), NA.add_comm(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), N.sub_add(Nat.add(EA, Nat.add(F.off(), 1021n)), EB, hle2))
104  +he1 = L.subst(Nat, z => {Nat.is_le(Nat.add(4044n, Nat.add(F.off(), 1021n)), z) == True{} : Bool}, Nat.add(EA, Nat.add(F.off(), 1021n)), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), Nat.add(EA, Nat.add(F.off(), 1021n)), hd), hEA2)
105  +he2 = N.le_trans(Nat.add(2180n, 6142n), Nat.add(4044n, Nat.add(F.off(), 1021n)), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n), {==}, N.le_trans(Nat.add(4044n, Nat.add(F.off(), 1021n)), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n), he1, N.le_add_left(EB, 6142n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), hEB)))
106  +he = Equal.trans(Bool, Nat.is_le(2180n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB)), Nat.is_le(Nat.add(2180n, 6142n), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(2180n, 6142n), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n)), Nat.is_le(2180n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB)), FR.le_cancel_r(2180n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n)), he2)
107  +hx = Equal.trans(Nat, Nat.add(Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), 2180n), Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), NA.add_comm(Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), 2180n), N.sub_add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n, he))
108  +hXl = Equal.trans(Bool, Nat.is_le(Nat.add(Nat.add(XY, 200n), 1n), Nat.add(3971n, 201n)), Nat.is_le(Nat.add(XY, 201n), Nat.add(3971n, 201n)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(3971n, 201n)), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.add(XY, 200n), Nat.add(XY, 200n), Equal.trans(Nat, Nat.add(XY, 200n), Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, 200n), Equal.cong(Nat, Nat, z => Nat.add(z, 200n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, Nat.add(0n, 200n)), Nat.add(XY, 200n), NA.add_assoc(XY, 0n, 200n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, Nat.add(200n, 1n)), Nat.add(XY, 201n), NA.add_assoc(XY, 200n, 1n), {==})), Equal.sym(Nat, Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(XY, 201n), Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 201n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_assoc(XY, 0n, 201n), {==}))))), Equal.trans(Bool, Nat.is_le(Nat.add(XY, 201n), Nat.add(3971n, 201n)), Nat.is_le(XY, 3971n), True{}, FR.le_cancel_r(XY, 3971n, 201n), hXY))
109  +hXx = Equal.trans(Bool, Nat.is_le(Nat.add(1926n, 3000n), Nat.add(XX, 3000n)), Nat.is_le(1926n, XX), True{}, FR.le_cancel_r(1926n, XX, 3000n), hXX)
110  +hXle = N.le_trans(Nat.add(Nat.add(XY, 200n), 1n), 4926n, Nat.add(XX, 3000n), N.le_trans(Nat.add(Nat.add(XY, 200n), 1n), 4172n, 4926n, hXl, {==}), hXx)
111  +ha = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(XX, 3000n), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(XY, 201n)), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), N.add_zero(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), z), Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(XY, 201n), Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 201n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_assoc(XY, 0n, 201n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(0n, Nat.add(XY, 201n))), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), NA.add_assoc(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n, Nat.add(XY, 201n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), z), Nat.add(0n, Nat.add(XY, 201n)), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(0n, Nat.add(XY, 201n)), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_swap(0n, XY, 201n), {==})))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 201n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.add(XY, 200n), Nat.add(XY, 200n), Equal.trans(Nat, Nat.add(XY, 200n), Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, 200n), Equal.cong(Nat, Nat, z => Nat.add(z, 200n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, Nat.add(0n, 200n)), Nat.add(XY, 200n), NA.add_assoc(XY, 0n, 200n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, Nat.add(200n, 1n)), Nat.add(XY, 201n), NA.add_assoc(XY, 200n, 1n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XY, 201n), z), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), N.add_zero(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)))))), Equal.trans(Nat, Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(XY, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(XY, Nat.add(201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n))), Nat.add(XY, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n)), NA.add_assoc(XY, 201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Equal.cong(Nat, Nat, z => Nat.add(XY, z), Nat.add(201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n), Equal.trans(Nat, Nat.add(201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(201n, 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n), NA.add_swap(201n, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), {==}))), NA.add_swap(XY, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n))))), N.sub_add(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n), hXle))
112  +hG = DX.dexp(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), XX, XY, Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.sub(Nat.add(62n, 1n+sx), sy), 1n+sx, 1021n, sx, sy, EA, EB, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), ha, hdp, hP, hf, hEAx, hEBy, hd)
113  +hEx = NR.add_cancel(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy))), Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), Equal.trans(Nat, Nat.add(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)))), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), Equal.trans(Nat, Nat.add(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)))), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy))), 2180n), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), NA.add_comm(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)))), hG), Equal.sym(Nat, Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), Equal.trans(Nat, Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), Nat.add(Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), 2180n), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), NA.add_comm(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), hx))))
114  DF.dgen(one, h1, s, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), hx, X.add(A, A), B, Nat.sub(SW.value(B), 1n), hBp, MX, yp, 1n+sx, sy, Nat.sub(Nat.add(62n, 1n+sx), sy), Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)), hva, hB, hP, hdp, hle, hRlt, hhi, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), hEx)