YES(O(1),O(n^2))
1181.24/297.13	YES(O(1),O(n^2))
1181.24/297.13	
1181.24/297.13	We are left with following problem, upon which TcT provides the
1181.24/297.13	certificate YES(O(1),O(n^2)).
1181.24/297.13	
1181.24/297.13	Strict Trs:
1181.24/297.13	  { f(c(s(x), y)) -> f(c(x, s(y)))
1181.24/297.13	  , f(c(s(x), s(y))) -> g(c(x, y))
1181.24/297.13	  , g(c(x, s(y))) -> g(c(s(x), y))
1181.24/297.13	  , g(c(s(x), s(y))) -> f(c(x, y)) }
1181.24/297.13	Obligation:
1181.24/297.13	  derivational complexity
1181.24/297.13	Answer:
1181.24/297.13	  YES(O(1),O(n^2))
1181.24/297.13	
1181.24/297.13	We use the processor 'matrix interpretation of dimension 1' to
1181.24/297.13	orient following rules strictly.
1181.24/297.13	
1181.24/297.13	Trs:
1181.24/297.13	  { f(c(s(x), s(y))) -> g(c(x, y))
1181.24/297.13	  , g(c(s(x), s(y))) -> f(c(x, y)) }
1181.24/297.13	
1181.24/297.13	The induced complexity on above rules (modulo remaining rules) is
1181.24/297.13	YES(?,O(n^1)) . These rules are removed from the problem. Note that
1181.24/297.13	no rule is size-increasing. The overall complexity is obtained by
1181.24/297.13	multiplication .
1181.24/297.13	
1181.24/297.13	Sub-proof:
1181.24/297.13	----------
1181.24/297.13	  TcT has computed the following triangular matrix interpretation.
1181.24/297.13	  
1181.24/297.13	        [f](x1) = [1] x1 + [1]         
1181.24/297.13	                                       
1181.24/297.13	    [c](x1, x2) = [1] x1 + [1] x2 + [2]
1181.24/297.13	                                       
1181.24/297.13	        [s](x1) = [1] x1 + [1]         
1181.24/297.13	                                       
1181.24/297.13	        [g](x1) = [1] x1 + [1]         
1181.24/297.13	  
1181.24/297.13	  The order satisfies the following ordering constraints:
1181.24/297.13	  
1181.24/297.13	       [f(c(s(x), y))] =  [1] x + [1] y + [4]
1181.24/297.13	                       >= [1] x + [1] y + [4]
1181.24/297.13	                       =  [f(c(x, s(y)))]    
1181.24/297.13	                                             
1181.24/297.13	    [f(c(s(x), s(y)))] =  [1] x + [1] y + [5]
1181.24/297.13	                       >  [1] x + [1] y + [3]
1181.24/297.13	                       =  [g(c(x, y))]       
1181.24/297.13	                                             
1181.24/297.13	       [g(c(x, s(y)))] =  [1] x + [1] y + [4]
1181.24/297.13	                       >= [1] x + [1] y + [4]
1181.24/297.13	                       =  [g(c(s(x), y))]    
1181.24/297.13	                                             
1181.24/297.13	    [g(c(s(x), s(y)))] =  [1] x + [1] y + [5]
1181.24/297.13	                       >  [1] x + [1] y + [3]
1181.24/297.13	                       =  [f(c(x, y))]       
1181.24/297.13	                                             
1181.24/297.13	
1181.24/297.13	We return to the main proof.
1181.24/297.13	
1181.24/297.13	We are left with following problem, upon which TcT provides the
1181.24/297.13	certificate YES(?,O(n^1)).
1181.24/297.13	
1181.24/297.13	Strict Trs:
1181.24/297.13	  { f(c(s(x), y)) -> f(c(x, s(y)))
1181.24/297.13	  , g(c(x, s(y))) -> g(c(s(x), y)) }
1181.24/297.13	Obligation:
1181.24/297.13	  derivational complexity
1181.24/297.13	Answer:
1181.24/297.13	  YES(?,O(n^1))
1181.24/297.13	
1181.24/297.13	The problem is match-bounded by 1. The enriched problem is
1181.24/297.13	compatible with the following automaton.
1181.24/297.13	{ f_0(1) -> 1
1181.24/297.13	, f_0(2) -> 1
1181.24/297.13	, f_0(3) -> 1
1181.24/297.13	, f_0(4) -> 1
1181.24/297.13	, f_1(5) -> 1
1181.24/297.13	, c_0(1, 1) -> 2
1181.24/297.13	, c_0(1, 2) -> 2
1181.24/297.13	, c_0(1, 3) -> 2
1181.24/297.13	, c_0(1, 4) -> 2
1181.24/297.13	, c_0(2, 1) -> 2
1181.24/297.13	, c_0(2, 2) -> 2
1181.24/297.13	, c_0(2, 3) -> 2
1181.24/297.13	, c_0(2, 4) -> 2
1181.24/297.13	, c_0(3, 1) -> 2
1181.24/297.13	, c_0(3, 2) -> 2
1181.24/297.13	, c_0(3, 3) -> 2
1181.24/297.13	, c_0(3, 4) -> 2
1181.24/297.13	, c_0(4, 1) -> 2
1181.24/297.13	, c_0(4, 2) -> 2
1181.24/297.13	, c_0(4, 3) -> 2
1181.24/297.13	, c_0(4, 4) -> 2
1181.24/297.13	, c_1(1, 6) -> 5
1181.24/297.13	, c_1(2, 6) -> 5
1181.24/297.13	, c_1(3, 6) -> 5
1181.24/297.13	, c_1(4, 6) -> 5
1181.24/297.13	, c_1(6, 1) -> 7
1181.24/297.13	, c_1(6, 2) -> 7
1181.24/297.13	, c_1(6, 3) -> 7
1181.24/297.13	, c_1(6, 4) -> 7
1181.24/297.13	, s_0(1) -> 3
1181.24/297.13	, s_0(2) -> 3
1181.24/297.13	, s_0(3) -> 3
1181.24/297.13	, s_0(4) -> 3
1181.24/297.13	, s_1(1) -> 6
1181.24/297.13	, s_1(2) -> 6
1181.24/297.13	, s_1(3) -> 6
1181.24/297.13	, s_1(4) -> 6
1181.24/297.13	, s_1(6) -> 6
1181.24/297.13	, g_0(1) -> 4
1181.24/297.13	, g_0(2) -> 4
1181.24/297.13	, g_0(3) -> 4
1181.24/297.13	, g_0(4) -> 4
1181.24/297.13	, g_1(7) -> 4 }
1181.24/297.13	
1181.24/297.13	Hurray, we answered YES(O(1),O(n^2))
1181.24/297.15	EOF