YES(O(1),O(n^1)) 77.62/24.04 YES(O(1),O(n^1)) 77.62/24.04 77.62/24.04 We are left with following problem, upon which TcT provides the 77.62/24.04 certificate YES(O(1),O(n^1)). 77.62/24.04 77.62/24.04 Strict Trs: 77.62/24.04 { a__f(X, X) -> a__f(a(), b()) 77.62/24.04 , a__f(X1, X2) -> f(X1, X2) 77.62/24.04 , a__b() -> a() 77.62/24.04 , a__b() -> b() 77.62/24.04 , mark(a()) -> a() 77.62/24.04 , mark(b()) -> a__b() 77.62/24.04 , mark(f(X1, X2)) -> a__f(mark(X1), X2) } 77.62/24.04 Obligation: 77.62/24.04 innermost runtime complexity 77.62/24.04 Answer: 77.62/24.04 YES(O(1),O(n^1)) 77.62/24.04 77.62/24.04 We add the following dependency tuples: 77.62/24.04 77.62/24.04 Strict DPs: 77.62/24.04 { a__f^#(X, X) -> c_1(a__f^#(a(), b())) 77.62/24.04 , a__f^#(X1, X2) -> c_2() 77.62/24.04 , a__b^#() -> c_3() 77.62/24.04 , a__b^#() -> c_4() 77.62/24.04 , mark^#(a()) -> c_5() 77.62/24.04 , mark^#(b()) -> c_6(a__b^#()) 77.62/24.04 , mark^#(f(X1, X2)) -> c_7(a__f^#(mark(X1), X2), mark^#(X1)) } 77.62/24.04 77.62/24.04 and mark the set of starting terms. 77.62/24.04 77.62/24.04 We are left with following problem, upon which TcT provides the 77.62/24.04 certificate YES(O(1),O(n^1)). 77.62/24.04 77.62/24.04 Strict DPs: 77.62/24.04 { a__f^#(X, X) -> c_1(a__f^#(a(), b())) 77.62/24.04 , a__f^#(X1, X2) -> c_2() 77.62/24.04 , a__b^#() -> c_3() 77.62/24.04 , a__b^#() -> c_4() 77.62/24.04 , mark^#(a()) -> c_5() 77.62/24.04 , mark^#(b()) -> c_6(a__b^#()) 77.62/24.04 , mark^#(f(X1, X2)) -> c_7(a__f^#(mark(X1), X2), mark^#(X1)) } 77.62/24.04 Weak Trs: 77.62/24.04 { a__f(X, X) -> a__f(a(), b()) 77.62/24.04 , a__f(X1, X2) -> f(X1, X2) 77.62/24.04 , a__b() -> a() 77.62/24.04 , a__b() -> b() 77.62/24.04 , mark(a()) -> a() 77.62/24.04 , mark(b()) -> a__b() 77.62/24.04 , mark(f(X1, X2)) -> a__f(mark(X1), X2) } 77.62/24.04 Obligation: 77.62/24.04 innermost runtime complexity 77.62/24.04 Answer: 77.62/24.04 YES(O(1),O(n^1)) 77.62/24.04 77.62/24.04 We estimate the number of application of {2,3,4,5} by applications 77.62/24.04 of Pre({2,3,4,5}) = {1,6,7}. Here rules are labeled as follows: 77.62/24.04 77.62/24.04 DPs: 77.62/24.04 { 1: a__f^#(X, X) -> c_1(a__f^#(a(), b())) 77.62/24.04 , 2: a__f^#(X1, X2) -> c_2() 77.62/24.04 , 3: a__b^#() -> c_3() 77.62/24.04 , 4: a__b^#() -> c_4() 77.62/24.04 , 5: mark^#(a()) -> c_5() 77.62/24.04 , 6: mark^#(b()) -> c_6(a__b^#()) 77.62/24.04 , 7: mark^#(f(X1, X2)) -> c_7(a__f^#(mark(X1), X2), mark^#(X1)) } 77.62/24.04 77.62/24.04 We are left with following problem, upon which TcT provides the 77.62/24.04 certificate YES(O(1),O(n^1)). 77.62/24.04 77.62/24.04 Strict DPs: 77.62/24.04 { a__f^#(X, X) -> c_1(a__f^#(a(), b())) 77.62/24.04 , mark^#(b()) -> c_6(a__b^#()) 77.62/24.04 , mark^#(f(X1, X2)) -> c_7(a__f^#(mark(X1), X2), mark^#(X1)) } 77.62/24.04 Weak DPs: 77.62/24.04 { a__f^#(X1, X2) -> c_2() 77.62/24.04 , a__b^#() -> c_3() 77.62/24.04 , a__b^#() -> c_4() 77.62/24.04 , mark^#(a()) -> c_5() } 77.62/24.04 Weak Trs: 77.62/24.04 { a__f(X, X) -> a__f(a(), b()) 77.62/24.04 , a__f(X1, X2) -> f(X1, X2) 77.62/24.04 , a__b() -> a() 77.62/24.04 , a__b() -> b() 77.62/24.04 , mark(a()) -> a() 77.62/24.04 , mark(b()) -> a__b() 77.62/24.04 , mark(f(X1, X2)) -> a__f(mark(X1), X2) } 77.62/24.04 Obligation: 77.62/24.04 innermost runtime complexity 77.62/24.04 Answer: 77.62/24.04 YES(O(1),O(n^1)) 77.62/24.04 77.62/24.04 We estimate the number of application of {1,2} by applications of 77.62/24.04 Pre({1,2}) = {3}. Here rules are labeled as follows: 77.62/24.04 77.62/24.04 DPs: 77.62/24.04 { 1: a__f^#(X, X) -> c_1(a__f^#(a(), b())) 77.62/24.04 , 2: mark^#(b()) -> c_6(a__b^#()) 77.62/24.04 , 3: mark^#(f(X1, X2)) -> c_7(a__f^#(mark(X1), X2), mark^#(X1)) 77.62/24.04 , 4: a__f^#(X1, X2) -> c_2() 77.62/24.04 , 5: a__b^#() -> c_3() 77.62/24.04 , 6: a__b^#() -> c_4() 77.62/24.04 , 7: mark^#(a()) -> c_5() } 77.62/24.04 77.62/24.04 We are left with following problem, upon which TcT provides the 77.62/24.04 certificate YES(O(1),O(n^1)). 77.62/24.04 77.62/24.04 Strict DPs: 77.62/24.04 { mark^#(f(X1, X2)) -> c_7(a__f^#(mark(X1), X2), mark^#(X1)) } 77.62/24.04 Weak DPs: 77.62/24.04 { a__f^#(X, X) -> c_1(a__f^#(a(), b())) 77.62/24.04 , a__f^#(X1, X2) -> c_2() 77.62/24.04 , a__b^#() -> c_3() 77.62/24.04 , a__b^#() -> c_4() 77.62/24.04 , mark^#(a()) -> c_5() 77.62/24.04 , mark^#(b()) -> c_6(a__b^#()) } 77.62/24.04 Weak Trs: 77.62/24.04 { a__f(X, X) -> a__f(a(), b()) 77.62/24.04 , a__f(X1, X2) -> f(X1, X2) 77.62/24.04 , a__b() -> a() 77.62/24.04 , a__b() -> b() 77.62/24.04 , mark(a()) -> a() 77.62/24.04 , mark(b()) -> a__b() 77.62/24.04 , mark(f(X1, X2)) -> a__f(mark(X1), X2) } 77.62/24.04 Obligation: 77.62/24.04 innermost runtime complexity 77.62/24.04 Answer: 77.62/24.04 YES(O(1),O(n^1)) 77.62/24.04 77.62/24.04 The following weak DPs constitute a sub-graph of the DG that is 77.62/24.04 closed under successors. The DPs are removed. 77.62/24.04 77.62/24.04 { a__f^#(X, X) -> c_1(a__f^#(a(), b())) 77.62/24.04 , a__f^#(X1, X2) -> c_2() 77.62/24.04 , a__b^#() -> c_3() 77.62/24.04 , a__b^#() -> c_4() 77.62/24.04 , mark^#(a()) -> c_5() 77.62/24.04 , mark^#(b()) -> c_6(a__b^#()) } 77.62/24.04 77.62/24.04 We are left with following problem, upon which TcT provides the 77.62/24.04 certificate YES(O(1),O(n^1)). 77.62/24.04 77.62/24.04 Strict DPs: 77.62/24.04 { mark^#(f(X1, X2)) -> c_7(a__f^#(mark(X1), X2), mark^#(X1)) } 77.62/24.04 Weak Trs: 77.62/24.04 { a__f(X, X) -> a__f(a(), b()) 77.62/24.04 , a__f(X1, X2) -> f(X1, X2) 77.62/24.04 , a__b() -> a() 77.62/24.04 , a__b() -> b() 77.62/24.04 , mark(a()) -> a() 77.62/24.04 , mark(b()) -> a__b() 77.62/24.04 , mark(f(X1, X2)) -> a__f(mark(X1), X2) } 77.62/24.04 Obligation: 77.62/24.04 innermost runtime complexity 77.62/24.04 Answer: 77.62/24.04 YES(O(1),O(n^1)) 77.62/24.04 77.62/24.04 Due to missing edges in the dependency-graph, the right-hand sides 77.62/24.04 of following rules could be simplified: 77.62/24.04 77.62/24.04 { mark^#(f(X1, X2)) -> c_7(a__f^#(mark(X1), X2), mark^#(X1)) } 77.62/24.04 77.62/24.04 We are left with following problem, upon which TcT provides the 77.62/24.04 certificate YES(O(1),O(n^1)). 77.62/24.04 77.62/24.04 Strict DPs: { mark^#(f(X1, X2)) -> c_1(mark^#(X1)) } 77.62/24.04 Weak Trs: 77.62/24.04 { a__f(X, X) -> a__f(a(), b()) 77.62/24.04 , a__f(X1, X2) -> f(X1, X2) 77.62/24.04 , a__b() -> a() 77.62/24.04 , a__b() -> b() 77.62/24.04 , mark(a()) -> a() 77.62/24.04 , mark(b()) -> a__b() 77.62/24.04 , mark(f(X1, X2)) -> a__f(mark(X1), X2) } 77.62/24.04 Obligation: 77.62/24.04 innermost runtime complexity 77.62/24.04 Answer: 77.62/24.04 YES(O(1),O(n^1)) 77.62/24.04 77.62/24.04 No rule is usable, rules are removed from the input problem. 77.62/24.04 77.62/24.04 We are left with following problem, upon which TcT provides the 77.62/24.04 certificate YES(O(1),O(n^1)). 77.62/24.04 77.62/24.04 Strict DPs: { mark^#(f(X1, X2)) -> c_1(mark^#(X1)) } 77.62/24.04 Obligation: 77.62/24.04 innermost runtime complexity 77.62/24.04 Answer: 77.62/24.04 YES(O(1),O(n^1)) 77.62/24.04 77.62/24.04 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 77.62/24.04 to orient following rules strictly. 77.62/24.04 77.62/24.04 DPs: 77.62/24.04 { 1: mark^#(f(X1, X2)) -> c_1(mark^#(X1)) } 77.62/24.04 77.62/24.04 Sub-proof: 77.62/24.04 ---------- 77.62/24.04 The input was oriented with the instance of 'Small Polynomial Path 77.62/24.04 Order (PS,1-bounded)' as induced by the safe mapping 77.62/24.04 77.62/24.04 safe(f) = {1, 2}, safe(mark^#) = {}, safe(c_1) = {} 77.62/24.04 77.62/24.04 and precedence 77.62/24.04 77.62/24.04 empty . 77.62/24.04 77.62/24.04 Following symbols are considered recursive: 77.62/24.04 77.62/24.04 {mark^#} 77.62/24.04 77.62/24.04 The recursion depth is 1. 77.62/24.04 77.62/24.04 Further, following argument filtering is employed: 77.62/24.04 77.62/24.04 pi(f) = [1, 2], pi(mark^#) = [1], pi(c_1) = [1] 77.62/24.04 77.62/24.04 Usable defined function symbols are a subset of: 77.62/24.04 77.62/24.04 {mark^#} 77.62/24.04 77.62/24.04 For your convenience, here are the satisfied ordering constraints: 77.62/24.04 77.62/24.04 pi(mark^#(f(X1, X2))) = mark^#(f(; X1, X2);) 77.62/24.04 > c_1(mark^#(X1;);) 77.62/24.04 = pi(c_1(mark^#(X1))) 77.62/24.04 77.62/24.04 77.62/24.04 The strictly oriented rules are moved into the weak component. 77.62/24.04 77.62/24.04 We are left with following problem, upon which TcT provides the 77.62/24.04 certificate YES(O(1),O(1)). 77.62/24.04 77.62/24.04 Weak DPs: { mark^#(f(X1, X2)) -> c_1(mark^#(X1)) } 77.62/24.04 Obligation: 77.62/24.04 innermost runtime complexity 77.62/24.04 Answer: 77.62/24.04 YES(O(1),O(1)) 77.62/24.04 77.62/24.04 The following weak DPs constitute a sub-graph of the DG that is 77.62/24.04 closed under successors. The DPs are removed. 77.62/24.04 77.62/24.04 { mark^#(f(X1, X2)) -> c_1(mark^#(X1)) } 77.62/24.04 77.62/24.04 We are left with following problem, upon which TcT provides the 77.62/24.04 certificate YES(O(1),O(1)). 77.62/24.04 77.62/24.04 Rules: Empty 77.62/24.04 Obligation: 77.62/24.04 innermost runtime complexity 77.62/24.04 Answer: 77.62/24.04 YES(O(1),O(1)) 77.62/24.04 77.62/24.04 Empty rules are trivially bounded 77.62/24.04 77.62/24.04 Hurray, we answered YES(O(1),O(n^1)) 77.62/24.04 EOF