(158steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: dfsl-properties 2 1 2 1

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. L: Vertices(the_graph) List
4. L1: Vertices(the_graph) List
5. s: traversal(the_graph)
6. i: Vertices(the_graph)
7. paren(Vertices(the_graph);s)
8. no_repeats(Vertices(the_graph)+Vertices(the_graph);s)
9. dfsl-traversal(the_graph;L1;s)
10. (inl(i) s)
11. df-traversal(the_graph;s)
dfsl-traversal(the_graph;L1 @ [i];s)

By:
BackThru Thm* For any graph L1,L2:V List, s:Traversal. L1-- > *L2 dfsl-traversal(the_graph;L1;s) dfsl-traversal(the_graph;L1 @ L2;s)
THEN
RWO Thm* For any graph A:V List, x:V. A-- > *[x] A-- > *x 0
THEN
Analyze 9
THEN
EasyHyp


Generated subgoals:

None

About:
listconsnilunioninlimpliesall

(158steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc