YES(O(1),O(n^1))
160.97/60.02	YES(O(1),O(n^1))
160.97/60.02	
160.97/60.02	We are left with following problem, upon which TcT provides the
160.97/60.02	certificate YES(O(1),O(n^1)).
160.97/60.02	
160.97/60.02	Strict Trs:
160.97/60.02	  { f(f(x)) -> g(f(x))
160.97/60.02	  , g(g(x)) -> f(x) }
160.97/60.02	Obligation:
160.97/60.02	  derivational complexity
160.97/60.02	Answer:
160.97/60.02	  YES(O(1),O(n^1))
160.97/60.02	
160.97/60.02	We use the processor 'matrix interpretation of dimension 1' to
160.97/60.02	orient following rules strictly.
160.97/60.02	
160.97/60.02	Trs:
160.97/60.02	  { f(f(x)) -> g(f(x))
160.97/60.02	  , g(g(x)) -> f(x) }
160.97/60.02	
160.97/60.02	The induced complexity on above rules (modulo remaining rules) is
160.97/60.02	YES(?,O(n^1)) . These rules are moved into the corresponding weak
160.97/60.02	component(s).
160.97/60.02	
160.97/60.02	Sub-proof:
160.97/60.02	----------
160.97/60.02	  TcT has computed the following triangular matrix interpretation.
160.97/60.02	  
160.97/60.02	    [f](x1) = [1] x1 + [40]
160.97/60.02	                           
160.97/60.02	    [g](x1) = [1] x1 + [32]
160.97/60.02	  
160.97/60.02	  The order satisfies the following ordering constraints:
160.97/60.02	  
160.97/60.02	    [f(f(x))] = [1] x + [80]
160.97/60.02	              > [1] x + [72]
160.97/60.02	              = [g(f(x))]   
160.97/60.02	                            
160.97/60.02	    [g(g(x))] = [1] x + [64]
160.97/60.02	              > [1] x + [40]
160.97/60.02	              = [f(x)]      
160.97/60.02	                            
160.97/60.02	
160.97/60.02	We return to the main proof.
160.97/60.02	
160.97/60.02	We are left with following problem, upon which TcT provides the
160.97/60.02	certificate YES(O(1),O(1)).
160.97/60.02	
160.97/60.02	Weak Trs:
160.97/60.02	  { f(f(x)) -> g(f(x))
160.97/60.02	  , g(g(x)) -> f(x) }
160.97/60.02	Obligation:
160.97/60.02	  derivational complexity
160.97/60.02	Answer:
160.97/60.02	  YES(O(1),O(1))
160.97/60.02	
160.97/60.02	Empty rules are trivially bounded
160.97/60.02	
160.97/60.02	Hurray, we answered YES(O(1),O(n^1))
160.97/60.04	EOF