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

Basically you'll have to take the complement of your set "seen" with respect to the set of reachable nodes (i.e., the transitive closure of the children function from the node "src"). And yes, you'll have to prove that transitive closure to be a finite set, otherwise the function wouldn't terminate.
```
```
We have recently formalized a very similar function in the context of an automaton construction for model checking, and I could send you the theories and a paper (off-list) if you are interested.
```
Regards,
Stephan

Scott West wrote:
```
```Hello all,

```
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.
```
So I recursively define this function to essentially be something like:

all_children :: obj => obj set => obj set
all_children src seen =
if src \<in> seen
then seen
else
foldr all_children (children src) (seen \<union> {src})

```
I can't for the life of me figure out what the measure function should be in this case. Been thinking on it for a few days and I don't know how to state a termination proof in a way that Isabelle will understand. I should preface that by saying I only know of the "measure" method... and even then, not really well.
```
```
If anyone could provide some hint on how to go about this, then that would be great.
```
Regards,
Scott

```
```begin:vcard
fn:Stephan Merz
n:Merz;Stephan
org:INRIA Nancy & LORIA