MAYBE

Problem:
 app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
 plus(x,0()) -> x
 plus(x,s(y)) -> s(plus(x,y))
 length(nil()) -> 0()
 length(cons(x,y)) -> s(length(y))
 helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
 ge(x,0()) -> true()
 ge(0(),s(x)) -> false()
 ge(s(x),s(y)) -> ge(x,y)
 if(true(),c,l,ys,zs) -> nil()
 if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
 greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
 smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
 helpc(true(),ys,zs) -> ys
 helpc(false(),ys,zs) -> zs
 helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))

Proof:
 DP Processor:
  DPs:
   app#(x,y) -> length#(y)
   app#(x,y) -> length#(x)
   app#(x,y) -> plus#(length(x),length(y))
   app#(x,y) -> helpa#(0(),plus(length(x),length(y)),x,y)
   plus#(x,s(y)) -> plus#(x,y)
   length#(cons(x,y)) -> length#(y)
   helpa#(c,l,ys,zs) -> ge#(c,l)
   helpa#(c,l,ys,zs) -> if#(ge(c,l),c,l,ys,zs)
   ge#(s(x),s(y)) -> ge#(x,y)
   if#(false(),c,l,ys,zs) -> smaller#(ys,zs)
   if#(false(),c,l,ys,zs) -> greater#(ys,zs)
   if#(false(),c,l,ys,zs) -> helpb#(c,l,greater(ys,zs),smaller(ys,zs))
   greater#(ys,zs) -> length#(zs)
   greater#(ys,zs) -> length#(ys)
   greater#(ys,zs) -> ge#(length(ys),length(zs))
   greater#(ys,zs) -> helpc#(ge(length(ys),length(zs)),ys,zs)
   smaller#(ys,zs) -> length#(zs)
   smaller#(ys,zs) -> length#(ys)
   smaller#(ys,zs) -> ge#(length(ys),length(zs))
   smaller#(ys,zs) -> helpc#(ge(length(ys),length(zs)),zs,ys)
   helpb#(c,l,cons(y,ys),zs) -> helpa#(s(c),l,ys,zs)
  TRS:
   app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
   plus(x,0()) -> x
   plus(x,s(y)) -> s(plus(x,y))
   length(nil()) -> 0()
   length(cons(x,y)) -> s(length(y))
   helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
   ge(x,0()) -> true()
   ge(0(),s(x)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
   if(true(),c,l,ys,zs) -> nil()
   if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
   greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
   smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
   helpc(true(),ys,zs) -> ys
   helpc(false(),ys,zs) -> zs
   helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))
  TDG Processor:
   DPs:
    app#(x,y) -> length#(y)
    app#(x,y) -> length#(x)
    app#(x,y) -> plus#(length(x),length(y))
    app#(x,y) -> helpa#(0(),plus(length(x),length(y)),x,y)
    plus#(x,s(y)) -> plus#(x,y)
    length#(cons(x,y)) -> length#(y)
    helpa#(c,l,ys,zs) -> ge#(c,l)
    helpa#(c,l,ys,zs) -> if#(ge(c,l),c,l,ys,zs)
    ge#(s(x),s(y)) -> ge#(x,y)
    if#(false(),c,l,ys,zs) -> smaller#(ys,zs)
    if#(false(),c,l,ys,zs) -> greater#(ys,zs)
    if#(false(),c,l,ys,zs) -> helpb#(c,l,greater(ys,zs),smaller(ys,zs))
    greater#(ys,zs) -> length#(zs)
    greater#(ys,zs) -> length#(ys)
    greater#(ys,zs) -> ge#(length(ys),length(zs))
    greater#(ys,zs) -> helpc#(ge(length(ys),length(zs)),ys,zs)
    smaller#(ys,zs) -> length#(zs)
    smaller#(ys,zs) -> length#(ys)
    smaller#(ys,zs) -> ge#(length(ys),length(zs))
    smaller#(ys,zs) -> helpc#(ge(length(ys),length(zs)),zs,ys)
    helpb#(c,l,cons(y,ys),zs) -> helpa#(s(c),l,ys,zs)
   TRS:
    app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
    plus(x,0()) -> x
    plus(x,s(y)) -> s(plus(x,y))
    length(nil()) -> 0()
    length(cons(x,y)) -> s(length(y))
    helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
    ge(x,0()) -> true()
    ge(0(),s(x)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    if(true(),c,l,ys,zs) -> nil()
    if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
    greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
    smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
    helpc(true(),ys,zs) -> ys
    helpc(false(),ys,zs) -> zs
    helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))
   graph:
    helpb#(c,l,cons(y,ys),zs) -> helpa#(s(c),l,ys,zs) ->
    helpa#(c,l,ys,zs) -> if#(ge(c,l),c,l,ys,zs)
    helpb#(c,l,cons(y,ys),zs) -> helpa#(s(c),l,ys,zs) ->
    helpa#(c,l,ys,zs) -> ge#(c,l)
    greater#(ys,zs) -> ge#(length(ys),length(zs)) ->
    ge#(s(x),s(y)) -> ge#(x,y)
    greater#(ys,zs) -> length#(zs) ->
    length#(cons(x,y)) -> length#(y)
    greater#(ys,zs) -> length#(ys) ->
    length#(cons(x,y)) -> length#(y)
    smaller#(ys,zs) -> ge#(length(ys),length(zs)) ->
    ge#(s(x),s(y)) -> ge#(x,y)
    smaller#(ys,zs) -> length#(zs) ->
    length#(cons(x,y)) -> length#(y)
    smaller#(ys,zs) -> length#(ys) ->
    length#(cons(x,y)) -> length#(y)
    if#(false(),c,l,ys,zs) -> helpb#(c,l,greater(ys,zs),smaller(ys,zs)) ->
    helpb#(c,l,cons(y,ys),zs) -> helpa#(s(c),l,ys,zs)
    if#(false(),c,l,ys,zs) -> greater#(ys,zs) ->
    greater#(ys,zs) -> helpc#(ge(length(ys),length(zs)),ys,zs)
    if#(false(),c,l,ys,zs) -> greater#(ys,zs) ->
    greater#(ys,zs) -> ge#(length(ys),length(zs))
    if#(false(),c,l,ys,zs) -> greater#(ys,zs) ->
    greater#(ys,zs) -> length#(ys)
    if#(false(),c,l,ys,zs) -> greater#(ys,zs) ->
    greater#(ys,zs) -> length#(zs)
    if#(false(),c,l,ys,zs) -> smaller#(ys,zs) ->
    smaller#(ys,zs) -> helpc#(ge(length(ys),length(zs)),zs,ys)
    if#(false(),c,l,ys,zs) -> smaller#(ys,zs) ->
    smaller#(ys,zs) -> ge#(length(ys),length(zs))
    if#(false(),c,l,ys,zs) -> smaller#(ys,zs) ->
    smaller#(ys,zs) -> length#(ys)
    if#(false(),c,l,ys,zs) -> smaller#(ys,zs) ->
    smaller#(ys,zs) -> length#(zs)
    ge#(s(x),s(y)) -> ge#(x,y) ->
    ge#(s(x),s(y)) -> ge#(x,y)
    helpa#(c,l,ys,zs) -> if#(ge(c,l),c,l,ys,zs) ->
    if#(false(),c,l,ys,zs) -> helpb#(c,l,greater(ys,zs),smaller(ys,zs))
    helpa#(c,l,ys,zs) -> if#(ge(c,l),c,l,ys,zs) ->
    if#(false(),c,l,ys,zs) -> greater#(ys,zs)
    helpa#(c,l,ys,zs) -> if#(ge(c,l),c,l,ys,zs) ->
    if#(false(),c,l,ys,zs) -> smaller#(ys,zs)
    helpa#(c,l,ys,zs) -> ge#(c,l) -> ge#(s(x),s(y)) -> ge#(x,y)
    plus#(x,s(y)) -> plus#(x,y) -> plus#(x,s(y)) -> plus#(x,y)
    length#(cons(x,y)) -> length#(y) ->
    length#(cons(x,y)) -> length#(y)
    app#(x,y) -> helpa#(0(),plus(length(x),length(y)),x,y) ->
    helpa#(c,l,ys,zs) -> if#(ge(c,l),c,l,ys,zs)
    app#(x,y) -> helpa#(0(),plus(length(x),length(y)),x,y) ->
    helpa#(c,l,ys,zs) -> ge#(c,l)
    app#(x,y) -> plus#(length(x),length(y)) -> plus#(x,s(y)) -> plus#(x,y)
    app#(x,y) -> length#(y) -> length#(cons(x,y)) -> length#(y)
    app#(x,y) -> length#(x) -> length#(cons(x,y)) -> length#(y)
   SCC Processor:
    #sccs: 4
    #rules: 6
    #arcs: 29/441
    DPs:
     plus#(x,s(y)) -> plus#(x,y)
    TRS:
     app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
     plus(x,0()) -> x
     plus(x,s(y)) -> s(plus(x,y))
     length(nil()) -> 0()
     length(cons(x,y)) -> s(length(y))
     helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     if(true(),c,l,ys,zs) -> nil()
     if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
     greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
     smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
     helpc(true(),ys,zs) -> ys
     helpc(false(),ys,zs) -> zs
     helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 1
     problem:
      DPs:
       
      TRS:
       app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
       plus(x,0()) -> x
       plus(x,s(y)) -> s(plus(x,y))
       length(nil()) -> 0()
       length(cons(x,y)) -> s(length(y))
       helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       if(true(),c,l,ys,zs) -> nil()
       if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
       greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
       smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
       helpc(true(),ys,zs) -> ys
       helpc(false(),ys,zs) -> zs
       helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))
     Qed
    
    DPs:
     helpb#(c,l,cons(y,ys),zs) -> helpa#(s(c),l,ys,zs)
     helpa#(c,l,ys,zs) -> if#(ge(c,l),c,l,ys,zs)
     if#(false(),c,l,ys,zs) -> helpb#(c,l,greater(ys,zs),smaller(ys,zs))
    TRS:
     app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
     plus(x,0()) -> x
     plus(x,s(y)) -> s(plus(x,y))
     length(nil()) -> 0()
     length(cons(x,y)) -> s(length(y))
     helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     if(true(),c,l,ys,zs) -> nil()
     if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
     greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
     smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
     helpc(true(),ys,zs) -> ys
     helpc(false(),ys,zs) -> zs
     helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))
    Open
    
    DPs:
     length#(cons(x,y)) -> length#(y)
    TRS:
     app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
     plus(x,0()) -> x
     plus(x,s(y)) -> s(plus(x,y))
     length(nil()) -> 0()
     length(cons(x,y)) -> s(length(y))
     helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     if(true(),c,l,ys,zs) -> nil()
     if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
     greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
     smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
     helpc(true(),ys,zs) -> ys
     helpc(false(),ys,zs) -> zs
     helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))
    Subterm Criterion Processor:
     simple projection:
      pi(length#) = 0
     problem:
      DPs:
       
      TRS:
       app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
       plus(x,0()) -> x
       plus(x,s(y)) -> s(plus(x,y))
       length(nil()) -> 0()
       length(cons(x,y)) -> s(length(y))
       helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       if(true(),c,l,ys,zs) -> nil()
       if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
       greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
       smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
       helpc(true(),ys,zs) -> ys
       helpc(false(),ys,zs) -> zs
       helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))
     Qed
    
    DPs:
     ge#(s(x),s(y)) -> ge#(x,y)
    TRS:
     app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
     plus(x,0()) -> x
     plus(x,s(y)) -> s(plus(x,y))
     length(nil()) -> 0()
     length(cons(x,y)) -> s(length(y))
     helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     if(true(),c,l,ys,zs) -> nil()
     if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
     greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
     smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
     helpc(true(),ys,zs) -> ys
     helpc(false(),ys,zs) -> zs
     helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))
    Subterm Criterion Processor:
     simple projection:
      pi(ge#) = 1
     problem:
      DPs:
       
      TRS:
       app(x,y) -> helpa(0(),plus(length(x),length(y)),x,y)
       plus(x,0()) -> x
       plus(x,s(y)) -> s(plus(x,y))
       length(nil()) -> 0()
       length(cons(x,y)) -> s(length(y))
       helpa(c,l,ys,zs) -> if(ge(c,l),c,l,ys,zs)
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       if(true(),c,l,ys,zs) -> nil()
       if(false(),c,l,ys,zs) -> helpb(c,l,greater(ys,zs),smaller(ys,zs))
       greater(ys,zs) -> helpc(ge(length(ys),length(zs)),ys,zs)
       smaller(ys,zs) -> helpc(ge(length(ys),length(zs)),zs,ys)
       helpc(true(),ys,zs) -> ys
       helpc(false(),ys,zs) -> zs
       helpb(c,l,cons(y,ys),zs) -> cons(y,helpa(s(c),l,ys,zs))
     Qed