kdrag.theories.real.rset

Module Attributes

lb_le_ub

@kd.PTheorem(smt.ForAll([A, x, y, z], A[x], has_lb(A, y), has_ub(A, z), y <= z)) def lb_le_ub(l): A, x, y, z = l.fixes() l.unfold(has_lb) l.unfold(has_ub) l.intros() l.split(at=0) l.specialize(1, x) l.specialize(2, x) l.have(y <= x, by=[]) l.have(x <= z, by=[]) l.auto()

kdrag.theories.real.rset.lb_le_ub = |= ForAll([A, x, y, z],        Implies(And(A[x], has_lb(A, y), has_ub(A, z)),                y <= z))

@kd.PTheorem(smt.ForAll([A, x, y, z], A[x], has_lb(A, y), has_ub(A, z), y <= z)) def lb_le_ub(l):

A, x, y, z = l.fixes() l.unfold(has_lb) l.unfold(has_ub) l.intros() l.split(at=0) l.specialize(1, x) l.specialize(2, x) l.have(y <= x, by=[]) l.have(x <= z, by=[]) l.auto()

Parameters:

args (smt.ExprRef | Proof)