FDL > PVS > Graphs > ramsey new > contains_indep : const-decl


contains_indep(g, n): bool = EXISTS (D:finite set[T]) : subset?(D, vert(g)) AND (card(D) > = n) AND (FORALL i, j : ((i /= j) AND D(i) AND D(j)) IMPLIES (NOT edge?(g)(i, j)));