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

In [1]:
import proveit
from proveit.logic import TRUE, FALSE
from proveit import A
from proveit.logic.booleans.disjunction import unary_or_lemma
from proveit.logic.booleans.disjunction  import or_f_t, or_f_f
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving unary_or_reduction

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
unary_or_reduction:
(see dependencies)
In [3]:
base_case_t_r_u_e = unary_or_lemma.instantiate({A:TRUE})

base_case_t_r_u_e:
In [4]:
base_case_f_a_l_s_e = unary_or_lemma.instantiate({A:FALSE})

base_case_f_a_l_s_e:
In [5]:
base_case_t_r_u_e.sub_left_side_into(or_f_t)

In [6]:
base_case_f_a_l_s_e.sub_left_side_into(or_f_f)

In [7]:
%qed

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

Out[7]:
step typerequirementsstatement
0instantiation1, 2, 3
: , :
1conjecture
proveit.logic.booleans.forall_over_bool_by_cases
2instantiation6, 4, 5*
:
3instantiation6, 7, 8*
:
4conjecture
proveit.logic.booleans.true_is_bool
5axiom
proveit.logic.booleans.disjunction.or_f_t
6conjecture
proveit.logic.booleans.disjunction.unary_or_lemma
7conjecture
proveit.logic.booleans.false_is_bool
8axiom
proveit.logic.booleans.disjunction.or_f_f
*equality replacement requirements