Conclusion
1.
FORALL
G:graph[T],
V:set[T]
:
(FORALL
e_4176:doubleton[T]
:
edges(G
WITH
[vert
:=
{i:T
|
vert(G)(i)
AND
V(i)},
edges
:=
{e:doubleton[T]
|
edges(G)(e)
AND
(FORALL
x:T
:
e(x)
IMPLIES
V(x))}])(e_4176)
IMPLIES
(FORALL
x_4177:T
:
e_4176(x_4177)
IMPLIES
vert(G
WITH
[vert
:=
{i:T
|
vert(G)(i)
AND
V(i)},
edges
:=
{e:doubleton[T]
|
edges(G)(e)
AND
(FORALL
x:T
:
e(x)
IMPLIES
V(x))}])(x_4177)))
AND
subgraph?(G
WITH
[vert
:=
{i:T
|
vert(G)(i)
AND
V(i)},
edges
:=
{e:doubleton[T]
|
edges(G)(e)
AND
(FORALL
x:T
:
e(x)
IMPLIES
V(x))}],
G)
Tactic
SKOSIMP*
Premise 1. (has proof of 14 steps)
1.
(FORALL
e_4176:doubleton[T]
:
edges(G!1
WITH
[vert
:=
{i:T
|
vert(G!1)(i)
AND
V!1(i)},
edges
:=
{e:doubleton[T]
|
edges(G!1)(e)
AND
(FORALL
x:T
:
e(x)
IMPLIES
V!1(x))}])(e_4176)
IMPLIES
(FORALL
x_4177:T
:
e_4176(x_4177)
IMPLIES
vert(G!1
WITH
[vert
:=
{i:T
|
vert(G!1)(i)
AND
V!1(i)},
edges
:=
{e:doubleton[T]
|
edges(G!1)(e)
AND
(FORALL
x:T
:
e(x)
IMPLIES
V!1(x))}])(x_4177)))
AND
subgraph?(G!1
WITH
[vert
:=
{i:T
|
vert(G!1)(i)
AND
V!1(i)},
edges
:=
{e:doubleton[T]
|
edges(G!1)(e)
AND
(FORALL
x:T
:
e(x)
IMPLIES
V!1(x))}],
G!1)
