FDL
>
PVS
>
Graphs
>
subgraphs
>
subgraph
lem
> pf:subgraph_lem
: proof (2 nodes)
Conclusion
1. FORALL G:
graph
[T], V:
set
[T] :
subgraph?
(
subgraph
(G, V), G)
Tactic
SKOSIMP*
Premise 1.
(has
proof
of 1 step)
1.
subgraph?
(
subgraph
(G!1, V!1), G!1)
1.
FORALL
G:graph[T],
V:set[T]
:
subgraph?(subgraph(G,
V),
G)
1.
FORALL
G:graph[T],
V:set[T]
:
subgraph?(subgraph(G,
V),
G)
1.
subgraph?(subgraph(G!1,
V!1),
G!1)