def AP.val_pw

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

import Base
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

433def AP.val_pw(n: Nat, d: Nat, h: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.to_nat(n, AP.pw(n, d)) == A.Arrays.slots(d) : Nat}:
434  match n:
435    case 0n:
436      match d:
437        case 0n:
438          Empty.absurd({Word.to_nat(0n, AP.pw(0n, 0n)) == A.Arrays.slots(0n) : Nat}, AP.ft(h))
439        case 1n+e:
440          Empty.absurd({Word.to_nat(0n, AP.pw(0n, 1n+e)) == A.Arrays.slots(1n+e) : Nat}, AP.ft(h))
441    case 1n+ +q:
442      match d:
443        case 0n:
444          %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, UL.word_zero_value(q)) : {1n+Nat.double(_) == 1n : Nat}
445          {==}
446        case 1n+ +e:
447          AP.double_cong(Word.to_nat(q, AP.pw(q, e)), A.Arrays.slots(e), AP.val_pw(q, e, h))