YES(?,O(n^2))
16.88/8.13	YES(?,O(n^2))
16.88/8.13	
16.88/8.13	Problem:
16.88/8.13	 U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
16.88/8.13	 U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
16.88/8.13	 plus(N,0()) -> N
16.88/8.13	 plus(N,s(M)) -> U11(tt(),M,N)
16.88/8.13	 activate(X) -> X
16.88/8.13	
16.88/8.13	Proof:
16.88/8.13	 Complexity Transformation Processor:
16.88/8.13	  strict:
16.88/8.13	   U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
16.88/8.13	   U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
16.88/8.13	   plus(N,0()) -> N
16.88/8.13	   plus(N,s(M)) -> U11(tt(),M,N)
16.88/8.13	   activate(X) -> X
16.88/8.13	  weak:
16.88/8.13	   
16.88/8.13	  Matrix Interpretation Processor: dim=1
16.88/8.13	   
16.88/8.13	   max_matrix:
16.88/8.13	    1
16.88/8.13	   interpretation:
16.88/8.13	    [0] = 72,
16.88/8.13	    
16.88/8.13	    [s](x0) = x0 + 1,
16.88/8.13	    
16.88/8.13	    [plus](x0, x1) = x0 + x1 + 191,
16.88/8.13	    
16.88/8.13	    [U12](x0, x1, x2) = x0 + x1 + x2 + 60,
16.88/8.13	    
16.88/8.13	    [activate](x0) = x0 + 1,
16.88/8.13	    
16.88/8.13	    [U11](x0, x1, x2) = x0 + x1 + x2 + 71,
16.88/8.13	    
16.88/8.13	    [tt] = 210
16.88/8.13	   orientation:
16.88/8.13	    U11(tt(),M,N) = M + N + 281 >= M + N + 272 = U12(tt(),activate(M),activate(N))
16.88/8.13	    
16.88/8.13	    U12(tt(),M,N) = M + N + 270 >= M + N + 194 = s(plus(activate(N),activate(M)))
16.88/8.13	    
16.88/8.13	    plus(N,0()) = N + 263 >= N = N
16.88/8.13	    
16.88/8.13	    plus(N,s(M)) = M + N + 192 >= M + N + 281 = U11(tt(),M,N)
16.88/8.13	    
16.88/8.13	    activate(X) = X + 1 >= X = X
16.88/8.13	   problem:
16.88/8.13	    strict:
16.88/8.13	     plus(N,s(M)) -> U11(tt(),M,N)
16.88/8.13	    weak:
16.88/8.13	     U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
16.88/8.13	     U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
16.88/8.13	     plus(N,0()) -> N
16.88/8.13	     activate(X) -> X
16.88/8.13	   Matrix Interpretation Processor: dim=2
16.88/8.13	    
16.88/8.13	    max_matrix:
16.88/8.13	     [1 3]
16.88/8.13	     [0 1]
16.88/8.13	    interpretation:
16.88/8.13	           [0]
16.88/8.13	     [0] = [0],
16.88/8.13	     
16.88/8.13	                    [3]
16.88/8.13	     [s](x0) = x0 + [2],
16.88/8.13	     
16.88/8.13	                           [1 2]     [3]
16.88/8.13	     [plus](x0, x1) = x0 + [0 1]x1 + [0],
16.88/8.13	     
16.88/8.13	                         [1 2]     [1 2]          [3]
16.88/8.13	     [U12](x0, x1, x2) = [0 0]x0 + [0 1]x1 + x2 + [2],
16.88/8.13	     
16.88/8.13	                        
16.88/8.13	     [activate](x0) = x0,
16.88/8.13	     
16.88/8.13	                         [1 3]     [1 2]          [0]
16.88/8.13	     [U11](x0, x1, x2) = [0 0]x0 + [0 1]x1 + x2 + [2],
16.88/8.13	     
16.88/8.13	            [0]
16.88/8.13	     [tt] = [3]
16.88/8.13	    orientation:
16.88/8.13	                    [1 2]        [10]    [1 2]        [9]                
16.88/8.13	     plus(N,s(M)) = [0 1]M + N + [2 ] >= [0 1]M + N + [2] = U11(tt(),M,N)
16.88/8.13	     
16.88/8.13	                     [1 2]        [9]    [1 2]        [9]                                    
16.88/8.13	     U11(tt(),M,N) = [0 1]M + N + [2] >= [0 1]M + N + [2] = U12(tt(),activate(M),activate(N))
16.88/8.13	     
16.88/8.13	                     [1 2]        [9]    [1 2]        [6]                                   
16.88/8.13	     U12(tt(),M,N) = [0 1]M + N + [2] >= [0 1]M + N + [2] = s(plus(activate(N),activate(M)))
16.88/8.13	     
16.88/8.13	                       [3]         
16.88/8.13	     plus(N,0()) = N + [0] >= N = N
16.88/8.13	     
16.88/8.13	                             
16.88/8.13	     activate(X) = X >= X = X
16.88/8.13	    problem:
16.88/8.13	     strict:
16.88/8.13	      
16.88/8.13	     weak:
16.88/8.13	      plus(N,s(M)) -> U11(tt(),M,N)
16.88/8.13	      U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
16.88/8.13	      U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
16.88/8.13	      plus(N,0()) -> N
16.88/8.13	      activate(X) -> X
16.88/8.13	    Qed
16.88/8.14	EOF