MAYBE

Problem:
 incr(nil()) -> nil()
 incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
 adx(nil()) -> nil()
 adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
 nats() -> adx(zeros())
 zeros() -> cons(0(),n__zeros())
 head(cons(X,L)) -> X
 tail(cons(X,L)) -> activate(L)
 incr(X) -> n__incr(X)
 adx(X) -> n__adx(X)
 zeros() -> n__zeros()
 activate(n__incr(X)) -> incr(activate(X))
 activate(n__adx(X)) -> adx(activate(X))
 activate(n__zeros()) -> zeros()
 activate(X) -> X

Proof:
 RT Transformation Processor:
  strict:
   incr(nil()) -> nil()
   incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
   adx(nil()) -> nil()
   adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
   nats() -> adx(zeros())
   zeros() -> cons(0(),n__zeros())
   head(cons(X,L)) -> X
   tail(cons(X,L)) -> activate(L)
   incr(X) -> n__incr(X)
   adx(X) -> n__adx(X)
   zeros() -> n__zeros()
   activate(n__incr(X)) -> incr(activate(X))
   activate(n__adx(X)) -> adx(activate(X))
   activate(n__zeros()) -> zeros()
   activate(X) -> X
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [tail](x0) = x0 + 22,
    
    [head](x0) = x0 + 16,
    
    [n__zeros] = 0,
    
    [0] = 4,
    
    [zeros] = 1,
    
    [nats] = 0,
    
    [n__adx](x0) = x0,
    
    [adx](x0) = x0 + 5,
    
    [n__incr](x0) = x0 + 25,
    
    [activate](x0) = x0 + 8,
    
    [s](x0) = x0 + 6,
    
    [cons](x0, x1) = x0 + x1 + 10,
    
    [incr](x0) = x0,
    
    [nil] = 1
   orientation:
    incr(nil()) = 1 >= 1 = nil()
    
    incr(cons(X,L)) = L + X + 10 >= L + X + 49 = cons(s(X),n__incr(activate(L)))
    
    adx(nil()) = 6 >= 1 = nil()
    
    adx(cons(X,L)) = L + X + 15 >= L + X + 18 = incr(cons(X,n__adx(activate(L))))
    
    nats() = 0 >= 6 = adx(zeros())
    
    zeros() = 1 >= 14 = cons(0(),n__zeros())
    
    head(cons(X,L)) = L + X + 26 >= X = X
    
    tail(cons(X,L)) = L + X + 32 >= L + 8 = activate(L)
    
    incr(X) = X >= X + 25 = n__incr(X)
    
    adx(X) = X + 5 >= X = n__adx(X)
    
    zeros() = 1 >= 0 = n__zeros()
    
    activate(n__incr(X)) = X + 33 >= X + 8 = incr(activate(X))
    
    activate(n__adx(X)) = X + 8 >= X + 13 = adx(activate(X))
    
    activate(n__zeros()) = 8 >= 1 = zeros()
    
    activate(X) = X + 8 >= X = X
   problem:
    strict:
     incr(nil()) -> nil()
     incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
     adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
     nats() -> adx(zeros())
     zeros() -> cons(0(),n__zeros())
     incr(X) -> n__incr(X)
     activate(n__adx(X)) -> adx(activate(X))
    weak:
     adx(nil()) -> nil()
     head(cons(X,L)) -> X
     tail(cons(X,L)) -> activate(L)
     adx(X) -> n__adx(X)
     zeros() -> n__zeros()
     activate(n__incr(X)) -> incr(activate(X))
     activate(n__zeros()) -> zeros()
     activate(X) -> X
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [tail](x0) = x0 + 1,
     
     [head](x0) = x0,
     
     [n__zeros] = 4,
     
     [0] = 3,
     
     [zeros] = 5,
     
     [nats] = 0,
     
     [n__adx](x0) = x0,
     
     [adx](x0) = x0,
     
     [n__incr](x0) = x0 + 16,
     
     [activate](x0) = x0 + 1,
     
     [s](x0) = x0 + 10,
     
     [cons](x0, x1) = x0 + x1,
     
     [incr](x0) = x0 + 7,
     
     [nil] = 16
    orientation:
     incr(nil()) = 23 >= 16 = nil()
     
     incr(cons(X,L)) = L + X + 7 >= L + X + 27 = cons(s(X),n__incr(activate(L)))
     
     adx(cons(X,L)) = L + X >= L + X + 8 = incr(cons(X,n__adx(activate(L))))
     
     nats() = 0 >= 5 = adx(zeros())
     
     zeros() = 5 >= 7 = cons(0(),n__zeros())
     
     incr(X) = X + 7 >= X + 16 = n__incr(X)
     
     activate(n__adx(X)) = X + 1 >= X + 1 = adx(activate(X))
     
     adx(nil()) = 16 >= 16 = nil()
     
     head(cons(X,L)) = L + X >= X = X
     
     tail(cons(X,L)) = L + X + 1 >= L + 1 = activate(L)
     
     adx(X) = X >= X = n__adx(X)
     
     zeros() = 5 >= 4 = n__zeros()
     
     activate(n__incr(X)) = X + 17 >= X + 8 = incr(activate(X))
     
     activate(n__zeros()) = 5 >= 5 = zeros()
     
     activate(X) = X + 1 >= X = X
    problem:
     strict:
      incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
      adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
      nats() -> adx(zeros())
      zeros() -> cons(0(),n__zeros())
      incr(X) -> n__incr(X)
      activate(n__adx(X)) -> adx(activate(X))
     weak:
      incr(nil()) -> nil()
      adx(nil()) -> nil()
      head(cons(X,L)) -> X
      tail(cons(X,L)) -> activate(L)
      adx(X) -> n__adx(X)
      zeros() -> n__zeros()
      activate(n__incr(X)) -> incr(activate(X))
      activate(n__zeros()) -> zeros()
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [tail](x0) = x0 + 29,
      
      [head](x0) = x0,
      
      [n__zeros] = 15,
      
      [0] = 9,
      
      [zeros] = 16,
      
      [nats] = 24,
      
      [n__adx](x0) = x0,
      
      [adx](x0) = x0 + 4,
      
      [n__incr](x0) = x0,
      
      [activate](x0) = x0 + 1,
      
      [s](x0) = x0 + 28,
      
      [cons](x0, x1) = x0 + x1 + 3,
      
      [incr](x0) = x0,
      
      [nil] = 4
     orientation:
      incr(cons(X,L)) = L + X + 3 >= L + X + 32 = cons(s(X),n__incr(activate(L)))
      
      adx(cons(X,L)) = L + X + 7 >= L + X + 4 = incr(cons(X,n__adx(activate(L))))
      
      nats() = 24 >= 20 = adx(zeros())
      
      zeros() = 16 >= 27 = cons(0(),n__zeros())
      
      incr(X) = X >= X = n__incr(X)
      
      activate(n__adx(X)) = X + 1 >= X + 5 = adx(activate(X))
      
      incr(nil()) = 4 >= 4 = nil()
      
      adx(nil()) = 8 >= 4 = nil()
      
      head(cons(X,L)) = L + X + 3 >= X = X
      
      tail(cons(X,L)) = L + X + 32 >= L + 1 = activate(L)
      
      adx(X) = X + 4 >= X = n__adx(X)
      
      zeros() = 16 >= 15 = n__zeros()
      
      activate(n__incr(X)) = X + 1 >= X + 1 = incr(activate(X))
      
      activate(n__zeros()) = 16 >= 16 = zeros()
      
      activate(X) = X + 1 >= X = X
     problem:
      strict:
       incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
       zeros() -> cons(0(),n__zeros())
       incr(X) -> n__incr(X)
       activate(n__adx(X)) -> adx(activate(X))
      weak:
       adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
       nats() -> adx(zeros())
       incr(nil()) -> nil()
       adx(nil()) -> nil()
       head(cons(X,L)) -> X
       tail(cons(X,L)) -> activate(L)
       adx(X) -> n__adx(X)
       zeros() -> n__zeros()
       activate(n__incr(X)) -> incr(activate(X))
       activate(n__zeros()) -> zeros()
       activate(X) -> X
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [tail](x0) = x0 + 4,
       
       [head](x0) = x0,
       
       [n__zeros] = 1,
       
       [0] = 2,
       
       [zeros] = 5,
       
       [nats] = 15,
       
       [n__adx](x0) = x0 + 1,
       
       [adx](x0) = x0 + 10,
       
       [n__incr](x0) = x0 + 3,
       
       [activate](x0) = x0 + 4,
       
       [s](x0) = x0,
       
       [cons](x0, x1) = x0 + x1 + 1,
       
       [incr](x0) = x0 + 3,
       
       [nil] = 19
      orientation:
       incr(cons(X,L)) = L + X + 4 >= L + X + 8 = cons(s(X),n__incr(activate(L)))
       
       zeros() = 5 >= 4 = cons(0(),n__zeros())
       
       incr(X) = X + 3 >= X + 3 = n__incr(X)
       
       activate(n__adx(X)) = X + 5 >= X + 14 = adx(activate(X))
       
       adx(cons(X,L)) = L + X + 11 >= L + X + 9 = incr(cons(X,n__adx(activate(L))))
       
       nats() = 15 >= 15 = adx(zeros())
       
       incr(nil()) = 22 >= 19 = nil()
       
       adx(nil()) = 29 >= 19 = nil()
       
       head(cons(X,L)) = L + X + 1 >= X = X
       
       tail(cons(X,L)) = L + X + 5 >= L + 4 = activate(L)
       
       adx(X) = X + 10 >= X + 1 = n__adx(X)
       
       zeros() = 5 >= 1 = n__zeros()
       
       activate(n__incr(X)) = X + 7 >= X + 7 = incr(activate(X))
       
       activate(n__zeros()) = 5 >= 5 = zeros()
       
       activate(X) = X + 4 >= X = X
      problem:
       strict:
        incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
        incr(X) -> n__incr(X)
        activate(n__adx(X)) -> adx(activate(X))
       weak:
        zeros() -> cons(0(),n__zeros())
        adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
        nats() -> adx(zeros())
        incr(nil()) -> nil()
        adx(nil()) -> nil()
        head(cons(X,L)) -> X
        tail(cons(X,L)) -> activate(L)
        adx(X) -> n__adx(X)
        zeros() -> n__zeros()
        activate(n__incr(X)) -> incr(activate(X))
        activate(n__zeros()) -> zeros()
        activate(X) -> X
      Open