(FUN
  f : o -> o -> o
  s : o -> o
  a : o
  b : o
  mu : (o -> o) -> o
)
(VAR
  x : o
  Z : o -> o
)
(RULES
  f x x -> a,
  f x (s x) -> b,
  mu (\x. Z x) -> Z (mu (\x. Z x))
)
(COMMENT Example 4.2 of \cite{AvOS10})