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()
  TDG 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()
   graph:
    isNat#(s(x)) -> isNat#(x) -> isNat#(s(x)) -> isNat#(x)
    isList#(Cons(x,xs)) -> isList#(xs) ->
    isList#(Cons(x,xs)) -> isList#(xs)
    add#(true(),x,xs) -> isNat#(x) -> isNat#(s(x)) -> isNat#(x)
    add#(true(),x,xs) -> isList#(xs) ->
    isList#(Cons(x,xs)) -> isList#(xs)
    add#(true(),x,xs) -> add#(and(isNat(x),isList(xs)),x,Cons(x,xs)) ->
    add#(true(),x,xs) -> add#(and(isNat(x),isList(xs)),x,Cons(x,xs))
    add#(true(),x,xs) -> add#(and(isNat(x),isList(xs)),x,Cons(x,xs)) ->
    add#(true(),x,xs) -> and#(isNat(x),isList(xs))
    add#(true(),x,xs) -> add#(and(isNat(x),isList(xs)),x,Cons(x,xs)) ->
    add#(true(),x,xs) -> isNat#(x)
    add#(true(),x,xs) -> add#(and(isNat(x),isList(xs)),x,Cons(x,xs)) ->
    add#(true(),x,xs) -> isList#(xs)
   SCC Processor:
    #sccs: 3
    #rules: 3
    #arcs: 8/36
    DPs:
     add#(true(),x,xs) -> add#(and(isNat(x),isList(xs)),x,Cons(x,xs))
    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()
    Open
    
    DPs:
     isList#(Cons(x,xs)) -> isList#(xs)
    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()
    Subterm Criterion Processor:
     simple projection:
      pi(isList#) = 0
     problem:
      DPs:
       
      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()
     Qed
    
    DPs:
     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()
    Subterm Criterion Processor:
     simple projection:
      pi(isNat#) = 0
     problem:
      DPs:
       
      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()
     Qed