PrintForm
Definitions
formula
list
Sections
ClassicalProps(jlc)
Doc
At:
list
rank
wf
1
1
2
1
1.
L:
Formula List
2.
u:
Formula
3.
v:
Formula List
4.
reduce(
x,y.
(x)+y;0;v)
(u)+reduce(
x,y.
(x)+y;0;v)
By:
GenConcl (reduce(
x,y.
(x)+y;0;v) = n)
Generated subgoal:
1
5.
n:
6.
reduce(
x,y.
(x)+y;0;v) = n
(u)+n
About:
x,y. 
(x)+y;0;v) = n
(u)+n 
x,y. (x)+y;0;v) (u)+reduce(x,y. (x)+y;0;v) x,y. (x)+y;0;v) = n)x,y. (x)+y;0;v) = n (u)+n 
