def parq

bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:69

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/spec/math/f64.bend as SF

69def parq(+q: Nat) -> {Nat.add(q, SF.b2n(Nat.is_eq(C.bit(q), 1n))) == Nat.double(C.half(Nat.add(q, 1n))) : Nat}:
70  match q:
71    case 0n:
72      {==}
73    case 1n:
74      {==}
75    case 2n+ +p:
76      Equal.cong(Nat, Nat, z => 2n+z, Nat.add(p, SF.b2n(Nat.is_eq(C.bit(p), 1n))), Nat.double(C.half(Nat.add(p, 1n))), parq(p))