MAYBE

Problem:
 nats() -> adx(zeros())
 zeros() -> cons(0(),zeros())
 incr(cons(X,Y)) -> cons(s(X),incr(Y))
 adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
 hd(cons(X,Y)) -> X
 tl(cons(X,Y)) -> Y

Proof:
 RT Transformation Processor:
  strict:
   nats() -> adx(zeros())
   zeros() -> cons(0(),zeros())
   incr(cons(X,Y)) -> cons(s(X),incr(Y))
   adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
   hd(cons(X,Y)) -> X
   tl(cons(X,Y)) -> Y
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [tl](x0) = x0,
    
    [hd](x0) = x0 + 3,
    
    [s](x0) = x0 + 12,
    
    [incr](x0) = x0 + 3,
    
    [cons](x0, x1) = x0 + x1 + 1,
    
    [0] = 1,
    
    [adx](x0) = x0 + 5,
    
    [zeros] = 0,
    
    [nats] = 0
   orientation:
    nats() = 0 >= 5 = adx(zeros())
    
    zeros() = 0 >= 2 = cons(0(),zeros())
    
    incr(cons(X,Y)) = X + Y + 4 >= X + Y + 16 = cons(s(X),incr(Y))
    
    adx(cons(X,Y)) = X + Y + 6 >= X + Y + 9 = incr(cons(X,adx(Y)))
    
    hd(cons(X,Y)) = X + Y + 4 >= X = X
    
    tl(cons(X,Y)) = X + Y + 1 >= Y = Y
   problem:
    strict:
     nats() -> adx(zeros())
     zeros() -> cons(0(),zeros())
     incr(cons(X,Y)) -> cons(s(X),incr(Y))
     adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
    weak:
     hd(cons(X,Y)) -> X
     tl(cons(X,Y)) -> Y
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [tl](x0) = x0,
     
     [hd](x0) = x0,
     
     [s](x0) = x0 + 16,
     
     [incr](x0) = x0 + 2,
     
     [cons](x0, x1) = x0 + x1,
     
     [0] = 2,
     
     [adx](x0) = x0,
     
     [zeros] = 14,
     
     [nats] = 16
    orientation:
     nats() = 16 >= 14 = adx(zeros())
     
     zeros() = 14 >= 16 = cons(0(),zeros())
     
     incr(cons(X,Y)) = X + Y + 2 >= X + Y + 18 = cons(s(X),incr(Y))
     
     adx(cons(X,Y)) = X + Y >= X + Y + 2 = incr(cons(X,adx(Y)))
     
     hd(cons(X,Y)) = X + Y >= X = X
     
     tl(cons(X,Y)) = X + Y >= Y = Y
    problem:
     strict:
      zeros() -> cons(0(),zeros())
      incr(cons(X,Y)) -> cons(s(X),incr(Y))
      adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
     weak:
      nats() -> adx(zeros())
      hd(cons(X,Y)) -> X
      tl(cons(X,Y)) -> Y
    Open