Conclusion
-1.
FORALL
A:finite
set[T],
S:set[T]
:
subset?(S,
A)
IMPLIES
is
finite(S)
-2.
subset?({n:T
|
vert(G!1)(n)
AND
(n
/=
choose[T](vert(G!1)))
AND
(NOT
edge?[T](G!1)(choose[T](vert(G!1)),
n))},
vert(G!1))
1.
is
finite[T](LET
(v0:(vert(G!1))
)
=
choose[T](vert(G!1))
IN
{n:T
|
vert(G!1)(n)
AND
(n
/=
v0)
AND
(NOT
edge?[T](G!1)(v0,
n))})
Tactic
INST?
Premise 1. (has proof of 1 step)
-1.
subset?({n:T
|
vert(G!1)(n)
AND
(n
/=
choose[T](vert(G!1)))
AND
(NOT
edge?[T](G!1)(choose[T](vert(G!1)),
n))},
vert(G!1))
IMPLIES
is
finite({n:T
|
vert(G!1)(n)
AND
(n
/=
choose[T](vert(G!1)))
AND
(NOT
edge?[T](G!1)(choose[T](vert(G!1)),
n))})
-2.
subset?({n:T
|
vert(G!1)(n)
AND
(n
/=
choose[T](vert(G!1)))
AND
(NOT
edge?[T](G!1)(choose[T](vert(G!1)),
n))},
vert(G!1))
1.
is
finite[T](LET
(v0:(vert(G!1))
)
=
choose[T](vert(G!1))
IN
{n:T
|
vert(G!1)(n)
AND
(n
/=
v0)
AND
(NOT
edge?[T](G!1)(v0,
n))})
