logo

Show the Proof

In [1]:
import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof
Out[1]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation2, 3, , , ,  ⊢  
  :
2axiom  ⊢  
 proveit.logic.booleans.eq_true_elim
3instantiation4, 5, 6, 7, 8, 9, 10, , , ,  ⊢  
  : , : , :
4theorem  ⊢  
 proveit.logic.booleans.disjunction.singular_constructive_dilemma_lemma
5assumption  ⊢  
6assumption  ⊢  
7instantiation11  ⊢  
  : , :
8assumption  ⊢  
9deduction12  ⊢  
10deduction13  ⊢  
11axiom  ⊢  
 proveit.logic.equality.equality_in_bool
12instantiation15, 14,  ⊢  
  :
13instantiation15, 16,  ⊢  
  :
14modus ponens17, 18,  ⊢  
15axiom  ⊢  
 proveit.logic.booleans.eq_true_intro
16modus ponens19, 20,  ⊢  
17assumption  ⊢  
18assumption  ⊢  
19assumption  ⊢  
20assumption  ⊢