def step_fin

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:287

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/f64.bend as SF
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/f64.bend as F
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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

287def step_fin(+x: F.F64, +W: WU.U64, +P2: Nat, +ev: {SW.value(W) == P2 : Nat}, +h63: {C.fits(63n, P2) == True{} : Bool}) -> {F.with_sign(F.signbit(x), W) == SF.of_pat(SF.sign(x), P2) : F.F64}:
288  +hW = L.subst(Nat, t => {C.fits(63n, t) == True{} : Bool}, P2, SW.value(W), Equal.sym(Nat, SW.value(W), P2, ev), h63)
289  +e1 = ws(F.signbit(x), W, hW)
290  +e2 = Equal.cong(Nat, F.F64, t => FR.bits(F.signbit(x), t), SW.value(W), P2, ev)
291  +e3 = Equal.cong(Bool, F.F64, t => FR.bits(t, P2), F.signbit(x), SF.sign(x), FB.signbit_value(x))
292  +e4 = Equal.sym(F.F64, SF.of_pat(SF.sign(x), P2), FR.bits(SF.sign(x), P2), opat(SF.sign(x), P2))
293  Equal.trans(F.F64, F.with_sign(F.signbit(x), W), FR.bits(F.signbit(x), SW.value(W)), SF.of_pat(SF.sign(x), P2), e1, Equal.trans(F.F64, FR.bits(F.signbit(x), SW.value(W)), FR.bits(F.signbit(x), P2), SF.of_pat(SF.sign(x), P2), e2, Equal.trans(F.F64, FR.bits(F.signbit(x), P2), FR.bits(SF.sign(x), P2), SF.of_pat(SF.sign(x), P2), e3, e4)))