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

[Darryl McAdams]

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
 
- darryl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130703/13e6f924/attachment-0001.html