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

(TCC) subgraph_TCC3: OBLIGATION FORALL (G:graph[T]), (V:set[T]) : (FORALL (e_250:doubleton[T]) : edges(G WITH [vert := {(i:T) | vert(G)(i) AND V(i)}, edges := {(e:doubleton[T]) | edges(G)(e) AND (FORALL (x:T) : e(x) IMPLIES V(x))}])(e_250) IMPLIES (FORALL (x_251:T) : e_250(x_251) IMPLIES vert(G WITH [vert := {(i:T) | vert(G)(i) AND V(i)}, edges := {(e:doubleton[T]) | edges(G)(e) AND (FORALL (x:T) : e(x) IMPLIES V(x))}])(x_251))) AND subgraph?(G WITH [vert := {(i:T) | vert(G)(i) AND V(i)}, edges := {(e:doubleton[T]) | edges(G)(e) AND (FORALL (x:T) : e(x) IMPLIES V(x))}], G)

Subproof Addresses (15 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 :
top 1 1 1 1 1 1 1 :
top 1 1 1 1 1 1 1 1 :
top 1 1 1 1 1 1 1 1 1 :
top 1 1 1 1 1 1 1 1 1 1 :
top 1 2 :
top 1 2 1 :
top 1 2 1 1 :
top 1 2 1 2 :