# Re: [isabelle] context-sensitive termination proof

```Andrei,

```
I am having trouble proving termination of a function whose recursive call argument decreases conditionally, in a context which is essentially the following:
```[...]
```
```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"
```
```
You need to add a congruence rule (here: conj_cong for the conjunction) to the definition. See the attached theory (and the function tutorial for some more explanation on congruence rules).
```
Hope this helps
Alex

```
```theory Scratch imports Main
begin
typedecl A
typedecl B
typedecl C

consts
u :: "A => C => B"
v :: "C => A"
w :: "C => B"
P :: "A => C => bool"
size :: "A => nat"

axioms conditional_decrease:
"P a c ==> size (v c) < size a"

declare conj_cong[fundef_cong]

function f :: "A => B set" where
"f a = {u a c| c. P a c  \<and>  w c : f (v c)}"
by auto

termination
by (relation "measure size") (auto simp: conditional_decrease)

```

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