[Agda] Termination-check doesn't know which case it should check?

[Andrés Sicard-Ramírez]

On 3 July 2013 03:34, Darryl McAdams <psygnisfive at yahoo.com> wrote:
> The following code gives a termination error on <+>-lemma even tho the
> recursion is guarded.
>
> _+>_ : ℕ → ℕ → ℕ
> zero  +> n = n
> suc m +> n = m +> suc n
>
> _<+_ : ℕ → ℕ → ℕ
> m <+ zero  = m
> m <+ suc n = suc m <+ n
>
> +>-suc-lemma : (m n : ℕ) → m +> suc n ≡ suc (m +> n)
> +>-suc-lemma m n = {!!}
>
> <+-suc-lemma : (m n : ℕ) → suc m <+ n ≡ suc (m <+ n)
> <+-suc-lemma m n = {!!}
>
> <+>-lemma : (m n : ℕ) → m +> n ≡ m <+ n
> <+>-lemma 0       0 = refl
> <+>-lemma 0       (suc n) rewrite <+-suc-lemma 0 n | cong suc (<+>-lemma 0
> n) = refl
> <+>-lemma (suc m) 0       rewrite +>-suc-lemma m 0 | cong suc (<+>-lemma m
> 0) = refl
> <+>-lemma (suc m) (suc n) rewrite <+-suc-lemma (suc m) n | <+-suc-lemma m n
>                                 | +>-suc-lemma m (suc n) | +>-suc-lemma m n
>                                 | cong (suc ∘ suc) (<+>-lemma m n) = refl
>

I couldn't reproduce the issue with Agda-2.3.2.1.

-- 
Andrés