I have a function like this where I can prove termination:

```
function to_dtree_aux :: "'a ⇒ ('a,'b) dtree" where
"to_dtree_aux r = Node r (Abs_fset {(x,e).
(if e ∈ out_arcs T r then x = to_dtree_aux (head T e) else False)})"
```

I would expect this to be equivalent to ("if P then Q else False" replaced by "P and Q"):

```
function to_dtree_aux :: "'a ⇒ ('a,'b) dtree" where
"to_dtree_aux r = Node r (Abs_fset {(x,e).
(e ∈ out_arcs T r ∧ x = to_dtree_aux (head T e))})"
```

But for the second function, I can't prove termination because the assumption `e ∈ out_arcs T r`

is missing in the goal. Is there a better way to introduce this assumption than using a "if P then Q else False" construct?

The goals generated by `apply(relation "measure (λr. Finite_Set.card {x. r →⇧*⇘T⇙ x})")`

look like this:

```
⋀r x xa. xa ∈ out_arcs T r ⟹ (head T xa, r) ∈ measure (λr. card {x. r →⇧*⇘T⇙ x})
⋀r x xa. (head T xa, r) ∈ measure (λr. card {x. r →⇧*⇘T⇙ x})
```

Last updated: Sep 25 2022 at 23:25 UTC