At:
path-tl
1
2
1
1
1.
the_graph: Graph
2.
p: Vertices(the_graph) List
3.
1 < ||p||
4.
0 < ||p||
5.
i:
(||p||-1). p[i]-the_graph- > p[(i+1)]
6.
q: Vertices(the_graph) List
7.
tl(p) = q
8.
||q|| = ||p||-1 
9.
i:(||p||-1). q[i] = p[(i+1)]
10.
i: (||q||-1)
q[i]-the_graph- > q[(i+1)]
By:
InstHyp [i+1] 5
THEN
NthHypEq -1
THEN
Analyze
THEN
Obvious
Generated subgoals:
None
About:
