MAYBE

Problem:
 leq(0(),x) -> tt()
 leq(s(x),0()) -> ff()
 leq(s(x),s(y)) -> leq(x,y)
 split(nil()) -> app(nil(),nil())
 split(cons(x,nil())) -> app(cons(x,nil()),nil())
 split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
 split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
 merge([](),xs) -> xs
 merge(xs,[]()) -> xs
 merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
 ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
 ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
 mergesort(xs) -> mergesort1(split(xs))
 mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))

Proof:
 DP Processor:
  DPs:
   leq#(s(x),s(y)) -> leq#(x,y)
   split#(cons(x,cons(y,xs))) -> split#(xs)
   split#(cons(x,cons(y,xs))) -> split1#(x,y,split(xs))
   merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
   merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
   ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
   ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys)
   mergesort#(xs) -> split#(xs)
   mergesort#(xs) -> mergesort1#(split(xs))
   mergesort1#(app(xs,ys)) -> mergesort#(ys)
   mergesort1#(app(xs,ys)) -> mergesort#(xs)
   mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys))
  TRS:
   leq(0(),x) -> tt()
   leq(s(x),0()) -> ff()
   leq(s(x),s(y)) -> leq(x,y)
   split(nil()) -> app(nil(),nil())
   split(cons(x,nil())) -> app(cons(x,nil()),nil())
   split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
   split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
   merge([](),xs) -> xs
   merge(xs,[]()) -> xs
   merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
   ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
   ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
   mergesort(xs) -> mergesort1(split(xs))
   mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
  TDG Processor:
   DPs:
    leq#(s(x),s(y)) -> leq#(x,y)
    split#(cons(x,cons(y,xs))) -> split#(xs)
    split#(cons(x,cons(y,xs))) -> split1#(x,y,split(xs))
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
    ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
    ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys)
    mergesort#(xs) -> split#(xs)
    mergesort#(xs) -> mergesort1#(split(xs))
    mergesort1#(app(xs,ys)) -> mergesort#(ys)
    mergesort1#(app(xs,ys)) -> mergesort#(xs)
    mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys))
   TRS:
    leq(0(),x) -> tt()
    leq(s(x),0()) -> ff()
    leq(s(x),s(y)) -> leq(x,y)
    split(nil()) -> app(nil(),nil())
    split(cons(x,nil())) -> app(cons(x,nil()),nil())
    split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
    split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
    merge([](),xs) -> xs
    merge(xs,[]()) -> xs
    merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
    ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
    ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
    mergesort(xs) -> mergesort1(split(xs))
    mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
   graph:
    mergesort1#(app(xs,ys)) -> mergesort#(ys) ->
    mergesort#(xs) -> mergesort1#(split(xs))
    mergesort1#(app(xs,ys)) -> mergesort#(ys) ->
    mergesort#(xs) -> split#(xs)
    mergesort1#(app(xs,ys)) -> mergesort#(xs) ->
    mergesort#(xs) -> mergesort1#(split(xs))
    mergesort1#(app(xs,ys)) -> mergesort#(xs) ->
    mergesort#(xs) -> split#(xs)
    mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys)) ->
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
    mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys)) ->
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
    mergesort#(xs) -> mergesort1#(split(xs)) ->
    mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys))
    mergesort#(xs) -> mergesort1#(split(xs)) ->
    mergesort1#(app(xs,ys)) -> mergesort#(xs)
    mergesort#(xs) -> mergesort1#(split(xs)) ->
    mergesort1#(app(xs,ys)) -> mergesort#(ys)
    mergesort#(xs) -> split#(xs) ->
    split#(cons(x,cons(y,xs))) -> split1#(x,y,split(xs))
    mergesort#(xs) -> split#(xs) ->
    split#(cons(x,cons(y,xs))) -> split#(xs)
    ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys) ->
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
    ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys) ->
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
    ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys)) ->
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
    ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys)) ->
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys) ->
    ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys)
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys) ->
    ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y) ->
    leq#(s(x),s(y)) -> leq#(x,y)
    split#(cons(x,cons(y,xs))) -> split#(xs) ->
    split#(cons(x,cons(y,xs))) -> split1#(x,y,split(xs))
    split#(cons(x,cons(y,xs))) -> split#(xs) ->
    split#(cons(x,cons(y,xs))) -> split#(xs)
    leq#(s(x),s(y)) -> leq#(x,y) -> leq#(s(x),s(y)) -> leq#(x,y)
   SCC Processor:
    #sccs: 4
    #rules: 8
    #arcs: 21/144
    DPs:
     mergesort1#(app(xs,ys)) -> mergesort#(ys)
     mergesort#(xs) -> mergesort1#(split(xs))
     mergesort1#(app(xs,ys)) -> mergesort#(xs)
    TRS:
     leq(0(),x) -> tt()
     leq(s(x),0()) -> ff()
     leq(s(x),s(y)) -> leq(x,y)
     split(nil()) -> app(nil(),nil())
     split(cons(x,nil())) -> app(cons(x,nil()),nil())
     split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
     split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
     merge([](),xs) -> xs
     merge(xs,[]()) -> xs
     merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
     ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
     ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
     mergesort(xs) -> mergesort1(split(xs))
     mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
    Open
    
    DPs:
     merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
     ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
     ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys)
    TRS:
     leq(0(),x) -> tt()
     leq(s(x),0()) -> ff()
     leq(s(x),s(y)) -> leq(x,y)
     split(nil()) -> app(nil(),nil())
     split(cons(x,nil())) -> app(cons(x,nil()),nil())
     split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
     split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
     merge([](),xs) -> xs
     merge(xs,[]()) -> xs
     merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
     ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
     ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
     mergesort(xs) -> mergesort1(split(xs))
     mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [ifmerge#](x0, x1, x2, x3, x4) = x4 + 1,
      
      [merge#](x0, x1) = x1,
      
      [mergesort1](x0) = 0,
      
      [mergesort](x0) = 0,
      
      [ifmerge](x0, x1, x2, x3, x4) = x3 + x4 + 2,
      
      [merge](x0, x1) = x0 + x1,
      
      [[]] = 1,
      
      [split1](x0, x1, x2) = 0,
      
      [cons](x0, x1) = x1 + 1,
      
      [app](x0, x1) = 0,
      
      [split](x0) = 0,
      
      [nil] = 2,
      
      [ff] = 0,
      
      [s](x0) = 0,
      
      [tt] = 0,
      
      [leq](x0, x1) = 0,
      
      [0] = 0
     orientation:
      merge#(cons(x,xs),cons(y,ys)) = ys + 1 >= ys + 1 = ifmerge#(leq(x,y),x,y,xs,ys)
      
      ifmerge#(tt(),x,y,xs,ys) = ys + 1 >= ys + 1 = merge#(xs,cons(y,ys))
      
      ifmerge#(ff(),x,y,xs,ys) = ys + 1 >= ys = merge#(cons(x,xs),ys)
      
      leq(0(),x) = 0 >= 0 = tt()
      
      leq(s(x),0()) = 0 >= 0 = ff()
      
      leq(s(x),s(y)) = 0 >= 0 = leq(x,y)
      
      split(nil()) = 0 >= 0 = app(nil(),nil())
      
      split(cons(x,nil())) = 0 >= 0 = app(cons(x,nil()),nil())
      
      split(cons(x,cons(y,xs))) = 0 >= 0 = split1(x,y,split(xs))
      
      split1(x,y,app(xs,ys)) = 0 >= 0 = app(cons(x,xs),cons(y,ys))
      
      merge([](),xs) = xs + 1 >= xs = xs
      
      merge(xs,[]()) = xs + 1 >= xs = xs
      
      merge(cons(x,xs),cons(y,ys)) = xs + ys + 2 >= xs + ys + 2 = ifmerge(leq(x,y),x,y,xs,ys)
      
      ifmerge(tt(),x,y,xs,ys) = xs + ys + 2 >= xs + ys + 2 = cons(x,merge(xs,cons(y,ys)))
      
      ifmerge(ff(),x,y,xs,ys) = xs + ys + 2 >= xs + ys + 2 = cons(y,merge(cons(x,xs),ys))
      
      mergesort(xs) = 0 >= 0 = mergesort1(split(xs))
      
      mergesort1(app(xs,ys)) = 0 >= 0 = merge(mergesort(xs),mergesort(ys))
     problem:
      DPs:
       merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
       ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
      TRS:
       leq(0(),x) -> tt()
       leq(s(x),0()) -> ff()
       leq(s(x),s(y)) -> leq(x,y)
       split(nil()) -> app(nil(),nil())
       split(cons(x,nil())) -> app(cons(x,nil()),nil())
       split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
       split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
       merge([](),xs) -> xs
       merge(xs,[]()) -> xs
       merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
       ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
       ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
       mergesort(xs) -> mergesort1(split(xs))
       mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
     Size-Change Termination Processor:
      DPs:
       
      TRS:
       leq(0(),x) -> tt()
       leq(s(x),0()) -> ff()
       leq(s(x),s(y)) -> leq(x,y)
       split(nil()) -> app(nil(),nil())
       split(cons(x,nil())) -> app(cons(x,nil()),nil())
       split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
       split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
       merge([](),xs) -> xs
       merge(xs,[]()) -> xs
       merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
       ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
       ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
       mergesort(xs) -> mergesort1(split(xs))
       mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
      The DP: merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys) has the edges:
        0 >   3
        0 >   1
        1 >   4
        1 >   2
      The DP: ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys)) has the edges:
        3 >=  0
      Qed
    
    DPs:
     leq#(s(x),s(y)) -> leq#(x,y)
    TRS:
     leq(0(),x) -> tt()
     leq(s(x),0()) -> ff()
     leq(s(x),s(y)) -> leq(x,y)
     split(nil()) -> app(nil(),nil())
     split(cons(x,nil())) -> app(cons(x,nil()),nil())
     split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
     split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
     merge([](),xs) -> xs
     merge(xs,[]()) -> xs
     merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
     ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
     ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
     mergesort(xs) -> mergesort1(split(xs))
     mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
    Subterm Criterion Processor:
     simple projection:
      pi(leq#) = 1
     problem:
      DPs:
       
      TRS:
       leq(0(),x) -> tt()
       leq(s(x),0()) -> ff()
       leq(s(x),s(y)) -> leq(x,y)
       split(nil()) -> app(nil(),nil())
       split(cons(x,nil())) -> app(cons(x,nil()),nil())
       split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
       split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
       merge([](),xs) -> xs
       merge(xs,[]()) -> xs
       merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
       ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
       ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
       mergesort(xs) -> mergesort1(split(xs))
       mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
     Qed
    
    DPs:
     split#(cons(x,cons(y,xs))) -> split#(xs)
    TRS:
     leq(0(),x) -> tt()
     leq(s(x),0()) -> ff()
     leq(s(x),s(y)) -> leq(x,y)
     split(nil()) -> app(nil(),nil())
     split(cons(x,nil())) -> app(cons(x,nil()),nil())
     split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
     split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
     merge([](),xs) -> xs
     merge(xs,[]()) -> xs
     merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
     ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
     ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
     mergesort(xs) -> mergesort1(split(xs))
     mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
    Subterm Criterion Processor:
     simple projection:
      pi(split#) = 0
     problem:
      DPs:
       
      TRS:
       leq(0(),x) -> tt()
       leq(s(x),0()) -> ff()
       leq(s(x),s(y)) -> leq(x,y)
       split(nil()) -> app(nil(),nil())
       split(cons(x,nil())) -> app(cons(x,nil()),nil())
       split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
       split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
       merge([](),xs) -> xs
       merge(xs,[]()) -> xs
       merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
       ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
       ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
       mergesort(xs) -> mergesort1(split(xs))
       mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
     Qed