YES(O(1),O(n^1)) 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(n^1)). 0.00/0.77 0.00/0.77 Strict Trs: 0.00/0.77 { gcd(x, y) -> gcd[Ite][False][Ite][False][Ite](equal0(x, y), x, y) 0.00/0.77 , monus(S(x'), S(x)) -> monus(x', x) 0.00/0.77 , equal0(a, b) -> equal0[Ite](<(a, b), a, b) } 0.00/0.77 Weak Trs: 0.00/0.77 { equal0[Ite][True][Ite](True(), a, b) -> True() 0.00/0.77 , equal0[Ite][True][Ite](False(), a, b) -> False() 0.00/0.77 , <(x, 0()) -> False() 0.00/0.77 , <(S(x), S(y)) -> <(x, y) 0.00/0.77 , <(0(), S(y)) -> True() 0.00/0.77 , equal0[Ite](True(), a, b) -> 0.00/0.77 equal0[Ite][True][Ite](<(b, a), a, b) 0.00/0.77 , equal0[Ite](False(), a, b) -> False() } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 We add the following weak dependency pairs: 0.00/0.77 0.00/0.77 Strict DPs: 0.00/0.77 { gcd^#(x, y) -> c_1(equal0^#(x, y)) 0.00/0.77 , equal0^#(a, b) -> c_3(equal0[Ite]^#(<(a, b), a, b)) 0.00/0.77 , monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Weak DPs: 0.00/0.77 { equal0[Ite]^#(True(), a, b) -> 0.00/0.77 c_9(equal0[Ite][True][Ite]^#(<(b, a), a, b)) 0.00/0.77 , equal0[Ite]^#(False(), a, b) -> c_10() 0.00/0.77 , equal0[Ite][True][Ite]^#(True(), a, b) -> c_4() 0.00/0.77 , equal0[Ite][True][Ite]^#(False(), a, b) -> c_5() 0.00/0.77 , <^#(x, 0()) -> c_6() 0.00/0.77 , <^#(S(x), S(y)) -> c_7(<^#(x, y)) 0.00/0.77 , <^#(0(), S(y)) -> c_8() } 0.00/0.77 0.00/0.77 and mark the set of starting terms. 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(n^1)). 0.00/0.77 0.00/0.77 Strict DPs: 0.00/0.77 { gcd^#(x, y) -> c_1(equal0^#(x, y)) 0.00/0.77 , equal0^#(a, b) -> c_3(equal0[Ite]^#(<(a, b), a, b)) 0.00/0.77 , monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Strict Trs: 0.00/0.77 { gcd(x, y) -> gcd[Ite][False][Ite][False][Ite](equal0(x, y), x, y) 0.00/0.77 , monus(S(x'), S(x)) -> monus(x', x) 0.00/0.77 , equal0(a, b) -> equal0[Ite](<(a, b), a, b) } 0.00/0.77 Weak DPs: 0.00/0.77 { equal0[Ite]^#(True(), a, b) -> 0.00/0.77 c_9(equal0[Ite][True][Ite]^#(<(b, a), a, b)) 0.00/0.77 , equal0[Ite]^#(False(), a, b) -> c_10() 0.00/0.77 , equal0[Ite][True][Ite]^#(True(), a, b) -> c_4() 0.00/0.77 , equal0[Ite][True][Ite]^#(False(), a, b) -> c_5() 0.00/0.77 , <^#(x, 0()) -> c_6() 0.00/0.77 , <^#(S(x), S(y)) -> c_7(<^#(x, y)) 0.00/0.77 , <^#(0(), S(y)) -> c_8() } 0.00/0.77 Weak Trs: 0.00/0.77 { equal0[Ite][True][Ite](True(), a, b) -> True() 0.00/0.77 , equal0[Ite][True][Ite](False(), a, b) -> False() 0.00/0.77 , <(x, 0()) -> False() 0.00/0.77 , <(S(x), S(y)) -> <(x, y) 0.00/0.77 , <(0(), S(y)) -> True() 0.00/0.77 , equal0[Ite](True(), a, b) -> 0.00/0.77 equal0[Ite][True][Ite](<(b, a), a, b) 0.00/0.77 , equal0[Ite](False(), a, b) -> False() } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 We replace rewrite rules by usable rules: 0.00/0.77 0.00/0.77 Weak Usable Rules: 0.00/0.77 { <(x, 0()) -> False() 0.00/0.77 , <(S(x), S(y)) -> <(x, y) 0.00/0.77 , <(0(), S(y)) -> True() } 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(n^1)). 0.00/0.77 0.00/0.77 Strict DPs: 0.00/0.77 { gcd^#(x, y) -> c_1(equal0^#(x, y)) 0.00/0.77 , equal0^#(a, b) -> c_3(equal0[Ite]^#(<(a, b), a, b)) 0.00/0.77 , monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Weak DPs: 0.00/0.77 { equal0[Ite]^#(True(), a, b) -> 0.00/0.77 c_9(equal0[Ite][True][Ite]^#(<(b, a), a, b)) 0.00/0.77 , equal0[Ite]^#(False(), a, b) -> c_10() 0.00/0.77 , equal0[Ite][True][Ite]^#(True(), a, b) -> c_4() 0.00/0.77 , equal0[Ite][True][Ite]^#(False(), a, b) -> c_5() 0.00/0.77 , <^#(x, 0()) -> c_6() 0.00/0.77 , <^#(S(x), S(y)) -> c_7(<^#(x, y)) 0.00/0.77 , <^#(0(), S(y)) -> c_8() } 0.00/0.77 Weak Trs: 0.00/0.77 { <(x, 0()) -> False() 0.00/0.77 , <(S(x), S(y)) -> <(x, y) 0.00/0.77 , <(0(), S(y)) -> True() } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 The weightgap principle applies (using the following constant 0.00/0.77 growth matrix-interpretation) 0.00/0.77 0.00/0.77 The following argument positions are usable: 0.00/0.77 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 0.00/0.77 Uargs(equal0[Ite]^#) = {1}, Uargs(equal0[Ite][True][Ite]^#) = {1}, 0.00/0.77 Uargs(c_7) = {1}, Uargs(c_9) = {1} 0.00/0.77 0.00/0.77 TcT has computed the following constructor-restricted matrix 0.00/0.77 interpretation. 0.00/0.77 0.00/0.77 [True] = [0] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 [S](x1) = [1 0] x1 + [0] 0.00/0.77 [0 0] [0] 0.00/0.77 0.00/0.77 [<](x1, x2) = [0] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 [0] = [0] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 [False] = [0] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 [gcd^#](x1, x2) = [2 2] x1 + [2 2] x2 + [2] 0.00/0.77 [2 2] [1 2] [2] 0.00/0.77 0.00/0.77 [c_1](x1) = [1 0] x1 + [0] 0.00/0.77 [0 1] [0] 0.00/0.77 0.00/0.77 [equal0^#](x1, x2) = [1 2] x1 + [1 2] x2 + [1] 0.00/0.77 [2 1] [1 1] [2] 0.00/0.77 0.00/0.77 [monus^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2] 0.00/0.77 [1 2] [1 2] [2] 0.00/0.77 0.00/0.77 [c_2](x1) = [1 0] x1 + [1] 0.00/0.77 [0 1] [1] 0.00/0.77 0.00/0.77 [c_3](x1) = [1 0] x1 + [2] 0.00/0.77 [0 1] [2] 0.00/0.77 0.00/0.77 [equal0[Ite]^#](x1, x2, x3) = [2 0] x1 + [0] 0.00/0.77 [0 0] [0] 0.00/0.77 0.00/0.77 [equal0[Ite][True][Ite]^#](x1, x2, x3) = [2 0] x1 + [0] 0.00/0.77 [0 0] [0] 0.00/0.77 0.00/0.77 [c_4] = [0] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 [c_5] = [0] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 [<^#](x1, x2) = [1] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 [c_6] = [1] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 [c_7](x1) = [1 0] x1 + [0] 0.00/0.77 [0 1] [0] 0.00/0.77 0.00/0.77 [c_8] = [1] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 [c_9](x1) = [1 0] x1 + [0] 0.00/0.77 [0 1] [0] 0.00/0.77 0.00/0.77 [c_10] = [0] 0.00/0.77 [0] 0.00/0.77 0.00/0.77 The order satisfies the following ordering constraints: 0.00/0.77 0.00/0.77 [<(x, 0())] = [0] 0.00/0.77 [0] 0.00/0.77 >= [0] 0.00/0.77 [0] 0.00/0.77 = [False()] 0.00/0.77 0.00/0.77 [<(S(x), S(y))] = [0] 0.00/0.77 [0] 0.00/0.77 >= [0] 0.00/0.77 [0] 0.00/0.77 = [<(x, y)] 0.00/0.77 0.00/0.77 [<(0(), S(y))] = [0] 0.00/0.77 [0] 0.00/0.77 >= [0] 0.00/0.77 [0] 0.00/0.77 = [True()] 0.00/0.77 0.00/0.77 [gcd^#(x, y)] = [2 2] x + [2 2] y + [2] 0.00/0.77 [2 2] [1 2] [2] 0.00/0.77 > [1 2] x + [1 2] y + [1] 0.00/0.77 [2 1] [1 1] [2] 0.00/0.77 = [c_1(equal0^#(x, y))] 0.00/0.77 0.00/0.77 [equal0^#(a, b)] = [1 2] a + [1 2] b + [1] 0.00/0.77 [2 1] [1 1] [2] 0.00/0.77 ? [2] 0.00/0.77 [2] 0.00/0.77 = [c_3(equal0[Ite]^#(<(a, b), a, b))] 0.00/0.77 0.00/0.77 [monus^#(S(x'), S(x))] = [0 0] x' + [0 0] x + [2] 0.00/0.77 [1 0] [1 0] [2] 0.00/0.77 ? [0 0] x' + [0 0] x + [3] 0.00/0.77 [1 2] [1 2] [3] 0.00/0.77 = [c_2(monus^#(x', x))] 0.00/0.77 0.00/0.77 [equal0[Ite]^#(True(), a, b)] = [0] 0.00/0.77 [0] 0.00/0.77 >= [0] 0.00/0.77 [0] 0.00/0.77 = [c_9(equal0[Ite][True][Ite]^#(<(b, a), a, b))] 0.00/0.77 0.00/0.77 [equal0[Ite]^#(False(), a, b)] = [0] 0.00/0.77 [0] 0.00/0.77 >= [0] 0.00/0.77 [0] 0.00/0.77 = [c_10()] 0.00/0.77 0.00/0.77 [equal0[Ite][True][Ite]^#(True(), a, b)] = [0] 0.00/0.77 [0] 0.00/0.77 >= [0] 0.00/0.77 [0] 0.00/0.77 = [c_4()] 0.00/0.77 0.00/0.77 [equal0[Ite][True][Ite]^#(False(), a, b)] = [0] 0.00/0.77 [0] 0.00/0.77 >= [0] 0.00/0.77 [0] 0.00/0.77 = [c_5()] 0.00/0.77 0.00/0.77 [<^#(x, 0())] = [1] 0.00/0.77 [0] 0.00/0.77 >= [1] 0.00/0.77 [0] 0.00/0.77 = [c_6()] 0.00/0.77 0.00/0.77 [<^#(S(x), S(y))] = [1] 0.00/0.77 [0] 0.00/0.77 >= [1] 0.00/0.77 [0] 0.00/0.77 = [c_7(<^#(x, y))] 0.00/0.77 0.00/0.77 [<^#(0(), S(y))] = [1] 0.00/0.77 [0] 0.00/0.77 >= [1] 0.00/0.77 [0] 0.00/0.77 = [c_8()] 0.00/0.77 0.00/0.77 0.00/0.77 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(n^1)). 0.00/0.77 0.00/0.77 Strict DPs: 0.00/0.77 { equal0^#(a, b) -> c_3(equal0[Ite]^#(<(a, b), a, b)) 0.00/0.77 , monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Weak DPs: 0.00/0.77 { gcd^#(x, y) -> c_1(equal0^#(x, y)) 0.00/0.77 , equal0[Ite]^#(True(), a, b) -> 0.00/0.77 c_9(equal0[Ite][True][Ite]^#(<(b, a), a, b)) 0.00/0.77 , equal0[Ite]^#(False(), a, b) -> c_10() 0.00/0.77 , equal0[Ite][True][Ite]^#(True(), a, b) -> c_4() 0.00/0.77 , equal0[Ite][True][Ite]^#(False(), a, b) -> c_5() 0.00/0.77 , <^#(x, 0()) -> c_6() 0.00/0.77 , <^#(S(x), S(y)) -> c_7(<^#(x, y)) 0.00/0.77 , <^#(0(), S(y)) -> c_8() } 0.00/0.77 Weak Trs: 0.00/0.77 { <(x, 0()) -> False() 0.00/0.77 , <(S(x), S(y)) -> <(x, y) 0.00/0.77 , <(0(), S(y)) -> True() } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.77 closed under successors. The DPs are removed. 0.00/0.77 0.00/0.77 { equal0[Ite]^#(True(), a, b) -> 0.00/0.77 c_9(equal0[Ite][True][Ite]^#(<(b, a), a, b)) 0.00/0.77 , equal0[Ite]^#(False(), a, b) -> c_10() 0.00/0.77 , equal0[Ite][True][Ite]^#(True(), a, b) -> c_4() 0.00/0.77 , equal0[Ite][True][Ite]^#(False(), a, b) -> c_5() 0.00/0.77 , <^#(x, 0()) -> c_6() 0.00/0.77 , <^#(S(x), S(y)) -> c_7(<^#(x, y)) 0.00/0.77 , <^#(0(), S(y)) -> c_8() } 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(n^1)). 0.00/0.77 0.00/0.77 Strict DPs: 0.00/0.77 { equal0^#(a, b) -> c_3(equal0[Ite]^#(<(a, b), a, b)) 0.00/0.77 , monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Weak DPs: { gcd^#(x, y) -> c_1(equal0^#(x, y)) } 0.00/0.77 Weak Trs: 0.00/0.77 { <(x, 0()) -> False() 0.00/0.77 , <(S(x), S(y)) -> <(x, y) 0.00/0.77 , <(0(), S(y)) -> True() } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 Due to missing edges in the dependency-graph, the right-hand sides 0.00/0.77 of following rules could be simplified: 0.00/0.77 0.00/0.77 { equal0^#(a, b) -> c_3(equal0[Ite]^#(<(a, b), a, b)) } 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(n^1)). 0.00/0.77 0.00/0.77 Strict DPs: 0.00/0.77 { equal0^#(a, b) -> c_1() 0.00/0.77 , monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Weak DPs: { gcd^#(x, y) -> c_3(equal0^#(x, y)) } 0.00/0.77 Weak Trs: 0.00/0.77 { <(x, 0()) -> False() 0.00/0.77 , <(S(x), S(y)) -> <(x, y) 0.00/0.77 , <(0(), S(y)) -> True() } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 No rule is usable, rules are removed from the input problem. 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(n^1)). 0.00/0.77 0.00/0.77 Strict DPs: 0.00/0.77 { equal0^#(a, b) -> c_1() 0.00/0.77 , monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Weak DPs: { gcd^#(x, y) -> c_3(equal0^#(x, y)) } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 Consider the dependency graph 0.00/0.77 0.00/0.77 1: equal0^#(a, b) -> c_1() 0.00/0.77 0.00/0.77 2: monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) 0.00/0.77 -->_1 monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) :2 0.00/0.77 0.00/0.77 3: gcd^#(x, y) -> c_3(equal0^#(x, y)) 0.00/0.77 -->_1 equal0^#(a, b) -> c_1() :1 0.00/0.77 0.00/0.77 0.00/0.77 Following roots of the dependency graph are removed, as the 0.00/0.77 considered set of starting terms is closed under reduction with 0.00/0.77 respect to these rules (modulo compound contexts). 0.00/0.77 0.00/0.77 { gcd^#(x, y) -> c_3(equal0^#(x, y)) } 0.00/0.77 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(n^1)). 0.00/0.77 0.00/0.77 Strict DPs: 0.00/0.77 { equal0^#(a, b) -> c_1() 0.00/0.77 , monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 Consider the dependency graph 0.00/0.77 0.00/0.77 1: equal0^#(a, b) -> c_1() 0.00/0.77 0.00/0.77 2: monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) 0.00/0.77 -->_1 monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) :2 0.00/0.77 0.00/0.77 0.00/0.77 Following roots of the dependency graph are removed, as the 0.00/0.77 considered set of starting terms is closed under reduction with 0.00/0.77 respect to these rules (modulo compound contexts). 0.00/0.77 0.00/0.77 { equal0^#(a, b) -> c_1() } 0.00/0.77 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(n^1)). 0.00/0.77 0.00/0.77 Strict DPs: { monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(n^1)) 0.00/0.77 0.00/0.77 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 0.00/0.77 to orient following rules strictly. 0.00/0.77 0.00/0.77 DPs: 0.00/0.77 { 1: monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 0.00/0.77 Sub-proof: 0.00/0.77 ---------- 0.00/0.77 The input was oriented with the instance of 'Small Polynomial Path 0.00/0.77 Order (PS,1-bounded)' as induced by the safe mapping 0.00/0.77 0.00/0.77 safe(S) = {1}, safe(monus^#) = {2}, safe(c_2) = {} 0.00/0.77 0.00/0.77 and precedence 0.00/0.77 0.00/0.77 empty . 0.00/0.77 0.00/0.77 Following symbols are considered recursive: 0.00/0.77 0.00/0.77 {monus^#} 0.00/0.77 0.00/0.77 The recursion depth is 1. 0.00/0.77 0.00/0.77 Further, following argument filtering is employed: 0.00/0.77 0.00/0.77 pi(S) = [1], pi(monus^#) = [1, 2], pi(c_2) = [1] 0.00/0.77 0.00/0.77 Usable defined function symbols are a subset of: 0.00/0.77 0.00/0.77 {monus^#} 0.00/0.77 0.00/0.77 For your convenience, here are the satisfied ordering constraints: 0.00/0.77 0.00/0.77 pi(monus^#(S(x'), S(x))) = monus^#(S(; x'); S(; x)) 0.00/0.77 > c_2(monus^#(x'; x);) 0.00/0.77 = pi(c_2(monus^#(x', x))) 0.00/0.77 0.00/0.77 0.00/0.77 The strictly oriented rules are moved into the weak component. 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(1)). 0.00/0.77 0.00/0.77 Weak DPs: { monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(1)) 0.00/0.77 0.00/0.77 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.77 closed under successors. The DPs are removed. 0.00/0.77 0.00/0.77 { monus^#(S(x'), S(x)) -> c_2(monus^#(x', x)) } 0.00/0.77 0.00/0.77 We are left with following problem, upon which TcT provides the 0.00/0.77 certificate YES(O(1),O(1)). 0.00/0.77 0.00/0.77 Rules: Empty 0.00/0.77 Obligation: 0.00/0.77 innermost runtime complexity 0.00/0.77 Answer: 0.00/0.77 YES(O(1),O(1)) 0.00/0.77 0.00/0.77 Empty rules are trivially bounded 0.00/0.77 0.00/0.77 Hurray, we answered YES(O(1),O(n^1)) 0.00/0.78 EOF