[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.