Demonstrations for the theory of proveit.logic.booleans.quantification.existence

In [1]:
import proveit
%begin demonstrations

from proveit import a, b
from proveit.logic import Exists, Equals
from proveit.numbers import Add, two, three, five, NaturalPos
In [2]:
eval_2p3 = Add(two, three).evaluation()
eval_2p3:  ⊢  
In [3]:
Exists((a, b), Equals(Add(a, b), five)).conclude_via_example((two, three))
In [4]:
Exists((a, b), Equals(Add(a, b), five), domain=NaturalPos).conclude_via_example((two, three))
In [5]:
%end demonstrations