YES(O(1),O(n^1))
61.75/24.04	YES(O(1),O(n^1))
61.75/24.04	
61.75/24.04	We are left with following problem, upon which TcT provides the
61.75/24.04	certificate YES(O(1),O(n^1)).
61.75/24.04	
61.75/24.04	Strict Trs:
61.75/24.04	  { implies(x, or(y, z)) -> or(y, implies(x, z))
61.75/24.04	  , implies(not(x), y) -> or(x, y)
61.75/24.04	  , implies(not(x), or(y, z)) -> implies(y, or(x, z)) }
61.75/24.04	Obligation:
61.75/24.04	  innermost runtime complexity
61.75/24.04	Answer:
61.75/24.04	  YES(O(1),O(n^1))
61.75/24.04	
61.75/24.04	The weightgap principle applies (using the following nonconstant
61.75/24.04	growth matrix-interpretation)
61.75/24.04	
61.75/24.04	The following argument positions are usable:
61.75/24.04	  Uargs(or) = {2}
61.75/24.04	
61.75/24.04	TcT has computed the following matrix interpretation satisfying
61.75/24.04	not(EDA) and not(IDA(1)).
61.75/24.04	
61.75/24.04	  [implies](x1, x2) = [1] x1 + [1] x2 + [0]
61.75/24.04	                                           
61.75/24.04	          [not](x1) = [1] x1 + [4]         
61.75/24.04	                                           
61.75/24.04	       [or](x1, x2) = [1] x1 + [1] x2 + [0]
61.75/24.04	
61.75/24.04	The order satisfies the following ordering constraints:
61.75/24.04	
61.75/24.04	       [implies(x, or(y, z))] =  [1] x + [1] y + [1] z + [0]
61.75/24.04	                              >= [1] x + [1] y + [1] z + [0]
61.75/24.04	                              =  [or(y, implies(x, z))]     
61.75/24.04	                                                            
61.75/24.04	         [implies(not(x), y)] =  [1] x + [1] y + [4]        
61.75/24.04	                              >  [1] x + [1] y + [0]        
61.75/24.04	                              =  [or(x, y)]                 
61.75/24.04	                                                            
61.75/24.04	  [implies(not(x), or(y, z))] =  [1] x + [1] y + [1] z + [4]
61.75/24.04	                              >  [1] x + [1] y + [1] z + [0]
61.75/24.04	                              =  [implies(y, or(x, z))]     
61.75/24.04	                                                            
61.75/24.04	
61.75/24.04	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
61.75/24.04	
61.75/24.04	We are left with following problem, upon which TcT provides the
61.75/24.04	certificate YES(O(1),O(n^1)).
61.75/24.04	
61.75/24.04	Strict Trs: { implies(x, or(y, z)) -> or(y, implies(x, z)) }
61.75/24.04	Weak Trs:
61.75/24.04	  { implies(not(x), y) -> or(x, y)
61.75/24.04	  , implies(not(x), or(y, z)) -> implies(y, or(x, z)) }
61.75/24.04	Obligation:
61.75/24.04	  innermost runtime complexity
61.75/24.04	Answer:
61.75/24.04	  YES(O(1),O(n^1))
61.75/24.04	
61.75/24.04	We use the processor 'matrix interpretation of dimension 1' to
61.75/24.04	orient following rules strictly.
61.75/24.04	
61.75/24.04	Trs: { implies(x, or(y, z)) -> or(y, implies(x, z)) }
61.75/24.04	
61.75/24.04	The induced complexity on above rules (modulo remaining rules) is
61.75/24.04	YES(?,O(n^1)) . These rules are moved into the corresponding weak
61.75/24.04	component(s).
61.75/24.04	
61.75/24.04	Sub-proof:
61.75/24.04	----------
61.75/24.04	  The following argument positions are usable:
61.75/24.04	    Uargs(or) = {2}
61.75/24.04	  
61.75/24.04	  TcT has computed the following constructor-based matrix
61.75/24.04	  interpretation satisfying not(EDA).
61.75/24.04	  
61.75/24.04	    [implies](x1, x2) = [2] x1 + [2] x2 + [5]
61.75/24.04	                                             
61.75/24.04	            [not](x1) = [1] x1 + [2]         
61.75/24.04	                                             
61.75/24.04	         [or](x1, x2) = [1] x1 + [1] x2 + [2]
61.75/24.04	  
61.75/24.04	  The order satisfies the following ordering constraints:
61.75/24.04	  
61.75/24.04	         [implies(x, or(y, z))] = [2] x + [2] y + [2] z + [9] 
61.75/24.04	                                > [2] x + [1] y + [2] z + [7] 
61.75/24.04	                                = [or(y, implies(x, z))]      
61.75/24.04	                                                              
61.75/24.04	           [implies(not(x), y)] = [2] x + [2] y + [9]         
61.75/24.04	                                > [1] x + [1] y + [2]         
61.75/24.04	                                = [or(x, y)]                  
61.75/24.04	                                                              
61.75/24.04	    [implies(not(x), or(y, z))] = [2] x + [2] y + [2] z + [13]
61.75/24.04	                                > [2] x + [2] y + [2] z + [9] 
61.75/24.04	                                = [implies(y, or(x, z))]      
61.75/24.04	                                                              
61.75/24.04	
61.75/24.04	We return to the main proof.
61.75/24.04	
61.75/24.04	We are left with following problem, upon which TcT provides the
61.75/24.04	certificate YES(O(1),O(1)).
61.75/24.04	
61.75/24.04	Weak Trs:
61.75/24.04	  { implies(x, or(y, z)) -> or(y, implies(x, z))
61.75/24.04	  , implies(not(x), y) -> or(x, y)
61.75/24.04	  , implies(not(x), or(y, z)) -> implies(y, or(x, z)) }
61.75/24.04	Obligation:
61.75/24.04	  innermost runtime complexity
61.75/24.04	Answer:
61.75/24.04	  YES(O(1),O(1))
61.75/24.04	
61.75/24.04	Empty rules are trivially bounded
61.75/24.04	
61.75/24.04	Hurray, we answered YES(O(1),O(n^1))
61.75/24.05	EOF