Proof of proveit.logic.equality.unary_evaluation theorem

import proveit
from proveit.logic import Equals
from proveit.logic.equality  import substitution
from proveit import a, c, x, y, fa
theory = proveit.Theory() # the theorem's theory

%proving unary_evaluation

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

substitution

 ⊢  

substitution.instantiate({y:a}, assumptions=[Equals(x, a)])

 ⊢  

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

assumptions = [unary_evaluation.instance_expr.antecedent,
              unary_evaluation.instance_expr.consequent.antecedent]

assumptions:

unary_evaluation.instance_expr.consequent.consequent.conclude_via_transitivity(assumptions=assumptions)

,  ⊢  

unary_evaluation.instance_expr.prove()

 ⊢  

%qed

proveit.logic.equality.unary_evaluation has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	deduction	2	⊢
2	deduction	3	⊢
3	instantiation	4, 5, 6	,  ⊢
	: , : , :
4	axiom		⊢
	proveit.logic.equality.equals_transitivity
5	instantiation	7, 8	⊢
	: , : , :
6	assumption		⊢
7	axiom		⊢
	proveit.logic.equality.substitution
8	assumption		⊢