YES(O(1),O(1)) 0.00/0.14 YES(O(1),O(1)) 0.00/0.14 0.00/0.14 We are left with following problem, upon which TcT provides the 0.00/0.14 certificate YES(O(1),O(1)). 0.00/0.14 0.00/0.14 Strict Trs: 0.00/0.14 { not(x) -> xor(x, true()) 0.00/0.14 , implies(x, y) -> xor(and(x, y), xor(x, true())) 0.00/0.14 , or(x, y) -> xor(and(x, y), xor(x, y)) 0.00/0.14 , =(x, y) -> xor(x, xor(y, true())) } 0.00/0.14 Obligation: 0.00/0.14 runtime complexity 0.00/0.14 Answer: 0.00/0.14 YES(O(1),O(1)) 0.00/0.14 0.00/0.14 We add the following weak dependency pairs: 0.00/0.14 0.00/0.14 Strict DPs: 0.00/0.14 { not^#(x) -> c_1(x) 0.00/0.14 , implies^#(x, y) -> c_2(x, y, x) 0.00/0.14 , or^#(x, y) -> c_3(x, y, x, y) 0.00/0.14 , =^#(x, y) -> c_4(x, y) } 0.00/0.14 0.00/0.14 and mark the set of starting terms. 0.00/0.14 0.00/0.14 We are left with following problem, upon which TcT provides the 0.00/0.14 certificate YES(O(1),O(1)). 0.00/0.14 0.00/0.14 Strict DPs: 0.00/0.14 { not^#(x) -> c_1(x) 0.00/0.14 , implies^#(x, y) -> c_2(x, y, x) 0.00/0.14 , or^#(x, y) -> c_3(x, y, x, y) 0.00/0.14 , =^#(x, y) -> c_4(x, y) } 0.00/0.14 Strict Trs: 0.00/0.14 { not(x) -> xor(x, true()) 0.00/0.14 , implies(x, y) -> xor(and(x, y), xor(x, true())) 0.00/0.14 , or(x, y) -> xor(and(x, y), xor(x, y)) 0.00/0.14 , =(x, y) -> xor(x, xor(y, true())) } 0.00/0.14 Obligation: 0.00/0.14 runtime complexity 0.00/0.14 Answer: 0.00/0.14 YES(O(1),O(1)) 0.00/0.14 0.00/0.14 No rule is usable, rules are removed from the input problem. 0.00/0.14 0.00/0.14 We are left with following problem, upon which TcT provides the 0.00/0.14 certificate YES(O(1),O(1)). 0.00/0.14 0.00/0.14 Strict DPs: 0.00/0.14 { not^#(x) -> c_1(x) 0.00/0.14 , implies^#(x, y) -> c_2(x, y, x) 0.00/0.14 , or^#(x, y) -> c_3(x, y, x, y) 0.00/0.14 , =^#(x, y) -> c_4(x, y) } 0.00/0.14 Obligation: 0.00/0.14 runtime complexity 0.00/0.14 Answer: 0.00/0.14 YES(O(1),O(1)) 0.00/0.14 0.00/0.14 The weightgap principle applies (using the following constant 0.00/0.14 growth matrix-interpretation) 0.00/0.14 0.00/0.14 The following argument positions are usable: 0.00/0.14 none 0.00/0.14 0.00/0.14 TcT has computed the following constructor-restricted matrix 0.00/0.14 interpretation. 0.00/0.14 0.00/0.14 [not^#](x1) = [1 1] x1 + [1] 0.00/0.14 [1 1] [1] 0.00/0.14 0.00/0.14 [c_1](x1) = [1 1] x1 + [0] 0.00/0.14 [1 1] [1] 0.00/0.14 0.00/0.14 [implies^#](x1, x2) = [2 2] x1 + [1 1] x2 + [1] 0.00/0.14 [2 1] [1 1] [1] 0.00/0.14 0.00/0.14 [c_2](x1, x2, x3) = [1 1] x1 + [1 1] x2 + [1 1] x3 + [0] 0.00/0.14 [1 2] [1 1] [2 1] [1] 0.00/0.14 0.00/0.14 [or^#](x1, x2) = [2 2] x1 + [1 2] x2 + [1] 0.00/0.14 [1 2] [2 1] [1] 0.00/0.14 0.00/0.14 [c_3](x1, x2, x3, x4) = [1 1] x1 + [0 1] x2 + [1 1] x3 + [1 0.00/0.14 1] x4 + [0] 0.00/0.14 [2 2] [2 2] [1 1] [2 0.00/0.14 2] [1] 0.00/0.14 0.00/0.14 [=^#](x1, x2) = [1 1] x1 + [1 1] x2 + [2] 0.00/0.14 [1 1] [1 1] [1] 0.00/0.14 0.00/0.14 [c_4](x1, x2) = [1 1] x1 + [1 1] x2 + [1] 0.00/0.14 [1 1] [1 1] [1] 0.00/0.14 0.00/0.14 The order satisfies the following ordering constraints: 0.00/0.14 0.00/0.14 [not^#(x)] = [1 1] x + [1] 0.00/0.14 [1 1] [1] 0.00/0.14 > [1 1] x + [0] 0.00/0.14 [1 1] [1] 0.00/0.14 = [c_1(x)] 0.00/0.14 0.00/0.14 [implies^#(x, y)] = [2 2] x + [1 1] y + [1] 0.00/0.14 [2 1] [1 1] [1] 0.00/0.14 ? [2 2] x + [1 1] y + [0] 0.00/0.14 [3 3] [1 1] [1] 0.00/0.14 = [c_2(x, y, x)] 0.00/0.14 0.00/0.14 [or^#(x, y)] = [2 2] x + [1 2] y + [1] 0.00/0.14 [1 2] [2 1] [1] 0.00/0.14 ? [2 2] x + [1 2] y + [0] 0.00/0.14 [3 3] [4 4] [1] 0.00/0.14 = [c_3(x, y, x, y)] 0.00/0.14 0.00/0.14 [=^#(x, y)] = [1 1] x + [1 1] y + [2] 0.00/0.14 [1 1] [1 1] [1] 0.00/0.14 > [1 1] x + [1 1] y + [1] 0.00/0.14 [1 1] [1 1] [1] 0.00/0.14 = [c_4(x, y)] 0.00/0.14 0.00/0.14 0.00/0.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.14 0.00/0.14 We are left with following problem, upon which TcT provides the 0.00/0.14 certificate YES(O(1),O(1)). 0.00/0.14 0.00/0.14 Strict DPs: 0.00/0.14 { implies^#(x, y) -> c_2(x, y, x) 0.00/0.14 , or^#(x, y) -> c_3(x, y, x, y) } 0.00/0.14 Weak DPs: 0.00/0.14 { not^#(x) -> c_1(x) 0.00/0.14 , =^#(x, y) -> c_4(x, y) } 0.00/0.14 Obligation: 0.00/0.14 runtime complexity 0.00/0.14 Answer: 0.00/0.14 YES(O(1),O(1)) 0.00/0.14 0.00/0.14 We use the processor 'matrix interpretation of dimension 1' to 0.00/0.14 orient following rules strictly. 0.00/0.14 0.00/0.14 DPs: 0.00/0.14 { 1: implies^#(x, y) -> c_2(x, y, x) 0.00/0.14 , 2: or^#(x, y) -> c_3(x, y, x, y) 0.00/0.14 , 3: not^#(x) -> c_1(x) 0.00/0.14 , 4: =^#(x, y) -> c_4(x, y) } 0.00/0.14 0.00/0.14 Sub-proof: 0.00/0.14 ---------- 0.00/0.14 The following argument positions are usable: 0.00/0.14 none 0.00/0.14 0.00/0.14 TcT has computed the following constructor-restricted matrix 0.00/0.14 interpretation. Note that the diagonal of the component-wise maxima 0.00/0.14 of interpretation-entries (of constructors) contains no more than 0 0.00/0.14 non-zero entries. 0.00/0.14 0.00/0.14 [not^#](x1) = [7] x1 + [7] 0.00/0.14 0.00/0.14 [c_1](x1) = [7] x1 + [3] 0.00/0.14 0.00/0.14 [implies^#](x1, x2) = [7] x1 + [7] x2 + [7] 0.00/0.14 0.00/0.14 [c_2](x1, x2, x3) = [3] x1 + [7] x2 + [3] x3 + [3] 0.00/0.14 0.00/0.14 [or^#](x1, x2) = [7] x1 + [7] x2 + [7] 0.00/0.14 0.00/0.14 [c_3](x1, x2, x3, x4) = [3] x1 + [3] x2 + [3] x3 + [3] x4 + [3] 0.00/0.14 0.00/0.14 [=^#](x1, x2) = [7] x1 + [7] x2 + [7] 0.00/0.14 0.00/0.14 [c_4](x1, x2) = [7] x1 + [7] x2 + [3] 0.00/0.14 0.00/0.14 The order satisfies the following ordering constraints: 0.00/0.14 0.00/0.14 [not^#(x)] = [7] x + [7] 0.00/0.14 > [7] x + [3] 0.00/0.14 = [c_1(x)] 0.00/0.14 0.00/0.14 [implies^#(x, y)] = [7] x + [7] y + [7] 0.00/0.14 > [6] x + [7] y + [3] 0.00/0.14 = [c_2(x, y, x)] 0.00/0.14 0.00/0.14 [or^#(x, y)] = [7] x + [7] y + [7] 0.00/0.14 > [6] x + [6] y + [3] 0.00/0.14 = [c_3(x, y, x, y)] 0.00/0.14 0.00/0.14 [=^#(x, y)] = [7] x + [7] y + [7] 0.00/0.14 > [7] x + [7] y + [3] 0.00/0.14 = [c_4(x, y)] 0.00/0.14 0.00/0.14 0.00/0.14 The strictly oriented rules are moved into the weak component. 0.00/0.14 0.00/0.14 We are left with following problem, upon which TcT provides the 0.00/0.14 certificate YES(O(1),O(1)). 0.00/0.14 0.00/0.14 Weak DPs: 0.00/0.14 { not^#(x) -> c_1(x) 0.00/0.14 , implies^#(x, y) -> c_2(x, y, x) 0.00/0.14 , or^#(x, y) -> c_3(x, y, x, y) 0.00/0.14 , =^#(x, y) -> c_4(x, y) } 0.00/0.14 Obligation: 0.00/0.14 runtime complexity 0.00/0.14 Answer: 0.00/0.14 YES(O(1),O(1)) 0.00/0.14 0.00/0.14 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.14 closed under successors. The DPs are removed. 0.00/0.14 0.00/0.14 { not^#(x) -> c_1(x) 0.00/0.14 , implies^#(x, y) -> c_2(x, y, x) 0.00/0.14 , or^#(x, y) -> c_3(x, y, x, y) 0.00/0.14 , =^#(x, y) -> c_4(x, y) } 0.00/0.14 0.00/0.14 We are left with following problem, upon which TcT provides the 0.00/0.14 certificate YES(O(1),O(1)). 0.00/0.14 0.00/0.14 Rules: Empty 0.00/0.14 Obligation: 0.00/0.14 runtime complexity 0.00/0.14 Answer: 0.00/0.14 YES(O(1),O(1)) 0.00/0.14 0.00/0.14 Empty rules are trivially bounded 0.00/0.14 0.00/0.14 Hurray, we answered YES(O(1),O(1)) 0.00/0.14 EOF