x,y:V. Dec(x = y)) 
(x,y:V. x-the_graph- > *y 
x = y 
(
z:V. 
z = x & x-the_graph- > z & z-the_graph- > *y))p:V List. 1 < ||p|| path(the_graph;p) path(the_graph;tl(p))l:A List. ||l||
1 ||tl(l)|| = ||l||-1 
as:A List, n:
(||as||-1). tl(as)[n] = as[(n+1)]L:T List, x:T. null(L) last([x / L]) = last(L)