def jam1_k

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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

321def jam1_k(+q: Nat, +m: Nat, +hm: {Nat.mod(q, 2n) == m : Nat}, +h2: {Nat.is_lt(m, 2n) == True{} : Bool}) -> {SW.jam(q, 1n) == 1n+Nat.double(C.half(q)) : Nat}:
322  match m:
323    case 0n:
324      L.subst(Nat, z => {Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.max(z, 1n)) == 1n+Nat.double(C.half(q)) : Nat}, 0n, Nat.mod(q, 2n), Equal.sym(Nat, Nat.mod(q, 2n), 0n, hm), jam1_eq(q))
325    case 1n:
326      L.subst(Nat, z => {Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.max(z, 1n)) == 1n+Nat.double(C.half(q)) : Nat}, 1n, Nat.mod(q, 2n), Equal.sym(Nat, Nat.mod(q, 2n), 1n, hm), jam1_eq(q))
327    case 2n+z:
328      Empty.absurd({SW.jam(q, 1n) == 1n+Nat.double(C.half(q)) : Nat}, N.lt_zero_absurd(z, h2))