FDL
>
PVS
>
Graphs
>
ramsey
new
>
card
r1
r2
> pf:card_r1_r2
: proof (12 nodes)
Conclusion
1. FORALL G:
Graph
[T] : (
card
(
r1
(G))
+
card
(
r2
(G)))
> =
(
size
(G)
-
1)
Tactic
SKOSIMP*
Premise 1.
(has
proof
of 11 steps)
1. (
card
(
r1
(G!1))
+
card
(
r2
(G!1)))
> =
(
size
(G!1)
-
1)
1.
FORALL
G:Graph[T]
:
(card(r1(G))
+
card(r2(G)))
>
=
(size(G)
-
1)
1.
FORALL
G:Graph[T]
:
(card(r1(G))
+
card(r2(G)))
>
=
(size(G)
-
1)
1.
(card(r1(G!1))
+
card(r2(G!1)))
>
=
(size(G!1)
-
1)