FDL > PVS > Graphs > ramsey new > card_r1_r2 : formula-decl

card_r1_r2: LEMMA (card(r1(G)) + card(r2(G))) > = (size(G) - 1)

Subproof Addresses (12 steps)
top :
top 1 :
top 1 1 :
top 1 1 1 :
top 1 1 1 1 :
top 1 1 1 1 1 :
top 1 1 1 1 1 1 :
top 1 1 1 1 1 1 1 :
top 1 1 1 1 1 1 1 1 :
top 1 2 :
top 1 2 1 :
top 1 2 1 1 :