module terminationnat1 where

data ℕ : Set where
  Z : ℕ 
  S : ℕ -> ℕ 

pred : ℕ -> ℕ
pred Z     = Z
pred (S n) = n

f : ℕ -> ℕ
f Z     = Z
f (S n) = f (pred n)