Conclusion
-1.
contains
indep(subgraph(g!1,
V!1),
p!1)
1.
contains
indep(g!1,
p!1)
Tactic
GROUND
Premise 1. (has proof of 19 steps)
-1.
EXISTS
D:finite
set[T]
:
(FORALL
x:T
:
D(x)
=
>
(vert(g!1)(x)
AND
V!1(x)))
AND
(card(D)
>
=
p!1)
AND
(FORALL
i_2016:T,
j
:
((NOT
(i_2016
=
j))
AND
D(i_2016)
AND
D(j))
IMPLIES
(NOT
((NOT
(i_2016
=
j))
AND
edges(g!1)(dbl[T](i_2016,
j))
AND
(FORALL
x:T
:
((x
=
i_2016)
OR
(x
=
j))
IMPLIES
V!1(x)))))
1.
EXISTS
D:finite
set[T]
:
(FORALL
x:T
:
D(x)
=
>
vert(g!1)(x))
AND
(card(D)
>
=
p!1)
AND
(FORALL
i,
j
:
((NOT
(i
=
j))
AND
D(i)
AND
D(j))
IMPLIES
(NOT
((NOT
(i
=
j))
AND
edges(g!1)(dbl[T](i,
j)))))
