# Re: [isabelle] Problem during goal simplification

Frankly, it is hard to say. Maybe the if-splits created some premises that constitute a nonterminating set of equations? That's heuristic proof automation for you.
```
```
The following proof script simplifies the goal completely. Although the resulting goal is unenlightening (for me), the script may be of use:
```
apply(split if_split)
apply(split if_split)
apply (simp split del: if_split)
apply(split if_split)
apply (simp split del: if_split)
apply(split if_split)
apply (simp split del: if_split)

Here is another gadget for tweaking the simplifier:

using [[simp_depth_limit = 3]] apply simp

```
This does the job. A second call to simp (which is not influenced by that "using") fails, showing that the result is fully simplified.
```
Tobias

On 21/04/2016 21:38, Omar MontaÃo Rivas wrote:
```
```Hi,

Does anyone know why the following goal loops after simplification (simp)?
Is there a way to avoid non-termination, e.g. by eliminating a rewrite rule
or a congruence rule from the simpset? I have tried changing the value of
linarith_split_limit but with no success.

Thanks,
Omar.

declare [[linarith_split_limit = 0]]

lemma "âf g. â(x::nat) y. f x y = (if 0 = y then if y = 0 then f 0 y else
if 0 - 1 - 1 = y then y else y else y) â
g x y =
(if y - 1 - 1 =
(if y - 1 - 1 =
(if 0 = y - 1 then y - 1 else (if y = (if y - 1 = y
- 1 then y - 1 else y - 1) - 1 - 1 - 1 then y else y) - 1) - 1 - 1 - 1
then if y = (if y = y - 1 - 1 then y - 1 else y) - 1 -
1 - 1 then y else y else y - 1) -
1 -
1
then x else y)"
using [[simp_trace]] apply simp

```
```
```

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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