def specA

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divn.bend:72

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/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

72# the spec's significand cut at bit 1+dp, where P + dp = 200
73def specA(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat, +hP: {Nat.add(dp, P) == 200n : 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)) : Nat}:
74  +e0 = NR.dm_eq(yp, C.shift(P, MX))
75  +e1 = Equal.trans(Nat, C.shift(200n, MX), C.shift(Nat.add(dp, P), MX), C.shift(dp, C.shift(P, MX)), Equal.cong(Nat, Nat, z => C.shift(z, MX), 200n, Nat.add(dp, P), Equal.sym(Nat, Nat.add(dp, P), 200n, hP)), WW.shift_comp(dp, P, MX))
76  +e2 = Equal.cong(Nat, Nat, z => C.shift(dp, z), C.shift(P, MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp)), e0)
77  +e3 = WW.shift_add(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))
78  +e4 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Equal.sym(Nat, Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), WW.shift_mul_l(dp, Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)))
79  +e5 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), z), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), NR.dm_eq(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))))
80  +e6 = Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.add_assoc(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
81  +e7 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Equal.sym(Nat, Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), NA.mul_add_right(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)))
82  +eN = Equal.trans(Nat, C.shift(200n, MX), C.shift(dp, C.shift(P, MX)), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e1, Equal.trans(Nat, C.shift(dp, C.shift(P, MX)), C.shift(dp, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e2, Equal.trans(Nat, C.shift(dp, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e3, Equal.trans(Nat, Nat.add(C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e4, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e5, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e6, e7))))))
83  +hb = NR.dm_lt(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)))
84  +eD = Equal.trans(Nat, Nat.div(C.shift(200n, MX), 1n+yp), Nat.div(Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Equal.cong(Nat, Nat, z => Nat.div(z, 1n+yp), C.shift(200n, MX), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eN), NR.div_of(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), yp, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), hb))
85  +eR = Equal.trans(Nat, Nat.mod(C.shift(200n, MX), 1n+yp), Nat.mod(Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+yp), C.shift(200n, MX), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eN), NR.mod_of(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), yp, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), hb))
86  +m1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, z), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.div(C.shift(200n, MX), 1n+yp), Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eD)
87  +m2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(z, 1n)), Nat.mod(C.shift(200n, MX), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), eR)
88  +m3 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Equal.sym(Nat, Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.double_mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))))
89  +m4 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.double_add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
90  +m5 = NA.add_assoc(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))
91  +m6 = NA.add_comm(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)))
92  +m7 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 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))), NA.add_comm(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)))
93  +ch = Equal.trans(Nat, 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.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 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))), m1, Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 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))), m2, Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 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))), m3, Equal.trans(Nat, Nat.add(Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 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))), m4, Equal.trans(Nat, Nat.add(Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 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))), m5, Equal.trans(Nat, Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))), Nat.add(Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), C.shift(1n+dp, Nat.div(C.shift(P, MX), 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))), m6, m7))))))
94  Equal.sym(Nat, 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))), ch)