FDL
>
PVS
>
Graphs
>
subgraphs
>
subgraph
vert
sub
>
pf:subgraph
vert
sub
>
1
>
1
>
1
>
1
>
1
> 1
(2 nodes)
Conclusion
-1. V!1(x!1)
= >
vert(G!1)(x!1)
1. (vert(G!1)(x!1)
AND
V!1(x!1))
=
V!1(x!1)
Tactic
IFF 1
Premise 1.
(has
proof
of 1 step)
-1. V!1(x!1)
= >
vert(G!1)(x!1)
1. (vert(G!1)(x!1)
AND
V!1(x!1))
IFF
V!1(x!1)
