comments

[Stephen Weeks]

> And, I'll be here for a while.  I'll drop an email before I leave for the
> evening (morning).

I am reading Theorem 2 and not having any luck understanding it.  I can not for
the life of me understand why the following statement is true.

Furthermore, there exists $l_i \in \Func$ and a path of calls from \main{}
to $l_i$ such that $k_j \neq l_{i+1}$ for each nontail call $(g_j,
g_{j+1}, k_j) \in \Nontail$ on the path and $g_j \neq l_{i+1}$ for
each tail call $(g_j, g_{j+1}) \in \Tail$ on the path.

I looked at the old proof in contify.txt, which only deals with cycles of
functions.  That one makes sense, because you can choose a shortest path that
leads into the cycle.  I don't see why that works here, though.

Anyways, it's getting late enough, and we're hurting for space enough that I'm
inclined to drop the proof of theorem 2 (possibly replacing it by a short
sketch, which you write, since I am confused).

Thoughts?