FDL
>
PVS
>
Graphs
>
subgraphs
>
subgraph
TCC2
> pf:subgraph_TCC2
: proof (7 nodes)
Conclusion
1. FORALL G:
graph
[T], V:
set
[T] :
is
finite
[T]({i:T | vert(G)(i)
AND
V(i)})
Tactic
SKOSIMP*
Premise 1.
(has
proof
of 6 steps)
1.
is
finite
[T]({i:T | vert(G!1)(i)
AND
V!1(i)})
1.
FORALL
G:graph[T],
V:set[T]
:
is
finite[T]({i:T
|
vert(G)(i)
AND
V(i)})
1.
FORALL
G:graph[T],
V:set[T]
:
is
finite[T]({i:T
|
vert(G)(i)
AND
V(i)})
1.
is
finite[T]({i:T
|
vert(G!1)(i)
AND
V!1(i)})