YES(O(1),O(n^1)) 263.89/94.58 YES(O(1),O(n^1)) 263.89/94.58 263.89/94.58 We are left with following problem, upon which TcT provides the 263.89/94.58 certificate YES(O(1),O(n^1)). 263.89/94.58 263.89/94.58 Strict Trs: 263.89/94.58 { b(y, z) -> f(c(c(y, z, z), a(), a())) 263.89/94.58 , b(b(z, y), a()) -> z 263.89/94.58 , c(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c(f(b(x, z)), c(z, y, a()), a()) } 263.89/94.58 Obligation: 263.89/94.58 innermost runtime complexity 263.89/94.58 Answer: 263.89/94.58 YES(O(1),O(n^1)) 263.89/94.58 263.89/94.58 Arguments of following rules are not normal-forms: 263.89/94.58 263.89/94.58 { b(b(z, y), a()) -> z } 263.89/94.58 263.89/94.58 All above mentioned rules can be savely removed. 263.89/94.58 263.89/94.58 We are left with following problem, upon which TcT provides the 263.89/94.58 certificate YES(O(1),O(n^1)). 263.89/94.58 263.89/94.58 Strict Trs: 263.89/94.58 { b(y, z) -> f(c(c(y, z, z), a(), a())) 263.89/94.58 , c(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c(f(b(x, z)), c(z, y, a()), a()) } 263.89/94.58 Obligation: 263.89/94.58 innermost runtime complexity 263.89/94.58 Answer: 263.89/94.58 YES(O(1),O(n^1)) 263.89/94.58 263.89/94.58 We add the following dependency tuples: 263.89/94.58 263.89/94.58 Strict DPs: 263.89/94.58 { b^#(y, z) -> c_1(c^#(c(y, z, z), a(), a()), c^#(y, z, z)) 263.89/94.58 , c^#(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c_2(c^#(f(b(x, z)), c(z, y, a()), a()), 263.89/94.58 b^#(x, z), 263.89/94.58 c^#(z, y, a())) } 263.89/94.58 263.89/94.58 and mark the set of starting terms. 263.89/94.58 263.89/94.58 We are left with following problem, upon which TcT provides the 263.89/94.58 certificate YES(O(1),O(n^1)). 263.89/94.58 263.89/94.58 Strict DPs: 263.89/94.58 { b^#(y, z) -> c_1(c^#(c(y, z, z), a(), a()), c^#(y, z, z)) 263.89/94.58 , c^#(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c_2(c^#(f(b(x, z)), c(z, y, a()), a()), 263.89/94.58 b^#(x, z), 263.89/94.58 c^#(z, y, a())) } 263.89/94.58 Weak Trs: 263.89/94.58 { b(y, z) -> f(c(c(y, z, z), a(), a())) 263.89/94.58 , c(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c(f(b(x, z)), c(z, y, a()), a()) } 263.89/94.58 Obligation: 263.89/94.58 innermost runtime complexity 263.89/94.58 Answer: 263.89/94.58 YES(O(1),O(n^1)) 263.89/94.58 263.89/94.58 We use the processor 'matrix interpretation of dimension 3' to 263.89/94.58 orient following rules strictly. 263.89/94.58 263.89/94.58 DPs: 263.89/94.58 { 2: c^#(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c_2(c^#(f(b(x, z)), c(z, y, a()), a()), 263.89/94.58 b^#(x, z), 263.89/94.58 c^#(z, y, a())) } 263.89/94.58 263.89/94.58 Sub-proof: 263.89/94.58 ---------- 263.89/94.58 The following argument positions are usable: 263.89/94.58 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2, 3} 263.89/94.58 263.89/94.58 TcT has computed the following constructor-based matrix 263.89/94.58 interpretation satisfying not(EDA) and not(IDA(1)). 263.89/94.58 263.89/94.58 [0] 263.89/94.58 [b](x1, x2) = [0] 263.89/94.58 [0] 263.89/94.58 263.89/94.58 [1 6 0] [0] 263.89/94.58 [f](x1) = [0 0 4] x1 + [0] 263.89/94.58 [0 0 0] [0] 263.89/94.58 263.89/94.58 [0 0 0] [0 0 0] [0] 263.89/94.58 [c](x1, x2, x3) = [0 0 0] x1 + [0 0 0] x2 + [0] 263.89/94.58 [0 3 0] [2 0 0] [0] 263.89/94.58 263.89/94.58 [0] 263.89/94.58 [a] = [1] 263.89/94.58 [0] 263.89/94.58 263.89/94.58 [4 0 0] [0 6 0] [3] 263.89/94.58 [b^#](x1, x2) = [4 4 4] x1 + [4 0 4] x2 + [0] 263.89/94.58 [4 0 0] [4 0 4] [0] 263.89/94.58 263.89/94.58 [1 0 0] [2 0 0] [0] 263.89/94.58 [c_1](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] 263.89/94.58 [0 0 0] [0 0 0] [0] 263.89/94.58 263.89/94.58 [2 0 0] [0 1 0] [0 2 0] [0] 263.89/94.58 [c^#](x1, x2, x3) = [0 0 0] x1 + [0 0 0] x2 + [4 4 4] x3 + [0] 263.89/94.58 [0 0 0] [0 0 0] [0 4 4] [0] 263.89/94.58 263.89/94.58 [1 0 0] [2 0 0] [1 0 0] [0] 263.89/94.58 [c_2](x1, x2, x3) = [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0] 263.89/94.58 [0 0 0] [0 0 0] [0 0 0] [0] 263.89/94.58 263.89/94.58 The order satisfies the following ordering constraints: 263.89/94.58 263.89/94.58 [b(y, z)] = [0] 263.89/94.58 [0] 263.89/94.58 [0] 263.89/94.58 >= [0] 263.89/94.58 [0] 263.89/94.58 [0] 263.89/94.58 = [f(c(c(y, z, z), a(), a()))] 263.89/94.58 263.89/94.58 [c(f(z), f(c(a(), x, a())), y)] = [0 0 0] [0] 263.89/94.58 [0 0 0] z + [0] 263.89/94.58 [0 0 12] [0] 263.89/94.58 >= [0] 263.89/94.58 [0] 263.89/94.58 [0] 263.89/94.58 = [c(f(b(x, z)), c(z, y, a()), a())] 263.89/94.58 263.89/94.58 [b^#(y, z)] = [4 0 0] [0 6 0] [3] 263.89/94.58 [4 4 4] y + [4 0 4] z + [0] 263.89/94.58 [4 0 0] [4 0 4] [0] 263.89/94.58 >= [4 0 0] [0 6 0] [3] 263.89/94.58 [0 0 0] y + [0 0 0] z + [0] 263.89/94.58 [0 0 0] [0 0 0] [0] 263.89/94.58 = [c_1(c^#(c(y, z, z), a(), a()), c^#(y, z, z))] 263.89/94.58 263.89/94.58 [c^#(f(z), f(c(a(), x, a())), y)] = [0 2 0] [2 12 0] [8 0 0] [12] 263.89/94.58 [4 4 4] y + [0 0 0] z + [0 0 0] x + [0] 263.89/94.58 [0 4 4] [0 0 0] [0 0 0] [0] 263.89/94.58 > [0 1 0] [2 12 0] [8 0 0] [10] 263.89/94.58 [0 0 0] y + [0 0 0] z + [0 0 0] x + [0] 263.89/94.58 [0 0 0] [0 0 0] [0 0 0] [0] 263.89/94.58 = [c_2(c^#(f(b(x, z)), c(z, y, a()), a()), 263.89/94.58 b^#(x, z), 263.89/94.58 c^#(z, y, a()))] 263.89/94.58 263.89/94.58 263.89/94.58 We return to the main proof. Consider the set of all dependency 263.89/94.58 pairs 263.89/94.58 263.89/94.58 : 263.89/94.58 { 1: b^#(y, z) -> c_1(c^#(c(y, z, z), a(), a()), c^#(y, z, z)) 263.89/94.58 , 2: c^#(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c_2(c^#(f(b(x, z)), c(z, y, a()), a()), 263.89/94.58 b^#(x, z), 263.89/94.58 c^#(z, y, a())) } 263.89/94.58 263.89/94.58 Processor 'matrix interpretation of dimension 3' induces the 263.89/94.58 complexity certificate YES(?,O(n^1)) on application of dependency 263.89/94.58 pairs {2}. These cover all (indirect) predecessors of dependency 263.89/94.58 pairs {1,2}, their number of application is equally bounded. The 263.89/94.58 dependency pairs are shifted into the weak component. 263.89/94.58 263.89/94.58 We are left with following problem, upon which TcT provides the 263.89/94.58 certificate YES(O(1),O(1)). 263.89/94.58 263.89/94.58 Weak DPs: 263.89/94.58 { b^#(y, z) -> c_1(c^#(c(y, z, z), a(), a()), c^#(y, z, z)) 263.89/94.58 , c^#(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c_2(c^#(f(b(x, z)), c(z, y, a()), a()), 263.89/94.58 b^#(x, z), 263.89/94.58 c^#(z, y, a())) } 263.89/94.58 Weak Trs: 263.89/94.58 { b(y, z) -> f(c(c(y, z, z), a(), a())) 263.89/94.58 , c(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c(f(b(x, z)), c(z, y, a()), a()) } 263.89/94.58 Obligation: 263.89/94.58 innermost runtime complexity 263.89/94.58 Answer: 263.89/94.58 YES(O(1),O(1)) 263.89/94.58 263.89/94.58 The following weak DPs constitute a sub-graph of the DG that is 263.89/94.58 closed under successors. The DPs are removed. 263.89/94.58 263.89/94.58 { b^#(y, z) -> c_1(c^#(c(y, z, z), a(), a()), c^#(y, z, z)) 263.89/94.58 , c^#(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c_2(c^#(f(b(x, z)), c(z, y, a()), a()), 263.89/94.58 b^#(x, z), 263.89/94.58 c^#(z, y, a())) } 263.89/94.58 263.89/94.58 We are left with following problem, upon which TcT provides the 263.89/94.58 certificate YES(O(1),O(1)). 263.89/94.58 263.89/94.58 Weak Trs: 263.89/94.58 { b(y, z) -> f(c(c(y, z, z), a(), a())) 263.89/94.58 , c(f(z), f(c(a(), x, a())), y) -> 263.89/94.58 c(f(b(x, z)), c(z, y, a()), a()) } 263.89/94.58 Obligation: 263.89/94.58 innermost runtime complexity 263.89/94.58 Answer: 263.89/94.58 YES(O(1),O(1)) 263.89/94.58 263.89/94.58 No rule is usable, rules are removed from the input problem. 263.89/94.58 263.89/94.58 We are left with following problem, upon which TcT provides the 263.89/94.58 certificate YES(O(1),O(1)). 263.89/94.58 263.89/94.58 Rules: Empty 263.89/94.58 Obligation: 263.89/94.58 innermost runtime complexity 263.89/94.58 Answer: 263.89/94.58 YES(O(1),O(1)) 263.89/94.58 263.89/94.58 Empty rules are trivially bounded 263.89/94.58 263.89/94.58 Hurray, we answered YES(O(1),O(n^1)) 264.21/94.68 EOF