Proof of proveit.logic.booleans.implication.negated_reflex theorem

import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic import Equals, TRUE, FALSE
from proveit.logic.booleans.implication import Implies
from proveit.logic.booleans.implication import not_true_via_contradiction
from proveit.logic.booleans.negation import Not
theory = proveit.Theory() # the theorem's theory

%proving negated_reflex

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
negated_reflex:
(see dependencies)

defaults.assumptions = negated_reflex.all_conditions()

defaults.assumptions:

BeqT = Equals(B,TRUE)

BeqT:

AimplBeqT = BeqT.prove(assumptions=[BeqT]).as_implication(A)

AimplBeqT:  ⊢  

n_impl_a_b = Not(Implies(A,B))

n_impl_a_b:

AimplB = n_impl_a_b.operands[0]

AimplB:

n_impl_a_b.evaluation()

 ⊢  

contradiction = n_impl_a_b.derive_contradiction(assumptions=[B, Not(Implies(A,B))])

contradiction: ,  ⊢  

B_impl_F = contradiction.as_implication(B)

B_impl_F:  ⊢  

B_impl_F.derive_via_contradiction()

 ⊢  

Implies(B, A).prove()

 ⊢  

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

%qed

proveit.logic.booleans.implication.negated_reflex has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , :
2	theorem		⊢
	proveit.logic.booleans.implication.untrue_antecedent_implication
3	instantiation	4, 5	⊢
	:
4	theorem		⊢
	proveit.logic.booleans.implication.not_true_via_contradiction
5	deduction	6	⊢
6	instantiation	7, 8, 9	,  ⊢
	:
7	theorem		⊢
	proveit.logic.booleans.negation.negation_contradiction
8	deduction	10	⊢
9	assumption		⊢
10	assumption		⊢