Proof of proveit.logic.booleans.disjunction.or_if_both theorem¶

In [1]:
import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic.booleans.disjunction import true_or_true
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving or_if_both

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
or_if_both:
(see dependencies)
In [3]:
defaults.assumptions = or_if_both.all_conditions()

defaults.assumptions:
In [4]:
AeqT = A.evaluation()

AeqT:
In [5]:
BeqT = B.evaluation()

BeqT:
In [6]:
true_or_true

In [7]:
AorT = AeqT.sub_left_side_into(true_or_true.inner_expr().operands[0],
auto_simplify=False)

AorT:
In [8]:
AorB = BeqT.sub_left_side_into(AorT, auto_simplify=False)

AorB: ,  ⊢
or_if_both may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [9]:
%qed

proveit.logic.booleans.disjunction.or_if_both has been proven.

Out[9]:
step typerequirementsstatement
0generalization1
1instantiation4, 2, 3,  ⊢
: , :
2instantiation4, 5, 6
: , :
3assumption
4theorem
proveit.logic.equality.substitute_truth
5theorem
proveit.logic.booleans.disjunction.true_or_true
6assumption