MAYBE

Problem:
 minus(x,0()) -> x
 minus(s(x),s(y)) -> minus(x,y)
 quot(0(),s(y)) -> 0()
 quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
 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(nil()) -> nil()
 shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
 concat(leaf(),y) -> y
 concat(cons(u,v),y) -> cons(u,concat(v,y))
 less_leaves(x,leaf()) -> false()
 less_leaves(leaf(),cons(w,z)) -> true()
 less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))

Proof:
 DP Processor:
  DPs:
   minus#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
   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#(add(n,x)) -> reverse#(x)
   shuffle#(add(n,x)) -> shuffle#(reverse(x))
   concat#(cons(u,v),y) -> concat#(v,y)
   less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
   less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
   less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
  TRS:
   minus(x,0()) -> x
   minus(s(x),s(y)) -> minus(x,y)
   quot(0(),s(y)) -> 0()
   quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
   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(nil()) -> nil()
   shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
   concat(leaf(),y) -> y
   concat(cons(u,v),y) -> cons(u,concat(v,y))
   less_leaves(x,leaf()) -> false()
   less_leaves(leaf(),cons(w,z)) -> true()
   less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
  Usable Rule Processor:
   DPs:
    minus#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    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#(add(n,x)) -> reverse#(x)
    shuffle#(add(n,x)) -> shuffle#(reverse(x))
    concat#(cons(u,v),y) -> concat#(v,y)
    less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
    less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
    less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
   TRS:
    f22(x,y) -> x
    f22(x,y) -> y
    minus(x,0()) -> x
    minus(s(x),s(y)) -> minus(x,y)
    reverse(nil()) -> nil()
    reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
    app(nil(),y) -> y
    app(add(n,x),y) -> add(n,app(x,y))
    concat(leaf(),y) -> y
    concat(cons(u,v),y) -> cons(u,concat(v,y))
   EDG Processor:
    DPs:
     minus#(s(x),s(y)) -> minus#(x,y)
     quot#(s(x),s(y)) -> minus#(x,y)
     quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
     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#(add(n,x)) -> reverse#(x)
     shuffle#(add(n,x)) -> shuffle#(reverse(x))
     concat#(cons(u,v),y) -> concat#(v,y)
     less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
     less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
     less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
    TRS:
     f22(x,y) -> x
     f22(x,y) -> y
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     concat(leaf(),y) -> y
     concat(cons(u,v),y) -> cons(u,concat(v,y))
    graph:
     less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)) ->
     less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
     less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)) ->
     less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
     less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)) ->
     less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
     less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z) ->
     concat#(cons(u,v),y) -> concat#(v,y)
     less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v) ->
     concat#(cons(u,v),y) -> concat#(v,y)
     concat#(cons(u,v),y) -> concat#(v,y) ->
     concat#(cons(u,v),y) -> concat#(v,y)
     shuffle#(add(n,x)) -> shuffle#(reverse(x)) ->
     shuffle#(add(n,x)) -> reverse#(x)
     shuffle#(add(n,x)) -> shuffle#(reverse(x)) ->
     shuffle#(add(n,x)) -> shuffle#(reverse(x))
     shuffle#(add(n,x)) -> reverse#(x) ->
     reverse#(add(n,x)) -> reverse#(x)
     shuffle#(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)) -> reverse#(x) ->
     reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
     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)
     quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) ->
     quot#(s(x),s(y)) -> minus#(x,y)
     quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) ->
     quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
     quot#(s(x),s(y)) -> minus#(x,y) ->
     minus#(s(x),s(y)) -> minus#(x,y)
     minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y)
    Restore Modifier:
     DPs:
      minus#(s(x),s(y)) -> minus#(x,y)
      quot#(s(x),s(y)) -> minus#(x,y)
      quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
      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#(add(n,x)) -> reverse#(x)
      shuffle#(add(n,x)) -> shuffle#(reverse(x))
      concat#(cons(u,v),y) -> concat#(v,y)
      less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
      less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
      less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
     TRS:
      minus(x,0()) -> x
      minus(s(x),s(y)) -> minus(x,y)
      quot(0(),s(y)) -> 0()
      quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
      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(nil()) -> nil()
      shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
      concat(leaf(),y) -> y
      concat(cons(u,v),y) -> cons(u,concat(v,y))
      less_leaves(x,leaf()) -> false()
      less_leaves(leaf(),cons(w,z)) -> true()
      less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
     SCC Processor:
      #sccs: 7
      #rules: 7
      #arcs: 18/144
      DPs:
       quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       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(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
      Open
      
      DPs:
       minus#(s(x),s(y)) -> minus#(x,y)
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       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(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
      Open
      
      DPs:
       shuffle#(add(n,x)) -> shuffle#(reverse(x))
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       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(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
      Open
      
      DPs:
       reverse#(add(n,x)) -> reverse#(x)
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       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(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
      Open
      
      DPs:
       app#(add(n,x),y) -> app#(x,y)
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       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(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
      Open
      
      DPs:
       less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       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(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
      Open
      
      DPs:
       concat#(cons(u,v),y) -> concat#(v,y)
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       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(nil()) -> nil()
       shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       concat(leaf(),y) -> y
       concat(cons(u,v),y) -> cons(u,concat(v,y))
       less_leaves(x,leaf()) -> false()
       less_leaves(leaf(),cons(w,z)) -> true()
       less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
      Open