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

subgraph_indep: LEMMA FORALL (V:set[T]) : contains indep(subgraph(g, V), p) IMPLIES contains indep(g, p)

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