kdrag.theories.logic.axioms.proj

kdrag.theories.logic.axioms.proj(p: Proof, n: int) → Proof

Project out of an And proof

>>> x = smt.Int("x")
>>> p = kd.prove(smt.And(x > x - 1, x > x - 2, x > x - 3))
>>> proj(p, 0)
|= x > x - 1
>>> proj(p, 2)
|= x > x - 3

Parameters:

• p (Proof)

• n (int)

Return type:

Proof