def jam0_m

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sh.bend:312

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

312def jam0_m(+q: Nat, +m: Nat, +hm: {Nat.mod(q, 2n) == m : Nat}, +h2: {Nat.is_lt(m, 2n) == True{} : Bool}) -> {SW.jam(q, 0n) == q : Nat}:
313  match m:
314    case 0n:
315      L.subst(Nat, z => {Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.max(z, 0n)) == q : Nat}, 0n, Nat.mod(q, 2n), Equal.sym(Nat, Nat.mod(q, 2n), 0n, hm), L.subst(Nat, z => {Nat.add(Nat.mul(2n, Nat.div(q, 2n)), z) == q : Nat}, Nat.mod(q, 2n), 0n, hm, jam0_eq(q)))
316    case 1n:
317      L.subst(Nat, z => {Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.max(z, 0n)) == q : Nat}, 1n, Nat.mod(q, 2n), Equal.sym(Nat, Nat.mod(q, 2n), 1n, hm), L.subst(Nat, z => {Nat.add(Nat.mul(2n, Nat.div(q, 2n)), z) == q : Nat}, Nat.mod(q, 2n), 1n, hm, jam0_eq(q)))
318    case 2n+z:
319      Empty.absurd({SW.jam(q, 0n) == q : Nat}, N.lt_zero_absurd(z, h2))