YES(?,O(n^2))
648.13/295.18	YES(?,O(n^2))
648.13/295.19	
648.13/295.19	Problem:
648.13/295.19	 g(s(x)) -> f(x)
648.13/295.19	 f(0()) -> s(0())
648.13/295.19	 f(s(x)) -> s(s(g(x)))
648.13/295.19	 g(0()) -> 0()
648.13/295.19	
648.13/295.19	Proof:
648.13/295.19	 Complexity Transformation Processor:
648.13/295.19	  strict:
648.13/295.19	   g(s(x)) -> f(x)
648.13/295.19	   f(0()) -> s(0())
648.13/295.19	   f(s(x)) -> s(s(g(x)))
648.13/295.19	   g(0()) -> 0()
648.13/295.19	  weak:
648.13/295.19	   
648.13/295.19	  Matrix Interpretation Processor: dim=1
648.13/295.19	   
648.13/295.19	   max_matrix:
648.13/295.19	    1
648.13/295.19	   interpretation:
648.13/295.19	    [0] = 28,
648.13/295.19	    
648.13/295.19	    [f](x0) = x0 + 222,
648.13/295.19	    
648.13/295.19	    [g](x0) = x0 + 33,
648.13/295.19	    
648.13/295.19	    [s](x0) = x0 + 37
648.13/295.19	   orientation:
648.13/295.19	    g(s(x)) = x + 70 >= x + 222 = f(x)
648.13/295.19	    
648.13/295.19	    f(0()) = 250 >= 65 = s(0())
648.13/295.19	    
648.13/295.19	    f(s(x)) = x + 259 >= x + 107 = s(s(g(x)))
648.13/295.19	    
648.13/295.19	    g(0()) = 61 >= 28 = 0()
648.13/295.19	   problem:
648.13/295.19	    strict:
648.13/295.19	     g(s(x)) -> f(x)
648.13/295.19	    weak:
648.13/295.19	     f(0()) -> s(0())
648.13/295.19	     f(s(x)) -> s(s(g(x)))
648.13/295.19	     g(0()) -> 0()
648.13/295.19	   Matrix Interpretation Processor: dim=2
648.13/295.19	    
648.13/295.19	    max_matrix:
648.13/295.19	     [1 1]
648.13/295.19	     [0 1]
648.13/295.19	    interpretation:
648.13/295.19	           [0]
648.13/295.19	     [0] = [0],
648.13/295.19	     
648.13/295.19	               [1 1]     [0]
648.13/295.19	     [f](x0) = [0 1]x0 + [4],
648.13/295.19	     
648.13/295.19	               [1 1]     [4]
648.13/295.19	     [g](x0) = [0 1]x0 + [0],
648.13/295.19	     
648.13/295.19	                    [0]
648.13/295.19	     [s](x0) = x0 + [4]
648.13/295.19	    orientation:
648.13/295.19	               [1 1]    [8]    [1 1]    [0]       
648.13/295.19	     g(s(x)) = [0 1]x + [4] >= [0 1]x + [4] = f(x)
648.13/295.19	     
648.13/295.19	              [0]    [0]         
648.13/295.19	     f(0()) = [4] >= [4] = s(0())
648.13/295.19	     
648.13/295.19	               [1 1]    [4]    [1 1]    [4]             
648.13/295.19	     f(s(x)) = [0 1]x + [8] >= [0 1]x + [8] = s(s(g(x)))
648.13/295.19	     
648.13/295.19	              [4]    [0]      
648.13/295.19	     g(0()) = [0] >= [0] = 0()
648.13/295.19	    problem:
648.13/295.19	     strict:
648.13/295.19	      
648.13/295.19	     weak:
648.13/295.19	      g(s(x)) -> f(x)
648.13/295.19	      f(0()) -> s(0())
648.13/295.19	      f(s(x)) -> s(s(g(x)))
648.13/295.19	      g(0()) -> 0()
648.13/295.19	    Qed
648.13/295.19	EOF