FDL > PVS > Graphs > ramsey new > subgraph clique > pf:subgraph clique > 1 (12 nodes)

Conclusion

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

Tactic
 GROUND
Premise 1.   (has proof of 11 steps)

1. FORALL g:graph[T], p:nat, V:set[T] : (EXISTS C:finite set[T] : (FORALL x:T : C(x) = > (vert(g)(x) AND V(x))) AND (card(C) > = p) AND (FORALL i_2004:T, j : ((NOT (i_2004 = j)) AND C(i_2004) AND C(j)) IMPLIES ((NOT (i_2004 = j)) AND edges(g)(dbl[T](i_2004, j)) AND (FORALL x:T : ((x = i_2004) OR (x = j)) IMPLIES V(x))))) IMPLIES (EXISTS C:finite set[T] : (FORALL x:T : C(x) = > vert(g)(x)) AND (card(C) > = p) AND (FORALL i, j : ((NOT (i = j)) AND C(i) AND C(j)) IMPLIES ((NOT (i = j)) AND edges(g)(dbl[T](i, j)))))