def par_shift

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:77

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/typed/width.bend as WW

77# the quotient's parity after at least one more bit
78def par_shift(+N0: Nat, +bp: Nat, +p: Nat) -> {Nat.mod(Nat.div(C.shift(1n+p, Nat.mod(N0, 1n+bp)), 1n+bp), 2n) == Nat.mod(Nat.div(C.shift(1n+p, N0), 1n+bp), 2n) : Nat}:
79  +B = Nat.add(1n, bp)
80  +t = Nat.add(1n, p)
81  +Q = Nat.div(N0, B)
82  +D = Nat.div(C.shift(t, Nat.mod(N0, B)), B)
83  +e1 = Equal.cong(Nat, Nat, u => Nat.div(u, B), C.shift(t, N0), Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, Nat.mod(N0, B))), shq(N0, bp, t))
84  +e2 = div_mul_add(C.shift(t, Q), bp, C.shift(t, Nat.mod(N0, B)))
85  +e3 = NA.add_comm(C.shift(t, Q), D)
86  +ed = Equal.trans(Nat, Nat.div(C.shift(t, N0), B), Nat.div(Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, Nat.mod(N0, B))), B), Nat.add(D, C.shift(t, Q)), e1, Equal.trans(Nat, Nat.div(Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, Nat.mod(N0, B))), B), Nat.add(C.shift(t, Q), D), Nat.add(D, C.shift(t, Q)), e2, e3))
87  +e4 = Equal.cong(Nat, Nat, u => Nat.mod(u, 2n), Nat.div(C.shift(t, N0), B), Nat.add(D, C.shift(t, Q)), ed)
88  Equal.sym(Nat, Nat.mod(Nat.div(C.shift(t, N0), B), 2n), Nat.mod(D, 2n), Equal.trans(Nat, Nat.mod(Nat.div(C.shift(t, N0), B), 2n), Nat.mod(Nat.add(D, C.shift(t, Q)), 2n), Nat.mod(D, 2n), e4, WW.odd_limb(p, D, Q)))