def jn_z

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

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/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

187def jn_z(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}, +T: Nat, +e: Nat, +hE: {Nat.add(Nat.mul(T, 1n+bp), e) == C.shift(62n, C.shift(u, MX)) : Nat}, +he: {Nat.is_lt(e, 1n+bp) == True{} : Bool}) -> {Nat.is_eq(e, 0n) == Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n) : Bool}:
188  +eq = Equal.trans(Nat, Nat.add(Nat.mul(T, 1n+bp), e), C.shift(62n, C.shift(u, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), hE, jn_eq(MX, yp, u, w, P, hP, bp, hB))
189  +mT = NR.mod_of(T, bp, e, he)
190  +mQ = NR.mod_of(Nat.div(C.shift(P, MX), 1n+yp), bp, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), jn_lt(MX, yp, w, P, bp, hB))
191  +ee = Equal.trans(Nat, e, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), e, mT), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.mod(Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(Nat.mul(T, 1n+bp), e), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), eq), mQ))
192  Equal.trans(Bool, Nat.is_eq(e, 0n), Nat.is_eq(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), e, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), ee), WW.shift_eq0(w, Nat.mod(C.shift(P, MX), 1n+yp)))