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()
    KBO Processor:
     argument filtering:
      pi(tt) = []
      pi(f) = []
      pi(isNat) = []
      pi(s) = [0]
      pi(0) = []
      pi(isNat#) = 0
     weight function:
      w0 = 1
      w(isNat#) = w(0) = w(s) = w(isNat) = w(f) = w(tt) = 1
     precedence:
      isNat# ~ 0 ~ s ~ isNat > f ~ tt
     problem:
      DPs:
       
      TRS:
       f(tt(),x) -> f(isNat(x),s(x))
       isNat(s(x)) -> isNat(x)
       isNat(0()) -> tt()
     Qed