## Stream: Beginner Questions

#### Bernhard Stöckl (Sep 27 2021 at 14:21):

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: Aug 13 2022 at 06:26 UTC