P(L' @ [x],list_accum(s,i.dfs(the_obj;s;i);nil;L' @ [x]))
traversal(the_graph)Prop
L:Vertices(the_graph) List, s:traversal(the_graph), i:Vertices(the_graph).
P(L,s) 
P(L @ [i],dfs(the_obj;s;i))
L1:Vertices(the_graph) List. ||L1|| < ||L|| P(L1,list_accum(s,i.dfs(the_obj;s;i);nil;L1))
L = nil
P(L' @ [x],list_accum(s,i.dfs(the_obj;s;i);nil;L' @ [x]))
as,bs:T List. ||as @ bs|| = ||as||+||bs|| 
0))
| 1 | 13. P(L',list_accum(s,i.dfs(the_obj;s;i);nil;L')) P(L' @ [x],list_accum(s,i.dfs(the_obj;s;i);nil;L' @ [x])) | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |  |  |