FDL > PVS > Graphs > ramsey new > card r1 r2 > pf:card r1 r2 > 1 > 1 > 1 > 1 > 1 > 1 > 1 (2 nodes)

Conclusion

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

Tactic
 LIFT-IF
Premise 1.   (has proof of 1 step)

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