YES(?,O(n^2))
11.35/6.97	YES(?,O(n^2))
11.35/6.97	
11.35/6.97	Problem:
11.35/6.97	 and(tt(),X) -> activate(X)
11.35/6.97	 plus(N,0()) -> N
11.35/6.97	 plus(N,s(M)) -> s(plus(N,M))
11.35/6.97	 activate(X) -> X
11.35/6.97	
11.35/6.97	Proof:
11.35/6.97	 Complexity Transformation Processor:
11.35/6.97	  strict:
11.35/6.97	   and(tt(),X) -> activate(X)
11.35/6.97	   plus(N,0()) -> N
11.35/6.97	   plus(N,s(M)) -> s(plus(N,M))
11.35/6.97	   activate(X) -> X
11.35/6.97	  weak:
11.35/6.97	   
11.35/6.97	  Matrix Interpretation Processor: dim=1
11.35/6.97	   
11.35/6.97	   max_matrix:
11.35/6.97	    1
11.35/6.97	   interpretation:
11.35/6.97	    [s](x0) = x0 + 36,
11.35/6.97	    
11.35/6.97	    [plus](x0, x1) = x0 + x1 + 4,
11.35/6.97	    
11.35/6.97	    [0] = 62,
11.35/6.97	    
11.35/6.97	    [activate](x0) = x0 + 1,
11.35/6.97	    
11.35/6.97	    [and](x0, x1) = x0 + x1 + 38,
11.35/6.97	    
11.35/6.97	    [tt] = 90
11.35/6.97	   orientation:
11.35/6.97	    and(tt(),X) = X + 128 >= X + 1 = activate(X)
11.35/6.97	    
11.35/6.97	    plus(N,0()) = N + 66 >= N = N
11.35/6.97	    
11.35/6.97	    plus(N,s(M)) = M + N + 40 >= M + N + 40 = s(plus(N,M))
11.35/6.97	    
11.35/6.97	    activate(X) = X + 1 >= X = X
11.35/6.97	   problem:
11.35/6.97	    strict:
11.35/6.97	     plus(N,s(M)) -> s(plus(N,M))
11.35/6.97	    weak:
11.35/6.97	     and(tt(),X) -> activate(X)
11.35/6.97	     plus(N,0()) -> N
11.35/6.97	     activate(X) -> X
11.35/6.97	   Matrix Interpretation Processor: dim=2
11.35/6.97	    
11.35/6.97	    max_matrix:
11.35/6.97	     [1 2]
11.35/6.97	     [0 1]
11.35/6.97	    interpretation:
11.35/6.97	                    [0]
11.35/6.97	     [s](x0) = x0 + [1],
11.35/6.97	     
11.35/6.97	                      [1 2]     [1 1]  
11.35/6.97	     [plus](x0, x1) = [0 1]x0 + [0 1]x1,
11.35/6.97	     
11.35/6.97	           [0]
11.35/6.97	     [0] = [0],
11.35/6.97	     
11.35/6.97	                           [1]
11.35/6.97	     [activate](x0) = x0 + [0],
11.35/6.97	     
11.35/6.97	                     [1 2]     [1 2]     [2]
11.35/6.97	     [and](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
11.35/6.97	     
11.35/6.97	            [2]
11.35/6.97	     [tt] = [2]
11.35/6.97	    orientation:
11.35/6.97	                    [1 1]    [1 2]    [1]    [1 1]    [1 2]    [0]               
11.35/6.97	     plus(N,s(M)) = [0 1]M + [0 1]N + [1] >= [0 1]M + [0 1]N + [1] = s(plus(N,M))
11.35/6.97	     
11.35/6.97	                   [1 2]    [8]        [1]              
11.35/6.97	     and(tt(),X) = [0 1]X + [2] >= X + [0] = activate(X)
11.35/6.97	     
11.35/6.97	                   [1 2]          
11.35/6.97	     plus(N,0()) = [0 1]N >= N = N
11.35/6.97	     
11.35/6.97	                       [1]         
11.35/6.97	     activate(X) = X + [0] >= X = X
11.35/6.97	    problem:
11.35/6.97	     strict:
11.35/6.97	      
11.35/6.97	     weak:
11.35/6.97	      plus(N,s(M)) -> s(plus(N,M))
11.35/6.97	      and(tt(),X) -> activate(X)
11.35/6.97	      plus(N,0()) -> N
11.35/6.97	      activate(X) -> X
11.35/6.97	    Qed
11.35/6.97	EOF