def AP.wh2

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

import Base

1686# bv(b, x) = 2s + k: x is s + (x - s)
1687def AP.wh2(x: Nat, s: Nat, b: Bool, -k: Nat, e: {AP.bv(b, x) == Nat.add(Nat.double(s), k) : Nat}) -> {x == Nat.add(s, Nat.sub(x, s)) : Nat}:
1688  match x s:
1689    case 0n 0n:
1690      {==}
1691    case 0n 1n+q:
1692      Empty.absurd({0n == Nat.add(1n+q, Nat.sub(0n, 1n+q)) : Nat}, AP.wh0(b, q, k, e))
1693    case 1n+p 0n:
1694      {==}
1695    case 1n+p 1n+q:
1696      match b:
1697        case False{}:
1698          AP.succ_cong(p, Nat.add(q, Nat.sub(p, q)), AP.wh2(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))))
1699        case True{}:
1700          AP.succ_cong(p, Nat.add(q, Nat.sub(p, q)), AP.wh2(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))))