logo
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving demorgans_law_and_to_or_bin_explicit
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
demorgans_law_and_to_or_bin_explicit:
(see dependencies)
In [3]:
%qed
proveit.logic.booleans.disjunction.demorgans_law_and_to_or_bin_explicit has been proven.
Out[3]:
 step typerequirementsstatement
0modus ponens1, 2  ⊢  
1instantiation3, 4, 5*  ⊢  
  : , : , : , : , : , : , :
2instantiation6, 7, 8  ⊢  
  : , :
3conjecture  ⊢  
 proveit.logic.booleans.quantification.universality.bundle
4conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat1
5instantiation9, 10, 11  ⊢  
  : , : , : , :
6conjecture  ⊢  
 proveit.logic.booleans.forall_over_bool_by_cases
7instantiation14, 12, 13  ⊢  
  : , : , :
8instantiation14, 15, 16  ⊢  
  : , : , :
9conjecture  ⊢  
 proveit.core_expr_types.conditionals.condition_prepend_reduction
10conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat2
11instantiation17  ⊢  
  : , :
12deduction18  ⊢  
13deduction19  ⊢  
14conjecture  ⊢  
 proveit.logic.booleans.conditioned_forall_over_bool_by_cases
15deduction20  ⊢  
16instantiation21, 22  ⊢  
  : , :
17conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
18theorem  ⊢  
 proveit.logic.booleans.disjunction.true_or_true
19theorem  ⊢  
 proveit.logic.booleans.disjunction.true_or_false
20theorem  ⊢  
 proveit.logic.booleans.disjunction.false_or_true
21theorem  ⊢  
 proveit.logic.booleans.implication.falsified_antecedent_implication
22instantiation23, 24  ⊢  
  :
23theorem  ⊢  
 proveit.logic.booleans.negation.double_negation_intro
24theorem  ⊢  
 proveit.logic.booleans.negation.not_false
*equality replacement requirements