<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>Aha! So I've just got an old version. Good to know! Thank you. :)</span></div><div></div><div>&nbsp;</div><div>- darryl<br></div>  <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <hr size="1">  <font size="2" face="Arial"> <b><span style="font-weight:bold;">From:</span></b> Andrés Sicard-Ramírez &lt;andres.sicard.ramirez@gmail.com&gt;<br> <b><span style="font-weight: bold;">To:</span></b> Darryl McAdams &lt;psygnisfive@yahoo.com&gt; <br><b><span style="font-weight: bold;">Cc:</span></b> "agda@lists.chalmers.se" &lt;agda@lists.chalmers.se&gt; <br> <b><span style="font-weight: bold;">Sent:</span></b> Wednesday, July 3, 2013 8:43 AM<br> <b><span style="font-weight: bold;">Subject:</span></b> Re:
 [Agda] Termination-check doesn't know which case it should check?<br> </font> </div> <div class="y_msg_container"><br>On 3 July 2013 03:34, Darryl McAdams &lt;<a ymailto="mailto:psygnisfive@yahoo.com" href="mailto:psygnisfive@yahoo.com">psygnisfive@yahoo.com</a>&gt; wrote:<br>&gt; The following code gives a termination error on &lt;+&gt;-lemma even tho the<br>&gt; recursion is guarded.<br>&gt;<br>&gt; _+&gt;_ : ℕ → ℕ → ℕ<br>&gt; zero&nbsp; +&gt; n = n<br>&gt; suc m +&gt; n = m +&gt; suc n<br>&gt;<br>&gt; _&lt;+_ : ℕ → ℕ → ℕ<br>&gt; m &lt;+ zero&nbsp; = m<br>&gt; m &lt;+ suc n = suc m &lt;+ n<br>&gt;<br>&gt; +&gt;-suc-lemma : (m n : ℕ) → m +&gt; suc n ≡ suc (m +&gt; n)<br>&gt; +&gt;-suc-lemma m n = {!!}<br>&gt;<br>&gt; &lt;+-suc-lemma : (m n : ℕ) → suc m &lt;+ n ≡ suc (m &lt;+ n)<br>&gt; &lt;+-suc-lemma m n = {!!}<br>&gt;<br>&gt; &lt;+&gt;-lemma : (m n : ℕ) → m +&gt; n ≡ m &lt;+ n<br>&gt; &lt;+&gt;-lemma 0&nbsp;
 &nbsp; &nbsp;  0 = refl<br>&gt; &lt;+&gt;-lemma 0&nbsp; &nbsp; &nbsp;  (suc n) rewrite &lt;+-suc-lemma 0 n | cong suc (&lt;+&gt;-lemma 0<br>&gt; n) = refl<br>&gt; &lt;+&gt;-lemma (suc m) 0&nbsp; &nbsp; &nbsp;  rewrite +&gt;-suc-lemma m 0 | cong suc (&lt;+&gt;-lemma m<br>&gt; 0) = refl<br>&gt; &lt;+&gt;-lemma (suc m) (suc n) rewrite &lt;+-suc-lemma (suc m) n | &lt;+-suc-lemma m n<br>&gt;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;  | +&gt;-suc-lemma m (suc n) | +&gt;-suc-lemma m n<br>&gt;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;  | cong (suc ∘ suc) (&lt;+&gt;-lemma m n) = refl<br>&gt;<br><br>I couldn't reproduce the issue with Agda-2.3.2.1.<br><br>-- <br>Andrés<br><br></div> </div> </div>  </div></body></html>