YES(O(1),O(n^3))
145.57/60.07	YES(O(1),O(n^3))
145.57/60.07	
145.57/60.07	We are left with following problem, upon which TcT provides the
145.57/60.07	certificate YES(O(1),O(n^3)).
145.57/60.07	
145.57/60.07	Strict Trs:
145.57/60.07	  { b(x, y) -> c(a(c(y), a(0(), x)))
145.57/60.07	  , a(y, x) -> y
145.57/60.07	  , a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()) }
145.57/60.07	Obligation:
145.57/60.07	  derivational complexity
145.57/60.07	Answer:
145.57/60.07	  YES(O(1),O(n^3))
145.57/60.07	
145.57/60.07	The weightgap principle applies (using the following nonconstant
145.57/60.07	growth matrix-interpretation)
145.57/60.07	
145.57/60.07	TcT has computed the following triangular matrix interpretation.
145.57/60.07	Note that the diagonal of the component-wise maxima of
145.57/60.07	interpretation-entries contains no more than 1 non-zero entries.
145.57/60.07	
145.57/60.07	  [b](x1, x2) = [1] x1 + [1] x2 + [1]
145.57/60.07	                                     
145.57/60.07	      [c](x1) = [1] x1 + [0]         
145.57/60.07	                                     
145.57/60.07	  [a](x1, x2) = [1] x1 + [1] x2 + [2]
145.57/60.07	                                     
145.57/60.07	          [0] = [0]                  
145.57/60.07	
145.57/60.07	The order satisfies the following ordering constraints:
145.57/60.07	
145.57/60.07	                     [b(x, y)] = [1] x + [1] y + [1]         
145.57/60.07	                               ? [1] x + [1] y + [4]         
145.57/60.07	                               = [c(a(c(y), a(0(), x)))]     
145.57/60.07	                                                             
145.57/60.07	                     [a(y, x)] = [1] x + [1] y + [2]         
145.57/60.07	                               > [1] y + [0]                 
145.57/60.07	                               = [y]                         
145.57/60.07	                                                             
145.57/60.07	  [a(y, c(b(a(0(), x), 0())))] = [1] x + [1] y + [5]         
145.57/60.07	                               > [1] x + [1] y + [4]         
145.57/60.07	                               = [b(a(c(b(0(), y)), x), 0())]
145.57/60.07	                                                             
145.57/60.07	
145.57/60.07	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
145.57/60.07	
145.57/60.07	We are left with following problem, upon which TcT provides the
145.57/60.07	certificate YES(O(1),O(n^3)).
145.57/60.07	
145.57/60.07	Strict Trs: { b(x, y) -> c(a(c(y), a(0(), x))) }
145.57/60.07	Weak Trs:
145.57/60.07	  { a(y, x) -> y
145.57/60.07	  , a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()) }
145.57/60.07	Obligation:
145.57/60.07	  derivational complexity
145.57/60.07	Answer:
145.57/60.07	  YES(O(1),O(n^3))
145.57/60.07	
145.57/60.07	We use the processor 'matrix interpretation of dimension 3' to
145.57/60.07	orient following rules strictly.
145.57/60.07	
145.57/60.07	Trs: { b(x, y) -> c(a(c(y), a(0(), x))) }
145.57/60.07	
145.57/60.07	The induced complexity on above rules (modulo remaining rules) is
145.57/60.07	YES(?,O(n^3)) . These rules are moved into the corresponding weak
145.57/60.07	component(s).
145.57/60.07	
145.57/60.07	Sub-proof:
145.57/60.07	----------
145.57/60.07	  TcT has computed the following triangular matrix interpretation.
145.57/60.07	  
145.57/60.07	                  [1 1 0]      [1 0 0]      [1]
145.57/60.07	    [b](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
145.57/60.07	                  [0 0 0]      [0 0 0]      [0]
145.57/60.07	                                               
145.57/60.07	                  [1 0 0]      [0]             
145.57/60.07	        [c](x1) = [0 0 0] x1 + [0]             
145.57/60.07	                  [0 0 0]      [0]             
145.57/60.07	                                               
145.57/60.07	                  [1 0 0]      [1 0 0]      [0]
145.57/60.07	    [a](x1, x2) = [0 1 2] x1 + [0 0 0] x2 + [0]
145.57/60.07	                  [0 0 1]      [0 0 0]      [0]
145.57/60.07	                                               
145.57/60.07	                  [0]                          
145.57/60.07	            [0] = [0]                          
145.57/60.07	                  [1]                          
145.57/60.07	  
145.57/60.07	  The order satisfies the following ordering constraints:
145.57/60.07	  
145.57/60.07	                       [b(x, y)] =  [1 1 0]     [1 0 0]     [1] 
145.57/60.07	                                    [0 0 0] x + [0 0 0] y + [0] 
145.57/60.07	                                    [0 0 0]     [0 0 0]     [0] 
145.57/60.07	                                 >  [1 0 0]     [1 0 0]     [0] 
145.57/60.07	                                    [0 0 0] x + [0 0 0] y + [0] 
145.57/60.07	                                    [0 0 0]     [0 0 0]     [0] 
145.57/60.07	                                 =  [c(a(c(y), a(0(), x)))]     
145.57/60.07	                                                                
145.57/60.07	                       [a(y, x)] =  [1 0 0]     [1 0 0]     [0] 
145.57/60.07	                                    [0 0 0] x + [0 1 2] y + [0] 
145.57/60.07	                                    [0 0 0]     [0 0 1]     [0] 
145.57/60.07	                                 >= [1 0 0]     [0]             
145.57/60.07	                                    [0 1 0] y + [0]             
145.57/60.07	                                    [0 0 1]     [0]             
145.57/60.07	                                 =  [y]                         
145.57/60.07	                                                                
145.57/60.07	    [a(y, c(b(a(0(), x), 0())))] =  [1 0 0]     [1 0 0]     [3] 
145.57/60.07	                                    [0 0 0] x + [0 1 2] y + [0] 
145.57/60.07	                                    [0 0 0]     [0 0 1]     [0] 
145.57/60.07	                                 >  [1 0 0]     [1 0 0]     [2] 
145.57/60.07	                                    [0 0 0] x + [0 0 0] y + [0] 
145.57/60.07	                                    [0 0 0]     [0 0 0]     [0] 
145.57/60.07	                                 =  [b(a(c(b(0(), y)), x), 0())]
145.57/60.07	                                                                
145.57/60.07	
145.57/60.07	We return to the main proof.
145.57/60.07	
145.57/60.07	We are left with following problem, upon which TcT provides the
145.57/60.07	certificate YES(O(1),O(1)).
145.57/60.07	
145.57/60.07	Weak Trs:
145.57/60.07	  { b(x, y) -> c(a(c(y), a(0(), x)))
145.57/60.07	  , a(y, x) -> y
145.57/60.07	  , a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()) }
145.57/60.07	Obligation:
145.57/60.07	  derivational complexity
145.57/60.07	Answer:
145.57/60.07	  YES(O(1),O(1))
145.57/60.07	
145.57/60.07	Empty rules are trivially bounded
145.57/60.07	
145.57/60.07	Hurray, we answered YES(O(1),O(n^3))
145.57/60.07	EOF