MiniAgda-0.2014.1.9: test/succeed/DescendAscendTerm.ma

data Nat : Set
{ zero : Nat
; succ : Nat -> Nat
}

fun plus : Nat -> Nat -> Nat {}

mutual {

  fun f : Nat -> Nat
  { f (succ (succ (succ n))) = g n n
  }

  fun g : Nat -> Nat -> Nat
  { g (succ n) m = plus (g n (succ m)) (f n)
  }
}