FDL > PVS > Graphs > subgraphs > subgraph_TCC2 : formula-decl

(TCC) subgraph_TCC2: OBLIGATION FORALL (G:graph[T]), (V:set[T]) : is finite[T]({(i:T) | vert(G)(i) AND V(i)})

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