At:
dfsl-traversal-nil
1
1
1.
the_graph: Graph
2.
i: Vertices(the_graph)
3.
s1: (Vertices(the_graph)+Vertices(the_graph)) List
4.
s2: (Vertices(the_graph)+Vertices(the_graph)) List
5.
nil = (s1 @ [inr(i)] @ s2)
6.
j: Vertices(the_graph)
7.
(inr(j) 
s2)
8.
(inl(j) s2)
j-the_graph- > *i
By:
ObviousContradiction [5]
Generated subgoals:
None
About:
