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

(TCC) subgraph_TCC1: OBLIGATION FORALL (G:graph[T]), (V:set[T]) : is finite[doubleton[T]]({(e:doubleton[T]) | edges(G)(e) AND (FORALL (x:T) : e(x) IMPLIES V(x))})

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 :