def AP.wh

bend-osdev-array@0.1.0.1 · PROOF.bend:1670

import Base

1670# bv(b, x) = 2s + k: k is bv(b, x - s)
1671def AP.wh(x: Nat, s: Nat, b: Bool, -k: Nat, e: {AP.bv(b, x) == Nat.add(Nat.double(s), k) : Nat}) -> {k == AP.bv(b, Nat.sub(x, s)) : Nat}:
1672  match x s:
1673    case 0n 0n:
1674      Equal.sym(Nat, AP.bv(b, 0n), k, e)
1675    case 0n 1n+q:
1676      Empty.absurd({k == AP.bv(b, Nat.sub(0n, 1n+q)) : Nat}, AP.wh0(b, q, k, e))
1677    case 1n+p 0n:
1678      Equal.sym(Nat, AP.bv(b, 1n+p), k, e)
1679    case 1n+p 1n+q:
1680      match b:
1681        case False{}:
1682          AP.wh(p, q, False{}, k, AP.pred_cong(Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(1n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e)))
1683        case True{}:
1684          AP.wh(p, q, True{}, k, AP.pred_cong(1n+Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(2n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e)))