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