YES(O(1),O(1))
0.00/0.04	YES(O(1),O(1))
0.00/0.04	
0.00/0.04	We are left with following problem, upon which TcT provides the
0.00/0.04	certificate YES(O(1),O(1)).
0.00/0.04	
0.00/0.04	Strict Trs:
0.00/0.04	  { not(x) -> xor(x, true())
0.00/0.04	  , implies(x, y) -> xor(and(x, y), xor(x, true()))
0.00/0.04	  , or(x, y) -> xor(and(x, y), xor(x, y))
0.00/0.04	  , =(x, y) -> xor(x, xor(y, true())) }
0.00/0.04	Obligation:
0.00/0.04	  innermost runtime complexity
0.00/0.04	Answer:
0.00/0.04	  YES(O(1),O(1))
0.00/0.04	
0.00/0.04	We add the following weak dependency pairs:
0.00/0.04	
0.00/0.04	Strict DPs:
0.00/0.04	  { not^#(x) -> c_1()
0.00/0.04	  , implies^#(x, y) -> c_2()
0.00/0.04	  , or^#(x, y) -> c_3()
0.00/0.04	  , =^#(x, y) -> c_4() }
0.00/0.04	
0.00/0.04	and mark the set of starting terms.
0.00/0.04	
0.00/0.04	We are left with following problem, upon which TcT provides the
0.00/0.04	certificate YES(O(1),O(1)).
0.00/0.04	
0.00/0.04	Strict DPs:
0.00/0.04	  { not^#(x) -> c_1()
0.00/0.04	  , implies^#(x, y) -> c_2()
0.00/0.04	  , or^#(x, y) -> c_3()
0.00/0.04	  , =^#(x, y) -> c_4() }
0.00/0.04	Strict Trs:
0.00/0.04	  { not(x) -> xor(x, true())
0.00/0.04	  , implies(x, y) -> xor(and(x, y), xor(x, true()))
0.00/0.04	  , or(x, y) -> xor(and(x, y), xor(x, y))
0.00/0.04	  , =(x, y) -> xor(x, xor(y, true())) }
0.00/0.04	Obligation:
0.00/0.04	  innermost runtime complexity
0.00/0.04	Answer:
0.00/0.04	  YES(O(1),O(1))
0.00/0.04	
0.00/0.04	No rule is usable, rules are removed from the input problem.
0.00/0.04	
0.00/0.04	We are left with following problem, upon which TcT provides the
0.00/0.04	certificate YES(O(1),O(1)).
0.00/0.04	
0.00/0.04	Strict DPs:
0.00/0.04	  { not^#(x) -> c_1()
0.00/0.04	  , implies^#(x, y) -> c_2()
0.00/0.04	  , or^#(x, y) -> c_3()
0.00/0.04	  , =^#(x, y) -> c_4() }
0.00/0.04	Obligation:
0.00/0.04	  innermost runtime complexity
0.00/0.04	Answer:
0.00/0.04	  YES(O(1),O(1))
0.00/0.04	
0.00/0.04	The weightgap principle applies (using the following constant
0.00/0.04	growth matrix-interpretation)
0.00/0.04	
0.00/0.04	The following argument positions are usable:
0.00/0.04	  none
0.00/0.04	
0.00/0.04	TcT has computed the following constructor-restricted matrix
0.00/0.04	interpretation.
0.00/0.04	
0.00/0.04	          [not^#](x1) = [2]
0.00/0.04	                        [1]
0.00/0.04	                           
0.00/0.04	                [c_1] = [1]
0.00/0.04	                        [1]
0.00/0.04	                           
0.00/0.04	  [implies^#](x1, x2) = [1]
0.00/0.04	                        [2]
0.00/0.04	                           
0.00/0.04	                [c_2] = [0]
0.00/0.04	                        [2]
0.00/0.04	                           
0.00/0.04	       [or^#](x1, x2) = [1]
0.00/0.04	                        [1]
0.00/0.04	                           
0.00/0.04	                [c_3] = [0]
0.00/0.04	                        [1]
0.00/0.04	                           
0.00/0.04	        [=^#](x1, x2) = [1]
0.00/0.04	                        [2]
0.00/0.04	                           
0.00/0.04	                [c_4] = [0]
0.00/0.04	                        [1]
0.00/0.04	
0.00/0.04	The order satisfies the following ordering constraints:
0.00/0.04	
0.00/0.04	         [not^#(x)] = [2]    
0.00/0.04	                      [1]    
0.00/0.04	                    > [1]    
0.00/0.04	                      [1]    
0.00/0.04	                    = [c_1()]
0.00/0.04	                             
0.00/0.04	  [implies^#(x, y)] = [1]    
0.00/0.04	                      [2]    
0.00/0.04	                    > [0]    
0.00/0.04	                      [2]    
0.00/0.04	                    = [c_2()]
0.00/0.04	                             
0.00/0.04	       [or^#(x, y)] = [1]    
0.00/0.04	                      [1]    
0.00/0.04	                    > [0]    
0.00/0.04	                      [1]    
0.00/0.04	                    = [c_3()]
0.00/0.04	                             
0.00/0.04	        [=^#(x, y)] = [1]    
0.00/0.04	                      [2]    
0.00/0.04	                    > [0]    
0.00/0.04	                      [1]    
0.00/0.04	                    = [c_4()]
0.00/0.04	                             
0.00/0.04	
0.00/0.04	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.04	
0.00/0.04	We are left with following problem, upon which TcT provides the
0.00/0.04	certificate YES(O(1),O(1)).
0.00/0.04	
0.00/0.04	Weak DPs:
0.00/0.04	  { not^#(x) -> c_1()
0.00/0.04	  , implies^#(x, y) -> c_2()
0.00/0.04	  , or^#(x, y) -> c_3()
0.00/0.04	  , =^#(x, y) -> c_4() }
0.00/0.04	Obligation:
0.00/0.04	  innermost runtime complexity
0.00/0.04	Answer:
0.00/0.04	  YES(O(1),O(1))
0.00/0.04	
0.00/0.04	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.04	closed under successors. The DPs are removed.
0.00/0.04	
0.00/0.04	{ not^#(x) -> c_1()
0.00/0.04	, implies^#(x, y) -> c_2()
0.00/0.04	, or^#(x, y) -> c_3()
0.00/0.04	, =^#(x, y) -> c_4() }
0.00/0.04	
0.00/0.04	We are left with following problem, upon which TcT provides the
0.00/0.04	certificate YES(O(1),O(1)).
0.00/0.04	
0.00/0.04	Rules: Empty
0.00/0.04	Obligation:
0.00/0.04	  innermost runtime complexity
0.00/0.04	Answer:
0.00/0.04	  YES(O(1),O(1))
0.00/0.04	
0.00/0.04	Empty rules are trivially bounded
0.00/0.04	
0.00/0.04	Hurray, we answered YES(O(1),O(1))
0.00/0.04	EOF