~/jendhub

def AP.sp

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

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

364def AP.sp(n: Nat, d: Nat) -> {Word.shl.put(n, False{}, AP.pw(n, d)) == AP.pw(n, 1n+d) : Word(n)}:
365  match n:
366    case 0n:
367      {==}
368    case 1n+ +q:
369      match d:
370        case 0n:
371          AP.wcon_cong(q, False{}, Word.shl.put(q, True{}, Word.zero(q)), AP.pw(q, 0n), AP.spz(q))
372        case 1n+ +e:
373          AP.wcon_cong(q, False{}, Word.shl.put(q, False{}, AP.pw(q, e)), AP.pw(q, 1n+e), AP.sp(q, e))

Uses (8)

Used by (1)