How to prove that the pre-order tree traversal algorithm terminates?
Hint (by Raphael):  How do you prove that the recursive factorial function terminates?

Answer (by Kejia): The recursive factorial function's universe is non-negative integers, which is countable and so well-found, and so it is very easy to prove with mathematical induction.  

By analogy, we can find a mapping from trees to a well-founded universe so that a similar proof works.


   Our mapping is to the size of the subtree.
 At each recursive call, the size of a subproblem (i.e. a subtree) is strictly decreasing and always non-negative. Therefore, we can proceed by induction.

 Suppose (induction hypothesis) that the function on a tree of size of at most k terminates. Now consider an input tree with k+1 nodes...