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()
  TDG 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()
   graph:
    isNat#(s(x)) -> isNat#(x) -> isNat#(s(x)) -> isNat#(x)
    f#(tt(),x) -> isNat#(x) -> isNat#(s(x)) -> isNat#(x)
    f#(tt(),x) -> f#(isNat(x),s(x)) ->
    f#(tt(),x) -> f#(isNat(x),s(x))
    f#(tt(),x) -> f#(isNat(x),s(x)) -> f#(tt(),x) -> isNat#(x)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 4/9
    DPs:
     f#(tt(),x) -> f#(isNat(x),s(x))
    TRS:
     f(tt(),x) -> f(isNat(x),s(x))
     isNat(s(x)) -> isNat(x)
     isNat(0()) -> tt()
    Open
    
    DPs:
     isNat#(s(x)) -> isNat#(x)
    TRS:
     f(tt(),x) -> f(isNat(x),s(x))
     isNat(s(x)) -> isNat(x)
     isNat(0()) -> tt()
    Subterm Criterion Processor:
     simple projection:
      pi(isNat#) = 0
     problem:
      DPs:
       
      TRS:
       f(tt(),x) -> f(isNat(x),s(x))
       isNat(s(x)) -> isNat(x)
       isNat(0()) -> tt()
     Qed