MAYBE

Problem:
 d(0()) -> 0()
 d(s(x)) -> s(s(d(x)))
 e(0(),x) -> x
 e(s(x),y) -> e(x,d(y))

Proof:
 Complexity Transformation Processor:
  strict:
   d(0()) -> 0()
   d(s(x)) -> s(s(d(x)))
   e(0(),x) -> x
   e(s(x),y) -> e(x,d(y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [e](x0, x1) = x0 + x1,
     
     [s](x0) = x0,
     
     [d](x0) = x0,
     
     [0] = 1
    orientation:
     d(0()) = 1 >= 1 = 0()
     
     d(s(x)) = x >= x = s(s(d(x)))
     
     e(0(),x) = x + 1 >= x = x
     
     e(s(x),y) = x + y >= x + y = e(x,d(y))
    problem:
     strict:
      d(0()) -> 0()
      d(s(x)) -> s(s(d(x)))
      e(s(x),y) -> e(x,d(y))
     weak:
      e(0(),x) -> x
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [e](x0, x1) = x0 + x1,
       
       [s](x0) = x0,
       
       [d](x0) = x0 + 1,
       
       [0] = 1
      orientation:
       d(0()) = 2 >= 1 = 0()
       
       d(s(x)) = x + 1 >= x + 1 = s(s(d(x)))
       
       e(s(x),y) = x + y >= x + y + 1 = e(x,d(y))
       
       e(0(),x) = x + 1 >= x = x
      problem:
       strict:
        d(s(x)) -> s(s(d(x)))
        e(s(x),y) -> e(x,d(y))
       weak:
        d(0()) -> 0()
        e(0(),x) -> x
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [e](x0, x1) = x0 + x1,
         
         [s](x0) = x0 + 1,
         
         [d](x0) = x0,
         
         [0] = 0
        orientation:
         d(s(x)) = x + 1 >= x + 2 = s(s(d(x)))
         
         e(s(x),y) = x + y + 1 >= x + y = e(x,d(y))
         
         d(0()) = 0 >= 0 = 0()
         
         e(0(),x) = x >= x = x
        problem:
         strict:
          d(s(x)) -> s(s(d(x)))
         weak:
          e(s(x),y) -> e(x,d(y))
          d(0()) -> 0()
          e(0(),x) -> x
        Open