def icd_t

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64close.bend:35

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC

35def icd_t(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64, +d: F.F64) -> {F.ic_d(a, b, rel, at, d) == SF.ic_near(a, b, rel, at, d) : Bool}:
36  or3(F.le(d, F.abs(F.mul(rel, b))), F.le(d, F.abs(F.mul(rel, a))), F.le(d, at), SF.le_s(d, SF.fabs(SF.mul(rel, b))), SF.le_s(d, SF.fabs(SF.mul(rel, a))), SF.le_s(d, at), lek(d, rel, b), lek(d, rel, a), FC.le_value(d, at))