PrintForm
Definitions
assignment
Sections
ClassicalProps(jlc)
Doc
At:
extension
lemma
1
1
1
1
1.
a:
Assignment
2.
a':
Assignment
3.
a'
a = a
4.
x:
Var
5.
a'
a(x) = 3
6.
a'
a(x) = a(x)
a(x) = a'(x)
By:
MoveToConcl -1
THEN
GenConcl (a(x) = n)
THEN
Analyze 0
Generated subgoal:
1
6.
n:
7.
a(x) = n
8.
a'
a(x) = n
n = a'(x)
About:
a(x) = n
n = a'(x)a = a
a'a(x) = 3
a(x) = a(x) a(x) = a'(x)a(x) = n n = a'(x)
