def wsd.pwv

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:90

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

90def wsd.pwv(n: Nat, k: Nat, h: {Nat.is_lt(k, n) == True{} : Bool}) -> {Word.to_nat(n, wsd.pw(n, k)) == U.U32Nat.dbl(k, 1n) : Nat}:
91  match n:
92    case 0n:
93      Empty.absurd({Word.to_nat(0n, wsd.pw(0n, k)) == U.U32Nat.dbl(k, 1n) : Nat}, wn.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, P.wn.not_lt_zero(k), h)))
94    case 1n+ +p:
95      match k:
96        case 0n:
97          Equal.cong(Nat, Nat, zz => 1n+Nat.double(zz), Word.to_nat(p, Word.zero(p)), 0n, UL.word_zero_value(p))
98        case 1n+ +j:
99          Equal.cong(Nat, Nat, zz => Nat.double(zz), Word.to_nat(p, wsd.pw(p, j)), U.U32Nat.dbl(j, 1n), wsd.pwv(p, j, h))