# [Agda] Termination problems with "with" and recursion

Jan Stolarek jan.stolarek at p.lodz.pl
Wed Oct 30 12:29:20 CET 2013

```Thanks for reply Jesper. Perhaps I ommitied something important when trying to simplify my
example. Full code is below:

========== START CODE ==========

module MergeSort where

record Sg (S : Set)(T : S → Set) : Set where
constructor _,_
field
fst : S
snd : T fst
open Sg public
_×_ : Set → Set → Set
S × T = Sg S λ _ → T
infixr 4 _,_ _×_

data Nat : Set where
zero : Nat
suc  : Nat → Nat

data Order : Set where
le ge : Order

data List (X : Set) : Set where
nil  : List X
_::_ : X → List X → List X

order : Nat → Nat → Order
order zero    y       = le
order (suc x) zero    = ge
order (suc x) (suc y) = order x y

merge : List Nat → List Nat → List Nat
merge nil       ys             = ys
merge xs        nil            = xs
merge (x :: xs) (y :: ys) with order x y
merge (x :: xs) (y :: ys) | le = x :: merge xs (y :: ys)
merge (x :: xs) (y :: ys) | ge = y :: merge (x :: xs) ys

deal : {X : Set} → List X → List X × List X
deal nil        = nil , nil
deal (x :: nil) = x :: nil , nil
deal (y :: (z :: xs)) with deal xs
deal (y :: (z :: xs)) | ys , zs = y :: ys , z :: zs

sort : List Nat → List Nat
sort xs with deal xs
sort xs | ys , nil = ys
sort xs | ys , zs  = merge (sort ys) (sort zs)

========== END CODE ==========

I have problems with merge and sort.

Janek
```