YES(O(1),O(n^5))
65.49/22.16	YES(O(1),O(n^5))
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^5)).
65.49/22.16	
65.49/22.16	Strict Trs:
65.49/22.16	  { f_0(x) -> a()
65.49/22.16	  , f_1(x) -> g_1(x, x)
65.49/22.16	  , g_1(s(x), y) -> b(f_0(y), g_1(x, y))
65.49/22.16	  , f_2(x) -> g_2(x, x)
65.49/22.16	  , g_2(s(x), y) -> b(f_1(y), g_2(x, y))
65.49/22.16	  , f_3(x) -> g_3(x, x)
65.49/22.16	  , g_3(s(x), y) -> b(f_2(y), g_3(x, y))
65.49/22.16	  , f_4(x) -> g_4(x, x)
65.49/22.16	  , g_4(s(x), y) -> b(f_3(y), g_4(x, y))
65.49/22.16	  , f_5(x) -> g_5(x, x)
65.49/22.16	  , g_5(s(x), y) -> b(f_4(y), g_5(x, y)) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^5))
65.49/22.16	
65.49/22.16	We add the following weak dependency pairs:
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_0^#(x) -> c_1()
65.49/22.16	  , f_1^#(x) -> c_2(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_4(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_6(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_8(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y))
65.49/22.16	  , f_5^#(x) -> c_10(g_5^#(x, x))
65.49/22.16	  , g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	
65.49/22.16	and mark the set of starting terms.
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^5)).
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_0^#(x) -> c_1()
65.49/22.16	  , f_1^#(x) -> c_2(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_4(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_6(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_8(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y))
65.49/22.16	  , f_5^#(x) -> c_10(g_5^#(x, x))
65.49/22.16	  , g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	Strict Trs:
65.49/22.16	  { f_0(x) -> a()
65.49/22.16	  , f_1(x) -> g_1(x, x)
65.49/22.16	  , g_1(s(x), y) -> b(f_0(y), g_1(x, y))
65.49/22.16	  , f_2(x) -> g_2(x, x)
65.49/22.16	  , g_2(s(x), y) -> b(f_1(y), g_2(x, y))
65.49/22.16	  , f_3(x) -> g_3(x, x)
65.49/22.16	  , g_3(s(x), y) -> b(f_2(y), g_3(x, y))
65.49/22.16	  , f_4(x) -> g_4(x, x)
65.49/22.16	  , g_4(s(x), y) -> b(f_3(y), g_4(x, y))
65.49/22.16	  , f_5(x) -> g_5(x, x)
65.49/22.16	  , g_5(s(x), y) -> b(f_4(y), g_5(x, y)) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^5))
65.49/22.16	
65.49/22.16	No rule is usable, rules are removed from the input problem.
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^5)).
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_0^#(x) -> c_1()
65.49/22.16	  , f_1^#(x) -> c_2(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_4(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_6(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_8(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y))
65.49/22.16	  , f_5^#(x) -> c_10(g_5^#(x, x))
65.49/22.16	  , g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^5))
65.49/22.16	
65.49/22.16	The weightgap principle applies (using the following constant
65.49/22.16	growth matrix-interpretation)
65.49/22.16	
65.49/22.16	The following argument positions are usable:
65.49/22.16	  Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1},
65.49/22.16	  Uargs(c_5) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_7) = {1, 2},
65.49/22.16	  Uargs(c_8) = {1}, Uargs(c_9) = {1, 2}, Uargs(c_10) = {1},
65.49/22.16	  Uargs(c_11) = {1, 2}
65.49/22.16	
65.49/22.16	TcT has computed the following constructor-restricted matrix
65.49/22.16	interpretation.
65.49/22.16	
65.49/22.16	          [s](x1) = [1 1] x1 + [1]           
65.49/22.16	                    [0 1]      [2]           
65.49/22.16	                                             
65.49/22.16	      [f_0^#](x1) = [0 0] x1 + [1]           
65.49/22.16	                    [1 1]      [1]           
65.49/22.16	                                             
65.49/22.16	            [c_1] = [0]                      
65.49/22.16	                    [1]                      
65.49/22.16	                                             
65.49/22.16	      [f_1^#](x1) = [0 0] x1 + [1]           
65.49/22.16	                    [1 2]      [2]           
65.49/22.16	                                             
65.49/22.16	        [c_2](x1) = [1 0] x1 + [1]           
65.49/22.16	                    [0 1]      [1]           
65.49/22.16	                                             
65.49/22.16	  [g_1^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2]
65.49/22.16	                    [2 2]      [1 1]      [1]
65.49/22.16	                                             
65.49/22.16	    [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
65.49/22.16	                    [0 1]      [0 1]      [1]
65.49/22.16	                                             
65.49/22.16	      [f_2^#](x1) = [0 0] x1 + [1]           
65.49/22.16	                    [2 2]      [1]           
65.49/22.16	                                             
65.49/22.16	        [c_4](x1) = [1 0] x1 + [1]           
65.49/22.16	                    [0 1]      [1]           
65.49/22.16	                                             
65.49/22.16	  [g_2^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2]
65.49/22.16	                    [2 2]      [1 1]      [1]
65.49/22.16	                                             
65.49/22.16	    [c_5](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
65.49/22.16	                    [0 1]      [0 1]      [0]
65.49/22.16	                                             
65.49/22.16	      [f_3^#](x1) = [0 0] x1 + [1]           
65.49/22.16	                    [2 1]      [1]           
65.49/22.16	                                             
65.49/22.16	        [c_6](x1) = [1 0] x1 + [2]           
65.49/22.16	                    [0 1]      [1]           
65.49/22.16	                                             
65.49/22.16	  [g_3^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2]
65.49/22.16	                    [1 1]      [1 1]      [1]
65.49/22.16	                                             
65.49/22.16	    [c_7](x1, x2) = [1 0] x1 + [1 0] x2 + [1]
65.49/22.16	                    [0 1]      [0 1]      [2]
65.49/22.16	                                             
65.49/22.16	      [f_4^#](x1) = [1]                      
65.49/22.16	                    [1]                      
65.49/22.16	                                             
65.49/22.16	        [c_8](x1) = [1 0] x1 + [0]           
65.49/22.16	                    [0 1]      [1]           
65.49/22.16	                                             
65.49/22.16	  [g_4^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2]
65.49/22.16	                    [2 1]      [1 1]      [2]
65.49/22.16	                                             
65.49/22.16	    [c_9](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
65.49/22.16	                    [0 1]      [0 1]      [1]
65.49/22.16	                                             
65.49/22.16	      [f_5^#](x1) = [2 2] x1 + [1]           
65.49/22.16	                    [1 2]      [2]           
65.49/22.16	                                             
65.49/22.16	       [c_10](x1) = [1 0] x1 + [1]           
65.49/22.16	                    [0 1]      [1]           
65.49/22.16	                                             
65.49/22.16	  [g_5^#](x1, x2) = [1 2] x1 + [1 0] x2 + [1]
65.49/22.16	                    [2 2]      [2 2]      [1]
65.49/22.16	                                             
65.49/22.16	   [c_11](x1, x2) = [1 0] x1 + [1 0] x2 + [1]
65.49/22.16	                    [0 1]      [0 1]      [1]
65.49/22.16	
65.49/22.16	The order satisfies the following ordering constraints:
65.49/22.16	
65.49/22.16	        [f_0^#(x)] = [0 0] x + [1]                
65.49/22.16	                     [1 1]     [1]                
65.49/22.16	                   > [0]                          
65.49/22.16	                     [1]                          
65.49/22.16	                   = [c_1()]                      
65.49/22.16	                                                  
65.49/22.16	        [f_1^#(x)] = [0 0] x + [1]                
65.49/22.16	                     [1 2]     [2]                
65.49/22.16	                   ? [0 0] x + [3]                
65.49/22.16	                     [3 3]     [2]                
65.49/22.16	                   = [c_2(g_1^#(x, x))]           
65.49/22.16	                                                  
65.49/22.16	  [g_1^#(s(x), y)] = [0 0] x + [0 0] y + [2]      
65.49/22.16	                     [2 4]     [1 1]     [7]      
65.49/22.16	                   ? [0 0] x + [0 0] y + [3]      
65.49/22.16	                     [2 2]     [2 2]     [3]      
65.49/22.16	                   = [c_3(f_0^#(y), g_1^#(x, y))] 
65.49/22.16	                                                  
65.49/22.16	        [f_2^#(x)] = [0 0] x + [1]                
65.49/22.16	                     [2 2]     [1]                
65.49/22.16	                   ? [0 0] x + [3]                
65.49/22.16	                     [3 3]     [2]                
65.49/22.16	                   = [c_4(g_2^#(x, x))]           
65.49/22.16	                                                  
65.49/22.16	  [g_2^#(s(x), y)] = [0 0] x + [0 0] y + [2]      
65.49/22.16	                     [2 4]     [1 1]     [7]      
65.49/22.16	                   ? [0 0] x + [0 0] y + [3]      
65.49/22.16	                     [2 2]     [2 3]     [3]      
65.49/22.16	                   = [c_5(f_1^#(y), g_2^#(x, y))] 
65.49/22.16	                                                  
65.49/22.16	        [f_3^#(x)] = [0 0] x + [1]                
65.49/22.16	                     [2 1]     [1]                
65.49/22.16	                   ? [0 0] x + [4]                
65.49/22.16	                     [2 2]     [2]                
65.49/22.16	                   = [c_6(g_3^#(x, x))]           
65.49/22.16	                                                  
65.49/22.16	  [g_3^#(s(x), y)] = [0 0] x + [0 0] y + [2]      
65.49/22.16	                     [1 2]     [1 1]     [4]      
65.49/22.16	                   ? [0 0] x + [0 0] y + [4]      
65.49/22.16	                     [1 1]     [3 3]     [4]      
65.49/22.16	                   = [c_7(f_2^#(y), g_3^#(x, y))] 
65.49/22.16	                                                  
65.49/22.16	        [f_4^#(x)] = [1]                          
65.49/22.16	                     [1]                          
65.49/22.16	                   ? [0 0] x + [2]                
65.49/22.16	                     [3 2]     [3]                
65.49/22.16	                   = [c_8(g_4^#(x, x))]           
65.49/22.16	                                                  
65.49/22.16	  [g_4^#(s(x), y)] = [0 0] x + [0 0] y + [2]      
65.49/22.16	                     [2 3]     [1 1]     [6]      
65.49/22.16	                   ? [0 0] x + [0 0] y + [3]      
65.49/22.16	                     [2 1]     [3 2]     [4]      
65.49/22.16	                   = [c_9(f_3^#(y), g_4^#(x, y))] 
65.49/22.16	                                                  
65.49/22.16	        [f_5^#(x)] = [2 2] x + [1]                
65.49/22.16	                     [1 2]     [2]                
65.49/22.16	                   ? [2 2] x + [2]                
65.49/22.16	                     [4 4]     [2]                
65.49/22.16	                   = [c_10(g_5^#(x, x))]          
65.49/22.16	                                                  
65.49/22.16	  [g_5^#(s(x), y)] = [1 3] x + [1 0] y + [6]      
65.49/22.16	                     [2 4]     [2 2]     [7]      
65.49/22.16	                   > [1 2] x + [1 0] y + [3]      
65.49/22.16	                     [2 2]     [2 2]     [3]      
65.49/22.16	                   = [c_11(f_4^#(y), g_5^#(x, y))]
65.49/22.16	                                                  
65.49/22.16	
65.49/22.16	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^5)).
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_1^#(x) -> c_2(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_4(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_6(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_8(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y))
65.49/22.16	  , f_5^#(x) -> c_10(g_5^#(x, x)) }
65.49/22.16	Weak DPs:
65.49/22.16	  { f_0^#(x) -> c_1()
65.49/22.16	  , g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^5))
65.49/22.16	
65.49/22.16	We estimate the number of application of {9} by applications of
65.49/22.16	Pre({9}) = {}. Here rules are labeled as follows:
65.49/22.16	
65.49/22.16	  DPs:
65.49/22.16	    { 1: f_1^#(x) -> c_2(g_1^#(x, x))
65.49/22.16	    , 2: g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y))
65.49/22.16	    , 3: f_2^#(x) -> c_4(g_2^#(x, x))
65.49/22.16	    , 4: g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y))
65.49/22.16	    , 5: f_3^#(x) -> c_6(g_3^#(x, x))
65.49/22.16	    , 6: g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y))
65.49/22.16	    , 7: f_4^#(x) -> c_8(g_4^#(x, x))
65.49/22.16	    , 8: g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y))
65.49/22.16	    , 9: f_5^#(x) -> c_10(g_5^#(x, x))
65.49/22.16	    , 10: f_0^#(x) -> c_1()
65.49/22.16	    , 11: g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^5)).
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_1^#(x) -> c_2(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_4(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_6(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_8(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y)) }
65.49/22.16	Weak DPs:
65.49/22.16	  { f_0^#(x) -> c_1()
65.49/22.16	  , f_5^#(x) -> c_10(g_5^#(x, x))
65.49/22.16	  , g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^5))
65.49/22.16	
65.49/22.16	The following weak DPs constitute a sub-graph of the DG that is
65.49/22.16	closed under successors. The DPs are removed.
65.49/22.16	
65.49/22.16	{ f_0^#(x) -> c_1() }
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^5)).
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_1^#(x) -> c_2(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_4(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_5(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_6(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_7(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_8(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_9(f_3^#(y), g_4^#(x, y)) }
65.49/22.16	Weak DPs:
65.49/22.16	  { f_5^#(x) -> c_10(g_5^#(x, x))
65.49/22.16	  , g_5^#(s(x), y) -> c_11(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^5))
65.49/22.16	
65.49/22.16	Due to missing edges in the dependency-graph, the right-hand sides
65.49/22.16	of following rules could be simplified:
65.49/22.16	
65.49/22.16	  { g_1^#(s(x), y) -> c_3(f_0^#(y), g_1^#(x, y)) }
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^5)).
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_5(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y)) }
65.49/22.16	Weak DPs:
65.49/22.16	  { f_5^#(x) -> c_9(g_5^#(x, x))
65.49/22.16	  , g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^5))
65.49/22.16	
65.49/22.16	Consider the dependency graph
65.49/22.16	
65.49/22.16	  1: f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.16	     -->_1 g_1^#(s(x), y) -> c_2(g_1^#(x, y)) :2
65.49/22.16	  
65.49/22.16	  2: g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.16	     -->_1 g_1^#(s(x), y) -> c_2(g_1^#(x, y)) :2
65.49/22.16	  
65.49/22.16	  3: f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.16	     -->_1 g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y)) :4
65.49/22.16	  
65.49/22.16	  4: g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y))
65.49/22.16	     -->_2 g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y)) :4
65.49/22.16	     -->_1 f_1^#(x) -> c_1(g_1^#(x, x)) :1
65.49/22.16	  
65.49/22.16	  5: f_3^#(x) -> c_5(g_3^#(x, x))
65.49/22.16	     -->_1 g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y)) :6
65.49/22.16	  
65.49/22.16	  6: g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y))
65.49/22.16	     -->_2 g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y)) :6
65.49/22.16	     -->_1 f_2^#(x) -> c_3(g_2^#(x, x)) :3
65.49/22.16	  
65.49/22.16	  7: f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	     -->_1 g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y)) :8
65.49/22.16	  
65.49/22.16	  8: g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y))
65.49/22.16	     -->_2 g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y)) :8
65.49/22.16	     -->_1 f_3^#(x) -> c_5(g_3^#(x, x)) :5
65.49/22.16	  
65.49/22.16	  9: f_5^#(x) -> c_9(g_5^#(x, x))
65.49/22.16	     -->_1 g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y)) :10
65.49/22.16	  
65.49/22.16	  10: g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y))
65.49/22.16	     -->_2 g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y)) :10
65.49/22.16	     -->_1 f_4^#(x) -> c_7(g_4^#(x, x)) :7
65.49/22.16	  
65.49/22.16	
65.49/22.16	Following roots of the dependency graph are removed, as the
65.49/22.16	considered set of starting terms is closed under reduction with
65.49/22.16	respect to these rules (modulo compound contexts).
65.49/22.16	
65.49/22.16	  { f_5^#(x) -> c_9(g_5^#(x, x)) }
65.49/22.16	
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^5)).
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_5(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y)) }
65.49/22.16	Weak DPs: { g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^5))
65.49/22.16	
65.49/22.16	We decompose the input problem according to the dependency graph
65.49/22.16	into the upper component
65.49/22.16	
65.49/22.16	  { g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	
65.49/22.16	and lower component
65.49/22.16	
65.49/22.16	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_5(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y)) }
65.49/22.16	
65.49/22.16	Further, following extension rules are added to the lower
65.49/22.16	component.
65.49/22.16	
65.49/22.16	{ g_5^#(s(x), y) -> f_4^#(y)
65.49/22.16	, g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.16	
65.49/22.16	TcT solves the upper component with certificate YES(O(1),O(n^1)).
65.49/22.16	
65.49/22.16	Sub-proof:
65.49/22.16	----------
65.49/22.16	  We are left with following problem, upon which TcT provides the
65.49/22.16	  certificate YES(O(1),O(n^1)).
65.49/22.16	  
65.49/22.16	  Strict DPs: { g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	  Obligation:
65.49/22.16	    runtime complexity
65.49/22.16	  Answer:
65.49/22.16	    YES(O(1),O(n^1))
65.49/22.16	  
65.49/22.16	  We use the processor 'matrix interpretation of dimension 1' to
65.49/22.16	  orient following rules strictly.
65.49/22.16	  
65.49/22.16	  DPs:
65.49/22.16	    { 1: g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	  
65.49/22.16	  Sub-proof:
65.49/22.16	  ----------
65.49/22.16	    The following argument positions are usable:
65.49/22.16	      Uargs(c_10) = {2}
65.49/22.16	    
65.49/22.16	    TcT has computed the following constructor-based matrix
65.49/22.16	    interpretation satisfying not(EDA).
65.49/22.16	    
65.49/22.16	              [s](x1) = [1] x1 + [4]
65.49/22.16	                                    
65.49/22.16	          [f_4^#](x1) = [7] x1 + [7]
65.49/22.16	                                    
65.49/22.16	      [g_5^#](x1, x2) = [2] x1 + [0]
65.49/22.16	                                    
65.49/22.16	       [c_10](x1, x2) = [1] x2 + [5]
65.49/22.16	    
65.49/22.16	    The order satisfies the following ordering constraints:
65.49/22.16	    
65.49/22.16	      [g_5^#(s(x), y)] = [2] x + [8]                  
65.49/22.16	                       > [2] x + [5]                  
65.49/22.16	                       = [c_10(f_4^#(y), g_5^#(x, y))]
65.49/22.16	                                                      
65.49/22.16	  
65.49/22.16	  The strictly oriented rules are moved into the weak component.
65.49/22.16	  
65.49/22.16	  We are left with following problem, upon which TcT provides the
65.49/22.16	  certificate YES(O(1),O(1)).
65.49/22.16	  
65.49/22.16	  Weak DPs: { g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	  Obligation:
65.49/22.16	    runtime complexity
65.49/22.16	  Answer:
65.49/22.16	    YES(O(1),O(1))
65.49/22.16	  
65.49/22.16	  The following weak DPs constitute a sub-graph of the DG that is
65.49/22.16	  closed under successors. The DPs are removed.
65.49/22.16	  
65.49/22.16	  { g_5^#(s(x), y) -> c_10(f_4^#(y), g_5^#(x, y)) }
65.49/22.16	  
65.49/22.16	  We are left with following problem, upon which TcT provides the
65.49/22.16	  certificate YES(O(1),O(1)).
65.49/22.16	  
65.49/22.16	  Rules: Empty
65.49/22.16	  Obligation:
65.49/22.16	    runtime complexity
65.49/22.16	  Answer:
65.49/22.16	    YES(O(1),O(1))
65.49/22.16	  
65.49/22.16	  Empty rules are trivially bounded
65.49/22.16	
65.49/22.16	We return to the main proof.
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^4)).
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_5(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y)) }
65.49/22.16	Weak DPs:
65.49/22.16	  { g_5^#(s(x), y) -> f_4^#(y)
65.49/22.16	  , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^4))
65.49/22.16	
65.49/22.16	We decompose the input problem according to the dependency graph
65.49/22.16	into the upper component
65.49/22.16	
65.49/22.16	  { f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y))
65.49/22.16	  , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.16	  , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.16	
65.49/22.16	and lower component
65.49/22.16	
65.49/22.16	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_5(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y)) }
65.49/22.16	
65.49/22.16	Further, following extension rules are added to the lower
65.49/22.16	component.
65.49/22.16	
65.49/22.16	{ f_4^#(x) -> g_4^#(x, x)
65.49/22.16	, g_4^#(s(x), y) -> f_3^#(y)
65.49/22.16	, g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.16	, g_5^#(s(x), y) -> f_4^#(y)
65.49/22.16	, g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.16	
65.49/22.16	TcT solves the upper component with certificate YES(O(1),O(n^1)).
65.49/22.16	
65.49/22.16	Sub-proof:
65.49/22.16	----------
65.49/22.16	  We are left with following problem, upon which TcT provides the
65.49/22.16	  certificate YES(O(1),O(n^1)).
65.49/22.16	  
65.49/22.16	  Strict DPs:
65.49/22.16	    { f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	    , g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y)) }
65.49/22.16	  Weak DPs:
65.49/22.16	    { g_5^#(s(x), y) -> f_4^#(y)
65.49/22.16	    , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.16	  Obligation:
65.49/22.16	    runtime complexity
65.49/22.16	  Answer:
65.49/22.16	    YES(O(1),O(n^1))
65.49/22.16	  
65.49/22.16	  We use the processor 'matrix interpretation of dimension 1' to
65.49/22.16	  orient following rules strictly.
65.49/22.16	  
65.49/22.16	  DPs:
65.49/22.16	    { 1: f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	    , 2: g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y)) }
65.49/22.16	  
65.49/22.16	  Sub-proof:
65.49/22.16	  ----------
65.49/22.16	    The following argument positions are usable:
65.49/22.16	      Uargs(c_7) = {1}, Uargs(c_8) = {2}
65.49/22.16	    
65.49/22.16	    TcT has computed the following constructor-based matrix
65.49/22.16	    interpretation satisfying not(EDA).
65.49/22.16	    
65.49/22.16	              [s](x1) = [1] x1 + [4]
65.49/22.16	                                    
65.49/22.16	          [f_3^#](x1) = [7] x1 + [7]
65.49/22.16	                                    
65.49/22.16	          [f_4^#](x1) = [7] x1 + [1]
65.49/22.16	                                    
65.49/22.16	      [g_4^#](x1, x2) = [2] x1 + [0]
65.49/22.16	                                    
65.49/22.16	      [g_5^#](x1, x2) = [7] x2 + [1]
65.49/22.16	                                    
65.49/22.16	            [c_7](x1) = [2] x1 + [0]
65.49/22.16	                                    
65.49/22.16	        [c_8](x1, x2) = [1] x2 + [1]
65.49/22.16	    
65.49/22.16	    The order satisfies the following ordering constraints:
65.49/22.16	    
65.49/22.16	            [f_4^#(x)] =  [7] x + [1]                 
65.49/22.16	                       >  [4] x + [0]                 
65.49/22.16	                       =  [c_7(g_4^#(x, x))]          
65.49/22.16	                                                      
65.49/22.16	      [g_4^#(s(x), y)] =  [2] x + [8]                 
65.49/22.16	                       >  [2] x + [1]                 
65.49/22.16	                       =  [c_8(f_3^#(y), g_4^#(x, y))]
65.49/22.16	                                                      
65.49/22.16	      [g_5^#(s(x), y)] =  [7] y + [1]                 
65.49/22.16	                       >= [7] y + [1]                 
65.49/22.16	                       =  [f_4^#(y)]                  
65.49/22.16	                                                      
65.49/22.16	      [g_5^#(s(x), y)] =  [7] y + [1]                 
65.49/22.16	                       >= [7] y + [1]                 
65.49/22.16	                       =  [g_5^#(x, y)]               
65.49/22.16	                                                      
65.49/22.16	  
65.49/22.16	  The strictly oriented rules are moved into the weak component.
65.49/22.16	  
65.49/22.16	  We are left with following problem, upon which TcT provides the
65.49/22.16	  certificate YES(O(1),O(1)).
65.49/22.16	  
65.49/22.16	  Weak DPs:
65.49/22.16	    { f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	    , g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y))
65.49/22.16	    , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.16	    , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.16	  Obligation:
65.49/22.16	    runtime complexity
65.49/22.16	  Answer:
65.49/22.16	    YES(O(1),O(1))
65.49/22.16	  
65.49/22.16	  The following weak DPs constitute a sub-graph of the DG that is
65.49/22.16	  closed under successors. The DPs are removed.
65.49/22.16	  
65.49/22.16	  { f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.16	  , g_4^#(s(x), y) -> c_8(f_3^#(y), g_4^#(x, y))
65.49/22.16	  , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.16	  , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.16	  
65.49/22.16	  We are left with following problem, upon which TcT provides the
65.49/22.16	  certificate YES(O(1),O(1)).
65.49/22.16	  
65.49/22.16	  Rules: Empty
65.49/22.16	  Obligation:
65.49/22.16	    runtime complexity
65.49/22.16	  Answer:
65.49/22.16	    YES(O(1),O(1))
65.49/22.16	  
65.49/22.16	  Empty rules are trivially bounded
65.49/22.16	
65.49/22.16	We return to the main proof.
65.49/22.16	
65.49/22.16	We are left with following problem, upon which TcT provides the
65.49/22.16	certificate YES(O(1),O(n^3)).
65.49/22.16	
65.49/22.16	Strict DPs:
65.49/22.16	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y))
65.49/22.16	  , f_3^#(x) -> c_5(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y)) }
65.49/22.16	Weak DPs:
65.49/22.16	  { f_4^#(x) -> g_4^#(x, x)
65.49/22.16	  , g_4^#(s(x), y) -> f_3^#(y)
65.49/22.16	  , g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.16	  , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.16	  , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.16	Obligation:
65.49/22.16	  runtime complexity
65.49/22.16	Answer:
65.49/22.16	  YES(O(1),O(n^3))
65.49/22.16	
65.49/22.16	We decompose the input problem according to the dependency graph
65.49/22.16	into the upper component
65.49/22.16	
65.49/22.16	  { f_3^#(x) -> c_5(g_3^#(x, x))
65.49/22.16	  , g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y))
65.49/22.16	  , f_4^#(x) -> g_4^#(x, x)
65.49/22.16	  , g_4^#(s(x), y) -> f_3^#(y)
65.49/22.16	  , g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.16	  , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.16	  , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.16	
65.49/22.16	and lower component
65.49/22.16	
65.49/22.16	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.16	  , g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.16	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.16	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y)) }
65.49/22.16	
65.49/22.16	Further, following extension rules are added to the lower
65.49/22.16	component.
65.49/22.16	
65.49/22.16	{ f_3^#(x) -> g_3^#(x, x)
65.49/22.17	, g_3^#(s(x), y) -> f_2^#(y)
65.49/22.17	, g_3^#(s(x), y) -> g_3^#(x, y)
65.49/22.17	, f_4^#(x) -> g_4^#(x, x)
65.49/22.17	, g_4^#(s(x), y) -> f_3^#(y)
65.49/22.17	, g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.17	, g_5^#(s(x), y) -> f_4^#(y)
65.49/22.17	, g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.17	
65.49/22.17	TcT solves the upper component with certificate YES(O(1),O(n^1)).
65.49/22.17	
65.49/22.17	Sub-proof:
65.49/22.17	----------
65.49/22.17	  We are left with following problem, upon which TcT provides the
65.49/22.17	  certificate YES(O(1),O(n^1)).
65.49/22.17	  
65.49/22.17	  Strict DPs:
65.49/22.17	    { f_3^#(x) -> c_5(g_3^#(x, x))
65.49/22.17	    , g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y)) }
65.49/22.17	  Weak DPs:
65.49/22.17	    { f_4^#(x) -> g_4^#(x, x)
65.49/22.17	    , g_4^#(s(x), y) -> f_3^#(y)
65.49/22.17	    , g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.17	    , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.17	    , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.17	  Obligation:
65.49/22.17	    runtime complexity
65.49/22.17	  Answer:
65.49/22.17	    YES(O(1),O(n^1))
65.49/22.17	  
65.49/22.17	  We use the processor 'matrix interpretation of dimension 1' to
65.49/22.17	  orient following rules strictly.
65.49/22.17	  
65.49/22.17	  DPs:
65.49/22.17	    { 2: g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y))
65.49/22.17	    , 3: f_4^#(x) -> g_4^#(x, x) }
65.49/22.17	  
65.49/22.17	  Sub-proof:
65.49/22.17	  ----------
65.49/22.17	    The following argument positions are usable:
65.49/22.17	      Uargs(c_5) = {1}, Uargs(c_6) = {2}
65.49/22.17	    
65.49/22.17	    TcT has computed the following constructor-based matrix
65.49/22.17	    interpretation satisfying not(EDA).
65.49/22.17	    
65.49/22.17	              [s](x1) = [1] x1 + [4]
65.49/22.17	                                    
65.49/22.17	          [f_2^#](x1) = [7] x1 + [7]
65.49/22.17	                                    
65.49/22.17	          [f_3^#](x1) = [5] x1 + [0]
65.49/22.17	                                    
65.49/22.17	      [g_3^#](x1, x2) = [2] x1 + [0]
65.49/22.17	                                    
65.49/22.17	          [f_4^#](x1) = [7] x1 + [1]
65.49/22.17	                                    
65.49/22.17	      [g_4^#](x1, x2) = [5] x2 + [0]
65.49/22.17	                                    
65.49/22.17	      [g_5^#](x1, x2) = [7] x2 + [1]
65.49/22.17	                                    
65.49/22.17	            [c_5](x1) = [2] x1 + [0]
65.49/22.17	                                    
65.49/22.17	        [c_6](x1, x2) = [1] x2 + [1]
65.49/22.17	    
65.49/22.17	    The order satisfies the following ordering constraints:
65.49/22.17	    
65.49/22.17	            [f_3^#(x)] =  [5] x + [0]                 
65.49/22.17	                       >= [4] x + [0]                 
65.49/22.17	                       =  [c_5(g_3^#(x, x))]          
65.49/22.17	                                                      
65.49/22.17	      [g_3^#(s(x), y)] =  [2] x + [8]                 
65.49/22.17	                       >  [2] x + [1]                 
65.49/22.17	                       =  [c_6(f_2^#(y), g_3^#(x, y))]
65.49/22.17	                                                      
65.49/22.17	            [f_4^#(x)] =  [7] x + [1]                 
65.49/22.17	                       >  [5] x + [0]                 
65.49/22.17	                       =  [g_4^#(x, x)]               
65.49/22.17	                                                      
65.49/22.17	      [g_4^#(s(x), y)] =  [5] y + [0]                 
65.49/22.17	                       >= [5] y + [0]                 
65.49/22.17	                       =  [f_3^#(y)]                  
65.49/22.17	                                                      
65.49/22.17	      [g_4^#(s(x), y)] =  [5] y + [0]                 
65.49/22.17	                       >= [5] y + [0]                 
65.49/22.17	                       =  [g_4^#(x, y)]               
65.49/22.17	                                                      
65.49/22.17	      [g_5^#(s(x), y)] =  [7] y + [1]                 
65.49/22.17	                       >= [7] y + [1]                 
65.49/22.17	                       =  [f_4^#(y)]                  
65.49/22.17	                                                      
65.49/22.17	      [g_5^#(s(x), y)] =  [7] y + [1]                 
65.49/22.17	                       >= [7] y + [1]                 
65.49/22.17	                       =  [g_5^#(x, y)]               
65.49/22.17	                                                      
65.49/22.17	  
65.49/22.17	  The strictly oriented rules are moved into the weak component.
65.49/22.17	  
65.49/22.17	  We are left with following problem, upon which TcT provides the
65.49/22.17	  certificate YES(O(1),O(1)).
65.49/22.17	  
65.49/22.17	  Strict DPs: { f_3^#(x) -> c_5(g_3^#(x, x)) }
65.49/22.17	  Weak DPs:
65.49/22.17	    { g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y))
65.49/22.17	    , f_4^#(x) -> g_4^#(x, x)
65.49/22.17	    , g_4^#(s(x), y) -> f_3^#(y)
65.49/22.17	    , g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.17	    , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.17	    , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.17	  Obligation:
65.49/22.17	    runtime complexity
65.49/22.17	  Answer:
65.49/22.17	    YES(O(1),O(1))
65.49/22.17	  
65.49/22.17	  The following weak DPs constitute a sub-graph of the DG that is
65.49/22.17	  closed under successors. The DPs are removed.
65.49/22.17	  
65.49/22.17	  { g_3^#(s(x), y) -> c_6(f_2^#(y), g_3^#(x, y)) }
65.49/22.17	  
65.49/22.17	  We are left with following problem, upon which TcT provides the
65.49/22.17	  certificate YES(O(1),O(1)).
65.49/22.17	  
65.49/22.17	  Strict DPs: { f_3^#(x) -> c_5(g_3^#(x, x)) }
65.49/22.17	  Weak DPs:
65.49/22.17	    { f_4^#(x) -> g_4^#(x, x)
65.49/22.17	    , g_4^#(s(x), y) -> f_3^#(y)
65.49/22.17	    , g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.17	    , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.17	    , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.17	  Obligation:
65.49/22.17	    runtime complexity
65.49/22.17	  Answer:
65.49/22.17	    YES(O(1),O(1))
65.49/22.17	  
65.49/22.17	  Due to missing edges in the dependency-graph, the right-hand sides
65.49/22.17	  of following rules could be simplified:
65.49/22.17	  
65.49/22.17	    { f_3^#(x) -> c_5(g_3^#(x, x)) }
65.49/22.17	  
65.49/22.17	  We are left with following problem, upon which TcT provides the
65.49/22.17	  certificate YES(O(1),O(1)).
65.49/22.17	  
65.49/22.17	  Strict DPs: { f_3^#(x) -> c_1() }
65.49/22.17	  Weak DPs:
65.49/22.17	    { f_4^#(x) -> c_2(g_4^#(x, x))
65.49/22.17	    , g_4^#(s(x), y) -> c_3(f_3^#(y))
65.49/22.17	    , g_4^#(s(x), y) -> c_4(g_4^#(x, y))
65.49/22.17	    , g_5^#(s(x), y) -> c_5(f_4^#(y))
65.49/22.17	    , g_5^#(s(x), y) -> c_6(g_5^#(x, y)) }
65.49/22.17	  Obligation:
65.49/22.17	    runtime complexity
65.49/22.17	  Answer:
65.49/22.17	    YES(O(1),O(1))
65.49/22.17	  
65.49/22.17	  We use the processor 'matrix interpretation of dimension 1' to
65.49/22.17	  orient following rules strictly.
65.49/22.17	  
65.49/22.17	  DPs:
65.49/22.17	    { 1: f_3^#(x) -> c_1()
65.49/22.17	    , 3: g_4^#(s(x), y) -> c_3(f_3^#(y)) }
65.49/22.17	  
65.49/22.17	  Sub-proof:
65.49/22.17	  ----------
65.49/22.17	    The following argument positions are usable:
65.49/22.17	      Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1},
65.49/22.17	      Uargs(c_5) = {1}, Uargs(c_6) = {1}
65.49/22.17	    
65.49/22.17	    TcT has computed the following constructor-restricted matrix
65.49/22.17	    interpretation. Note that the diagonal of the component-wise maxima
65.49/22.17	    of interpretation-entries (of constructors) contains no more than 0
65.49/22.17	    non-zero entries.
65.49/22.17	    
65.49/22.17	              [s](x1) = [0]         
65.49/22.17	                                    
65.49/22.17	          [f_2^#](x1) = [0]         
65.49/22.17	                                    
65.49/22.17	          [f_3^#](x1) = [1]         
65.49/22.17	                                    
65.49/22.17	      [g_3^#](x1, x2) = [0]         
65.49/22.17	                                    
65.49/22.17	          [f_4^#](x1) = [4]         
65.49/22.17	                                    
65.49/22.17	      [g_4^#](x1, x2) = [4]         
65.49/22.17	                                    
65.49/22.17	      [g_5^#](x1, x2) = [4] x2 + [4]
65.49/22.17	                                    
65.49/22.17	            [c_5](x1) = [0]         
65.49/22.17	                                    
65.49/22.17	        [c_6](x1, x2) = [0]         
65.49/22.17	                                    
65.49/22.17	                  [c] = [0]         
65.49/22.17	                                    
65.49/22.17	                [c_1] = [0]         
65.49/22.17	                                    
65.49/22.17	            [c_2](x1) = [1] x1 + [0]
65.49/22.17	                                    
65.49/22.17	            [c_3](x1) = [1] x1 + [1]
65.49/22.17	                                    
65.49/22.17	            [c_4](x1) = [1] x1 + [0]
65.49/22.17	                                    
65.49/22.17	            [c_5](x1) = [1] x1 + [0]
65.49/22.17	                                    
65.49/22.17	            [c_6](x1) = [1] x1 + [0]
65.49/22.17	    
65.49/22.17	    The order satisfies the following ordering constraints:
65.49/22.17	    
65.49/22.17	            [f_3^#(x)] =  [1]               
65.49/22.17	                       >  [0]               
65.49/22.17	                       =  [c_1()]           
65.49/22.17	                                            
65.49/22.17	            [f_4^#(x)] =  [4]               
65.49/22.17	                       >= [4]               
65.49/22.17	                       =  [c_2(g_4^#(x, x))]
65.49/22.17	                                            
65.49/22.17	      [g_4^#(s(x), y)] =  [4]               
65.49/22.17	                       >  [2]               
65.49/22.17	                       =  [c_3(f_3^#(y))]   
65.49/22.17	                                            
65.49/22.17	      [g_4^#(s(x), y)] =  [4]               
65.49/22.17	                       >= [4]               
65.49/22.17	                       =  [c_4(g_4^#(x, y))]
65.49/22.17	                                            
65.49/22.17	      [g_5^#(s(x), y)] =  [4] y + [4]       
65.49/22.17	                       >= [4]               
65.49/22.17	                       =  [c_5(f_4^#(y))]   
65.49/22.17	                                            
65.49/22.17	      [g_5^#(s(x), y)] =  [4] y + [4]       
65.49/22.17	                       >= [4] y + [4]       
65.49/22.17	                       =  [c_6(g_5^#(x, y))]
65.49/22.17	                                            
65.49/22.17	  
65.49/22.17	  The strictly oriented rules are moved into the weak component.
65.49/22.17	  
65.49/22.17	  We are left with following problem, upon which TcT provides the
65.49/22.17	  certificate YES(O(1),O(1)).
65.49/22.17	  
65.49/22.17	  Weak DPs:
65.49/22.17	    { f_3^#(x) -> c_1()
65.49/22.17	    , f_4^#(x) -> c_2(g_4^#(x, x))
65.49/22.17	    , g_4^#(s(x), y) -> c_3(f_3^#(y))
65.49/22.17	    , g_4^#(s(x), y) -> c_4(g_4^#(x, y))
65.49/22.17	    , g_5^#(s(x), y) -> c_5(f_4^#(y))
65.49/22.17	    , g_5^#(s(x), y) -> c_6(g_5^#(x, y)) }
65.49/22.17	  Obligation:
65.49/22.17	    runtime complexity
65.49/22.17	  Answer:
65.49/22.17	    YES(O(1),O(1))
65.49/22.17	  
65.49/22.17	  The following weak DPs constitute a sub-graph of the DG that is
65.49/22.17	  closed under successors. The DPs are removed.
65.49/22.17	  
65.49/22.17	  { f_3^#(x) -> c_1()
65.49/22.17	  , f_4^#(x) -> c_2(g_4^#(x, x))
65.49/22.17	  , g_4^#(s(x), y) -> c_3(f_3^#(y))
65.49/22.17	  , g_4^#(s(x), y) -> c_4(g_4^#(x, y))
65.49/22.17	  , g_5^#(s(x), y) -> c_5(f_4^#(y))
65.49/22.17	  , g_5^#(s(x), y) -> c_6(g_5^#(x, y)) }
65.49/22.17	  
65.49/22.17	  We are left with following problem, upon which TcT provides the
65.49/22.17	  certificate YES(O(1),O(1)).
65.49/22.17	  
65.49/22.17	  Rules: Empty
65.49/22.17	  Obligation:
65.49/22.17	    runtime complexity
65.49/22.17	  Answer:
65.49/22.17	    YES(O(1),O(1))
65.49/22.17	  
65.49/22.17	  Empty rules are trivially bounded
65.49/22.17	
65.49/22.17	We return to the main proof.
65.49/22.17	
65.49/22.17	We are left with following problem, upon which TcT provides the
65.49/22.17	certificate YES(O(1),O(n^2)).
65.49/22.17	
65.49/22.17	Strict DPs:
65.49/22.17	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.17	  , g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.17	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.17	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y)) }
65.49/22.17	Weak DPs:
65.49/22.17	  { f_3^#(x) -> g_3^#(x, x)
65.49/22.17	  , g_3^#(s(x), y) -> f_2^#(y)
65.49/22.17	  , g_3^#(s(x), y) -> g_3^#(x, y)
65.49/22.17	  , f_4^#(x) -> g_4^#(x, x)
65.49/22.17	  , g_4^#(s(x), y) -> f_3^#(y)
65.49/22.17	  , g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.17	  , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.17	  , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.17	Obligation:
65.49/22.17	  runtime complexity
65.49/22.17	Answer:
65.49/22.17	  YES(O(1),O(n^2))
65.49/22.17	
65.49/22.17	We use the processor 'polynomial interpretation' to orient
65.49/22.17	following rules strictly.
65.49/22.17	
65.49/22.17	DPs:
65.49/22.17	  { 2: g_1^#(s(x), y) -> c_2(g_1^#(x, y)) }
65.49/22.17	
65.49/22.17	Sub-proof:
65.49/22.17	----------
65.49/22.17	  We consider the following typing:
65.49/22.17	  
65.49/22.17	    s :: a -> a
65.49/22.17	    f_1^# :: a -> d
65.49/22.17	    g_1^# :: (a,a) -> b
65.49/22.17	    f_2^# :: a -> c
65.49/22.17	    g_2^# :: (a,a) -> e
65.49/22.17	    f_3^# :: a -> c
65.49/22.17	    g_3^# :: (a,a) -> c
65.49/22.17	    f_4^# :: a -> c
65.49/22.17	    g_4^# :: (a,a) -> c
65.49/22.17	    g_5^# :: (a,a) -> c
65.49/22.17	    c_1 :: b -> d
65.49/22.17	    c_2 :: b -> b
65.49/22.17	    c_3 :: e -> c
65.49/22.17	    c_4 :: (d,e) -> e
65.49/22.17	  
65.49/22.17	  The following argument positions are considered usable:
65.49/22.17	  
65.49/22.17	    Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
65.49/22.17	    Uargs(c_4) = {1, 2}
65.49/22.17	  
65.49/22.17	  TcT has computed the following constructor-restricted
65.49/22.17	  typedpolynomial interpretation.
65.49/22.17	  
65.49/22.17	          [s](x1) = 1 + x1                     
65.49/22.17	                                               
65.49/22.17	      [f_1^#](x1) = x1                         
65.49/22.17	                                               
65.49/22.17	  [g_1^#](x1, x2) = x1                         
65.49/22.17	                                               
65.49/22.17	      [f_2^#](x1) = 3 + x1^2                   
65.49/22.17	                                               
65.49/22.17	  [g_2^#](x1, x2) = x1*x2                      
65.49/22.17	                                               
65.49/22.17	      [f_3^#](x1) = 3 + 2*x1^2                 
65.49/22.17	                                               
65.49/22.17	  [g_3^#](x1, x2) = 3 + 2*x2^2                 
65.49/22.17	                                               
65.49/22.17	      [f_4^#](x1) = 3 + 3*x1 + 3*x1^2          
65.49/22.17	                                               
65.49/22.17	  [g_4^#](x1, x2) = 3 + 2*x2^2                 
65.49/22.17	                                               
65.49/22.17	  [g_5^#](x1, x2) = 3 + 3*x1*x2 + 3*x2 + 3*x2^2
65.49/22.17	                                               
65.49/22.17	        [c_1](x1) = x1                         
65.49/22.17	                                               
65.49/22.17	        [c_2](x1) = x1                         
65.49/22.17	                                               
65.49/22.17	        [c_3](x1) = 3 + x1                     
65.49/22.17	                                               
65.49/22.17	    [c_4](x1, x2) = x1 + x2                    
65.49/22.17	                                               
65.49/22.17	  
65.49/22.17	  This order satisfies the following ordering constraints.
65.49/22.17	  
65.49/22.17	          [f_1^#(x)] =  x                           
65.49/22.17	                     >= x                           
65.49/22.17	                     =  [c_1(g_1^#(x, x))]          
65.49/22.17	                                                    
65.49/22.17	    [g_1^#(s(x), y)] =  1 + x                       
65.49/22.17	                     >  x                           
65.49/22.17	                     =  [c_2(g_1^#(x, y))]          
65.49/22.17	                                                    
65.49/22.17	          [f_2^#(x)] =  3 + x^2                     
65.49/22.17	                     >= 3 + x^2                     
65.49/22.17	                     =  [c_3(g_2^#(x, x))]          
65.49/22.17	                                                    
65.49/22.17	    [g_2^#(s(x), y)] =  y + x*y                     
65.49/22.17	                     >= y + x*y                     
65.49/22.17	                     =  [c_4(f_1^#(y), g_2^#(x, y))]
65.49/22.17	                                                    
65.49/22.17	          [f_3^#(x)] =  3 + 2*x^2                   
65.49/22.17	                     >= 3 + 2*x^2                   
65.49/22.17	                     =  [g_3^#(x, x)]               
65.49/22.17	                                                    
65.49/22.17	    [g_3^#(s(x), y)] =  3 + 2*y^2                   
65.49/22.17	                     >= 3 + y^2                     
65.49/22.17	                     =  [f_2^#(y)]                  
65.49/22.17	                                                    
65.49/22.17	    [g_3^#(s(x), y)] =  3 + 2*y^2                   
65.49/22.17	                     >= 3 + 2*y^2                   
65.49/22.17	                     =  [g_3^#(x, y)]               
65.49/22.17	                                                    
65.49/22.17	          [f_4^#(x)] =  3 + 3*x + 3*x^2             
65.49/22.17	                     >= 3 + 2*x^2                   
65.49/22.17	                     =  [g_4^#(x, x)]               
65.49/22.17	                                                    
65.49/22.17	    [g_4^#(s(x), y)] =  3 + 2*y^2                   
65.49/22.17	                     >= 3 + 2*y^2                   
65.49/22.17	                     =  [f_3^#(y)]                  
65.49/22.17	                                                    
65.49/22.17	    [g_4^#(s(x), y)] =  3 + 2*y^2                   
65.49/22.17	                     >= 3 + 2*y^2                   
65.49/22.17	                     =  [g_4^#(x, y)]               
65.49/22.17	                                                    
65.49/22.17	    [g_5^#(s(x), y)] =  3 + 6*y + 3*x*y + 3*y^2     
65.49/22.17	                     >= 3 + 3*y + 3*y^2             
65.49/22.17	                     =  [f_4^#(y)]                  
65.49/22.17	                                                    
65.49/22.17	    [g_5^#(s(x), y)] =  3 + 6*y + 3*x*y + 3*y^2     
65.49/22.17	                     >= 3 + 3*x*y + 3*y + 3*y^2     
65.49/22.17	                     =  [g_5^#(x, y)]               
65.49/22.17	                                                    
65.49/22.17	
65.49/22.17	The strictly oriented rules are moved into the weak component.
65.49/22.17	
65.49/22.17	We are left with following problem, upon which TcT provides the
65.49/22.17	certificate YES(O(1),O(n^1)).
65.49/22.17	
65.49/22.17	Strict DPs:
65.49/22.17	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.17	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.17	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y)) }
65.49/22.17	Weak DPs:
65.49/22.17	  { g_1^#(s(x), y) -> c_2(g_1^#(x, y))
65.49/22.17	  , f_3^#(x) -> g_3^#(x, x)
65.49/22.17	  , g_3^#(s(x), y) -> f_2^#(y)
65.49/22.17	  , g_3^#(s(x), y) -> g_3^#(x, y)
65.49/22.17	  , f_4^#(x) -> g_4^#(x, x)
65.49/22.17	  , g_4^#(s(x), y) -> f_3^#(y)
65.49/22.17	  , g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.17	  , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.17	  , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.17	Obligation:
65.49/22.17	  runtime complexity
65.49/22.17	Answer:
65.49/22.17	  YES(O(1),O(n^1))
65.49/22.17	
65.49/22.17	The following weak DPs constitute a sub-graph of the DG that is
65.49/22.17	closed under successors. The DPs are removed.
65.49/22.17	
65.49/22.17	{ g_1^#(s(x), y) -> c_2(g_1^#(x, y)) }
65.49/22.17	
65.49/22.17	We are left with following problem, upon which TcT provides the
65.49/22.17	certificate YES(O(1),O(n^1)).
65.49/22.17	
65.49/22.17	Strict DPs:
65.49/22.17	  { f_1^#(x) -> c_1(g_1^#(x, x))
65.49/22.17	  , f_2^#(x) -> c_3(g_2^#(x, x))
65.49/22.17	  , g_2^#(s(x), y) -> c_4(f_1^#(y), g_2^#(x, y)) }
65.49/22.17	Weak DPs:
65.49/22.17	  { f_3^#(x) -> g_3^#(x, x)
65.49/22.17	  , g_3^#(s(x), y) -> f_2^#(y)
65.49/22.17	  , g_3^#(s(x), y) -> g_3^#(x, y)
65.49/22.17	  , f_4^#(x) -> g_4^#(x, x)
65.49/22.17	  , g_4^#(s(x), y) -> f_3^#(y)
65.49/22.17	  , g_4^#(s(x), y) -> g_4^#(x, y)
65.49/22.17	  , g_5^#(s(x), y) -> f_4^#(y)
65.49/22.17	  , g_5^#(s(x), y) -> g_5^#(x, y) }
65.49/22.17	Obligation:
65.49/22.17	  runtime complexity
65.49/22.17	Answer:
65.49/22.17	  YES(O(1),O(n^1))
65.49/22.17	
65.49/22.17	Due to missing edges in the dependency-graph, the right-hand sides
65.49/22.17	of following rules could be simplified:
65.49/22.17	
65.49/22.17	  { f_1^#(x) -> c_1(g_1^#(x, x)) }
65.49/22.17	
65.49/22.17	We are left with following problem, upon which TcT provides the
65.49/22.17	certificate YES(O(1),O(n^1)).
65.49/22.17	
65.49/22.17	Strict DPs:
65.49/22.17	  { f_1^#(x) -> c_1()
65.49/22.17	  , f_2^#(x) -> c_2(g_2^#(x, x))
65.49/22.17	  , g_2^#(s(x), y) -> c_3(f_1^#(y), g_2^#(x, y)) }
65.49/22.17	Weak DPs:
65.49/22.17	  { f_3^#(x) -> c_4(g_3^#(x, x))
65.49/22.17	  , g_3^#(s(x), y) -> c_5(f_2^#(y))
65.49/22.17	  , g_3^#(s(x), y) -> c_6(g_3^#(x, y))
65.49/22.17	  , f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.17	  , g_4^#(s(x), y) -> c_8(f_3^#(y))
65.49/22.17	  , g_4^#(s(x), y) -> c_9(g_4^#(x, y))
65.49/22.17	  , g_5^#(s(x), y) -> c_10(f_4^#(y))
65.49/22.17	  , g_5^#(s(x), y) -> c_11(g_5^#(x, y)) }
65.49/22.17	Obligation:
65.49/22.17	  runtime complexity
65.49/22.17	Answer:
65.49/22.17	  YES(O(1),O(n^1))
65.49/22.17	
65.49/22.17	We use the processor 'matrix interpretation of dimension 1' to
65.49/22.17	orient following rules strictly.
65.49/22.17	
65.49/22.17	DPs:
65.49/22.17	  { 1: f_1^#(x) -> c_1()
65.49/22.17	  , 3: g_2^#(s(x), y) -> c_3(f_1^#(y), g_2^#(x, y)) }
65.49/22.17	
65.49/22.17	Sub-proof:
65.49/22.17	----------
65.49/22.17	  The following argument positions are usable:
65.49/22.17	    Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1},
65.49/22.17	    Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1},
65.49/22.17	    Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1},
65.49/22.17	    Uargs(c_11) = {1}
65.49/22.17	  
65.49/22.17	  TcT has computed the following constructor-based matrix
65.49/22.17	  interpretation satisfying not(EDA).
65.49/22.17	  
65.49/22.17	            [s](x1) = [1] x1 + [4]         
65.49/22.17	                                           
65.49/22.17	        [f_1^#](x1) = [2]                  
65.49/22.17	                                           
65.49/22.17	    [g_1^#](x1, x2) = [7] x1 + [7] x2 + [0]
65.49/22.17	                                           
65.49/22.17	        [f_2^#](x1) = [3] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	    [g_2^#](x1, x2) = [3] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	        [f_3^#](x1) = [3] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	    [g_3^#](x1, x2) = [3] x2 + [0]         
65.49/22.17	                                           
65.49/22.17	        [f_4^#](x1) = [6] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	    [g_4^#](x1, x2) = [3] x2 + [0]         
65.49/22.17	                                           
65.49/22.17	    [g_5^#](x1, x2) = [7] x2 + [0]         
65.49/22.17	                                           
65.49/22.17	          [c_1](x1) = [7] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	          [c_2](x1) = [7] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	          [c_3](x1) = [7] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	      [c_4](x1, x2) = [7] x1 + [7] x2 + [0]
65.49/22.17	                                           
65.49/22.17	                [c] = [0]                  
65.49/22.17	                                           
65.49/22.17	              [c_1] = [0]                  
65.49/22.17	                                           
65.49/22.17	          [c_2](x1) = [1] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	      [c_3](x1, x2) = [4] x1 + [1] x2 + [3]
65.49/22.17	                                           
65.49/22.17	          [c_4](x1) = [1] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	          [c_5](x1) = [1] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	          [c_6](x1) = [1] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	          [c_7](x1) = [2] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	          [c_8](x1) = [1] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	          [c_9](x1) = [1] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	         [c_10](x1) = [1] x1 + [0]         
65.49/22.17	                                           
65.49/22.17	         [c_11](x1) = [1] x1 + [0]         
65.49/22.17	  
65.49/22.17	  The order satisfies the following ordering constraints:
65.49/22.17	  
65.49/22.17	          [f_1^#(x)] =  [2]                         
65.49/22.17	                     >  [0]                         
65.49/22.17	                     =  [c_1()]                     
65.49/22.17	                                                    
65.49/22.17	          [f_2^#(x)] =  [3] x + [0]                 
65.49/22.17	                     >= [3] x + [0]                 
65.49/22.17	                     =  [c_2(g_2^#(x, x))]          
65.49/22.17	                                                    
65.49/22.17	    [g_2^#(s(x), y)] =  [3] x + [12]                
65.49/22.17	                     >  [3] x + [11]                
65.49/22.17	                     =  [c_3(f_1^#(y), g_2^#(x, y))]
65.49/22.17	                                                    
65.49/22.17	          [f_3^#(x)] =  [3] x + [0]                 
65.49/22.17	                     >= [3] x + [0]                 
65.49/22.17	                     =  [c_4(g_3^#(x, x))]          
65.49/22.17	                                                    
65.49/22.17	    [g_3^#(s(x), y)] =  [3] y + [0]                 
65.49/22.17	                     >= [3] y + [0]                 
65.49/22.17	                     =  [c_5(f_2^#(y))]             
65.49/22.17	                                                    
65.49/22.17	    [g_3^#(s(x), y)] =  [3] y + [0]                 
65.49/22.17	                     >= [3] y + [0]                 
65.49/22.17	                     =  [c_6(g_3^#(x, y))]          
65.49/22.17	                                                    
65.49/22.17	          [f_4^#(x)] =  [6] x + [0]                 
65.49/22.17	                     >= [6] x + [0]                 
65.49/22.17	                     =  [c_7(g_4^#(x, x))]          
65.49/22.17	                                                    
65.49/22.17	    [g_4^#(s(x), y)] =  [3] y + [0]                 
65.49/22.17	                     >= [3] y + [0]                 
65.49/22.17	                     =  [c_8(f_3^#(y))]             
65.49/22.17	                                                    
65.49/22.17	    [g_4^#(s(x), y)] =  [3] y + [0]                 
65.49/22.17	                     >= [3] y + [0]                 
65.49/22.17	                     =  [c_9(g_4^#(x, y))]          
65.49/22.17	                                                    
65.49/22.17	    [g_5^#(s(x), y)] =  [7] y + [0]                 
65.49/22.17	                     >= [6] y + [0]                 
65.49/22.17	                     =  [c_10(f_4^#(y))]            
65.49/22.17	                                                    
65.49/22.17	    [g_5^#(s(x), y)] =  [7] y + [0]                 
65.49/22.17	                     >= [7] y + [0]                 
65.49/22.17	                     =  [c_11(g_5^#(x, y))]         
65.49/22.17	                                                    
65.49/22.17	
65.49/22.17	The strictly oriented rules are moved into the weak component.
65.49/22.17	
65.49/22.17	We are left with following problem, upon which TcT provides the
65.49/22.17	certificate YES(O(1),O(1)).
65.49/22.17	
65.49/22.17	Strict DPs: { f_2^#(x) -> c_2(g_2^#(x, x)) }
65.49/22.17	Weak DPs:
65.49/22.17	  { f_1^#(x) -> c_1()
65.49/22.17	  , g_2^#(s(x), y) -> c_3(f_1^#(y), g_2^#(x, y))
65.49/22.17	  , f_3^#(x) -> c_4(g_3^#(x, x))
65.49/22.17	  , g_3^#(s(x), y) -> c_5(f_2^#(y))
65.49/22.17	  , g_3^#(s(x), y) -> c_6(g_3^#(x, y))
65.49/22.17	  , f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.17	  , g_4^#(s(x), y) -> c_8(f_3^#(y))
65.49/22.17	  , g_4^#(s(x), y) -> c_9(g_4^#(x, y))
65.49/22.17	  , g_5^#(s(x), y) -> c_10(f_4^#(y))
65.49/22.17	  , g_5^#(s(x), y) -> c_11(g_5^#(x, y)) }
65.49/22.17	Obligation:
65.49/22.17	  runtime complexity
65.49/22.17	Answer:
65.49/22.17	  YES(O(1),O(1))
65.49/22.17	
65.49/22.17	The following weak DPs constitute a sub-graph of the DG that is
65.49/22.17	closed under successors. The DPs are removed.
65.49/22.17	
65.49/22.17	{ f_1^#(x) -> c_1()
65.49/22.17	, g_2^#(s(x), y) -> c_3(f_1^#(y), g_2^#(x, y)) }
65.49/22.17	
65.49/22.17	We are left with following problem, upon which TcT provides the
65.49/22.17	certificate YES(O(1),O(1)).
65.49/22.17	
65.49/22.17	Strict DPs: { f_2^#(x) -> c_2(g_2^#(x, x)) }
65.49/22.17	Weak DPs:
65.49/22.17	  { f_3^#(x) -> c_4(g_3^#(x, x))
65.49/22.17	  , g_3^#(s(x), y) -> c_5(f_2^#(y))
65.49/22.17	  , g_3^#(s(x), y) -> c_6(g_3^#(x, y))
65.49/22.17	  , f_4^#(x) -> c_7(g_4^#(x, x))
65.49/22.17	  , g_4^#(s(x), y) -> c_8(f_3^#(y))
65.49/22.17	  , g_4^#(s(x), y) -> c_9(g_4^#(x, y))
65.49/22.17	  , g_5^#(s(x), y) -> c_10(f_4^#(y))
65.49/22.17	  , g_5^#(s(x), y) -> c_11(g_5^#(x, y)) }
65.49/22.17	Obligation:
65.49/22.17	  runtime complexity
65.49/22.17	Answer:
65.49/22.17	  YES(O(1),O(1))
65.49/22.17	
65.49/22.17	Due to missing edges in the dependency-graph, the right-hand sides
65.49/22.17	of following rules could be simplified:
65.49/22.17	
65.49/22.17	  { f_2^#(x) -> c_2(g_2^#(x, x)) }
65.49/22.17	
65.49/22.17	We are left with following problem, upon which TcT provides the
65.49/22.17	certificate YES(O(1),O(1)).
65.49/22.17	
65.49/22.17	Strict DPs: { f_2^#(x) -> c_1() }
65.49/22.17	Weak DPs:
65.49/22.17	  { f_3^#(x) -> c_2(g_3^#(x, x))
65.49/22.17	  , g_3^#(s(x), y) -> c_3(f_2^#(y))
65.49/22.17	  , g_3^#(s(x), y) -> c_4(g_3^#(x, y))
65.49/22.17	  , f_4^#(x) -> c_5(g_4^#(x, x))
65.49/22.17	  , g_4^#(s(x), y) -> c_6(f_3^#(y))
65.49/22.17	  , g_4^#(s(x), y) -> c_7(g_4^#(x, y))
65.49/22.17	  , g_5^#(s(x), y) -> c_8(f_4^#(y))
65.49/22.17	  , g_5^#(s(x), y) -> c_9(g_5^#(x, y)) }
65.49/22.17	Obligation:
65.49/22.17	  runtime complexity
65.49/22.17	Answer:
65.49/22.17	  YES(O(1),O(1))
65.49/22.17	
65.49/22.17	We use the processor 'matrix interpretation of dimension 1' to
65.49/22.17	orient following rules strictly.
65.49/22.17	
65.49/22.17	DPs:
65.49/22.17	  { 1: f_2^#(x) -> c_1()
65.49/22.17	  , 6: g_4^#(s(x), y) -> c_6(f_3^#(y)) }
65.49/22.17	
65.49/22.17	Sub-proof:
65.49/22.17	----------
65.49/22.17	  The following argument positions are usable:
65.49/22.17	    Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1},
65.49/22.17	    Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1},
65.49/22.17	    Uargs(c_8) = {1}, Uargs(c_9) = {1}
65.49/22.17	  
65.49/22.17	  TcT has computed the following constructor-restricted matrix
65.49/22.17	  interpretation. Note that the diagonal of the component-wise maxima
65.49/22.17	  of interpretation-entries (of constructors) contains no more than 0
65.49/22.17	  non-zero entries.
65.49/22.17	  
65.49/22.17	            [s](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	        [f_1^#](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	    [g_1^#](x1, x2) = [0]         
65.49/22.17	                                  
65.49/22.17	        [f_2^#](x1) = [1]         
65.49/22.17	                                  
65.49/22.17	    [g_2^#](x1, x2) = [0]         
65.49/22.17	                                  
65.49/22.17	        [f_3^#](x1) = [3]         
65.49/22.17	                                  
65.49/22.17	    [g_3^#](x1, x2) = [2]         
65.49/22.17	                                  
65.49/22.17	        [f_4^#](x1) = [4]         
65.49/22.17	                                  
65.49/22.17	    [g_4^#](x1, x2) = [4]         
65.49/22.17	                                  
65.49/22.17	    [g_5^#](x1, x2) = [4] x2 + [4]
65.49/22.17	                                  
65.49/22.17	          [c_1](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_2](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_3](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	      [c_4](x1, x2) = [0]         
65.49/22.17	                                  
65.49/22.17	                [c] = [0]         
65.49/22.17	                                  
65.49/22.17	              [c_1] = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_2](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	      [c_3](x1, x2) = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_4](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_5](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_6](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_7](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_8](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_9](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	         [c_10](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	         [c_11](x1) = [0]         
65.49/22.17	                                  
65.49/22.17	                [c] = [0]         
65.49/22.17	                                  
65.49/22.17	              [c_1] = [0]         
65.49/22.17	                                  
65.49/22.17	          [c_2](x1) = [1] x1 + [1]
65.49/22.17	                                  
65.49/22.17	          [c_3](x1) = [1] x1 + [1]
65.49/22.17	                                  
65.49/22.17	          [c_4](x1) = [1] x1 + [0]
65.49/22.17	                                  
65.49/22.17	          [c_5](x1) = [1] x1 + [0]
65.49/22.17	                                  
65.49/22.17	          [c_6](x1) = [1] x1 + [0]
65.49/22.17	                                  
65.49/22.17	          [c_7](x1) = [1] x1 + [0]
65.49/22.17	                                  
65.49/22.17	          [c_8](x1) = [1] x1 + [0]
65.49/22.17	                                  
65.49/22.17	          [c_9](x1) = [1] x1 + [0]
65.49/22.17	  
65.49/22.17	  The order satisfies the following ordering constraints:
65.49/22.17	  
65.49/22.17	          [f_2^#(x)] =  [1]               
65.49/22.17	                     >  [0]               
65.49/22.17	                     =  [c_1()]           
65.49/22.17	                                          
65.49/22.17	          [f_3^#(x)] =  [3]               
65.49/22.17	                     >= [3]               
65.49/22.17	                     =  [c_2(g_3^#(x, x))]
65.49/22.17	                                          
65.49/22.17	    [g_3^#(s(x), y)] =  [2]               
65.49/22.17	                     >= [2]               
65.49/22.17	                     =  [c_3(f_2^#(y))]   
65.49/22.17	                                          
65.49/22.17	    [g_3^#(s(x), y)] =  [2]               
65.49/22.17	                     >= [2]               
65.49/22.17	                     =  [c_4(g_3^#(x, y))]
65.49/22.17	                                          
65.49/22.17	          [f_4^#(x)] =  [4]               
65.49/22.17	                     >= [4]               
65.49/22.17	                     =  [c_5(g_4^#(x, x))]
65.49/22.17	                                          
65.49/22.17	    [g_4^#(s(x), y)] =  [4]               
65.49/22.17	                     >  [3]               
65.49/22.17	                     =  [c_6(f_3^#(y))]   
65.49/22.17	                                          
65.49/22.17	    [g_4^#(s(x), y)] =  [4]               
65.49/22.17	                     >= [4]               
65.49/22.17	                     =  [c_7(g_4^#(x, y))]
65.49/22.17	                                          
65.49/22.17	    [g_5^#(s(x), y)] =  [4] y + [4]       
65.49/22.17	                     >= [4]               
65.49/22.17	                     =  [c_8(f_4^#(y))]   
65.49/22.17	                                          
65.49/22.17	    [g_5^#(s(x), y)] =  [4] y + [4]       
65.49/22.17	                     >= [4] y + [4]       
65.49/22.17	                     =  [c_9(g_5^#(x, y))]
65.49/22.17	                                          
65.49/22.17	
65.49/22.17	We return to the main proof. Consider the set of all dependency
65.49/22.17	pairs
65.49/22.17	
65.49/22.17	:
65.49/22.17	  { 1: f_2^#(x) -> c_1()
65.49/22.17	  , 2: f_3^#(x) -> c_2(g_3^#(x, x))
65.49/22.17	  , 3: g_3^#(s(x), y) -> c_3(f_2^#(y))
65.49/22.17	  , 4: g_3^#(s(x), y) -> c_4(g_3^#(x, y))
65.49/22.17	  , 5: f_4^#(x) -> c_5(g_4^#(x, x))
65.49/22.17	  , 6: g_4^#(s(x), y) -> c_6(f_3^#(y))
65.49/22.17	  , 7: g_4^#(s(x), y) -> c_7(g_4^#(x, y))
65.49/22.17	  , 8: g_5^#(s(x), y) -> c_8(f_4^#(y))
65.49/22.17	  , 9: g_5^#(s(x), y) -> c_9(g_5^#(x, y)) }
65.49/22.17	
65.49/22.17	Processor 'matrix interpretation of dimension 1' induces the
65.49/22.17	complexity certificate YES(?,O(1)) on application of dependency
65.49/22.17	pairs {1,6}. These cover all (indirect) predecessors of dependency
65.49/22.17	pairs {1,2,6}, their number of application is equally bounded. The
65.49/22.17	dependency pairs are shifted into the weak component.
65.49/22.17	
65.49/22.17	We are left with following problem, upon which TcT provides the
65.49/22.17	certificate YES(O(1),O(1)).
65.49/22.17	
65.49/22.17	Weak DPs:
65.49/22.17	  { f_2^#(x) -> c_1()
65.49/22.17	  , f_3^#(x) -> c_2(g_3^#(x, x))
65.49/22.17	  , g_3^#(s(x), y) -> c_3(f_2^#(y))
65.49/22.17	  , g_3^#(s(x), y) -> c_4(g_3^#(x, y))
65.49/22.17	  , f_4^#(x) -> c_5(g_4^#(x, x))
65.49/22.17	  , g_4^#(s(x), y) -> c_6(f_3^#(y))
65.49/22.17	  , g_4^#(s(x), y) -> c_7(g_4^#(x, y))
65.49/22.17	  , g_5^#(s(x), y) -> c_8(f_4^#(y))
65.49/22.17	  , g_5^#(s(x), y) -> c_9(g_5^#(x, y)) }
65.49/22.17	Obligation:
65.49/22.17	  runtime complexity
65.49/22.17	Answer:
65.49/22.17	  YES(O(1),O(1))
65.49/22.17	
65.49/22.17	The following weak DPs constitute a sub-graph of the DG that is
65.49/22.17	closed under successors. The DPs are removed.
65.49/22.17	
65.49/22.17	{ f_2^#(x) -> c_1()
65.49/22.17	, f_3^#(x) -> c_2(g_3^#(x, x))
65.49/22.17	, g_3^#(s(x), y) -> c_3(f_2^#(y))
65.49/22.17	, g_3^#(s(x), y) -> c_4(g_3^#(x, y))
65.49/22.17	, f_4^#(x) -> c_5(g_4^#(x, x))
65.49/22.17	, g_4^#(s(x), y) -> c_6(f_3^#(y))
65.49/22.17	, g_4^#(s(x), y) -> c_7(g_4^#(x, y))
65.49/22.17	, g_5^#(s(x), y) -> c_8(f_4^#(y))
65.49/22.17	, g_5^#(s(x), y) -> c_9(g_5^#(x, y)) }
65.49/22.17	
65.49/22.17	We are left with following problem, upon which TcT provides the
65.49/22.17	certificate YES(O(1),O(1)).
65.49/22.17	
65.49/22.17	Rules: Empty
65.49/22.17	Obligation:
65.49/22.17	  runtime complexity
65.49/22.17	Answer:
65.49/22.17	  YES(O(1),O(1))
65.49/22.17	
65.49/22.17	Empty rules are trivially bounded
65.49/22.17	
65.49/22.17	Hurray, we answered YES(O(1),O(n^5))
65.49/22.18	EOF