MAYBE

Problem:
 null(nil()) -> true()
 null(add(n,x)) -> false()
 tail(add(n,x)) -> x
 tail(nil()) -> nil()
 head(add(n,x)) -> n
 app(nil(),y) -> y
 app(add(n,x),y) -> add(n,app(x,y))
 reverse(nil()) -> nil()
 reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
 shuffle(x) -> shuff(x,nil())
 shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
 if(true(),x,y,z) -> y
 if(false(),x,y,z) -> shuff(reverse(tail(x)),z)

Proof:
 DP Processor:
  DPs:
   app#(add(n,x),y) -> app#(x,y)
   reverse#(add(n,x)) -> reverse#(x)
   reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
   shuffle#(x) -> shuff#(x,nil())
   shuff#(x,y) -> head#(x)
   shuff#(x,y) -> app#(y,add(head(x),nil()))
   shuff#(x,y) -> null#(x)
   shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
   if#(false(),x,y,z) -> tail#(x)
   if#(false(),x,y,z) -> reverse#(tail(x))
   if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
  TRS:
   null(nil()) -> true()
   null(add(n,x)) -> false()
   tail(add(n,x)) -> x
   tail(nil()) -> nil()
   head(add(n,x)) -> n
   app(nil(),y) -> y
   app(add(n,x),y) -> add(n,app(x,y))
   reverse(nil()) -> nil()
   reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
   shuffle(x) -> shuff(x,nil())
   shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
   if(true(),x,y,z) -> y
   if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
  TDG Processor:
   DPs:
    app#(add(n,x),y) -> app#(x,y)
    reverse#(add(n,x)) -> reverse#(x)
    reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
    shuffle#(x) -> shuff#(x,nil())
    shuff#(x,y) -> head#(x)
    shuff#(x,y) -> app#(y,add(head(x),nil()))
    shuff#(x,y) -> null#(x)
    shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
    if#(false(),x,y,z) -> tail#(x)
    if#(false(),x,y,z) -> reverse#(tail(x))
    if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
   TRS:
    null(nil()) -> true()
    null(add(n,x)) -> false()
    tail(add(n,x)) -> x
    tail(nil()) -> nil()
    head(add(n,x)) -> n
    app(nil(),y) -> y
    app(add(n,x),y) -> add(n,app(x,y))
    reverse(nil()) -> nil()
    reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
    shuffle(x) -> shuff(x,nil())
    shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
    if(true(),x,y,z) -> y
    if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
   graph:
    if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z) ->
    shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
    if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z) ->
    shuff#(x,y) -> null#(x)
    if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z) ->
    shuff#(x,y) -> app#(y,add(head(x),nil()))
    if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z) ->
    shuff#(x,y) -> head#(x)
    if#(false(),x,y,z) -> reverse#(tail(x)) ->
    reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
    if#(false(),x,y,z) -> reverse#(tail(x)) ->
    reverse#(add(n,x)) -> reverse#(x)
    shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil()))) ->
    if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
    shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil()))) ->
    if#(false(),x,y,z) -> reverse#(tail(x))
    shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil()))) ->
    if#(false(),x,y,z) -> tail#(x)
    shuff#(x,y) -> app#(y,add(head(x),nil())) ->
    app#(add(n,x),y) -> app#(x,y)
    shuffle#(x) -> shuff#(x,nil()) ->
    shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
    shuffle#(x) -> shuff#(x,nil()) -> shuff#(x,y) -> null#(x)
    shuffle#(x) -> shuff#(x,nil()) ->
    shuff#(x,y) -> app#(y,add(head(x),nil()))
    shuffle#(x) -> shuff#(x,nil()) -> shuff#(x,y) -> head#(x)
    reverse#(add(n,x)) -> reverse#(x) ->
    reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
    reverse#(add(n,x)) -> reverse#(x) ->
    reverse#(add(n,x)) -> reverse#(x)
    reverse#(add(n,x)) -> app#(reverse(x),add(n,nil())) ->
    app#(add(n,x),y) -> app#(x,y)
    app#(add(n,x),y) -> app#(x,y) -> app#(add(n,x),y) -> app#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 18/121
    DPs:
     if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
     shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
    TRS:
     null(nil()) -> true()
     null(add(n,x)) -> false()
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
     head(add(n,x)) -> n
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(x) -> shuff(x,nil())
     shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
     if(true(),x,y,z) -> y
     if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
    Open
    
    DPs:
     reverse#(add(n,x)) -> reverse#(x)
    TRS:
     null(nil()) -> true()
     null(add(n,x)) -> false()
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
     head(add(n,x)) -> n
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(x) -> shuff(x,nil())
     shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
     if(true(),x,y,z) -> y
     if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
    Subterm Criterion Processor:
     simple projection:
      pi(reverse#) = 0
     problem:
      DPs:
       
      TRS:
       null(nil()) -> true()
       null(add(n,x)) -> false()
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       head(add(n,x)) -> n
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(x) -> shuff(x,nil())
       shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
       if(true(),x,y,z) -> y
       if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
     Qed
    
    DPs:
     app#(add(n,x),y) -> app#(x,y)
    TRS:
     null(nil()) -> true()
     null(add(n,x)) -> false()
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
     head(add(n,x)) -> n
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(x) -> shuff(x,nil())
     shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
     if(true(),x,y,z) -> y
     if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       null(nil()) -> true()
       null(add(n,x)) -> false()
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       head(add(n,x)) -> n
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(x) -> shuff(x,nil())
       shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
       if(true(),x,y,z) -> y
       if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
     Qed