(10steps total) PrintForm Definitions graph 1 2 Sections Graphs Doc

At: df-traversal-cons2 2 2
1. the_graph: Graph
2. i: Vertices(the_graph)
3. s: traversal(the_graph)
4. j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *i
5. i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i) / s2]) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > *i)
6. i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > *j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i) / s2]) traversal(the_graph) (j:Vertices(the_graph). i-the_graph- > *j (inr(j) s2))
7. i@0: Vertices(the_graph)
8. u: Vertices(the_graph)+Vertices(the_graph)
9. v: (Vertices(the_graph)+Vertices(the_graph)) List
10. s2: traversal(the_graph)
11. j:Vertices(the_graph). i@0-the_graph- > *j non-trivial-loop(the_graph;j)
12. j: Vertices(the_graph)
13. i@0-the_graph- > *j
14. inr(i) = u
15. s = (v @ [inl(i@0) / s2]) traversal(the_graph)
(inr(j) s2)
By: AutoInst [i@0;v;s2;j]
Generated subgoals:

None

About:
listconsunioninlinrequalimpliesall

(10steps total) PrintForm Definitions graph 1 2 Sections Graphs Doc