YES(?,O(n^2))
16.70/8.20	YES(?,O(n^2))
16.70/8.21	
16.70/8.21	Problem:
16.70/8.21	 U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
16.70/8.21	 U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
16.70/8.21	 plus(N,0()) -> N
16.70/8.21	 plus(N,s(M)) -> U11(tt(),M,N)
16.70/8.21	 activate(X) -> X
16.70/8.21	
16.70/8.21	Proof:
16.70/8.21	 Complexity Transformation Processor:
16.70/8.21	  strict:
16.70/8.21	   U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
16.70/8.21	   U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
16.70/8.21	   plus(N,0()) -> N
16.70/8.21	   plus(N,s(M)) -> U11(tt(),M,N)
16.70/8.21	   activate(X) -> X
16.70/8.21	  weak:
16.70/8.21	   
16.70/8.21	  Matrix Interpretation Processor: dim=1
16.70/8.21	   
16.70/8.21	   max_matrix:
16.70/8.21	    1
16.70/8.21	   interpretation:
16.70/8.21	    [0] = 8,
16.70/8.21	    
16.70/8.21	    [s](x0) = x0 + 6,
16.70/8.21	    
16.70/8.21	    [plus](x0, x1) = x0 + x1 + 12,
16.70/8.21	    
16.70/8.21	    [U12](x0, x1, x2) = x0 + x1 + x2 + 7,
16.70/8.21	    
16.70/8.21	    [activate](x0) = x0 + 1,
16.70/8.21	    
16.70/8.21	    [U11](x0, x1, x2) = x0 + x1 + x2,
16.70/8.21	    
16.70/8.21	    [tt] = 1
16.70/8.21	   orientation:
16.70/8.21	    U11(tt(),M,N) = M + N + 1 >= M + N + 10 = U12(tt(),activate(M),activate(N))
16.70/8.21	    
16.70/8.21	    U12(tt(),M,N) = M + N + 8 >= M + N + 20 = s(plus(activate(N),activate(M)))
16.70/8.21	    
16.70/8.21	    plus(N,0()) = N + 20 >= N = N
16.70/8.21	    
16.70/8.21	    plus(N,s(M)) = M + N + 18 >= M + N + 1 = U11(tt(),M,N)
16.70/8.21	    
16.70/8.21	    activate(X) = X + 1 >= X = X
16.70/8.21	   problem:
16.70/8.21	    strict:
16.70/8.21	     U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
16.70/8.21	     U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
16.70/8.21	    weak:
16.70/8.21	     plus(N,0()) -> N
16.70/8.21	     plus(N,s(M)) -> U11(tt(),M,N)
16.70/8.21	     activate(X) -> X
16.70/8.21	   Matrix Interpretation Processor: dim=1
16.70/8.21	    
16.70/8.21	    max_matrix:
16.70/8.21	     1
16.70/8.21	    interpretation:
16.70/8.21	     [0] = 0,
16.70/8.21	     
16.70/8.21	     [s](x0) = x0 + 128,
16.70/8.21	     
16.70/8.21	     [plus](x0, x1) = x0 + x1,
16.70/8.21	     
16.70/8.21	     [U12](x0, x1, x2) = x0 + x1 + x2 + 78,
16.70/8.21	     
16.70/8.21	     [activate](x0) = x0,
16.70/8.21	     
16.70/8.21	     [U11](x0, x1, x2) = x0 + x1 + x2 + 30,
16.70/8.21	     
16.70/8.21	     [tt] = 98
16.70/8.21	    orientation:
16.70/8.21	     U11(tt(),M,N) = M + N + 128 >= M + N + 176 = U12(tt(),activate(M),activate(N))
16.70/8.21	     
16.70/8.21	     U12(tt(),M,N) = M + N + 176 >= M + N + 128 = s(plus(activate(N),activate(M)))
16.70/8.21	     
16.70/8.21	     plus(N,0()) = N >= N = N
16.70/8.21	     
16.70/8.21	     plus(N,s(M)) = M + N + 128 >= M + N + 128 = U11(tt(),M,N)
16.70/8.21	     
16.70/8.21	     activate(X) = X >= X = X
16.70/8.21	    problem:
16.70/8.21	     strict:
16.70/8.21	      U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
16.70/8.21	     weak:
16.70/8.21	      U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
16.70/8.21	      plus(N,0()) -> N
16.70/8.21	      plus(N,s(M)) -> U11(tt(),M,N)
16.70/8.21	      activate(X) -> X
16.70/8.21	    Matrix Interpretation Processor: dim=2
16.70/8.21	     
16.70/8.21	     max_matrix:
16.70/8.21	      [1 3]
16.70/8.21	      [0 1]
16.70/8.21	     interpretation:
16.70/8.21	            [1]
16.70/8.21	      [0] = [3],
16.70/8.21	      
16.70/8.21	                     [0]
16.70/8.21	      [s](x0) = x0 + [3],
16.70/8.21	      
16.70/8.21	                            [1 3]  
16.70/8.21	      [plus](x0, x1) = x0 + [0 1]x1,
16.70/8.21	      
16.70/8.21	                               [1 3]          [1]
16.70/8.21	      [U12](x0, x1, x2) = x0 + [0 1]x1 + x2 + [0],
16.70/8.21	      
16.70/8.21	                         
16.70/8.21	      [activate](x0) = x0,
16.70/8.21	      
16.70/8.21	                          [1 2]     [1 3]          [3]
16.70/8.21	      [U11](x0, x1, x2) = [0 1]x0 + [0 1]x1 + x2 + [0],
16.70/8.21	      
16.70/8.21	             [0]
16.70/8.21	      [tt] = [3]
16.70/8.21	     orientation:
16.70/8.21	                      [1 3]        [9]    [1 3]        [1]                                    
16.70/8.21	      U11(tt(),M,N) = [0 1]M + N + [3] >= [0 1]M + N + [3] = U12(tt(),activate(M),activate(N))
16.70/8.21	      
16.70/8.21	                      [1 3]        [1]    [1 3]        [0]                                   
16.70/8.21	      U12(tt(),M,N) = [0 1]M + N + [3] >= [0 1]M + N + [3] = s(plus(activate(N),activate(M)))
16.70/8.21	      
16.70/8.21	                        [10]         
16.70/8.21	      plus(N,0()) = N + [3 ] >= N = N
16.70/8.21	      
16.70/8.21	                     [1 3]        [9]    [1 3]        [9]                
16.70/8.21	      plus(N,s(M)) = [0 1]M + N + [3] >= [0 1]M + N + [3] = U11(tt(),M,N)
16.70/8.21	      
16.70/8.21	                              
16.70/8.21	      activate(X) = X >= X = X
16.70/8.21	     problem:
16.70/8.21	      strict:
16.70/8.21	       
16.70/8.21	      weak:
16.70/8.21	       U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
16.70/8.21	       U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
16.70/8.21	       plus(N,0()) -> N
16.70/8.21	       plus(N,s(M)) -> U11(tt(),M,N)
16.70/8.21	       activate(X) -> X
16.70/8.21	     Qed
16.70/8.21	EOF