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))
  Usable Rule 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:
    f23(x,y) -> x
    f23(x,y) -> y
    length(nil()) -> 0()
    length(cons(x,y)) -> s(length(y))
    plus(x,0()) -> x
    plus(x,s(y)) -> s(plus(x,y))
    ge(x,0()) -> true()
    ge(0(),s(x)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
   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:
     f23(x,y) -> x
     f23(x,y) -> y
     length(nil()) -> 0()
     length(cons(x,y)) -> s(length(y))
     plus(x,0()) -> x
     plus(x,s(y)) -> s(plus(x,y))
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
    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)
    EDG 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:
      f23(x,y) -> x
      f23(x,y) -> y
      length(nil()) -> 0()
      length(cons(x,y)) -> s(length(y))
      plus(x,0()) -> x
      plus(x,s(y)) -> s(plus(x,y))
      ge(x,0()) -> true()
      ge(0(),s(x)) -> false()
      ge(s(x),s(y)) -> ge(x,y)
     graph:
      take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys) ->
      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) -> take#(c,ys,zs) ->
      take#(s(c),nil(),cons(y,ys)) -> take#(c,nil(),ys)
      helpb#(c,l,ys,zs) -> helpa#(s(c),l,ys,zs) ->
      helpa#(c,l,ys,zs) -> ge#(c,l)
      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) ->
      helpb#(c,l,ys,zs) -> helpa#(s(c),l,ys,zs)
      if#(false(),c,l,ys,zs) -> helpb#(c,l,ys,zs) ->
      helpb#(c,l,ys,zs) -> take#(c,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) -> ge#(c,l)
      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) -> 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)
     Restore Modifier:
      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))
      SCC Processor:
       #sccs: 5
       #rules: 7
       #arcs: 17/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))
       Open
       
       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))
       Open
       
       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))
       Open
       
       DPs:
        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))
       Open