<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>In relation to issue 59:</div><div><br></div><div><a href="http://code.google.com/p/agda/issues/detail?id=59&can=1&q=termination">http://code.google.com/p/agda/issues/detail?id=59&can=1&q=termination</a></div><div><br></div><div>Here is another problem I've encountered along similar lines. In the code below, the functions f, g, h, and i all are in principal the same. However, only g and h pass the termination checker. Function f suffers from the problem in issue 59. Function g solves it with the same workaround suggested in issue 59. Function h solves it in a similar way. The problem is function i. It is very similar to function h but the argument (sn < ssn) in the helper function is concealed inside a product type and needs to be extracted using proj₂ which breaks this example. Is this a bug? Sorry for the hard to read code and function names..</div><div><br></div><div>The code below is based on Andreas Abel's earlier example..</div><div><br></div><div>Ruben</div><div><br></div><div>----------</div><div><br></div><div>module TerminationTwoConstructors where</div><div><br></div><div>open import Data.Nat</div><div>open import Relation.Binary</div><div>open import Relation.Binary.PropositionalEquality</div><div>open import Data.Product</div><div><br></div><div>bla : ℕ -> ℕ</div><div>bla m = m</div><div><br></div><div>f : ℕ -> ℕ</div><div>f zero = zero</div><div>f (suc zero) = zero</div><div>f (suc (suc n)) with bla (suc (suc n))</div><div>... | m = f (suc n)</div><div><br></div><div>g : ℕ -> ℕ</div><div>g zero = zero</div><div>g (suc zero) = zero</div><div>g (suc (suc n)) = helper (suc (suc n)) (suc n) refl (bla (suc (suc n)))</div><div> where</div><div> helper : (ssn : ℕ) -> (sn : ℕ) -> (suc sn ≡ ssn) -> (m : ℕ) -> ℕ</div><div> helper ssn sn _ m = g sn</div><div><br></div><div>≤-refl : _≡_ ⇒ _≤_</div><div>≤-refl = IsPreorder.reflexive (IsPartialOrder.isPreorder (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))))</div><div><br></div><div>h : ℕ -> ℕ</div><div>h zero = zero</div><div>h (suc zero) = zero</div><div>h (suc (suc n)) = helper (suc (suc n)) (suc n) (≤-refl refl) (bla (suc (suc n)))</div><div> where</div><div> helper : (ssn : ℕ) -> (sn : ℕ) -> (sn < ssn) -> (m : ℕ) -> ℕ</div><div> helper ssn sn _ m = h sn</div><div><br></div><div>zog : (n : ℕ) -> (ℕ × n < suc n)</div><div>zog n = n , ≤-refl refl</div><div><br></div><div>i : ℕ -> ℕ</div><div>i zero = zero</div><div>i (suc zero) = zero</div><div>i (suc (suc n)) = let whee = zog (suc n) in helper (suc (suc n)) (proj₁ whee) (proj₂ whee) (bla (suc (suc n)))</div><div> where</div><div> helper : (ssn : ℕ) -> (sn : ℕ) -> (sn < ssn) -> (m : ℕ) -> ℕ</div><div> helper ssn sn _ m = i sn</div><div><br></div></body></html>