def specA_z

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

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

103# the low part is zero exactly when MX * 2^P is a multiple of MY
104def specA_z(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat) -> {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) : Bool}:
105  +z1 = add_eq0(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)))
106  +z2 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), min1_eq0(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
107  +z3 = Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), t), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), WW.dbl_eq0(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
108  +z4 = and_comm(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n))
109  +z5 = Equal.sym(Bool, Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), mul_eq0(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), yp))
110  +z6 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), z5)
111  +z7 = Equal.sym(Bool, Nat.is_eq(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)), 0n), Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), add_eq0(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)))
112  +z8 = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), 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)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.sym(Nat, 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)))))
113  +z9 = WW.shift_eq0(dp, Nat.mod(C.shift(P, MX), 1n+yp))
114  Equal.trans(Bool, 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), Bool.and(Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(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), z1, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(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), z2, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(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), z3, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Bool.and(Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mod(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), z4, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(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), z6, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(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)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z7, Equal.trans(Bool, Nat.is_eq(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)), 0n), Nat.is_eq(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z8, z9)))))))