MAYBE

Problem:
 isEmpty(cons(x,xs)) -> false()
 isEmpty(nil()) -> true()
 isZero(0()) -> true()
 isZero(s(x)) -> false()
 head(cons(x,xs)) -> x
 tail(cons(x,xs)) -> xs
 tail(nil()) -> nil()
 append(nil(),x) -> cons(x,nil())
 append(cons(y,ys),x) -> cons(y,append(ys,x))
 p(s(s(x))) -> s(p(s(x)))
 p(s(0())) -> 0()
 p(0()) -> 0()
 inc(s(x)) -> s(inc(x))
 inc(0()) -> s(0())
 addLists(xs,ys,zs) ->
 if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
    cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
 if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
 if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
 if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
 if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
 if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
 addList(xs,ys) -> addLists(xs,ys,nil())

Proof:
 DP Processor:
  DPs:
   append#(cons(y,ys),x) -> append#(ys,x)
   p#(s(s(x))) -> p#(s(x))
   inc#(s(x)) -> inc#(x)
   addLists#(xs,ys,zs) -> append#(zs,head(ys))
   addLists#(xs,ys,zs) -> head#(ys)
   addLists#(xs,ys,zs) -> inc#(head(ys))
   addLists#(xs,ys,zs) -> p#(head(xs))
   addLists#(xs,ys,zs) -> tail#(ys)
   addLists#(xs,ys,zs) -> tail#(xs)
   addLists#(xs,ys,zs) -> head#(xs)
   addLists#(xs,ys,zs) -> isZero#(head(xs))
   addLists#(xs,ys,zs) -> isEmpty#(ys)
   addLists#(xs,ys,zs) -> isEmpty#(xs)
   addLists#(xs,ys,zs) ->
   if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
       cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
   if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs)
   if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2)
   addList#(xs,ys) -> addLists#(xs,ys,nil())
  TRS:
   isEmpty(cons(x,xs)) -> false()
   isEmpty(nil()) -> true()
   isZero(0()) -> true()
   isZero(s(x)) -> false()
   head(cons(x,xs)) -> x
   tail(cons(x,xs)) -> xs
   tail(nil()) -> nil()
   append(nil(),x) -> cons(x,nil())
   append(cons(y,ys),x) -> cons(y,append(ys,x))
   p(s(s(x))) -> s(p(s(x)))
   p(s(0())) -> 0()
   p(0()) -> 0()
   inc(s(x)) -> s(inc(x))
   inc(0()) -> s(0())
   addLists(xs,ys,zs) ->
   if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
      cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
   if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
   if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
   if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
   if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
   if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
   addList(xs,ys) -> addLists(xs,ys,nil())
  TDG Processor:
   DPs:
    append#(cons(y,ys),x) -> append#(ys,x)
    p#(s(s(x))) -> p#(s(x))
    inc#(s(x)) -> inc#(x)
    addLists#(xs,ys,zs) -> append#(zs,head(ys))
    addLists#(xs,ys,zs) -> head#(ys)
    addLists#(xs,ys,zs) -> inc#(head(ys))
    addLists#(xs,ys,zs) -> p#(head(xs))
    addLists#(xs,ys,zs) -> tail#(ys)
    addLists#(xs,ys,zs) -> tail#(xs)
    addLists#(xs,ys,zs) -> head#(xs)
    addLists#(xs,ys,zs) -> isZero#(head(xs))
    addLists#(xs,ys,zs) -> isEmpty#(ys)
    addLists#(xs,ys,zs) -> isEmpty#(xs)
    addLists#(xs,ys,zs) ->
    if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs)
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2)
    addList#(xs,ys) -> addLists#(xs,ys,nil())
   TRS:
    isEmpty(cons(x,xs)) -> false()
    isEmpty(nil()) -> true()
    isZero(0()) -> true()
    isZero(s(x)) -> false()
    head(cons(x,xs)) -> x
    tail(cons(x,xs)) -> xs
    tail(nil()) -> nil()
    append(nil(),x) -> cons(x,nil())
    append(cons(y,ys),x) -> cons(y,append(ys,x))
    p(s(s(x))) -> s(p(s(x)))
    p(s(0())) -> 0()
    p(0()) -> 0()
    inc(s(x)) -> s(inc(x))
    inc(0()) -> s(0())
    addLists(xs,ys,zs) ->
    if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
       cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
    if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
    if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
    if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
    if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
    if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
    addList(xs,ys) -> addLists(xs,ys,nil())
   graph:
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) ->
    if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> isEmpty#(xs)
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> isEmpty#(ys)
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> isZero#(head(xs))
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> head#(xs)
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> tail#(xs)
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> tail#(ys)
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> p#(head(xs))
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> inc#(head(ys))
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> head#(ys)
    addList#(xs,ys) -> addLists#(xs,ys,nil()) ->
    addLists#(xs,ys,zs) -> append#(zs,head(ys))
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) ->
    if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> isEmpty#(xs)
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> isEmpty#(ys)
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> isZero#(head(xs))
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> head#(xs)
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> tail#(xs)
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> tail#(ys)
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> p#(head(xs))
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> inc#(head(ys))
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> head#(ys)
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2) ->
    addLists#(xs,ys,zs) -> append#(zs,head(ys))
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) ->
    if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> isEmpty#(xs)
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> isEmpty#(ys)
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> isZero#(head(xs))
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> head#(xs)
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> tail#(xs)
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> tail#(ys)
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> p#(head(xs))
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> inc#(head(ys))
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> head#(ys)
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs) ->
    addLists#(xs,ys,zs) -> append#(zs,head(ys))
    addLists#(xs,ys,zs) ->
    if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
    ->
    if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2)
    addLists#(xs,ys,zs) ->
    if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
    ->
    if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs)
    addLists#(xs,ys,zs) -> inc#(head(ys)) ->
    inc#(s(x)) -> inc#(x)
    addLists#(xs,ys,zs) -> p#(head(xs)) ->
    p#(s(s(x))) -> p#(s(x))
    addLists#(xs,ys,zs) -> append#(zs,head(ys)) ->
    append#(cons(y,ys),x) -> append#(ys,x)
    inc#(s(x)) -> inc#(x) -> inc#(s(x)) -> inc#(x)
    p#(s(s(x))) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
    append#(cons(y,ys),x) -> append#(ys,x) -> append#(cons(y,ys),x) -> append#(ys,x)
   SCC Processor:
    #sccs: 4
    #rules: 6
    #arcs: 41/289
    DPs:
     addLists#(xs,ys,zs) ->
     if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
         cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
     if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs2,ys2,zs)
     if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists#(xs,ys,zs2)
    TRS:
     isEmpty(cons(x,xs)) -> false()
     isEmpty(nil()) -> true()
     isZero(0()) -> true()
     isZero(s(x)) -> false()
     head(cons(x,xs)) -> x
     tail(cons(x,xs)) -> xs
     tail(nil()) -> nil()
     append(nil(),x) -> cons(x,nil())
     append(cons(y,ys),x) -> cons(y,append(ys,x))
     p(s(s(x))) -> s(p(s(x)))
     p(s(0())) -> 0()
     p(0()) -> 0()
     inc(s(x)) -> s(inc(x))
     inc(0()) -> s(0())
     addLists(xs,ys,zs) ->
     if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
     if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
     if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
     if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
     if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
     if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
     addList(xs,ys) -> addLists(xs,ys,nil())
    Open
    
    DPs:
     p#(s(s(x))) -> p#(s(x))
    TRS:
     isEmpty(cons(x,xs)) -> false()
     isEmpty(nil()) -> true()
     isZero(0()) -> true()
     isZero(s(x)) -> false()
     head(cons(x,xs)) -> x
     tail(cons(x,xs)) -> xs
     tail(nil()) -> nil()
     append(nil(),x) -> cons(x,nil())
     append(cons(y,ys),x) -> cons(y,append(ys,x))
     p(s(s(x))) -> s(p(s(x)))
     p(s(0())) -> 0()
     p(0()) -> 0()
     inc(s(x)) -> s(inc(x))
     inc(0()) -> s(0())
     addLists(xs,ys,zs) ->
     if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
     if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
     if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
     if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
     if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
     if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
     addList(xs,ys) -> addLists(xs,ys,nil())
    Subterm Criterion Processor:
     simple projection:
      pi(p#) = 0
     problem:
      DPs:
       
      TRS:
       isEmpty(cons(x,xs)) -> false()
       isEmpty(nil()) -> true()
       isZero(0()) -> true()
       isZero(s(x)) -> false()
       head(cons(x,xs)) -> x
       tail(cons(x,xs)) -> xs
       tail(nil()) -> nil()
       append(nil(),x) -> cons(x,nil())
       append(cons(y,ys),x) -> cons(y,append(ys,x))
       p(s(s(x))) -> s(p(s(x)))
       p(s(0())) -> 0()
       p(0()) -> 0()
       inc(s(x)) -> s(inc(x))
       inc(0()) -> s(0())
       addLists(xs,ys,zs) ->
       if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),
          cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,
          append(zs,head(ys)))
       if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
       if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
       if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
       if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
       if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
       addList(xs,ys) -> addLists(xs,ys,nil())
     Qed
    
    DPs:
     inc#(s(x)) -> inc#(x)
    TRS:
     isEmpty(cons(x,xs)) -> false()
     isEmpty(nil()) -> true()
     isZero(0()) -> true()
     isZero(s(x)) -> false()
     head(cons(x,xs)) -> x
     tail(cons(x,xs)) -> xs
     tail(nil()) -> nil()
     append(nil(),x) -> cons(x,nil())
     append(cons(y,ys),x) -> cons(y,append(ys,x))
     p(s(s(x))) -> s(p(s(x)))
     p(s(0())) -> 0()
     p(0()) -> 0()
     inc(s(x)) -> s(inc(x))
     inc(0()) -> s(0())
     addLists(xs,ys,zs) ->
     if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
     if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
     if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
     if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
     if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
     if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
     addList(xs,ys) -> addLists(xs,ys,nil())
    Subterm Criterion Processor:
     simple projection:
      pi(inc#) = 0
     problem:
      DPs:
       
      TRS:
       isEmpty(cons(x,xs)) -> false()
       isEmpty(nil()) -> true()
       isZero(0()) -> true()
       isZero(s(x)) -> false()
       head(cons(x,xs)) -> x
       tail(cons(x,xs)) -> xs
       tail(nil()) -> nil()
       append(nil(),x) -> cons(x,nil())
       append(cons(y,ys),x) -> cons(y,append(ys,x))
       p(s(s(x))) -> s(p(s(x)))
       p(s(0())) -> 0()
       p(0()) -> 0()
       inc(s(x)) -> s(inc(x))
       inc(0()) -> s(0())
       addLists(xs,ys,zs) ->
       if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),
          cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,
          append(zs,head(ys)))
       if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
       if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
       if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
       if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
       if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
       addList(xs,ys) -> addLists(xs,ys,nil())
     Qed
    
    DPs:
     append#(cons(y,ys),x) -> append#(ys,x)
    TRS:
     isEmpty(cons(x,xs)) -> false()
     isEmpty(nil()) -> true()
     isZero(0()) -> true()
     isZero(s(x)) -> false()
     head(cons(x,xs)) -> x
     tail(cons(x,xs)) -> xs
     tail(nil()) -> nil()
     append(nil(),x) -> cons(x,nil())
     append(cons(y,ys),x) -> cons(y,append(ys,x))
     p(s(s(x))) -> s(p(s(x)))
     p(s(0())) -> 0()
     p(0()) -> 0()
     inc(s(x)) -> s(inc(x))
     inc(0()) -> s(0())
     addLists(xs,ys,zs) ->
     if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
        cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
     if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
     if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
     if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
     if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
     if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
     addList(xs,ys) -> addLists(xs,ys,nil())
    Subterm Criterion Processor:
     simple projection:
      pi(append#) = 0
     problem:
      DPs:
       
      TRS:
       isEmpty(cons(x,xs)) -> false()
       isEmpty(nil()) -> true()
       isZero(0()) -> true()
       isZero(s(x)) -> false()
       head(cons(x,xs)) -> x
       tail(cons(x,xs)) -> xs
       tail(nil()) -> nil()
       append(nil(),x) -> cons(x,nil())
       append(cons(y,ys),x) -> cons(y,append(ys,x))
       p(s(s(x))) -> s(p(s(x)))
       p(s(0())) -> 0()
       p(0()) -> 0()
       inc(s(x)) -> s(inc(x))
       inc(0()) -> s(0())
       addLists(xs,ys,zs) ->
       if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),
          cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,
          append(zs,head(ys)))
       if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
       if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
       if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
       if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
       if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
       addList(xs,ys) -> addLists(xs,ys,nil())
     Qed