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