FDL
>
PVS
>
Graphs
>
ramsey
new
>
r1
TCC1
> pf:r1_TCC1
: proof (3 nodes)
Conclusion
1. FORALL G:
Graph
[T] :
nonempty?
[T](vert(G))
Tactic
SKOSIMP*
Premise 1.
(has
proof
of 2 steps)
1.
nonempty?
[T](vert(G!1))
1.
FORALL
G:Graph[T]
:
nonempty?[T](vert(G))
1.
FORALL
G:Graph[T]
:
nonempty?[T](vert(G))
1.
nonempty?[T](vert(G!1))