<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>The following code gives a termination error on &lt;+&gt;-lemma even tho the recursion is guarded.</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><div style="background-color: transparent; ">_+&gt;_ : ℕ → ℕ → ℕ</div><div style="background-color: transparent; ">zero &nbsp;+&gt; n = n</div><div style="background-color: transparent; ">suc m +&gt; n = m +&gt; suc n</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">_&lt;+_ : ℕ → ℕ → ℕ</div><div style="background-color:
 transparent; ">m &lt;+ zero &nbsp;= m</div><div style="background-color: transparent; ">m &lt;+ suc n = suc m &lt;+ n</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">+&gt;-suc-lemma : (m n : ℕ) → m +&gt; suc n ≡ suc (m +&gt; n)</div><div style="background-color: transparent; ">+&gt;-suc-lemma m n = {!!}</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">&lt;+-suc-lemma : (m n : ℕ) → suc m &lt;+ n ≡ suc (m &lt;+ n)</div><div style="background-color: transparent; ">&lt;+-suc-lemma m n = {!!}</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">&lt;+&gt;-lemma : (m n : ℕ) → m +&gt; n ≡ m &lt;+ n</div><div style="background-color: transparent; ">&lt;+&gt;-lemma 0 &nbsp; &nbsp; &nbsp; 0 = refl</div><div style="background-color: transparent; ">&lt;+&gt;-lemma 0 &nbsp; &nbsp; &nbsp;
 (suc n) rewrite &lt;+-suc-lemma 0 n | cong suc (&lt;+&gt;-lemma 0 n) = refl</div><div style="background-color: transparent; ">&lt;+&gt;-lemma (suc m) 0 &nbsp; &nbsp; &nbsp; rewrite +&gt;-suc-lemma m 0 | cong suc (&lt;+&gt;-lemma m 0) = refl</div><div style="background-color: transparent; ">&lt;+&gt;-lemma (suc m) (suc n) rewrite &lt;+-suc-lemma (suc m) n | &lt;+-suc-lemma m n</div><div style="background-color: transparent; ">&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</div><div style="background-color: transparent; ">&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</div></span></div><div></div><div>&nbsp;</div><div>- darryl</div>  </div></body></html>