# [isabelle] context-sensitive termination proof

```Hello,

I am having trouble proving termination of a function whose recursive call argument decreases conditionally, in a context which is essentially the following:

typedecl A&nbsp; typedecl B&nbsp; typedecl C

consts
&nbsp;u :: "A =&gt; C =&gt; B"
&nbsp;v :: "C =&gt; A"
&nbsp;w :: "C =&gt; B"
&nbsp;P :: "A =&gt; C =&gt; bool"
&nbsp;size :: "A =&gt; nat"

axioms conditional_decrease:
"P a c ==&gt; size (v c) &lt; size a"

function f :: "A =&gt; B set" where
"f a = {u a c| c. P a c&nbsp; &amp;&nbsp; w c : f (v c)}"

The only tool I see available for proving termination of f is the lemma

f.termination: "[|wf ?R; !! a x c. (v c, a) : ?R|] ==&gt; ALL x. f_dom x"

while I would need something like:

f.context_sensitive_termination:
"[|wf ?R; !! a x c. P a c ==&gt; (v c, a) : ?R|] ==&gt; ALL x. f_dom x"

or rather

"[|wf (?R Int {(v c,a)| a c. P a c}); !! a x c. (v c, a) : ?R|] ==&gt; ALL x. f_dom x"

Thanks in advance for any hint on how to handle this.

&nbsp;&nbsp; Andrei Popescu

```

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