MAYBE

Problem:
 add(true(),x,xs) -> add(and(isNat(x),isList(xs)),x,Cons(x,xs))
 isList(Cons(x,xs)) -> isList(xs)
 isList(nil()) -> true()
 isNat(s(x)) -> isNat(x)
 isNat(0()) -> true()
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 and(true(),true()) -> true()
 and(false(),x) -> false()
 and(x,false()) -> false()

Proof:
 DP Processor:
  DPs:
   add#(true(),x,xs) -> isList#(xs)
   add#(true(),x,xs) -> isNat#(x)
   add#(true(),x,xs) -> and#(isNat(x),isList(xs))
   add#(true(),x,xs) -> add#(and(isNat(x),isList(xs)),x,Cons(x,xs))
   isList#(Cons(x,xs)) -> isList#(xs)
   isNat#(s(x)) -> isNat#(x)
  TRS:
   add(true(),x,xs) -> add(and(isNat(x),isList(xs)),x,Cons(x,xs))
   isList(Cons(x,xs)) -> isList(xs)
   isList(nil()) -> true()
   isNat(s(x)) -> isNat(x)
   isNat(0()) -> true()
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   and(true(),true()) -> true()
   and(false(),x) -> false()
   and(x,false()) -> false()
  Usable Rule Processor:
   DPs:
    add#(true(),x,xs) -> isList#(xs)
    add#(true(),x,xs) -> isNat#(x)
    add#(true(),x,xs) -> and#(isNat(x),isList(xs))
    add#(true(),x,xs) -> add#(and(isNat(x),isList(xs)),x,Cons(x,xs))
    isList#(Cons(x,xs)) -> isList#(xs)
    isNat#(s(x)) -> isNat#(x)
   TRS:
    isList(Cons(x,xs)) -> isList(xs)
    isList(nil()) -> true()
    isNat(s(x)) -> isNat(x)
    isNat(0()) -> true()
    and(true(),true()) -> true()
    and(false(),x) -> false()
    and(x,false()) -> false()
   Open