YES(?,O(n^2))
48.88/22.94	YES(?,O(n^2))
48.88/22.95	
48.88/22.95	Problem:
48.88/22.95	 a__f(X,X) -> a__f(a(),b())
48.88/22.95	 a__b() -> a()
48.88/22.95	 mark(f(X1,X2)) -> a__f(mark(X1),X2)
48.88/22.95	 mark(b()) -> a__b()
48.88/22.95	 mark(a()) -> a()
48.88/22.95	 a__f(X1,X2) -> f(X1,X2)
48.88/22.95	 a__b() -> b()
48.88/22.95	
48.88/22.95	Proof:
48.88/22.95	 Complexity Transformation Processor:
48.88/22.95	  strict:
48.88/22.95	   a__f(X,X) -> a__f(a(),b())
48.88/22.95	   a__b() -> a()
48.88/22.95	   mark(f(X1,X2)) -> a__f(mark(X1),X2)
48.88/22.95	   mark(b()) -> a__b()
48.88/22.95	   mark(a()) -> a()
48.88/22.95	   a__f(X1,X2) -> f(X1,X2)
48.88/22.95	   a__b() -> b()
48.88/22.95	  weak:
48.88/22.95	   
48.88/22.95	  Matrix Interpretation Processor: dim=1
48.88/22.95	   
48.88/22.95	   max_matrix:
48.88/22.95	    1
48.88/22.95	   interpretation:
48.88/22.95	    [mark](x0) = x0 + 4,
48.88/22.95	    
48.88/22.95	    [f](x0, x1) = x0 + x1 + 130,
48.88/22.95	    
48.88/22.95	    [a__b] = 1,
48.88/22.95	    
48.88/22.95	    [b] = 0,
48.88/22.95	    
48.88/22.95	    [a] = 0,
48.88/22.95	    
48.88/22.95	    [a__f](x0, x1) = x0 + x1 + 254
48.88/22.95	   orientation:
48.88/22.95	    a__f(X,X) = 2X + 254 >= 254 = a__f(a(),b())
48.88/22.95	    
48.88/22.95	    a__b() = 1 >= 0 = a()
48.88/22.95	    
48.88/22.95	    mark(f(X1,X2)) = X1 + X2 + 134 >= X1 + X2 + 258 = a__f(mark(X1),X2)
48.88/22.95	    
48.88/22.95	    mark(b()) = 4 >= 1 = a__b()
48.88/22.95	    
48.88/22.95	    mark(a()) = 4 >= 0 = a()
48.88/22.95	    
48.88/22.95	    a__f(X1,X2) = X1 + X2 + 254 >= X1 + X2 + 130 = f(X1,X2)
48.88/22.95	    
48.88/22.95	    a__b() = 1 >= 0 = b()
48.88/22.95	   problem:
48.88/22.95	    strict:
48.88/22.95	     a__f(X,X) -> a__f(a(),b())
48.88/22.95	     mark(f(X1,X2)) -> a__f(mark(X1),X2)
48.88/22.95	    weak:
48.88/22.95	     a__b() -> a()
48.88/22.95	     mark(b()) -> a__b()
48.88/22.95	     mark(a()) -> a()
48.88/22.95	     a__f(X1,X2) -> f(X1,X2)
48.88/22.95	     a__b() -> b()
48.88/22.95	   Matrix Interpretation Processor: dim=2
48.88/22.95	    
48.88/22.95	    max_matrix:
48.88/22.95	     [1 4]
48.88/22.95	     [0 1]
48.88/22.95	    interpretation:
48.88/22.95	                  [1 4]     [0]
48.88/22.95	     [mark](x0) = [0 1]x0 + [4],
48.88/22.95	     
48.88/22.95	                   [1 1]     [1 0]     [3]
48.88/22.95	     [f](x0, x1) = [0 1]x0 + [0 0]x1 + [2],
48.88/22.95	     
48.88/22.95	              [0]
48.88/22.95	     [a__b] = [1],
48.88/22.95	     
48.88/22.95	           [0]
48.88/22.95	     [b] = [1],
48.88/22.95	     
48.88/22.95	           [0]
48.88/22.95	     [a] = [0],
48.88/22.95	     
48.88/22.95	                      [1 1]     [1 0]     [4]
48.88/22.95	     [a__f](x0, x1) = [0 1]x0 + [0 0]x1 + [2]
48.88/22.95	    orientation:
48.88/22.95	                 [2 1]    [4]    [4]                
48.88/22.95	     a__f(X,X) = [0 1]X + [2] >= [2] = a__f(a(),b())
48.88/22.95	     
48.88/22.95	                      [1 5]     [1 0]     [11]    [1 5]     [1 0]     [8]                    
48.88/22.95	     mark(f(X1,X2)) = [0 1]X1 + [0 0]X2 + [6 ] >= [0 1]X1 + [0 0]X2 + [6] = a__f(mark(X1),X2)
48.88/22.95	     
48.88/22.95	              [0]    [0]      
48.88/22.95	     a__b() = [1] >= [0] = a()
48.88/22.95	     
48.88/22.95	                 [4]    [0]         
48.88/22.95	     mark(b()) = [5] >= [1] = a__b()
48.88/22.95	     
48.88/22.95	                 [0]    [0]      
48.88/22.95	     mark(a()) = [4] >= [0] = a()
48.88/22.95	     
48.88/22.95	                   [1 1]     [1 0]     [4]    [1 1]     [1 0]     [3]           
48.88/22.95	     a__f(X1,X2) = [0 1]X1 + [0 0]X2 + [2] >= [0 1]X1 + [0 0]X2 + [2] = f(X1,X2)
48.88/22.95	     
48.88/22.95	              [0]    [0]      
48.88/22.95	     a__b() = [1] >= [1] = b()
48.88/22.95	    problem:
48.88/22.95	     strict:
48.88/22.95	      a__f(X,X) -> a__f(a(),b())
48.88/22.95	     weak:
48.88/22.95	      mark(f(X1,X2)) -> a__f(mark(X1),X2)
48.88/22.95	      a__b() -> a()
48.88/22.95	      mark(b()) -> a__b()
48.88/22.95	      mark(a()) -> a()
48.88/22.95	      a__f(X1,X2) -> f(X1,X2)
48.88/22.95	      a__b() -> b()
48.88/22.95	    Bounds Processor:
48.88/22.95	     bound: 1
48.88/22.95	     enrichment: match
48.88/22.95	     automaton:
48.88/22.95	      final states: {11,10,7}
48.88/22.95	      transitions:
48.88/22.95	       a__f0(10,7) -> 7*
48.88/22.95	       a__f0(10,11) -> 7*
48.88/22.95	       a__f0(11,10) -> 7*
48.88/22.95	       a__f0(7,7) -> 7*
48.88/22.95	       a__f0(7,11) -> 7*
48.88/22.95	       a__f0(10,10) -> 7*
48.88/22.95	       a__f0(11,7) -> 7*
48.88/22.95	       a__f0(11,11) -> 7*
48.88/22.95	       a__f0(7,10) -> 7*
48.88/22.95	       a0() -> 7*
48.88/22.95	       b0() -> 7*
48.88/22.95	       mark0(10) -> 7*
48.88/22.95	       mark0(7) -> 7*
48.88/22.95	       mark0(11) -> 7*
48.88/22.95	       f0(10,7) -> 7*
48.88/22.95	       f0(10,11) -> 7*
48.88/22.95	       f0(11,10) -> 7*
48.88/22.95	       f0(7,7) -> 7*
48.88/22.95	       f0(7,11) -> 7*
48.88/22.95	       f0(10,10) -> 7*
48.88/22.95	       f0(11,7) -> 7*
48.88/22.95	       f0(11,11) -> 7*
48.88/22.95	       f0(7,10) -> 7*
48.88/22.95	       a__b0() -> 7*
48.88/22.95	       a__f1(9,8) -> 7*
48.88/22.95	       a__f1(10,11) -> 7*
48.88/22.95	       a__f1(9,11) -> 7*
48.88/22.95	       a__f1(10,8) -> 7*
48.88/22.95	       a1() -> 10*,7,9
48.88/22.95	       b1() -> 11*,7,8
48.88/22.95	       f1(9,8) -> 7*
48.88/22.95	       f1(10,11) -> 7*
48.88/22.95	       f1(9,11) -> 7*
48.88/22.95	       f1(10,8) -> 7*
48.88/22.95	       a__b1() -> 7*
48.88/22.95	       mark1(10) -> 10*,7,9
48.88/22.95	       mark1(9) -> 9*
48.88/22.95	     problem:
48.88/22.95	      strict:
48.88/22.95	       
48.88/22.95	      weak:
48.88/22.95	       a__f(X,X) -> a__f(a(),b())
48.88/22.95	       mark(f(X1,X2)) -> a__f(mark(X1),X2)
48.88/22.95	       a__b() -> a()
48.88/22.95	       mark(b()) -> a__b()
48.88/22.95	       mark(a()) -> a()
48.88/22.95	       a__f(X1,X2) -> f(X1,X2)
48.88/22.95	       a__b() -> b()
48.88/22.95	     Qed
48.88/22.95	EOF