MAYBE

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

Proof:
 Complexity Transformation Processor:
  strict:
   d(0()) -> 0()
   d(s(x)) -> s(s(d(x)))
   e(s(x),y) -> e(x,d(y))
   sup(s(x),e(0(),y)) -> sup(x,e(y,s(0())))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [sup](x0, x1) = x0 + x1 + 1,
     
     [e](x0, x1) = x0 + x1,
     
     [s](x0) = x0,
     
     [d](x0) = x0 + 1,
     
     [0] = 0
    orientation:
     d(0()) = 1 >= 0 = 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))
     
     sup(s(x),e(0(),y)) = x + y + 1 >= x + y + 1 = sup(x,e(y,s(0())))
    problem:
     strict:
      d(s(x)) -> s(s(d(x)))
      e(s(x),y) -> e(x,d(y))
      sup(s(x),e(0(),y)) -> sup(x,e(y,s(0())))
     weak:
      d(0()) -> 0()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [sup](x0, x1) = x0 + x1 + 1,
       
       [e](x0, x1) = x0 + x1,
       
       [s](x0) = x0 + 1,
       
       [d](x0) = x0,
       
       [0] = 1
      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))
       
       sup(s(x),e(0(),y)) = x + y + 3 >= x + y + 3 = sup(x,e(y,s(0())))
       
       d(0()) = 1 >= 1 = 0()
      problem:
       strict:
        d(s(x)) -> s(s(d(x)))
        sup(s(x),e(0(),y)) -> sup(x,e(y,s(0())))
       weak:
        e(s(x),y) -> e(x,d(y))
        d(0()) -> 0()
      Bounds Processor:
       bound: 0
       enrichment: match
       automaton:
        final states: {5,4,3}
        transitions:
         d0(10) -> 1*
         d0(2) -> 3*
         d0(1) -> 3*
         d0(3) -> 1*
         s0(10) -> 3*
         s0(2) -> 1*
         s0(1) -> 1*
         s0(3) -> 10*
         sup0(1,2) -> 4*
         sup0(2,1) -> 4*
         sup0(1,1) -> 4*
         sup0(2,2) -> 4*
         e0(1,2) -> 5*
         e0(2,1) -> 5*
         e0(2,3) -> 5*
         e0(1,1) -> 5*
         e0(1,3) -> 5*
         e0(2,2) -> 5*
         00() -> 1,3,2
       problem:
        strict:
         d(s(x)) -> s(s(d(x)))
        weak:
         sup(s(x),e(0(),y)) -> sup(x,e(y,s(0())))
         e(s(x),y) -> e(x,d(y))
         d(0()) -> 0()
       Open