# [isabelle] Problem during goal simplification

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

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