MAYBE

Problem:
 nats() -> adx(zeros())
 zeros() -> cons(n__0(),n__zeros())
 incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
 adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
 hd(cons(X,Y)) -> activate(X)
 tl(cons(X,Y)) -> activate(Y)
 0() -> n__0()
 zeros() -> n__zeros()
 s(X) -> n__s(X)
 incr(X) -> n__incr(X)
 adx(X) -> n__adx(X)
 activate(n__0()) -> 0()
 activate(n__zeros()) -> zeros()
 activate(n__s(X)) -> s(X)
 activate(n__incr(X)) -> incr(activate(X))
 activate(n__adx(X)) -> adx(activate(X))
 activate(X) -> X

Proof:
 RT Transformation Processor:
  strict:
   nats() -> adx(zeros())
   zeros() -> cons(n__0(),n__zeros())
   incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
   adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
   hd(cons(X,Y)) -> activate(X)
   tl(cons(X,Y)) -> activate(Y)
   0() -> n__0()
   zeros() -> n__zeros()
   s(X) -> n__s(X)
   incr(X) -> n__incr(X)
   adx(X) -> n__adx(X)
   activate(n__0()) -> 0()
   activate(n__zeros()) -> zeros()
   activate(n__s(X)) -> s(X)
   activate(n__incr(X)) -> incr(activate(X))
   activate(n__adx(X)) -> adx(activate(X))
   activate(X) -> X
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [s](x0) = x0,
    
    [0] = 0,
    
    [tl](x0) = x0,
    
    [hd](x0) = x0 + 20,
    
    [n__adx](x0) = x0 + 3,
    
    [n__incr](x0) = x0 + 1,
    
    [n__s](x0) = x0 + 24,
    
    [activate](x0) = x0 + 13,
    
    [incr](x0) = x0 + 6,
    
    [cons](x0, x1) = x0 + x1 + 12,
    
    [n__zeros] = 0,
    
    [n__0] = 26,
    
    [adx](x0) = x0 + 20,
    
    [zeros] = 0,
    
    [nats] = 0
   orientation:
    nats() = 0 >= 20 = adx(zeros())
    
    zeros() = 0 >= 38 = cons(n__0(),n__zeros())
    
    incr(cons(X,Y)) = X + Y + 18 >= X + Y + 63 = cons(n__s(activate(X)),n__incr(activate(Y)))
    
    adx(cons(X,Y)) = X + Y + 32 >= X + Y + 47 = incr(cons(activate(X),n__adx(activate(Y))))
    
    hd(cons(X,Y)) = X + Y + 32 >= X + 13 = activate(X)
    
    tl(cons(X,Y)) = X + Y + 12 >= Y + 13 = activate(Y)
    
    0() = 0 >= 26 = n__0()
    
    zeros() = 0 >= 0 = n__zeros()
    
    s(X) = X >= X + 24 = n__s(X)
    
    incr(X) = X + 6 >= X + 1 = n__incr(X)
    
    adx(X) = X + 20 >= X + 3 = n__adx(X)
    
    activate(n__0()) = 39 >= 0 = 0()
    
    activate(n__zeros()) = 13 >= 0 = zeros()
    
    activate(n__s(X)) = X + 37 >= X = s(X)
    
    activate(n__incr(X)) = X + 14 >= X + 19 = incr(activate(X))
    
    activate(n__adx(X)) = X + 16 >= X + 33 = adx(activate(X))
    
    activate(X) = X + 13 >= X = X
   problem:
    strict:
     nats() -> adx(zeros())
     zeros() -> cons(n__0(),n__zeros())
     incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
     adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
     tl(cons(X,Y)) -> activate(Y)
     0() -> n__0()
     zeros() -> n__zeros()
     s(X) -> n__s(X)
     activate(n__incr(X)) -> incr(activate(X))
     activate(n__adx(X)) -> adx(activate(X))
    weak:
     hd(cons(X,Y)) -> activate(X)
     incr(X) -> n__incr(X)
     adx(X) -> n__adx(X)
     activate(n__0()) -> 0()
     activate(n__zeros()) -> zeros()
     activate(n__s(X)) -> s(X)
     activate(X) -> X
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [s](x0) = x0,
     
     [0] = 0,
     
     [tl](x0) = x0 + 20,
     
     [hd](x0) = x0 + 12,
     
     [n__adx](x0) = x0 + 4,
     
     [n__incr](x0) = x0 + 4,
     
     [n__s](x0) = x0 + 31,
     
     [activate](x0) = x0,
     
     [incr](x0) = x0 + 4,
     
     [cons](x0, x1) = x0 + x1 + 12,
     
     [n__zeros] = 16,
     
     [n__0] = 29,
     
     [adx](x0) = x0 + 20,
     
     [zeros] = 9,
     
     [nats] = 0
    orientation:
     nats() = 0 >= 29 = adx(zeros())
     
     zeros() = 9 >= 57 = cons(n__0(),n__zeros())
     
     incr(cons(X,Y)) = X + Y + 16 >= X + Y + 47 = cons(n__s(activate(X)),n__incr(activate(Y)))
     
     adx(cons(X,Y)) = X + Y + 32 >= X + Y + 20 = incr(cons(activate(X),n__adx(activate(Y))))
     
     tl(cons(X,Y)) = X + Y + 32 >= Y = activate(Y)
     
     0() = 0 >= 29 = n__0()
     
     zeros() = 9 >= 16 = n__zeros()
     
     s(X) = X >= X + 31 = n__s(X)
     
     activate(n__incr(X)) = X + 4 >= X + 4 = incr(activate(X))
     
     activate(n__adx(X)) = X + 4 >= X + 20 = adx(activate(X))
     
     hd(cons(X,Y)) = X + Y + 24 >= X = activate(X)
     
     incr(X) = X + 4 >= X + 4 = n__incr(X)
     
     adx(X) = X + 20 >= X + 4 = n__adx(X)
     
     activate(n__0()) = 29 >= 0 = 0()
     
     activate(n__zeros()) = 16 >= 9 = zeros()
     
     activate(n__s(X)) = X + 31 >= X = s(X)
     
     activate(X) = X >= X = X
    problem:
     strict:
      nats() -> adx(zeros())
      zeros() -> cons(n__0(),n__zeros())
      incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
      0() -> n__0()
      zeros() -> n__zeros()
      s(X) -> n__s(X)
      activate(n__incr(X)) -> incr(activate(X))
      activate(n__adx(X)) -> adx(activate(X))
     weak:
      adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
      tl(cons(X,Y)) -> activate(Y)
      hd(cons(X,Y)) -> activate(X)
      incr(X) -> n__incr(X)
      adx(X) -> n__adx(X)
      activate(n__0()) -> 0()
      activate(n__zeros()) -> zeros()
      activate(n__s(X)) -> s(X)
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [s](x0) = x0,
      
      [0] = 0,
      
      [tl](x0) = x0,
      
      [hd](x0) = x0,
      
      [n__adx](x0) = x0 + 8,
      
      [n__incr](x0) = x0,
      
      [n__s](x0) = x0 + 18,
      
      [activate](x0) = x0,
      
      [incr](x0) = x0,
      
      [cons](x0, x1) = x0 + x1,
      
      [n__zeros] = 8,
      
      [n__0] = 31,
      
      [adx](x0) = x0 + 8,
      
      [zeros] = 0,
      
      [nats] = 16
     orientation:
      nats() = 16 >= 8 = adx(zeros())
      
      zeros() = 0 >= 39 = cons(n__0(),n__zeros())
      
      incr(cons(X,Y)) = X + Y >= X + Y + 18 = cons(n__s(activate(X)),n__incr(activate(Y)))
      
      0() = 0 >= 31 = n__0()
      
      zeros() = 0 >= 8 = n__zeros()
      
      s(X) = X >= X + 18 = n__s(X)
      
      activate(n__incr(X)) = X >= X = incr(activate(X))
      
      activate(n__adx(X)) = X + 8 >= X + 8 = adx(activate(X))
      
      adx(cons(X,Y)) = X + Y + 8 >= X + Y + 8 = incr(cons(activate(X),n__adx(activate(Y))))
      
      tl(cons(X,Y)) = X + Y >= Y = activate(Y)
      
      hd(cons(X,Y)) = X + Y >= X = activate(X)
      
      incr(X) = X >= X = n__incr(X)
      
      adx(X) = X + 8 >= X + 8 = n__adx(X)
      
      activate(n__0()) = 31 >= 0 = 0()
      
      activate(n__zeros()) = 8 >= 0 = zeros()
      
      activate(n__s(X)) = X + 18 >= X = s(X)
      
      activate(X) = X >= X = X
     problem:
      strict:
       zeros() -> cons(n__0(),n__zeros())
       incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
       0() -> n__0()
       zeros() -> n__zeros()
       s(X) -> n__s(X)
       activate(n__incr(X)) -> incr(activate(X))
       activate(n__adx(X)) -> adx(activate(X))
      weak:
       nats() -> adx(zeros())
       adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
       tl(cons(X,Y)) -> activate(Y)
       hd(cons(X,Y)) -> activate(X)
       incr(X) -> n__incr(X)
       adx(X) -> n__adx(X)
       activate(n__0()) -> 0()
       activate(n__zeros()) -> zeros()
       activate(n__s(X)) -> s(X)
       activate(X) -> X
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [s](x0) = x0 + 16,
       
       [0] = 0,
       
       [tl](x0) = x0 + 12,
       
       [hd](x0) = x0 + 18,
       
       [n__adx](x0) = x0 + 1,
       
       [n__incr](x0) = x0,
       
       [n__s](x0) = x0 + 15,
       
       [activate](x0) = x0 + 1,
       
       [incr](x0) = x0,
       
       [cons](x0, x1) = x0 + x1 + 16,
       
       [n__zeros] = 0,
       
       [n__0] = 8,
       
       [adx](x0) = x0 + 3,
       
       [zeros] = 1,
       
       [nats] = 4
      orientation:
       zeros() = 1 >= 24 = cons(n__0(),n__zeros())
       
       incr(cons(X,Y)) = X + Y + 16 >= X + Y + 33 = cons(n__s(activate(X)),n__incr(activate(Y)))
       
       0() = 0 >= 8 = n__0()
       
       zeros() = 1 >= 0 = n__zeros()
       
       s(X) = X + 16 >= X + 15 = n__s(X)
       
       activate(n__incr(X)) = X + 1 >= X + 1 = incr(activate(X))
       
       activate(n__adx(X)) = X + 2 >= X + 4 = adx(activate(X))
       
       nats() = 4 >= 4 = adx(zeros())
       
       adx(cons(X,Y)) = X + Y + 19 >= X + Y + 19 = incr(cons(activate(X),n__adx(activate(Y))))
       
       tl(cons(X,Y)) = X + Y + 28 >= Y + 1 = activate(Y)
       
       hd(cons(X,Y)) = X + Y + 34 >= X + 1 = activate(X)
       
       incr(X) = X >= X = n__incr(X)
       
       adx(X) = X + 3 >= X + 1 = n__adx(X)
       
       activate(n__0()) = 9 >= 0 = 0()
       
       activate(n__zeros()) = 1 >= 1 = zeros()
       
       activate(n__s(X)) = X + 16 >= X + 16 = s(X)
       
       activate(X) = X + 1 >= X = X
      problem:
       strict:
        zeros() -> cons(n__0(),n__zeros())
        incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
        0() -> n__0()
        activate(n__incr(X)) -> incr(activate(X))
        activate(n__adx(X)) -> adx(activate(X))
       weak:
        zeros() -> n__zeros()
        s(X) -> n__s(X)
        nats() -> adx(zeros())
        adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
        tl(cons(X,Y)) -> activate(Y)
        hd(cons(X,Y)) -> activate(X)
        incr(X) -> n__incr(X)
        adx(X) -> n__adx(X)
        activate(n__0()) -> 0()
        activate(n__zeros()) -> zeros()
        activate(n__s(X)) -> s(X)
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [s](x0) = x0 + 8,
        
        [0] = 0,
        
        [tl](x0) = x0 + 16,
        
        [hd](x0) = x0 + 18,
        
        [n__adx](x0) = x0 + 3,
        
        [n__incr](x0) = x0,
        
        [n__s](x0) = x0 + 8,
        
        [activate](x0) = x0,
        
        [incr](x0) = x0 + 16,
        
        [cons](x0, x1) = x0 + x1 + 1,
        
        [n__zeros] = 1,
        
        [n__0] = 0,
        
        [adx](x0) = x0 + 24,
        
        [zeros] = 1,
        
        [nats] = 26
       orientation:
        zeros() = 1 >= 2 = cons(n__0(),n__zeros())
        
        incr(cons(X,Y)) = X + Y + 17 >= X + Y + 9 = cons(n__s(activate(X)),n__incr(activate(Y)))
        
        0() = 0 >= 0 = n__0()
        
        activate(n__incr(X)) = X >= X + 16 = incr(activate(X))
        
        activate(n__adx(X)) = X + 3 >= X + 24 = adx(activate(X))
        
        zeros() = 1 >= 1 = n__zeros()
        
        s(X) = X + 8 >= X + 8 = n__s(X)
        
        nats() = 26 >= 25 = adx(zeros())
        
        adx(cons(X,Y)) = X + Y + 25 >= X + Y + 20 = incr(cons(activate(X),n__adx(activate(Y))))
        
        tl(cons(X,Y)) = X + Y + 17 >= Y = activate(Y)
        
        hd(cons(X,Y)) = X + Y + 19 >= X = activate(X)
        
        incr(X) = X + 16 >= X = n__incr(X)
        
        adx(X) = X + 24 >= X + 3 = n__adx(X)
        
        activate(n__0()) = 0 >= 0 = 0()
        
        activate(n__zeros()) = 1 >= 1 = zeros()
        
        activate(n__s(X)) = X + 8 >= X + 8 = s(X)
        
        activate(X) = X >= X = X
       problem:
        strict:
         zeros() -> cons(n__0(),n__zeros())
         0() -> n__0()
         activate(n__incr(X)) -> incr(activate(X))
         activate(n__adx(X)) -> adx(activate(X))
        weak:
         incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
         zeros() -> n__zeros()
         s(X) -> n__s(X)
         nats() -> adx(zeros())
         adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
         tl(cons(X,Y)) -> activate(Y)
         hd(cons(X,Y)) -> activate(X)
         incr(X) -> n__incr(X)
         adx(X) -> n__adx(X)
         activate(n__0()) -> 0()
         activate(n__zeros()) -> zeros()
         activate(n__s(X)) -> s(X)
         activate(X) -> X
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [s](x0) = x0 + 5,
         
         [0] = 9,
         
         [tl](x0) = x0 + 31,
         
         [hd](x0) = x0 + 14,
         
         [n__adx](x0) = x0,
         
         [n__incr](x0) = x0 + 1,
         
         [n__s](x0) = x0 + 5,
         
         [activate](x0) = x0 + 1,
         
         [incr](x0) = x0 + 8,
         
         [cons](x0, x1) = x0 + x1,
         
         [n__zeros] = 7,
         
         [n__0] = 8,
         
         [adx](x0) = x0 + 10,
         
         [zeros] = 7,
         
         [nats] = 24
        orientation:
         zeros() = 7 >= 15 = cons(n__0(),n__zeros())
         
         0() = 9 >= 8 = n__0()
         
         activate(n__incr(X)) = X + 2 >= X + 9 = incr(activate(X))
         
         activate(n__adx(X)) = X + 1 >= X + 11 = adx(activate(X))
         
         incr(cons(X,Y)) = X + Y + 8 >= X + Y + 8 = cons(n__s(activate(X)),n__incr(activate(Y)))
         
         zeros() = 7 >= 7 = n__zeros()
         
         s(X) = X + 5 >= X + 5 = n__s(X)
         
         nats() = 24 >= 17 = adx(zeros())
         
         adx(cons(X,Y)) = X + Y + 10 >= X + Y + 10 = incr(cons(activate(X),n__adx(activate(Y))))
         
         tl(cons(X,Y)) = X + Y + 31 >= Y + 1 = activate(Y)
         
         hd(cons(X,Y)) = X + Y + 14 >= X + 1 = activate(X)
         
         incr(X) = X + 8 >= X + 1 = n__incr(X)
         
         adx(X) = X + 10 >= X = n__adx(X)
         
         activate(n__0()) = 9 >= 9 = 0()
         
         activate(n__zeros()) = 8 >= 7 = zeros()
         
         activate(n__s(X)) = X + 6 >= X + 5 = s(X)
         
         activate(X) = X + 1 >= X = X
        problem:
         strict:
          zeros() -> cons(n__0(),n__zeros())
          activate(n__incr(X)) -> incr(activate(X))
          activate(n__adx(X)) -> adx(activate(X))
         weak:
          0() -> n__0()
          incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
          zeros() -> n__zeros()
          s(X) -> n__s(X)
          nats() -> adx(zeros())
          adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
          tl(cons(X,Y)) -> activate(Y)
          hd(cons(X,Y)) -> activate(X)
          incr(X) -> n__incr(X)
          adx(X) -> n__adx(X)
          activate(n__0()) -> 0()
          activate(n__zeros()) -> zeros()
          activate(n__s(X)) -> s(X)
          activate(X) -> X
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [s](x0) = x0,
          
          [0] = 1,
          
          [tl](x0) = x0 + 4,
          
          [hd](x0) = x0 + 3,
          
          [n__adx](x0) = x0 + 1,
          
          [n__incr](x0) = x0 + 1,
          
          [n__s](x0) = x0,
          
          [activate](x0) = x0 + 1,
          
          [incr](x0) = x0 + 4,
          
          [cons](x0, x1) = x0 + x1,
          
          [n__zeros] = 0,
          
          [n__0] = 0,
          
          [adx](x0) = x0 + 7,
          
          [zeros] = 1,
          
          [nats] = 8
         orientation:
          zeros() = 1 >= 0 = cons(n__0(),n__zeros())
          
          activate(n__incr(X)) = X + 2 >= X + 5 = incr(activate(X))
          
          activate(n__adx(X)) = X + 2 >= X + 8 = adx(activate(X))
          
          0() = 1 >= 0 = n__0()
          
          incr(cons(X,Y)) = X + Y + 4 >= X + Y + 3 = cons(n__s(activate(X)),n__incr(activate(Y)))
          
          zeros() = 1 >= 0 = n__zeros()
          
          s(X) = X >= X = n__s(X)
          
          nats() = 8 >= 8 = adx(zeros())
          
          adx(cons(X,Y)) = X + Y + 7 >= X + Y + 7 = incr(cons(activate(X),n__adx(activate(Y))))
          
          tl(cons(X,Y)) = X + Y + 4 >= Y + 1 = activate(Y)
          
          hd(cons(X,Y)) = X + Y + 3 >= X + 1 = activate(X)
          
          incr(X) = X + 4 >= X + 1 = n__incr(X)
          
          adx(X) = X + 7 >= X + 1 = n__adx(X)
          
          activate(n__0()) = 1 >= 1 = 0()
          
          activate(n__zeros()) = 1 >= 1 = zeros()
          
          activate(n__s(X)) = X + 1 >= X = s(X)
          
          activate(X) = X + 1 >= X = X
         problem:
          strict:
           activate(n__incr(X)) -> incr(activate(X))
           activate(n__adx(X)) -> adx(activate(X))
          weak:
           zeros() -> cons(n__0(),n__zeros())
           0() -> n__0()
           incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
           zeros() -> n__zeros()
           s(X) -> n__s(X)
           nats() -> adx(zeros())
           adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
           tl(cons(X,Y)) -> activate(Y)
           hd(cons(X,Y)) -> activate(X)
           incr(X) -> n__incr(X)
           adx(X) -> n__adx(X)
           activate(n__0()) -> 0()
           activate(n__zeros()) -> zeros()
           activate(n__s(X)) -> s(X)
           activate(X) -> X
         Open