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

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

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