FDL > PVS > Graphs > ramsey new > subgraph indep > pf:subgraph indep > 1 > 1 > 1 > 1 > 1 > 2 > 1 > 1 > 1 > 1 > 1 > 1 > 1 > 1 (5 nodes)


Conclusion

-1. x!1 = j!1
-2. D!1(i!1)
-3. D!1(j!1)
-4. edges(g!1)(dbl[T](i!1, j!1))
-5. vert(g!1)(i!1)
-6. V!1(i!1)
-7. card(D!1) > = p!1

1. i!1 = j!1
2. i!1 = j!1
3. V!1(x!1)


Tactic
REPLACE "-1"

Premise 1.   (has proof of 4 steps)

-1. x!1 = j!1
-2. D!1(i!1)
-3. D!1(j!1)
-4. edges(g!1)(dbl[T](i!1, j!1))
-5. vert(g!1)(i!1)
-6. V!1(i!1)
-7. card(D!1) > = p!1

1. i!1 = j!1
2. i!1 = j!1
3. V!1(j!1)