def AP.inc

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

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

959def AP.inc(n: Nat, w: Word(n), d: Nat, h: {Nat.is_lt(1n+Word.to_nat(n, w), A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_le(d, n) == True{} : Bool}) -> {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}:
960  match n:
961    case 0n:
962      match w d:
963        case WNil{} 0n:
964          Empty.absurd({0n == 1n : Nat}, AP.ft(h))
965        case WNil{} 1n+e:
966          Empty.absurd({0n == 1n : Nat}, AP.ft(hd))
967    case 1n+ +q:
968      match w d:
969        case WCon{False{}, t} _:
970          {==}
971        case WCon{True{}, +t} 0n:
972          Empty.absurd({Word.to_nat(1n+q, Word.inc(1n+q, WCon{True{}, t})) == 1n+Word.to_nat(1n+q, WCon{True{}, t}) : Nat}, AP.ft(h))
973        case WCon{True{}, +t} 1n+ +e:
974          +x = Word.to_nat(q, t)
975          %Equal.sym(Nat, Word.to_nat(q, Word.inc(q, t)), 1n+x, AP.inc(q, t, e, AP.lt_bv_inv(False{}, 1n+x, A.Arrays.slots(e), h), hd)) : {Nat.double(_) == 2n+Nat.double(x) : Nat}
976          {==}