def wq.shlbig.go

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

import Base
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
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

271def wq.shlbig.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, -a: W.W64, ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, +h: {Nat.is_le(64n, k) == True{} : Bool}) -> {W.W64.shl.pick(z, l32, l64, k, a) == W.W64.zero() : W.W64}:
272  match z l32 l64:
273    case True{} _ _:
274      Empty.absurd({a == W.W64.zero() : W.W64}, PS.ns.tf(Equal.trans(Bool, True{}, Nat.is_lt(k, 64n), False{}, Equal.sym(Bool, Nat.is_lt(k, 64n), Nat.is_lt(0n, 64n), Equal.cong(Nat, Bool, v => Nat.is_lt(v, 64n), k, 0n, PS.ns.eq_zero(k, ez))), P.wn.le_not_lt(64n, k, h))))
275    case False{} True{} _:
276      Empty.absurd({W.W64.shl.pick(False{}, True{}, l64, k, a) == W.W64.zero() : W.W64}, PS.ns.tf(Equal.trans(Bool, True{}, Nat.is_lt(k, 32n), False{}, Equal.sym(Bool, Nat.is_lt(k, 32n), True{}, e32), P.wn.le_not_lt(32n, k, UO.nat_le_trans(32n, 64n, k, {==}, h)))))
277    case False{} False{} True{}:
278      Empty.absurd({W.W64.shl.pick(False{}, False{}, True{}, k, a) == W.W64.zero() : W.W64}, PS.ns.tf(Equal.trans(Bool, True{}, Nat.is_lt(k, 64n), False{}, Equal.sym(Bool, Nat.is_lt(k, 64n), True{}, e64), P.wn.le_not_lt(64n, k, h))))
279    case False{} False{} False{}:
280      {==}