def half_dbl

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

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

55def half_dbl(+r: Nat, +x: Nat) -> {C.half(Nat.add(r, Nat.double(x))) == Nat.add(C.half(r), x) : Nat}:
56  match r:
57    case 0n:
58      match x:
59        case 0n:
60          {==}
61        case 1n+ +y:
62          Equal.cong(Nat, Nat, t => 1n+t, C.half(Nat.double(y)), y, half_dbl(0n, y))
63    case 1n:
64      match x:
65        case 0n:
66          {==}
67        case 1n+ +y:
68          Equal.cong(Nat, Nat, t => 1n+t, C.half(1n+Nat.double(y)), y, half_dbl(1n, y))
69    case 2n+ +s:
70      Equal.cong(Nat, Nat, t => 1n+t, C.half(Nat.add(s, Nat.double(x))), Nat.add(C.half(s), x), half_dbl(s, x))