Re: [isabelle] Termination Proof ``fun'' ;)

Scott West wrote:

I have recently been trying to write a function, which Isabelle
would like to know terminates. The basic task is to find
reachability, but I don't have an explicit graph, I have a function
which returns children of the current node. [...]

I can't for the life of me figure out what the measure function should
be in this case. [...]

If anyone could provide some hint on how to go about this, then that
would be great.

This example, and others similar to it, are described in the paper by
Slind and Owens, available from


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.