FDL > PVS > Graphs > ramsey new > r2 TCC1 > pf:r2 TCC1 > 1 (9 nodes)

Conclusion

1. is finite[T](LET (v0:(vert(G!1)) ) = choose[T](vert(G!1)) IN
{n:T | vert(G!1)(n) AND (n /= v0) AND (NOT edge?[T](G!1)(v0, n))})

Tactic
 CASE "subset?({n: T |
vert(G!1)(n) AND
n /= choose[T](vert(G!1)) AND
NOT edge?[T](G!1)(choose[T](vert(G!1)), n)},vert(G!1))"
Premise 1.   (has proof of 3 steps)

-1. subset?({n:T | vert(G!1)(n) AND (n /= choose[T](vert(G!1))) AND (NOT edge?[T](G!1)(choose[T](vert(G!1)), n))}, vert(G!1))

1. is finite[T](LET (v0:(vert(G!1)) ) = choose[T](vert(G!1)) IN
{n:T | vert(G!1)(n) AND (n /= v0) AND (NOT edge?[T](G!1)(v0, n))})
Premise 2.   (has proof of 5 steps)

1. subset?({n:T | vert(G!1)(n) AND (n /= choose[T](vert(G!1))) AND (NOT edge?[T](G!1)(choose[T](vert(G!1)), n))}, vert(G!1))
2. is finite[T](LET (v0:(vert(G!1)) ) = choose[T](vert(G!1)) IN
{n:T | vert(G!1)(n) AND (n /= v0) AND (NOT edge?[T](G!1)(v0, n))})