kdrag.theories.logic.temporal.Always

kdrag.theories.logic.temporal.Always(x: DatatypeRef, vs=None) → DatatypeRef

Returns the TBool signal that x is always true after time t (inclusive).

>>> t = smt.Int("t")
>>> s = TBool(smt.Lambda([t], t >= 1))
>>> _ = kd.prove(smt.Not(Valid(Always(s))))
>>> _ = kd.prove(Valid(Always(Next(s))))