def pair_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/random/lemire.bend:384

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

384# [2a == k] + [2a + 1 == k] == [a == k / 2]
385def pair_eq(+a: Nat, +k: Nat) -> {Nat.add(b2n(Nat.is_eq(Nat.double(a), k)), b2n(Nat.is_eq(1n+Nat.double(a), k))) == b2n(Nat.is_eq(a, C.half(k))) : Nat}:
386  match a k:
387    case 0n 0n:
388      {==}
389    case 0n 1n:
390      {==}
391    case 0n 2n+q:
392      {==}
393    case 1n+p 0n:
394      {==}
395    case 1n+p 1n:
396      {==}
397    case 1n+p 2n+q:
398      pair_eq(p, q)