def wq.shln

bend-osdev-word64@0.1.1.0 · PROOF.bend:193

import Base
import bend-osdev-word64@0.1.1.0/proof_shift.bend as PS

193def wq.shln(+w: Word(32n), k: Nat) -> {U32.shln(U32{w}, k) == U32{PS.ws.shl(32n, k, w)} : U32}:
194  match k:
195    case 0n:
196      {==}
197    case 1n+ +p:
198      %Equal.sym(U32, U32.shln(U32{w}, p), U32{PS.ws.shl(32n, p, w)}, wq.shln(w, p)) : {U32.shl(_) == U32{PS.ws.shl(32n, 1n+p, w)} : U32}
199      {==}