def low_shift

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64est.bend:119

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

119# C.low(n, y << k) == y << k when y < 2^t and k + t == n; n stays a variable,
120# as a closed 2^64 in a goal is expanded by the checker.
121def low_shift(+n: Nat, +k: Nat, +t: Nat, +y: Nat, +e: {Nat.add(k, t) == n : Nat}, +hs0: {Nat.is_lt(C.shift(k, y), C.shift(k, C.pow2(t))) == True{} : Bool}) -> {C.low(n, C.shift(k, y)) == C.shift(k, y) : Nat}:
122  +hs = L.subst(Nat, z => {Nat.is_lt(C.shift(k, y), z) == True{} : Bool}, C.shift(k, C.pow2(t)), C.pow2(n), Equal.trans(Nat, C.shift(k, C.pow2(t)), C.pow2(Nat.add(k, t)), C.pow2(n), WW.shift_pow2(k, t), Equal.cong(Nat, Nat, z => C.pow2(z), Nat.add(k, t), n, e)), hs0)
123  WW.low_fit(n, C.shift(k, y), WW.fits_of_lt(n, C.shift(k, y), hs))