FDL > PVS > Graphs > ramsey new > r1_TCC1 : formula-decl

(TCC) r1_TCC1: OBLIGATION FORALL (G:Graph[T]) : nonempty?[T](vert(G))

Subproof Addresses (3 steps)
top :
top 1 :
top 1 1 :