<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 <+>-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; ">_+>_ : ℕ → ℕ → ℕ</div><div style="background-color: transparent; ">zero +> n = n</div><div style="background-color: transparent; ">suc m +> n = m +> suc n</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">_<+_ : ℕ → ℕ → ℕ</div><div style="background-color:
transparent; ">m <+ zero = m</div><div style="background-color: transparent; ">m <+ suc n = suc m <+ n</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">+>-suc-lemma : (m n : ℕ) → m +> suc n ≡ suc (m +> n)</div><div style="background-color: transparent; ">+>-suc-lemma m n = {!!}</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; "><+-suc-lemma : (m n : ℕ) → suc m <+ n ≡ suc (m <+ n)</div><div style="background-color: transparent; "><+-suc-lemma m n = {!!}</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; "><+>-lemma : (m n : ℕ) → m +> n ≡ m <+ n</div><div style="background-color: transparent; "><+>-lemma 0 0 = refl</div><div style="background-color: transparent; "><+>-lemma 0
(suc n) rewrite <+-suc-lemma 0 n | cong suc (<+>-lemma 0 n) = refl</div><div style="background-color: transparent; "><+>-lemma (suc m) 0 rewrite +>-suc-lemma m 0 | cong suc (<+>-lemma m 0) = refl</div><div style="background-color: transparent; "><+>-lemma (suc m) (suc n) rewrite <+-suc-lemma (suc m) n | <+-suc-lemma m n</div><div style="background-color: transparent; "> | +>-suc-lemma m (suc n) | +>-suc-lemma m n</div><div style="background-color: transparent; "> | cong (suc ∘ suc) (<+>-lemma m n) = refl</div></span></div><div></div><div> </div><div>- darryl</div> </div></body></html>