PROOF.wq.shl.go: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF.bend as PROOF
Lines 209-222 of bend-osdev-word64@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&start_line=209&end_line=222

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-word64@0.1.1.0/proof_value.bend as P
import bend-osdev-word64@0.1.1.0/proof_shift.bend as PS

def wq.shl.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, +hw: Word(32n), +lw: Word(32n), +chw: Word(32n), +clw: Word(32n), ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, hk: {Nat.is_lt(k, 64n) == True{} : Bool}, +h: {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), W.W64.to_nat(W.W64{U32{chw}, U32{clw}})) == True{} : Bool}) -> {W.W64.to_nat(W.W64.shl.pick(z, l32, l64, k, W.W64{U32{hw}, U32{lw}})) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}:
  match z l32 l64:
    case True{} _ _:
      Equal.sym(Nat, U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(v, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), k, 0n, PS.ns.eq_zero(k, ez)))
    case False{} True{} _:
      %Equal.sym(U32, U32.shln(U32{hw}, k), U32{PS.ws.shl(32n, k, hw)}, wq.shln(hw, k)) : {W.W64.to_nat(W.W64{U32.or(_, U32.shrn(U32{lw}, Nat.sub(32n, k))), U32.shln(U32{lw}, k)}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
      %Equal.sym(U32, U32.shrn(U32{lw}, Nat.sub(32n, k)), U32{PS.ws.shr(32n, Nat.sub(32n, k), lw)}, wq.shrn(lw, Nat.sub(32n, k))) : {W.W64.to_nat(W.W64{U32.or(U32{PS.ws.shl(32n, k, hw)}, _), U32.shln(U32{lw}, k)}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
      %Equal.sym(U32, U32.shln(U32{lw}, k), U32{PS.ws.shl(32n, k, lw)}, wq.shln(lw, k)) : {W.W64.to_nat(W.W64{U32.or(U32{PS.ws.shl(32n, k, hw)}, U32{PS.ws.shr(32n, Nat.sub(32n, k), lw)}), _}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
      PS.ws.gshl_lo(32n, k, hw, lw, chw, clw, e32, h)
    case False{} False{} True{}:
      %Equal.sym(U32, U32.shln(U32{lw}, Nat.sub(k, 32n)), U32{PS.ws.shl(32n, Nat.sub(k, 32n), lw)}, wq.shln(lw, Nat.sub(k, 32n))) : {W.W64.to_nat(W.W64{_, 0}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
      PS.ws.gshl_hi(32n, k, hw, lw, chw, clw, PS.ns.le_of_not_lt(k, 32n, e32), h)
    case False{} False{} False{}:
      Empty.absurd({W.W64.to_nat(W.W64.shl.pick(False{}, False{}, False{}, k, W.W64{U32{hw}, U32{lw}})) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}, P.wn.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 64n), True{}, Equal.sym(Bool, Nat.is_lt(k, 64n), False{}, e64), hk)))

Uses (28):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wq.shln
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF.bend&name=wq.shrn
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.eq_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.le_of_not_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.gshl_hi
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.gshl_lo
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.shl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.shr
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.shl.pick
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat