Conclusion
1.
FORALL
g:graph[T],
p:nat,
V:set[T]
:
(EXISTS
C:finite
set[T]
:
(FORALL
x:T
:
C(x)
=
>
(vert(g)(x)
AND
V(x)))
AND
(card(C)
>
=
p)
AND
(FORALL
i_2004:T,
j
:
((NOT
(i_2004
=
j))
AND
C(i_2004)
AND
C(j))
IMPLIES
((NOT
(i_2004
=
j))
AND
edges(g)(dbl[T](i_2004,
j))
AND
(FORALL
x:T
:
((x
=
i_2004)
OR
(x
=
j))
IMPLIES
V(x)))))
IMPLIES
(EXISTS
C:finite
set[T]
:
(FORALL
x:T
:
C(x)
=
>
vert(g)(x))
AND
(card(C)
>
=
p)
AND
(FORALL
i,
j
:
((NOT
(i
=
j))
AND
C(i)
AND
C(j))
IMPLIES
((NOT
(i
=
j))
AND
edges(g)(dbl[T](i,
j)))))
Tactic
SKOSIMP*
Premise 1. (has proof of 10 steps)
-1.
FORALL
x:T
:
C!1(x)
=
>
(vert(g!1)(x)
AND
V!1(x))
-2.
card(C!1)
>
=
p!1
-3.
FORALL
i_2004:T,
j
:
((NOT
(i_2004
=
j))
AND
C!1(i_2004)
AND
C!1(j))
IMPLIES
((NOT
(i_2004
=
j))
AND
edges(g!1)(dbl[T](i_2004,
j))
AND
(FORALL
x:T
:
((x
=
i_2004)
OR
(x
=
j))
IMPLIES
V!1(x)))
1.
EXISTS
C:finite
set[T]
:
(FORALL
x:T
:
C(x)
=
>
vert(g!1)(x))
AND
(card(C)
>
=
p!1)
AND
(FORALL
i,
j
:
((NOT
(i
=
j))
AND
C(i)
AND
C(j))
IMPLIES
((NOT
(i
=
j))
AND
edges(g!1)(dbl[T](i,
j))))
