def bit_dbl

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:72

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

72def bit_dbl(+r: Nat, +x: Nat) -> {C.bit(Nat.add(r, Nat.double(x))) == C.bit(r) : Nat}:
73  match r:
74    case 0n:
75      match x:
76        case 0n:
77          {==}
78        case 1n+ +y:
79          bit_dbl(0n, y)
80    case 1n:
81      match x:
82        case 0n:
83          {==}
84        case 1n+ +y:
85          bit_dbl(1n, y)
86    case 2n+ +s:
87      bit_dbl(s, x)