YES(O(1),O(n^9))
1168.22/297.03	YES(O(1),O(n^9))
1168.22/297.03	
1168.22/297.03	We are left with following problem, upon which TcT provides the
1168.22/297.03	certificate YES(O(1),O(n^9)).
1168.22/297.03	
1168.22/297.03	Strict Trs:
1168.22/297.03	  { a(l(x1)) -> l(a(x1))
1168.22/297.03	  , r(a(a(x1))) -> a(a(r(x1)))
1168.22/297.03	  , r(b(x1)) -> l(b(x1))
1168.22/297.03	  , b(l(x1)) -> b(a(r(x1))) }
1168.22/297.03	Obligation:
1168.22/297.03	  derivational complexity
1168.22/297.03	Answer:
1168.22/297.03	  YES(O(1),O(n^9))
1168.22/297.03	
1168.22/297.03	We use the processor 'matrix interpretation of dimension 3' to
1168.22/297.03	orient following rules strictly.
1168.22/297.03	
1168.22/297.03	Trs:
1168.22/297.03	  { r(b(x1)) -> l(b(x1))
1168.22/297.03	  , b(l(x1)) -> b(a(r(x1))) }
1168.22/297.03	
1168.22/297.03	The induced complexity on above rules (modulo remaining rules) is
1168.22/297.03	YES(?,O(n^3)) . These rules are removed from the problem. Note that
1168.22/297.03	none of the weakly oriented rules is size-increasing. The overall
1168.22/297.03	complexity is obtained by composition .
1168.22/297.03	
1168.22/297.03	Sub-proof:
1168.22/297.03	----------
1168.22/297.03	  TcT has computed the following matrix interpretation satisfying
1168.22/297.03	  not(EDA).
1168.22/297.03	  
1168.22/297.03	              [1 0 0]      [0]
1168.22/297.03	    [a](x1) = [0 0 1] x1 + [0]
1168.22/297.03	              [0 1 0]      [0]
1168.22/297.03	                              
1168.22/297.03	              [1 0 0]      [1]
1168.22/297.03	    [l](x1) = [0 1 0] x1 + [0]
1168.22/297.03	              [0 0 1]      [0]
1168.22/297.03	                              
1168.22/297.03	              [1 0 2]      [0]
1168.22/297.03	    [r](x1) = [0 0 0] x1 + [0]
1168.22/297.03	              [0 0 1]      [0]
1168.22/297.03	                              
1168.22/297.03	              [1 0 4]      [0]
1168.22/297.03	    [b](x1) = [0 0 0] x1 + [0]
1168.22/297.03	              [0 0 0]      [4]
1168.22/297.03	  
1168.22/297.03	  The order satisfies the following ordering constraints:
1168.22/297.03	  
1168.22/297.03	       [a(l(x1))] =  [1 0 0]      [1]
1168.22/297.03	                     [0 0 1] x1 + [0]
1168.22/297.03	                     [0 1 0]      [0]
1168.22/297.03	                  >= [1 0 0]      [1]
1168.22/297.03	                     [0 0 1] x1 + [0]
1168.22/297.03	                     [0 1 0]      [0]
1168.22/297.03	                  =  [l(a(x1))]      
1168.22/297.03	                                     
1168.22/297.03	    [r(a(a(x1)))] =  [1 0 2]      [0]
1168.22/297.03	                     [0 0 0] x1 + [0]
1168.22/297.03	                     [0 0 1]      [0]
1168.22/297.03	                  >= [1 0 2]      [0]
1168.22/297.03	                     [0 0 0] x1 + [0]
1168.22/297.03	                     [0 0 1]      [0]
1168.22/297.03	                  =  [a(a(r(x1)))]   
1168.22/297.03	                                     
1168.22/297.03	       [r(b(x1))] =  [1 0 4]      [8]
1168.22/297.03	                     [0 0 0] x1 + [0]
1168.22/297.03	                     [0 0 0]      [4]
1168.22/297.03	                  >  [1 0 4]      [1]
1168.22/297.03	                     [0 0 0] x1 + [0]
1168.22/297.03	                     [0 0 0]      [4]
1168.22/297.03	                  =  [l(b(x1))]      
1168.22/297.03	                                     
1168.22/297.03	       [b(l(x1))] =  [1 0 4]      [1]
1168.22/297.03	                     [0 0 0] x1 + [0]
1168.22/297.03	                     [0 0 0]      [4]
1168.22/297.03	                  >  [1 0 2]      [0]
1168.22/297.03	                     [0 0 0] x1 + [0]
1168.22/297.03	                     [0 0 0]      [4]
1168.22/297.03	                  =  [b(a(r(x1)))]   
1168.22/297.03	                                     
1168.22/297.03	
1168.22/297.03	We return to the main proof.
1168.22/297.03	
1168.22/297.03	We are left with following problem, upon which TcT provides the
1168.22/297.03	certificate YES(O(1),O(n^2)).
1168.22/297.03	
1168.22/297.03	Strict Trs:
1168.22/297.03	  { a(l(x1)) -> l(a(x1))
1168.22/297.03	  , r(a(a(x1))) -> a(a(r(x1))) }
1168.22/297.03	Obligation:
1168.22/297.03	  derivational complexity
1168.22/297.03	Answer:
1168.22/297.03	  YES(O(1),O(n^2))
1168.22/297.03	
1168.22/297.03	We use the processor 'matrix interpretation of dimension 2' to
1168.22/297.03	orient following rules strictly.
1168.22/297.03	
1168.22/297.03	Trs:
1168.22/297.03	  { a(l(x1)) -> l(a(x1))
1168.22/297.03	  , r(a(a(x1))) -> a(a(r(x1))) }
1168.22/297.03	
1168.22/297.03	The induced complexity on above rules (modulo remaining rules) is
1168.22/297.03	YES(?,O(n^2)) . These rules are removed from the problem. Note that
1168.22/297.03	no rule is size-increasing. The overall complexity is obtained by
1168.22/297.03	multiplication .
1168.22/297.03	
1168.22/297.03	Sub-proof:
1168.22/297.03	----------
1168.22/297.03	  TcT has computed the following triangular matrix interpretation.
1168.22/297.03	  
1168.22/297.03	    [a](x1) = [1 1] x1 + [0]
1168.22/297.03	              [0 1]      [2]
1168.22/297.03	                            
1168.22/297.03	    [l](x1) = [1 0] x1 + [0]
1168.22/297.03	              [0 1]      [1]
1168.22/297.03	                            
1168.22/297.03	    [r](x1) = [1 1] x1 + [0]
1168.22/297.03	              [0 1]      [0]
1168.22/297.03	  
1168.22/297.03	  The order satisfies the following ordering constraints:
1168.22/297.03	  
1168.22/297.03	       [a(l(x1))] = [1 1] x1 + [1]
1168.22/297.03	                    [0 1]      [3]
1168.22/297.03	                  > [1 1] x1 + [0]
1168.22/297.03	                    [0 1]      [3]
1168.22/297.03	                  = [l(a(x1))]    
1168.22/297.03	                                  
1168.22/297.03	    [r(a(a(x1)))] = [1 3] x1 + [6]
1168.22/297.03	                    [0 1]      [4]
1168.22/297.03	                  > [1 3] x1 + [2]
1168.22/297.03	                    [0 1]      [4]
1168.22/297.03	                  = [a(a(r(x1)))] 
1168.22/297.03	                                  
1168.22/297.03	
1168.22/297.03	We return to the main proof.
1168.22/297.03	
1168.22/297.03	We are left with following problem, upon which TcT provides the
1168.22/297.03	certificate YES(O(1),O(1)).
1168.22/297.03	
1168.22/297.03	Rules: Empty
1168.22/297.03	Obligation:
1168.22/297.03	  derivational complexity
1168.22/297.03	Answer:
1168.22/297.03	  YES(O(1),O(1))
1168.22/297.03	
1168.22/297.03	Empty rules are trivially bounded
1168.22/297.03	
1168.22/297.03	Hurray, we answered YES(O(1),O(n^9))
1168.22/297.05	EOF