At:
dfl-traversal-consl
3
1
1.
the_graph: Graph
2.
L: Vertices(the_graph) List
3.
i: Vertices(the_graph)
4.
s: traversal(the_graph)
5.
(inr(i) 
s)
6.
dfl-traversal(the_graph;L;s)
7.
i@0: Vertices(the_graph)
8.
s2: traversal(the_graph)
9.
j:Vertices(the_graph). i@0-the_graph- > *j 
non-trivial-loop(the_graph;j)
10.
inl(i) = inl(i@0) Vertices(the_graph)+Vertices(the_graph)
11.
s = s2
L-the_graph- > *i@0
By:
AllHyps (
h.(Analyze h) THEN (Analyze h) THEN (BackThru h+1) THEN (ObviousFrom [5;-2]))
Generated subgoals:
None
About:
