FDL > PVS > Graphs > ramsey new > subgraph indep > pf:subgraph_indep : proof (22 nodes)

Conclusion

1. FORALL g:graph[T], p:nat, V:set[T] : contains indep(subgraph(g, V), p) IMPLIES contains indep(g, p)

Tactic
 INSTALL-REWRITES DEFS !
Premise 1.   (has proof of 21 steps)

1. FORALL g:graph[T], p:nat, V:set[T] : contains indep(subgraph(g, V), p) IMPLIES contains indep(g, p)