FDL
>
PVS
>
Graphs
>
subgraphs
>
subgraph
vert
sub
> pf:subgraph_vert_sub
: proof (8 nodes)
Conclusion
1. FORALL G:
graph
[T], V:
set
[T] :
subset?
(V, vert(G))
IMPLIES
(vert(
subgraph
(G, V))
=
V)
Tactic
SKOSIMP*
Premise 1.
(has
proof
of 7 steps)
-1.
subset?
(V!1, vert(G!1))
1. vert(
subgraph
(G!1, V!1))
=
V!1
1.
FORALL
G:graph[T],
V:set[T]
:
subset?(V,
vert(G))
IMPLIES
(vert(subgraph(G,
V))
=
V)
1.
FORALL
G:graph[T],
V:set[T]
:
subset?(V,
vert(G))
IMPLIES
(vert(subgraph(G,
V))
=
V)