def uq.shr_w
bend-osdev-algo@0.1.0.0 · proof_u32.bend:547
import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
import Base
547def uq.shr_w(n: Nat, w: Word(n)) -> {Word.to_nat(n, Word.shr(n, w)) == uq.half(Word.to_nat(n, w)) : Nat}:
548 match n:
549 case 0n:
550 {==}
551 case 1n+ +p:
552 match w:
553 case WCon{False{}, +t}:
554 Equal.trans(Nat, Word.to_nat(1n+p, Word.shr.pad(p, t)), Word.to_nat(p, t), uq.half(Nat.double(Word.to_nat(p, t))), uq.pad(p, t), Equal.sym(Nat, uq.half(Nat.double(Word.to_nat(p, t))), Word.to_nat(p, t), uq.half_dbl(Word.to_nat(p, t))))
555 case WCon{True{}, +t}:
556 Equal.trans(Nat, Word.to_nat(1n+p, Word.shr.pad(p, t)), Word.to_nat(p, t), uq.half(1n+Nat.double(Word.to_nat(p, t))), uq.pad(p, t), Equal.sym(Nat, uq.half(1n+Nat.double(Word.to_nat(p, t))), Word.to_nat(p, t), uq.half_dbl1(Word.to_nat(p, t))))