MAYBE

Problem:
 f(x,y) -> cond(and(isNat(x),isNat(y)),x,y)
 cond(tt(),x,y) -> f(s(x),s(y))
 isNat(s(x)) -> isNat(x)
 isNat(0()) -> tt()
 and(tt(),tt()) -> tt()
 and(ff(),x) -> ff()
 and(x,ff()) -> ff()

Proof:
 DP Processor:
  DPs:
   f#(x,y) -> isNat#(y)
   f#(x,y) -> isNat#(x)
   f#(x,y) -> and#(isNat(x),isNat(y))
   f#(x,y) -> cond#(and(isNat(x),isNat(y)),x,y)
   cond#(tt(),x,y) -> f#(s(x),s(y))
   isNat#(s(x)) -> isNat#(x)
  TRS:
   f(x,y) -> cond(and(isNat(x),isNat(y)),x,y)
   cond(tt(),x,y) -> f(s(x),s(y))
   isNat(s(x)) -> isNat(x)
   isNat(0()) -> tt()
   and(tt(),tt()) -> tt()
   and(ff(),x) -> ff()
   and(x,ff()) -> ff()
  TDG Processor:
   DPs:
    f#(x,y) -> isNat#(y)
    f#(x,y) -> isNat#(x)
    f#(x,y) -> and#(isNat(x),isNat(y))
    f#(x,y) -> cond#(and(isNat(x),isNat(y)),x,y)
    cond#(tt(),x,y) -> f#(s(x),s(y))
    isNat#(s(x)) -> isNat#(x)
   TRS:
    f(x,y) -> cond(and(isNat(x),isNat(y)),x,y)
    cond(tt(),x,y) -> f(s(x),s(y))
    isNat(s(x)) -> isNat(x)
    isNat(0()) -> tt()
    and(tt(),tt()) -> tt()
    and(ff(),x) -> ff()
    and(x,ff()) -> ff()
   graph:
    cond#(tt(),x,y) -> f#(s(x),s(y)) ->
    f#(x,y) -> cond#(and(isNat(x),isNat(y)),x,y)
    cond#(tt(),x,y) -> f#(s(x),s(y)) ->
    f#(x,y) -> and#(isNat(x),isNat(y))
    cond#(tt(),x,y) -> f#(s(x),s(y)) -> f#(x,y) -> isNat#(x)
    cond#(tt(),x,y) -> f#(s(x),s(y)) -> f#(x,y) -> isNat#(y)
    isNat#(s(x)) -> isNat#(x) ->
    isNat#(s(x)) -> isNat#(x)
    f#(x,y) -> cond#(and(isNat(x),isNat(y)),x,y) ->
    cond#(tt(),x,y) -> f#(s(x),s(y))
    f#(x,y) -> isNat#(y) -> isNat#(s(x)) -> isNat#(x)
    f#(x,y) -> isNat#(x) -> isNat#(s(x)) -> isNat#(x)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 8/36
    DPs:
     cond#(tt(),x,y) -> f#(s(x),s(y))
     f#(x,y) -> cond#(and(isNat(x),isNat(y)),x,y)
    TRS:
     f(x,y) -> cond(and(isNat(x),isNat(y)),x,y)
     cond(tt(),x,y) -> f(s(x),s(y))
     isNat(s(x)) -> isNat(x)
     isNat(0()) -> tt()
     and(tt(),tt()) -> tt()
     and(ff(),x) -> ff()
     and(x,ff()) -> ff()
    Open
    
    DPs:
     isNat#(s(x)) -> isNat#(x)
    TRS:
     f(x,y) -> cond(and(isNat(x),isNat(y)),x,y)
     cond(tt(),x,y) -> f(s(x),s(y))
     isNat(s(x)) -> isNat(x)
     isNat(0()) -> tt()
     and(tt(),tt()) -> tt()
     and(ff(),x) -> ff()
     and(x,ff()) -> ff()
    Subterm Criterion Processor:
     simple projection:
      pi(isNat#) = 0
     problem:
      DPs:
       
      TRS:
       f(x,y) -> cond(and(isNat(x),isNat(y)),x,y)
       cond(tt(),x,y) -> f(s(x),s(y))
       isNat(s(x)) -> isNat(x)
       isNat(0()) -> tt()
       and(tt(),tt()) -> tt()
       and(ff(),x) -> ff()
       and(x,ff()) -> ff()
     Qed