MAYBE

Problem:
 intlist(nil()) -> nil()
 intlist(cons(x,y)) -> cons(s(x),intlist(y))
 int(0(),0()) -> cons(0(),nil())
 int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
 int(s(x),0()) -> nil()
 int(s(x),s(y)) -> intlist(int(x,y))

Proof:
 DP Processor:
  DPs:
   intlist#(cons(x,y)) -> intlist#(y)
   int#(0(),s(y)) -> int#(s(0()),s(y))
   int#(s(x),s(y)) -> int#(x,y)
   int#(s(x),s(y)) -> intlist#(int(x,y))
  TRS:
   intlist(nil()) -> nil()
   intlist(cons(x,y)) -> cons(s(x),intlist(y))
   int(0(),0()) -> cons(0(),nil())
   int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
   int(s(x),0()) -> nil()
   int(s(x),s(y)) -> intlist(int(x,y))
  TDG Processor:
   DPs:
    intlist#(cons(x,y)) -> intlist#(y)
    int#(0(),s(y)) -> int#(s(0()),s(y))
    int#(s(x),s(y)) -> int#(x,y)
    int#(s(x),s(y)) -> intlist#(int(x,y))
   TRS:
    intlist(nil()) -> nil()
    intlist(cons(x,y)) -> cons(s(x),intlist(y))
    int(0(),0()) -> cons(0(),nil())
    int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
    int(s(x),0()) -> nil()
    int(s(x),s(y)) -> intlist(int(x,y))
   graph:
    int#(0(),s(y)) -> int#(s(0()),s(y)) ->
    int#(s(x),s(y)) -> intlist#(int(x,y))
    int#(0(),s(y)) -> int#(s(0()),s(y)) ->
    int#(s(x),s(y)) -> int#(x,y)
    int#(0(),s(y)) -> int#(s(0()),s(y)) ->
    int#(0(),s(y)) -> int#(s(0()),s(y))
    int#(s(x),s(y)) -> int#(x,y) ->
    int#(s(x),s(y)) -> intlist#(int(x,y))
    int#(s(x),s(y)) -> int#(x,y) -> int#(s(x),s(y)) -> int#(x,y)
    int#(s(x),s(y)) -> int#(x,y) ->
    int#(0(),s(y)) -> int#(s(0()),s(y))
    int#(s(x),s(y)) -> intlist#(int(x,y)) ->
    intlist#(cons(x,y)) -> intlist#(y)
    intlist#(cons(x,y)) -> intlist#(y) -> intlist#(cons(x,y)) -> intlist#(y)
   EDG Processor:
    DPs:
     intlist#(cons(x,y)) -> intlist#(y)
     int#(0(),s(y)) -> int#(s(0()),s(y))
     int#(s(x),s(y)) -> int#(x,y)
     int#(s(x),s(y)) -> intlist#(int(x,y))
    TRS:
     intlist(nil()) -> nil()
     intlist(cons(x,y)) -> cons(s(x),intlist(y))
     int(0(),0()) -> cons(0(),nil())
     int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
     int(s(x),0()) -> nil()
     int(s(x),s(y)) -> intlist(int(x,y))
    graph:
     int#(0(),s(y)) -> int#(s(0()),s(y)) ->
     int#(s(x),s(y)) -> int#(x,y)
     int#(0(),s(y)) -> int#(s(0()),s(y)) ->
     int#(s(x),s(y)) -> intlist#(int(x,y))
     int#(s(x),s(y)) -> int#(x,y) ->
     int#(0(),s(y)) -> int#(s(0()),s(y))
     int#(s(x),s(y)) -> int#(x,y) -> int#(s(x),s(y)) -> int#(x,y)
     int#(s(x),s(y)) -> int#(x,y) ->
     int#(s(x),s(y)) -> intlist#(int(x,y))
     int#(s(x),s(y)) -> intlist#(int(x,y)) ->
     intlist#(cons(x,y)) -> intlist#(y)
     intlist#(cons(x,y)) -> intlist#(y) -> intlist#(cons(x,y)) -> intlist#(y)
    SCC Processor:
     #sccs: 2
     #rules: 3
     #arcs: 7/16
     DPs:
      int#(0(),s(y)) -> int#(s(0()),s(y))
      int#(s(x),s(y)) -> int#(x,y)
     TRS:
      intlist(nil()) -> nil()
      intlist(cons(x,y)) -> cons(s(x),intlist(y))
      int(0(),0()) -> cons(0(),nil())
      int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
      int(s(x),0()) -> nil()
      int(s(x),s(y)) -> intlist(int(x,y))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [int#](x0, x1) = x1 + 1,
       
       [int](x0, x1) = 0,
       
       [0] = 1,
       
       [s](x0) = x0 + 1,
       
       [cons](x0, x1) = 0,
       
       [intlist](x0) = 0,
       
       [nil] = 0
      orientation:
       int#(0(),s(y)) = y + 2 >= y + 2 = int#(s(0()),s(y))
       
       int#(s(x),s(y)) = y + 2 >= y + 1 = int#(x,y)
       
       intlist(nil()) = 0 >= 0 = nil()
       
       intlist(cons(x,y)) = 0 >= 0 = cons(s(x),intlist(y))
       
       int(0(),0()) = 0 >= 0 = cons(0(),nil())
       
       int(0(),s(y)) = 0 >= 0 = cons(0(),int(s(0()),s(y)))
       
       int(s(x),0()) = 0 >= 0 = nil()
       
       int(s(x),s(y)) = 0 >= 0 = intlist(int(x,y))
      problem:
       DPs:
        int#(0(),s(y)) -> int#(s(0()),s(y))
       TRS:
        intlist(nil()) -> nil()
        intlist(cons(x,y)) -> cons(s(x),intlist(y))
        int(0(),0()) -> cons(0(),nil())
        int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
        int(s(x),0()) -> nil()
        int(s(x),s(y)) -> intlist(int(x,y))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [int#](x0, x1) = x0,
        
        [int](x0, x1) = x0 + 1,
        
        [0] = 1,
        
        [s](x0) = 0,
        
        [cons](x0, x1) = x0 + 1,
        
        [intlist](x0) = 1,
        
        [nil] = 1
       orientation:
        int#(0(),s(y)) = 1 >= 0 = int#(s(0()),s(y))
        
        intlist(nil()) = 1 >= 1 = nil()
        
        intlist(cons(x,y)) = 1 >= 1 = cons(s(x),intlist(y))
        
        int(0(),0()) = 2 >= 2 = cons(0(),nil())
        
        int(0(),s(y)) = 2 >= 2 = cons(0(),int(s(0()),s(y)))
        
        int(s(x),0()) = 1 >= 1 = nil()
        
        int(s(x),s(y)) = 1 >= 1 = intlist(int(x,y))
       problem:
        DPs:
         
        TRS:
         intlist(nil()) -> nil()
         intlist(cons(x,y)) -> cons(s(x),intlist(y))
         int(0(),0()) -> cons(0(),nil())
         int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
         int(s(x),0()) -> nil()
         int(s(x),s(y)) -> intlist(int(x,y))
       Qed
     
     DPs:
      intlist#(cons(x,y)) -> intlist#(y)
     TRS:
      intlist(nil()) -> nil()
      intlist(cons(x,y)) -> cons(s(x),intlist(y))
      int(0(),0()) -> cons(0(),nil())
      int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
      int(s(x),0()) -> nil()
      int(s(x),s(y)) -> intlist(int(x,y))
     Open