def f63s

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addb.bend:55

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/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as AA

55def f63s(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +Fr: Nat, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hk: {Nat.is_le(Nat.add(k, 53n), 63n) == True{} : Bool}) -> {C.fits(63n, C.shift(k, Nat.add(Fr, C.shift(52n, one)))) == True{} : Bool}:
56  SH.fits_mono(Nat.add(k, 53n), 63n, C.shift(k, Nat.add(Fr, C.shift(52n, one))), hk, Equal.trans(Bool, C.fits(Nat.add(k, 53n), C.shift(k, Nat.add(Fr, C.shift(52n, one)))), C.fits(53n, Nat.add(Fr, C.shift(52n, one))), True{}, RT.fits_sh(k, 53n, Nat.add(Fr, C.shift(52n, one))), AA.f53(one, h1, Fr, hF)))