def AP.val0

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

import Base

886def AP.val0(n: Nat, w: Word(n), e: {Word.to_nat(n, w) == 0n : Nat}) -> {w == Word.zero(n) : Word(n)}:
887  match n:
888    case 0n:
889      match w:
890        case WNil{}:
891          {==}
892    case 1n+ +q:
893      match w:
894        case WCon{False{}, +t}:
895          AP.wcon_cong(q, False{}, t, Word.zero(q), AP.val0(q, t, AP.double_zero(Word.to_nat(q, t), e)))
896        case WCon{True{}, +t}:
897          Empty.absurd({WCon{True{}, t} == Word.zero(1n+q) : Word(1n+q)}, AP.sz(Nat.double(Word.to_nat(q, t)), e))