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,ys,zs)
 take(0(),cons(x,xs()),ys) -> x
 take(0(),nil(),cons(y,ys)) -> y
 take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
 take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
 helpb(c,l,ys,zs) -> cons(take(c,ys,zs),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) -> helpb#(c,l,ys,zs)
   take#(s(c),cons(x,xs()),ys) -> take#(c,xs(),ys)
   take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys)
   helpb#(c,l,ys,zs) -> helpa#(s(c),l,ys,zs)
   helpb#(c,l,ys,zs) -> take#(c,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,ys,zs)
   take(0(),cons(x,xs()),ys) -> x
   take(0(),nil(),cons(y,ys)) -> y
   take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
   take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
   helpb(c,l,ys,zs) -> cons(take(c,ys,zs),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) -> helpb#(c,l,ys,zs)
    take#(s(c),cons(x,xs()),ys) -> take#(c,xs(),ys)
    take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys)
    helpb#(c,l,ys,zs) -> helpa#(s(c),l,ys,zs)
    helpb#(c,l,ys,zs) -> take#(c,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,ys,zs)
    take(0(),cons(x,xs()),ys) -> x
    take(0(),nil(),cons(y,ys)) -> y
    take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
    take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
    helpb(c,l,ys,zs) -> cons(take(c,ys,zs),helpa(s(c),l,ys,zs))
   graph:
    take#(s(c),cons(x,xs()),ys) -> take#(c,xs(),ys) ->
    take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys)
    take#(s(c),cons(x,xs()),ys) -> take#(c,xs(),ys) ->
    take#(s(c),cons(x,xs()),ys) -> take#(c,xs(),ys)
    take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys) ->
    take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys)
    take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys) ->
    take#(s(c),cons(x,xs()),ys) -> take#(c,xs(),ys)
    helpb#(c,l,ys,zs) -> take#(c,ys,zs) ->
    take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys)
    helpb#(c,l,ys,zs) -> take#(c,ys,zs) ->
    take#(s(c),cons(x,xs()),ys) -> take#(c,xs(),ys)
    helpb#(c,l,ys,zs) -> helpa#(s(c),l,ys,zs) ->
    helpa#(c,l,ys,zs) -> if#(ge(c,l),c,l,ys,zs)
    helpb#(c,l,ys,zs) -> helpa#(s(c),l,ys,zs) ->
    helpa#(c,l,ys,zs) -> ge#(c,l)
    if#(false(),c,l,ys,zs) -> helpb#(c,l,ys,zs) ->
    helpb#(c,l,ys,zs) -> take#(c,ys,zs)
    if#(false(),c,l,ys,zs) -> helpb#(c,l,ys,zs) ->
    helpb#(c,l,ys,zs) -> helpa#(s(c),l,ys,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,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: 5
    #rules: 8
    #arcs: 20/196
    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,ys,zs)
     take(0(),cons(x,xs()),ys) -> x
     take(0(),nil(),cons(y,ys)) -> y
     take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
     take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
     helpb(c,l,ys,zs) -> cons(take(c,ys,zs),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,ys,zs)
       take(0(),cons(x,xs()),ys) -> x
       take(0(),nil(),cons(y,ys)) -> y
       take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
       take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
       helpb(c,l,ys,zs) -> cons(take(c,ys,zs),helpa(s(c),l,ys,zs))
     Qed
    
    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,ys,zs)
     take(0(),cons(x,xs()),ys) -> x
     take(0(),nil(),cons(y,ys)) -> y
     take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
     take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
     helpb(c,l,ys,zs) -> cons(take(c,ys,zs),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,ys,zs)
       take(0(),cons(x,xs()),ys) -> x
       take(0(),nil(),cons(y,ys)) -> y
       take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
       take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
       helpb(c,l,ys,zs) -> cons(take(c,ys,zs),helpa(s(c),l,ys,zs))
     Qed
    
    DPs:
     helpb#(c,l,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,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,ys,zs)
     take(0(),cons(x,xs()),ys) -> x
     take(0(),nil(),cons(y,ys)) -> y
     take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
     take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
     helpb(c,l,ys,zs) -> cons(take(c,ys,zs),helpa(s(c),l,ys,zs))
    Open
    
    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,ys,zs)
     take(0(),cons(x,xs()),ys) -> x
     take(0(),nil(),cons(y,ys)) -> y
     take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
     take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
     helpb(c,l,ys,zs) -> cons(take(c,ys,zs),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,ys,zs)
       take(0(),cons(x,xs()),ys) -> x
       take(0(),nil(),cons(y,ys)) -> y
       take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
       take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
       helpb(c,l,ys,zs) -> cons(take(c,ys,zs),helpa(s(c),l,ys,zs))
     Qed
    
    DPs:
     take#(s(c),cons(x,xs()),ys) -> take#(c,xs(),ys)
     take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys)
    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,ys,zs)
     take(0(),cons(x,xs()),ys) -> x
     take(0(),nil(),cons(y,ys)) -> y
     take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
     take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
     helpb(c,l,ys,zs) -> cons(take(c,ys,zs),helpa(s(c),l,ys,zs))
    Subterm Criterion Processor:
     simple projection:
      pi(take#) = 2
     problem:
      DPs:
       take#(s(c),cons(x,xs()),ys) -> take#(c,xs(),ys)
      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,ys,zs)
       take(0(),cons(x,xs()),ys) -> x
       take(0(),nil(),cons(y,ys)) -> y
       take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
       take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
       helpb(c,l,ys,zs) -> cons(take(c,ys,zs),helpa(s(c),l,ys,zs))
     Subterm Criterion Processor:
      simple projection:
       pi(take#) = 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,ys,zs)
        take(0(),cons(x,xs()),ys) -> x
        take(0(),nil(),cons(y,ys)) -> y
        take(s(c),cons(x,xs()),ys) -> take(c,xs(),ys)
        take(s(c),nil(),cons(y,ys)) -> take(c,nil(),ys)
        helpb(c,l,ys,zs) -> cons(take(c,ys,zs),helpa(s(c),l,ys,zs))
      Qed