# Proof of proveit.logic.booleans.disjunction.or_if_right theorem¶

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

In [2]:
%proving or_if_right

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

defaults.assumptions:
In [4]:
AeqT_or_AeqF = in_bool(A).unfold(assumptions=[in_bool(A)])

AeqT_or_AeqF:
In [5]:
AeqT = AeqT_or_AeqF.operands[0]

AeqT:
In [6]:
AeqF = AeqT_or_AeqF.operands[1]

AeqF:

By proving $\vdash (B = \top) \in \mathbb{B}$ and $\vdash (B = \bot) \in \mathbb{B}$ (under no assumptions) we can force the proof to be shorter than otherwise (since it automatically deduces these assuming $B \in \mathbb{B}$ in a convoluted manner).

In [7]:
in_bool(AeqT).prove(assumptions=[])

In [8]:
in_bool(AeqF).prove(assumptions=[])

In [9]:
Or(A, B).prove(assumptions=[AeqT, B])

In [10]:
Or(A, B).prove(assumptions=[AeqF, B])

In [11]:
AeqT_or_AeqF.derive_via_singular_dilemma(Or(A, B), assumptions=[in_bool(A), B])

or_if_right may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [12]:
%qed

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

Out[12]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4, 5, 6, 7,  ⊢
: , : , :
2theorem
proveit.logic.booleans.disjunction.singular_constructive_dilemma
3instantiation8
: , :
4instantiation8
: , :
5instantiation9, 10
:
6deduction11
7deduction12
8axiom
proveit.logic.equality.equality_in_bool
9conjecture
proveit.logic.booleans.unfold_is_bool_explicit
10assumption
11instantiation13, 14, 17,  ⊢
: , :
12instantiation15, 16, 17,  ⊢
: , :
13theorem
proveit.logic.booleans.disjunction.or_if_both
14instantiation18, 19
:
15theorem
proveit.logic.booleans.disjunction.or_if_only_right
16instantiation20, 21
:
17assumption
18axiom
proveit.logic.booleans.eq_true_elim
19assumption
20theorem
proveit.logic.booleans.negation.negation_intro
21assumption