MAYBE

Problem:
 f(tt(),x) -> f(isNat(x),s(x))
 isNat(s(x)) -> isNat(x)
 isNat(0()) -> tt()

Proof:
 DP Processor:
  DPs:
   f#(tt(),x) -> isNat#(x)
   f#(tt(),x) -> f#(isNat(x),s(x))
   isNat#(s(x)) -> isNat#(x)
  TRS:
   f(tt(),x) -> f(isNat(x),s(x))
   isNat(s(x)) -> isNat(x)
   isNat(0()) -> tt()
  Open