def shl_t

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:114

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

114def shl_t(+rw: WU.U64, +t: Nat, +ht: {Nat.is_le(t, 10n) == True{} : Bool}, +hf: {C.fits(53n, SW.value(rw)) == True{} : Bool}) -> {SW.value(X.shl(rw, t)) == C.shift(t, SW.value(rw)) : Nat}:
115  +hk = N.le_lt_trans(t, 10n, 64n, ht, {==})
116  +hj = N.le_trans(Nat.add(t, 53n), Nat.add(10n, 53n), 64n, Equal.trans(Bool, Nat.is_le(Nat.add(t, 53n), Nat.add(10n, 53n)), Nat.is_le(t, 10n), True{}, FR.le_cancel_r(t, 10n, 53n), ht), {==})
117  FL.shl_v(rw, t, 53n, hk, hj, hf)