PrintForm
Definitions
sequent
rank
Sections
ClassicalProps(jlc)
Doc
At:
not
list
exists
rank
gt
0
rank
0
2
1
1
1
1
1
1
1.
u:
Formula
2.
v:
Formula List
3.
concl:
Formula List
4.
f
v.(
(f) > 0)
False
(v)+0 = 0
5.
(
(u) > 0
f
v.(
(f) > 0))
6.
False
7.
(
(u) > 0
f
v.(
(f) > 0))
(u) > 0 &
f
v.(
(f) > 0)
(u)+
(v)+0 = 0
By:
FwdThru -1 [-3]
THEN
Sel 2 (FwdThru -2 [-4])
Generated subgoal:
1
8.
(u) > 0
9.
f
v.(
(f) > 0)
(u)+
(v)+0 = 0
About:
(u) > 0
f
v.((f) > 0)
(u)+(v)+0 = 0fv.((f) > 0) 
False (v)+0 = 0((u) > 0 
fv.((f) > 0))False((u) > 0 fv.((f) > 0)) 
(u) > 0 & fv.((f) > 0) (u)+(v)+0 = 0(u) > 0fv.((f) > 0) (u)+(v)+0 = 0
