PrintForm
Definitions
sequent
rank
Sections
ClassicalProps(jlc)
Doc
At:
not
list
exists
rank
gt
0
rank
0
1
1
1
2
1.
hyp:
Formula List
2.
concl:
Formula List
3.
u:
Formula
4.
v:
Formula List
5.
f
v.(
(f) > 0)
0+
(v) = 0
f
(u.v).(
(f) > 0)
0+
(u.v) = 0
By:
AbReduce 0
THEN
UnivCD
Generated subgoal:
1
6.
(
(u) > 0
f
v.(
(f) > 0))
0+
(u)+
(v) = 0
About:
(
(u) > 0 
f
v.((f) > 0))
0+(u)+(v) = 0fv.((f) > 0) 
0+(v) = 0 f(u.v).((f) > 0) 0+(u.v) = 0((u) > 0 fv.((f) > 0)) 0+(u)+(v) = 0
