~/jendhub

def AP.shr_pw

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

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

415def AP.shr_pw(n: Nat, d: Nat, h: {Nat.is_lt(1n+d, n) == True{} : Bool}) -> {Word.shr(n, AP.pw(n, 1n+d)) == AP.pw(n, d) : Word(n)}:
416  match n:
417    case 0n:
418      Empty.absurd({Word.shr(0n, AP.pw(0n, 1n+d)) == AP.pw(0n, d) : Word(0n)}, AP.ft(h))
419    case 1n+q:
420      AP.padp(q, d, h)

Uses (9)

Used by (1)