kdrag.theories.real.arb.sin_bnd

kdrag.theories.real.arb.sin_bnd(x: object) → Proof

>>> sin_bnd(arb(0))
|- ForAll(x,
    Implies(And(0 - 0 <= x, x <= 0 + 0),
            And(0 - 0 <= sin(x), sin(x) <= 0 + 0)))
>>> kd.prove(real.sin(0) <= 2, by=[sin_bnd(arb(0,0.1))(smt.RealVal(0))])
|- sin(0) <= 2
>>> kd.prove(real.sin(3.14) <= 0.02, by=[sin_bnd(arb(3.14, 0.01))])
|- sin(157/50) <= 1/50

Parameters:

x (object)

Return type:

Proof