YES(O(1),O(n^1))
169.72/60.08	YES(O(1),O(n^1))
169.72/60.08	
169.72/60.08	We are left with following problem, upon which TcT provides the
169.72/60.08	certificate YES(O(1),O(n^1)).
169.72/60.08	
169.72/60.08	Strict Trs:
169.72/60.08	  { a(a(x1)) -> b(b(b(x1)))
169.72/60.08	  , b(x1) -> d(d(x1))
169.72/60.08	  , b(b(x1)) -> c(c(c(x1)))
169.72/60.08	  , c(c(x1)) -> d(d(d(x1)))
169.72/60.08	  , c(d(d(x1))) -> a(x1) }
169.72/60.08	Obligation:
169.72/60.08	  derivational complexity
169.72/60.08	Answer:
169.72/60.08	  YES(O(1),O(n^1))
169.72/60.08	
169.72/60.08	We use the processor 'matrix interpretation of dimension 1' to
169.72/60.08	orient following rules strictly.
169.72/60.08	
169.72/60.08	Trs:
169.72/60.08	  { b(x1) -> d(d(x1))
169.72/60.08	  , c(d(d(x1))) -> a(x1) }
169.72/60.08	
169.72/60.08	The induced complexity on above rules (modulo remaining rules) is
169.72/60.08	YES(?,O(n^1)) . These rules are moved into the corresponding weak
169.72/60.08	component(s).
169.72/60.08	
169.72/60.08	Sub-proof:
169.72/60.08	----------
169.72/60.08	  TcT has computed the following triangular matrix interpretation.
169.72/60.08	  
169.72/60.08	    [a](x1) = [1] x1 + [54]
169.72/60.08	                           
169.72/60.08	    [b](x1) = [1] x1 + [36]
169.72/60.08	                           
169.72/60.08	    [c](x1) = [1] x1 + [24]
169.72/60.08	                           
169.72/60.08	    [d](x1) = [1] x1 + [16]
169.72/60.08	  
169.72/60.08	  The order satisfies the following ordering constraints:
169.72/60.08	  
169.72/60.08	       [a(a(x1))] =  [1] x1 + [108]
169.72/60.08	                  >= [1] x1 + [108]
169.72/60.08	                  =  [b(b(b(x1)))] 
169.72/60.08	                                   
169.72/60.08	          [b(x1)] =  [1] x1 + [36] 
169.72/60.08	                  >  [1] x1 + [32] 
169.72/60.08	                  =  [d(d(x1))]    
169.72/60.08	                                   
169.72/60.08	       [b(b(x1))] =  [1] x1 + [72] 
169.72/60.08	                  >= [1] x1 + [72] 
169.72/60.08	                  =  [c(c(c(x1)))] 
169.72/60.08	                                   
169.72/60.08	       [c(c(x1))] =  [1] x1 + [48] 
169.72/60.08	                  >= [1] x1 + [48] 
169.72/60.08	                  =  [d(d(d(x1)))] 
169.72/60.08	                                   
169.72/60.08	    [c(d(d(x1)))] =  [1] x1 + [56] 
169.72/60.08	                  >  [1] x1 + [54] 
169.72/60.08	                  =  [a(x1)]       
169.72/60.08	                                   
169.72/60.08	
169.72/60.08	We return to the main proof.
169.72/60.08	
169.72/60.08	We are left with following problem, upon which TcT provides the
169.72/60.08	certificate YES(O(1),O(n^1)).
169.72/60.08	
169.72/60.08	Strict Trs:
169.72/60.08	  { a(a(x1)) -> b(b(b(x1)))
169.72/60.08	  , b(b(x1)) -> c(c(c(x1)))
169.72/60.08	  , c(c(x1)) -> d(d(d(x1))) }
169.72/60.08	Weak Trs:
169.72/60.08	  { b(x1) -> d(d(x1))
169.72/60.08	  , c(d(d(x1))) -> a(x1) }
169.72/60.08	Obligation:
169.72/60.08	  derivational complexity
169.72/60.08	Answer:
169.72/60.08	  YES(O(1),O(n^1))
169.72/60.08	
169.72/60.08	We use the processor 'matrix interpretation of dimension 1' to
169.72/60.08	orient following rules strictly.
169.72/60.08	
169.72/60.08	Trs: { c(c(x1)) -> d(d(d(x1))) }
169.72/60.08	
169.72/60.08	The induced complexity on above rules (modulo remaining rules) is
169.72/60.08	YES(?,O(n^1)) . These rules are moved into the corresponding weak
169.72/60.08	component(s).
169.72/60.08	
169.72/60.08	Sub-proof:
169.72/60.08	----------
169.72/60.08	  TcT has computed the following triangular matrix interpretation.
169.72/60.08	  
169.72/60.08	    [a](x1) = [1] x1 + [36]
169.72/60.08	                           
169.72/60.08	    [b](x1) = [1] x1 + [24]
169.72/60.08	                           
169.72/60.08	    [c](x1) = [1] x1 + [16]
169.72/60.08	                           
169.72/60.08	    [d](x1) = [1] x1 + [10]
169.72/60.08	  
169.72/60.08	  The order satisfies the following ordering constraints:
169.72/60.08	  
169.72/60.08	       [a(a(x1))] =  [1] x1 + [72]
169.72/60.08	                  >= [1] x1 + [72]
169.72/60.08	                  =  [b(b(b(x1)))]
169.72/60.08	                                  
169.72/60.08	          [b(x1)] =  [1] x1 + [24]
169.72/60.08	                  >  [1] x1 + [20]
169.72/60.08	                  =  [d(d(x1))]   
169.72/60.08	                                  
169.72/60.08	       [b(b(x1))] =  [1] x1 + [48]
169.72/60.08	                  >= [1] x1 + [48]
169.72/60.08	                  =  [c(c(c(x1)))]
169.72/60.08	                                  
169.72/60.08	       [c(c(x1))] =  [1] x1 + [32]
169.72/60.08	                  >  [1] x1 + [30]
169.72/60.08	                  =  [d(d(d(x1)))]
169.72/60.08	                                  
169.72/60.08	    [c(d(d(x1)))] =  [1] x1 + [36]
169.72/60.08	                  >= [1] x1 + [36]
169.72/60.08	                  =  [a(x1)]      
169.72/60.08	                                  
169.72/60.08	
169.72/60.08	We return to the main proof.
169.72/60.08	
169.72/60.08	We are left with following problem, upon which TcT provides the
169.72/60.08	certificate YES(O(1),O(n^1)).
169.72/60.08	
169.72/60.08	Strict Trs:
169.72/60.08	  { a(a(x1)) -> b(b(b(x1)))
169.72/60.08	  , b(b(x1)) -> c(c(c(x1))) }
169.72/60.08	Weak Trs:
169.72/60.08	  { b(x1) -> d(d(x1))
169.72/60.08	  , c(c(x1)) -> d(d(d(x1)))
169.72/60.08	  , c(d(d(x1))) -> a(x1) }
169.72/60.08	Obligation:
169.72/60.08	  derivational complexity
169.72/60.08	Answer:
169.72/60.08	  YES(O(1),O(n^1))
169.72/60.08	
169.72/60.08	We use the processor 'matrix interpretation of dimension 1' to
169.72/60.08	orient following rules strictly.
169.72/60.08	
169.72/60.08	Trs: { a(a(x1)) -> b(b(b(x1))) }
169.72/60.08	
169.72/60.08	The induced complexity on above rules (modulo remaining rules) is
169.72/60.08	YES(?,O(n^1)) . These rules are moved into the corresponding weak
169.72/60.08	component(s).
169.72/60.08	
169.72/60.08	Sub-proof:
169.72/60.08	----------
169.72/60.08	  TcT has computed the following triangular matrix interpretation.
169.72/60.08	  
169.72/60.08	    [a](x1) = [1] x1 + [14]
169.72/60.08	                           
169.72/60.08	    [b](x1) = [1] x1 + [9] 
169.72/60.08	                           
169.72/60.08	    [c](x1) = [1] x1 + [6] 
169.72/60.08	                           
169.72/60.08	    [d](x1) = [1] x1 + [4] 
169.72/60.08	  
169.72/60.08	  The order satisfies the following ordering constraints:
169.72/60.08	  
169.72/60.08	       [a(a(x1))] =  [1] x1 + [28]
169.72/60.08	                  >  [1] x1 + [27]
169.72/60.08	                  =  [b(b(b(x1)))]
169.72/60.08	                                  
169.72/60.08	          [b(x1)] =  [1] x1 + [9] 
169.72/60.08	                  >  [1] x1 + [8] 
169.72/60.08	                  =  [d(d(x1))]   
169.72/60.08	                                  
169.72/60.08	       [b(b(x1))] =  [1] x1 + [18]
169.72/60.08	                  >= [1] x1 + [18]
169.72/60.08	                  =  [c(c(c(x1)))]
169.72/60.08	                                  
169.72/60.08	       [c(c(x1))] =  [1] x1 + [12]
169.72/60.08	                  >= [1] x1 + [12]
169.72/60.08	                  =  [d(d(d(x1)))]
169.72/60.08	                                  
169.72/60.08	    [c(d(d(x1)))] =  [1] x1 + [14]
169.72/60.08	                  >= [1] x1 + [14]
169.72/60.08	                  =  [a(x1)]      
169.72/60.08	                                  
169.72/60.08	
169.72/60.08	We return to the main proof.
169.72/60.08	
169.72/60.08	We are left with following problem, upon which TcT provides the
169.72/60.08	certificate YES(O(1),O(n^1)).
169.72/60.08	
169.72/60.08	Strict Trs: { b(b(x1)) -> c(c(c(x1))) }
169.72/60.08	Weak Trs:
169.72/60.08	  { a(a(x1)) -> b(b(b(x1)))
169.72/60.08	  , b(x1) -> d(d(x1))
169.72/60.08	  , c(c(x1)) -> d(d(d(x1)))
169.72/60.08	  , c(d(d(x1))) -> a(x1) }
169.72/60.08	Obligation:
169.72/60.08	  derivational complexity
169.72/60.08	Answer:
169.72/60.08	  YES(O(1),O(n^1))
169.72/60.08	
169.72/60.08	We use the processor 'matrix interpretation of dimension 1' to
169.72/60.08	orient following rules strictly.
169.72/60.08	
169.72/60.08	Trs: { b(b(x1)) -> c(c(c(x1))) }
169.72/60.08	
169.72/60.08	The induced complexity on above rules (modulo remaining rules) is
169.72/60.08	YES(?,O(n^1)) . These rules are moved into the corresponding weak
169.72/60.08	component(s).
169.72/60.08	
169.72/60.08	Sub-proof:
169.72/60.08	----------
169.72/60.08	  TcT has computed the following triangular matrix interpretation.
169.72/60.08	  
169.72/60.08	    [a](x1) = [1] x1 + [21]
169.72/60.08	                           
169.72/60.08	    [b](x1) = [1] x1 + [14]
169.72/60.08	                           
169.72/60.08	    [c](x1) = [1] x1 + [9] 
169.72/60.08	                           
169.72/60.08	    [d](x1) = [1] x1 + [6] 
169.72/60.08	  
169.72/60.08	  The order satisfies the following ordering constraints:
169.72/60.08	  
169.72/60.08	       [a(a(x1))] =  [1] x1 + [42]
169.72/60.08	                  >= [1] x1 + [42]
169.72/60.08	                  =  [b(b(b(x1)))]
169.72/60.08	                                  
169.72/60.08	          [b(x1)] =  [1] x1 + [14]
169.72/60.08	                  >  [1] x1 + [12]
169.72/60.08	                  =  [d(d(x1))]   
169.72/60.08	                                  
169.72/60.08	       [b(b(x1))] =  [1] x1 + [28]
169.72/60.08	                  >  [1] x1 + [27]
169.72/60.08	                  =  [c(c(c(x1)))]
169.72/60.08	                                  
169.72/60.08	       [c(c(x1))] =  [1] x1 + [18]
169.72/60.08	                  >= [1] x1 + [18]
169.72/60.08	                  =  [d(d(d(x1)))]
169.72/60.08	                                  
169.72/60.08	    [c(d(d(x1)))] =  [1] x1 + [21]
169.72/60.08	                  >= [1] x1 + [21]
169.72/60.08	                  =  [a(x1)]      
169.72/60.08	                                  
169.72/60.08	
169.72/60.08	We return to the main proof.
169.72/60.08	
169.72/60.08	We are left with following problem, upon which TcT provides the
169.72/60.08	certificate YES(O(1),O(1)).
169.72/60.08	
169.72/60.08	Weak Trs:
169.72/60.08	  { a(a(x1)) -> b(b(b(x1)))
169.72/60.08	  , b(x1) -> d(d(x1))
169.72/60.08	  , b(b(x1)) -> c(c(c(x1)))
169.72/60.08	  , c(c(x1)) -> d(d(d(x1)))
169.72/60.08	  , c(d(d(x1))) -> a(x1) }
169.72/60.08	Obligation:
169.72/60.08	  derivational complexity
169.72/60.08	Answer:
169.72/60.08	  YES(O(1),O(1))
169.72/60.08	
169.72/60.08	Empty rules are trivially bounded
169.72/60.08	
169.72/60.08	Hurray, we answered YES(O(1),O(n^1))
169.97/60.13	EOF