FDL > PVS > Graphs > ramsey new > card r1 r2 > pf:card r1 r2 > 1 > 1 > 1 > 1 > 1 > 1 > 1 > 1


Conclusion

1. IF union(r1(G!1), r2(G!1))(choose(vert(G!1))) THEN (card(r1(G!1)) + card(r2(G!1))) > = ((((card(r1(G!1)) + card(r2(G!1))) - card(intersection(r1(G!1), r2(G!1)))) + 0) - 1) ELSE (card(r1(G!1)) + card(r2(G!1))) > = ((((card(r1(G!1)) + card(r2(G!1))) - card(intersection(r1(G!1), r2(G!1)))) + 1) - 1) ENDIF


Tactic
GROUND


No Premises