Problem:
 U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
 U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
 plus(N,0()) -> N
 plus(N,s(M)) -> U11(tt(),M,N)
 activate(X) -> X

Proof:
 Complexity Transformation Processor:
  strict:
   U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
   U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
   plus(N,0()) -> N
   plus(N,s(M)) -> U11(tt(),M,N)
   activate(X) -> X
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [0] = 6,
     
     [s](x0) = x0 + 10,
     
     [plus](x0, x1) = x0 + x1 + 10,
     
     [U12](x0, x1, x2) = x0 + x1 + x2 + 5,
     
     [activate](x0) = x0 + 1,
     
     [U11](x0, x1, x2) = x0 + x1 + x2 + 12,
     
     [tt] = 4
    orientation:
     U11(tt(),M,N) = M + N + 16 >= M + N + 11 = U12(tt(),activate(M),activate(N))
     
     U12(tt(),M,N) = M + N + 9 >= M + N + 22 = s(plus(activate(N),activate(M)))
     
     plus(N,0()) = N + 16 >= N = N
     
     plus(N,s(M)) = M + N + 20 >= M + N + 16 = U11(tt(),M,N)
     
     activate(X) = X + 1 >= X = X
    problem:
     strict:
      U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
     weak:
      U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
      plus(N,0()) -> N
      plus(N,s(M)) -> U11(tt(),M,N)
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 2
     max_matrix:
      [1 3]
      [0 1]
      interpretation:
             [0]
       [0] = [2],
       
                      [1]
       [s](x0) = x0 + [3],
       
                        [1 3]     [1 2]     [3]
       [plus](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
       
                           [1 2]     [1 2]     [1 3]     [2]
       [U12](x0, x1, x2) = [0 1]x0 + [0 1]x1 + [0 1]x2 + [0],
       
                             [1]
       [activate](x0) = x0 + [0],
       
                           [1 3]     [1 2]     [1 3]     [1]
       [U11](x0, x1, x2) = [0 0]x0 + [0 1]x1 + [0 1]x2 + [3],
       
              [0]
       [tt] = [3]
      orientation:
                       [1 2]    [1 3]    [8]    [1 2]    [1 3]    [6]                                   
       U12(tt(),M,N) = [0 1]M + [0 1]N + [3] >= [0 1]M + [0 1]N + [3] = s(plus(activate(N),activate(M)))
       
                       [1 2]    [1 3]    [10]    [1 2]    [1 3]    [10]                                    
       U11(tt(),M,N) = [0 1]M + [0 1]N + [3 ] >= [0 1]M + [0 1]N + [3 ] = U12(tt(),activate(M),activate(N))
       
                     [1 3]    [7]         
       plus(N,0()) = [0 1]N + [2] >= N = N
       
                      [1 2]    [1 3]    [10]    [1 2]    [1 3]    [10]                
       plus(N,s(M)) = [0 1]M + [0 1]N + [3 ] >= [0 1]M + [0 1]N + [3 ] = U11(tt(),M,N)
       
                         [1]         
       activate(X) = X + [0] >= X = X
      problem:
       strict:
        
       weak:
        U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
        U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
        plus(N,0()) -> N
        plus(N,s(M)) -> U11(tt(),M,N)
        activate(X) -> X
      Qed