YES(O(1),O(n^1))
0.00/0.57	YES(O(1),O(n^1))
0.00/0.57	
0.00/0.57	We are left with following problem, upon which TcT provides the
0.00/0.57	certificate YES(O(1),O(n^1)).
0.00/0.57	
0.00/0.57	Strict Trs:
0.00/0.57	  { or(x, true()) -> true()
0.00/0.57	  , or(true(), y) -> true()
0.00/0.57	  , or(false(), false()) -> false()
0.00/0.57	  , mem(x, nil()) -> false()
0.00/0.57	  , mem(x, set(y)) -> =(x, y)
0.00/0.57	  , mem(x, union(y, z)) -> or(mem(x, y), mem(x, z)) }
0.00/0.57	Obligation:
0.00/0.57	  runtime complexity
0.00/0.57	Answer:
0.00/0.57	  YES(O(1),O(n^1))
0.00/0.57	
0.00/0.57	The weightgap principle applies (using the following nonconstant
0.00/0.57	growth matrix-interpretation)
0.00/0.57	
0.00/0.57	The following argument positions are usable:
0.00/0.57	  Uargs(or) = {1, 2}
0.00/0.57	
0.00/0.57	TcT has computed the following matrix interpretation satisfying
0.00/0.57	not(EDA) and not(IDA(1)).
0.00/0.57	
0.00/0.57	     [or](x1, x2) = [1] x1 + [1] x2 + [7]
0.00/0.57	                                         
0.00/0.57	           [true] = [7]                  
0.00/0.57	                                         
0.00/0.57	          [false] = [3]                  
0.00/0.57	                                         
0.00/0.57	    [mem](x1, x2) = [1] x2 + [3]         
0.00/0.57	                                         
0.00/0.57	            [nil] = [7]                  
0.00/0.57	                                         
0.00/0.57	        [set](x1) = [1] x1 + [7]         
0.00/0.57	                                         
0.00/0.57	      [=](x1, x2) = [1] x2 + [1]         
0.00/0.57	                                         
0.00/0.57	  [union](x1, x2) = [1] x1 + [1] x2 + [7]
0.00/0.57	
0.00/0.57	The order satisfies the following ordering constraints:
0.00/0.57	
0.00/0.57	         [or(x, true())] = [1] x + [14]              
0.00/0.57	                         > [7]                       
0.00/0.57	                         = [true()]                  
0.00/0.57	                                                     
0.00/0.57	         [or(true(), y)] = [1] y + [14]              
0.00/0.57	                         > [7]                       
0.00/0.57	                         = [true()]                  
0.00/0.57	                                                     
0.00/0.57	  [or(false(), false())] = [13]                      
0.00/0.57	                         > [3]                       
0.00/0.57	                         = [false()]                 
0.00/0.57	                                                     
0.00/0.57	         [mem(x, nil())] = [10]                      
0.00/0.57	                         > [3]                       
0.00/0.57	                         = [false()]                 
0.00/0.57	                                                     
0.00/0.57	        [mem(x, set(y))] = [1] y + [10]              
0.00/0.57	                         > [1] y + [1]               
0.00/0.57	                         = [=(x, y)]                 
0.00/0.57	                                                     
0.00/0.57	   [mem(x, union(y, z))] = [1] y + [1] z + [10]      
0.00/0.57	                         ? [1] y + [1] z + [13]      
0.00/0.57	                         = [or(mem(x, y), mem(x, z))]
0.00/0.57	                                                     
0.00/0.57	
0.00/0.57	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.57	
0.00/0.57	We are left with following problem, upon which TcT provides the
0.00/0.57	certificate YES(O(1),O(n^1)).
0.00/0.57	
0.00/0.57	Strict Trs: { mem(x, union(y, z)) -> or(mem(x, y), mem(x, z)) }
0.00/0.57	Weak Trs:
0.00/0.57	  { or(x, true()) -> true()
0.00/0.57	  , or(true(), y) -> true()
0.00/0.57	  , or(false(), false()) -> false()
0.00/0.57	  , mem(x, nil()) -> false()
0.00/0.57	  , mem(x, set(y)) -> =(x, y) }
0.00/0.57	Obligation:
0.00/0.57	  runtime complexity
0.00/0.57	Answer:
0.00/0.57	  YES(O(1),O(n^1))
0.00/0.57	
0.00/0.57	The weightgap principle applies (using the following nonconstant
0.00/0.57	growth matrix-interpretation)
0.00/0.57	
0.00/0.57	The following argument positions are usable:
0.00/0.57	  Uargs(or) = {1, 2}
0.00/0.57	
0.00/0.57	TcT has computed the following matrix interpretation satisfying
0.00/0.57	not(EDA) and not(IDA(1)).
0.00/0.57	
0.00/0.57	     [or](x1, x2) = [1] x1 + [1] x2 + [0]
0.00/0.57	                                         
0.00/0.57	           [true] = [7]                  
0.00/0.57	                                         
0.00/0.57	          [false] = [4]                  
0.00/0.57	                                         
0.00/0.57	    [mem](x1, x2) = [1] x2 + [0]         
0.00/0.57	                                         
0.00/0.57	            [nil] = [7]                  
0.00/0.57	                                         
0.00/0.57	        [set](x1) = [1] x1 + [7]         
0.00/0.57	                                         
0.00/0.57	      [=](x1, x2) = [1] x2 + [7]         
0.00/0.57	                                         
0.00/0.57	  [union](x1, x2) = [1] x1 + [1] x2 + [7]
0.00/0.57	
0.00/0.57	The order satisfies the following ordering constraints:
0.00/0.57	
0.00/0.57	         [or(x, true())] =  [1] x + [7]               
0.00/0.57	                         >= [7]                       
0.00/0.57	                         =  [true()]                  
0.00/0.57	                                                      
0.00/0.57	         [or(true(), y)] =  [1] y + [7]               
0.00/0.57	                         >= [7]                       
0.00/0.57	                         =  [true()]                  
0.00/0.57	                                                      
0.00/0.57	  [or(false(), false())] =  [8]                       
0.00/0.57	                         >  [4]                       
0.00/0.57	                         =  [false()]                 
0.00/0.57	                                                      
0.00/0.57	         [mem(x, nil())] =  [7]                       
0.00/0.57	                         >  [4]                       
0.00/0.57	                         =  [false()]                 
0.00/0.57	                                                      
0.00/0.57	        [mem(x, set(y))] =  [1] y + [7]               
0.00/0.57	                         >= [1] y + [7]               
0.00/0.57	                         =  [=(x, y)]                 
0.00/0.57	                                                      
0.00/0.57	   [mem(x, union(y, z))] =  [1] y + [1] z + [7]       
0.00/0.57	                         >  [1] y + [1] z + [0]       
0.00/0.57	                         =  [or(mem(x, y), mem(x, z))]
0.00/0.57	                                                      
0.00/0.57	
0.00/0.57	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.57	
0.00/0.57	We are left with following problem, upon which TcT provides the
0.00/0.57	certificate YES(O(1),O(1)).
0.00/0.57	
0.00/0.57	Weak Trs:
0.00/0.57	  { or(x, true()) -> true()
0.00/0.57	  , or(true(), y) -> true()
0.00/0.57	  , or(false(), false()) -> false()
0.00/0.57	  , mem(x, nil()) -> false()
0.00/0.57	  , mem(x, set(y)) -> =(x, y)
0.00/0.57	  , mem(x, union(y, z)) -> or(mem(x, y), mem(x, z)) }
0.00/0.57	Obligation:
0.00/0.57	  runtime complexity
0.00/0.57	Answer:
0.00/0.57	  YES(O(1),O(1))
0.00/0.57	
0.00/0.57	Empty rules are trivially bounded
0.00/0.57	
0.00/0.57	Hurray, we answered YES(O(1),O(n^1))
0.00/0.58	EOF