At:
dfl-traversal-consl
1
2
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.
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)
12.
(inr(j) s2)
13.
(inl(j) s2)
14.
inl(i) = u
15.
s = (v @ [inr(i@0) / s2]) traversal(the_graph)
j-the_graph- > *i@0
By:
AllHyps (
h.(Unfold `dfl-traversal` h) THEN (Analyze h) THEN (Analyze h) THEN (InstHyp [i@0;v;s2;j] h) THEN (Reduce 0))
Generated subgoals:
None
About:
