FDL
>
PVS
>
Graphs
>
ramsey
new
>
card
r1
r2
>
pf:card
r1
r2
>
1
>
2
> 1
(2 nodes)
Conclusion
1.
add
(
choose
(vert(G!1)),
union
(
r1
(G!1),
r2
(G!1)))
=
vert(G!1)
Tactic
APPLY-EXTENSIONALITY 1 HIDE? T
Premise 1.
(has
proof
of 1 step)
1.
add
(
choose
(vert(G!1)),
union
(
r1
(G!1),
r2
(G!1)))(x!1)
=
vert(G!1)(x!1)
1.
add(choose(vert(G!1)),
union(r1(G!1),
r2(G!1)))
=
vert(G!1)
1.
add(choose(vert(G!1)),
union(r1(G!1),
r2(G!1)))
=
vert(G!1)
1.
add(choose(vert(G!1)),
union(r1(G!1),
r2(G!1)))(x!1)
=
vert(G!1)(x!1)