YES(O(1),O(n^1)) 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict Trs: 8.09/2.34 { prime(0()) -> false() 8.09/2.34 , prime(s(0())) -> false() 8.09/2.34 , prime(s(s(x))) -> prime1(s(s(x)), s(x)) 8.09/2.34 , prime1(x, 0()) -> false() 8.09/2.34 , prime1(x, s(0())) -> true() 8.09/2.34 , prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y))) 8.09/2.34 , divp(x, y) -> =(rem(x, y), 0()) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 We add the following weak dependency pairs: 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime^#(0()) -> c_1() 8.09/2.34 , prime^#(s(0())) -> c_2() 8.09/2.34 , prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, 0()) -> c_4() 8.09/2.34 , prime1^#(x, s(0())) -> c_5() 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.34 , divp^#(x, y) -> c_7(x, y) } 8.09/2.34 8.09/2.34 and mark the set of starting terms. 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime^#(0()) -> c_1() 8.09/2.34 , prime^#(s(0())) -> c_2() 8.09/2.34 , prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, 0()) -> c_4() 8.09/2.34 , prime1^#(x, s(0())) -> c_5() 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.34 , divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Strict Trs: 8.09/2.34 { prime(0()) -> false() 8.09/2.34 , prime(s(0())) -> false() 8.09/2.34 , prime(s(s(x))) -> prime1(s(s(x)), s(x)) 8.09/2.34 , prime1(x, 0()) -> false() 8.09/2.34 , prime1(x, s(0())) -> true() 8.09/2.34 , prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y))) 8.09/2.34 , divp(x, y) -> =(rem(x, y), 0()) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 No rule is usable, rules are removed from the input problem. 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime^#(0()) -> c_1() 8.09/2.34 , prime^#(s(0())) -> c_2() 8.09/2.34 , prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, 0()) -> c_4() 8.09/2.34 , prime1^#(x, s(0())) -> c_5() 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.34 , divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 The weightgap principle applies (using the following constant 8.09/2.34 growth matrix-interpretation) 8.09/2.34 8.09/2.34 The following argument positions are usable: 8.09/2.34 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.34 8.09/2.34 TcT has computed the following constructor-restricted matrix 8.09/2.34 interpretation. 8.09/2.34 8.09/2.34 [0] = [0] 8.09/2.34 [0] 8.09/2.34 8.09/2.34 [s](x1) = [0] 8.09/2.34 [0] 8.09/2.34 8.09/2.34 [prime^#](x1) = [0] 8.09/2.34 [0] 8.09/2.34 8.09/2.34 [c_1] = [1] 8.09/2.34 [0] 8.09/2.34 8.09/2.34 [c_2] = [1] 8.09/2.34 [0] 8.09/2.34 8.09/2.34 [c_3](x1) = [1 0] x1 + [1] 8.09/2.34 [0 1] [0] 8.09/2.34 8.09/2.34 [prime1^#](x1, x2) = [0] 8.09/2.34 [0] 8.09/2.34 8.09/2.34 [c_4] = [1] 8.09/2.34 [0] 8.09/2.34 8.09/2.34 [c_5] = [1] 8.09/2.34 [0] 8.09/2.34 8.09/2.34 [c_6](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 8.09/2.34 [0 1] [0 1] [0] 8.09/2.34 8.09/2.34 [divp^#](x1, x2) = [0 0] x2 + [1] 8.09/2.34 [2 2] [0] 8.09/2.34 8.09/2.34 [c_7](x1, x2) = [0 0] x2 + [0] 8.09/2.34 [1 1] [0] 8.09/2.34 8.09/2.34 The order satisfies the following ordering constraints: 8.09/2.34 8.09/2.34 [prime^#(0())] = [0] 8.09/2.34 [0] 8.09/2.34 ? [1] 8.09/2.34 [0] 8.09/2.34 = [c_1()] 8.09/2.34 8.09/2.34 [prime^#(s(0()))] = [0] 8.09/2.34 [0] 8.09/2.34 ? [1] 8.09/2.34 [0] 8.09/2.34 = [c_2()] 8.09/2.34 8.09/2.34 [prime^#(s(s(x)))] = [0] 8.09/2.34 [0] 8.09/2.34 ? [1] 8.09/2.34 [0] 8.09/2.34 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.34 8.09/2.34 [prime1^#(x, 0())] = [0] 8.09/2.34 [0] 8.09/2.34 ? [1] 8.09/2.34 [0] 8.09/2.34 = [c_4()] 8.09/2.34 8.09/2.34 [prime1^#(x, s(0()))] = [0] 8.09/2.34 [0] 8.09/2.34 ? [1] 8.09/2.34 [0] 8.09/2.34 = [c_5()] 8.09/2.34 8.09/2.34 [prime1^#(x, s(s(y)))] = [0] 8.09/2.34 [0] 8.09/2.34 ? [0 0] x + [1] 8.09/2.34 [2 2] [0] 8.09/2.34 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.34 8.09/2.34 [divp^#(x, y)] = [0 0] y + [1] 8.09/2.34 [2 2] [0] 8.09/2.34 > [0 0] y + [0] 8.09/2.34 [1 1] [0] 8.09/2.34 = [c_7(x, y)] 8.09/2.34 8.09/2.34 8.09/2.34 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(?,O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime^#(0()) -> c_1() 8.09/2.34 , prime^#(s(0())) -> c_2() 8.09/2.34 , prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, 0()) -> c_4() 8.09/2.34 , prime1^#(x, s(0())) -> c_5() 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.34 Weak DPs: { divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(?,O(n^1)) 8.09/2.34 8.09/2.34 We employ 'linear path analysis' using the following approximated 8.09/2.34 dependency graph: 8.09/2.34 ->{3,7,6} [ ? ] 8.09/2.34 | 8.09/2.34 |->{1} [ YES(O(1),O(n^1)) ] 8.09/2.34 | 8.09/2.34 |->{2} [ YES(O(1),O(n^1)) ] 8.09/2.34 | 8.09/2.34 |->{4} [ YES(O(1),O(n^1)) ] 8.09/2.34 | 8.09/2.34 `->{5} [ YES(O(1),O(n^1)) ] 8.09/2.34 8.09/2.34 8.09/2.34 Here dependency-pairs are as follows: 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { 1: prime^#(0()) -> c_1() 8.09/2.34 , 2: prime^#(s(0())) -> c_2() 8.09/2.34 , 3: prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , 4: prime1^#(x, 0()) -> c_4() 8.09/2.34 , 5: prime1^#(x, s(0())) -> c_5() 8.09/2.34 , 6: prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.34 Weak DPs: 8.09/2.34 { 7: divp^#(x, y) -> c_7(x, y) } 8.09/2.34 8.09/2.34 * Path {3,7,6}->{1}: YES(O(1),O(n^1)) 8.09/2.34 ----------------------------------- 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime^#(0()) -> c_1() 8.09/2.34 , prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.34 Weak DPs: { divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.34 orient following rules strictly. 8.09/2.34 8.09/2.34 DPs: 8.09/2.34 { 1: prime^#(0()) -> c_1() 8.09/2.34 , 2: prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) } 8.09/2.34 8.09/2.34 Sub-proof: 8.09/2.34 ---------- 8.09/2.34 The following argument positions are usable: 8.09/2.34 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.34 8.09/2.34 TcT has computed the following constructor-based matrix 8.09/2.34 interpretation satisfying not(EDA). 8.09/2.34 8.09/2.34 [0] = [7] 8.09/2.34 8.09/2.34 [s](x1) = [0] 8.09/2.34 8.09/2.34 [prime^#](x1) = [4] 8.09/2.34 8.09/2.34 [c_1] = [3] 8.09/2.34 8.09/2.34 [c_3](x1) = [4] x1 + [3] 8.09/2.34 8.09/2.34 [prime1^#](x1, x2) = [0] 8.09/2.34 8.09/2.34 [c_6](x1, x2) = [4] x1 + [4] x2 + [0] 8.09/2.34 8.09/2.34 [divp^#](x1, x2) = [0] 8.09/2.34 8.09/2.34 [c_7](x1, x2) = [0] 8.09/2.34 8.09/2.34 The order satisfies the following ordering constraints: 8.09/2.34 8.09/2.34 [prime^#(0())] = [4] 8.09/2.34 > [3] 8.09/2.34 = [c_1()] 8.09/2.34 8.09/2.34 [prime^#(s(s(x)))] = [4] 8.09/2.34 > [3] 8.09/2.34 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.34 8.09/2.34 [prime1^#(x, s(s(y)))] = [0] 8.09/2.34 >= [0] 8.09/2.34 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.34 8.09/2.34 [divp^#(x, y)] = [0] 8.09/2.34 >= [0] 8.09/2.34 = [c_7(x, y)] 8.09/2.34 8.09/2.34 8.09/2.34 The strictly oriented rules are moved into the weak component. 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.34 Weak DPs: 8.09/2.34 { prime^#(0()) -> c_1() 8.09/2.34 , prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 The following weak DPs constitute a sub-graph of the DG that is 8.09/2.34 closed under successors. The DPs are removed. 8.09/2.34 8.09/2.34 { prime^#(0()) -> c_1() } 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.34 Weak DPs: 8.09/2.34 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.34 orient following rules strictly. 8.09/2.34 8.09/2.34 DPs: 8.09/2.34 { 1: prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.34 , 2: prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) } 8.09/2.34 8.09/2.34 Sub-proof: 8.09/2.34 ---------- 8.09/2.34 The following argument positions are usable: 8.09/2.34 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.34 8.09/2.34 TcT has computed the following constructor-based matrix 8.09/2.34 interpretation satisfying not(EDA). 8.09/2.34 8.09/2.34 [0] = [0] 8.09/2.34 8.09/2.34 [s](x1) = [1] x1 + [4] 8.09/2.34 8.09/2.34 [prime^#](x1) = [1] x1 + [7] 8.09/2.34 8.09/2.34 [c_1] = [0] 8.09/2.34 8.09/2.34 [c_3](x1) = [1] x1 + [7] 8.09/2.34 8.09/2.34 [prime1^#](x1, x2) = [1] x2 + [0] 8.09/2.34 8.09/2.34 [c_6](x1, x2) = [4] x1 + [1] x2 + [1] 8.09/2.34 8.09/2.34 [divp^#](x1, x2) = [0] 8.09/2.34 8.09/2.34 [c_7](x1, x2) = [0] 8.09/2.34 8.09/2.34 The order satisfies the following ordering constraints: 8.09/2.34 8.09/2.34 [prime^#(s(s(x)))] = [1] x + [15] 8.09/2.34 > [1] x + [11] 8.09/2.34 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.34 8.09/2.34 [prime1^#(x, s(s(y)))] = [1] y + [8] 8.09/2.34 > [1] y + [5] 8.09/2.34 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.34 8.09/2.34 [divp^#(x, y)] = [0] 8.09/2.34 >= [0] 8.09/2.34 = [c_7(x, y)] 8.09/2.34 8.09/2.34 8.09/2.34 The strictly oriented rules are moved into the weak component. 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(1)). 8.09/2.34 8.09/2.34 Weak DPs: 8.09/2.34 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.34 , divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(1)) 8.09/2.34 8.09/2.34 The following weak DPs constitute a sub-graph of the DG that is 8.09/2.34 closed under successors. The DPs are removed. 8.09/2.34 8.09/2.34 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.34 , divp^#(x, y) -> c_7(x, y) } 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(1)). 8.09/2.34 8.09/2.34 Rules: Empty 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(1)) 8.09/2.34 8.09/2.34 Empty rules are trivially bounded 8.09/2.34 8.09/2.34 * Path {3,7,6}->{2}: YES(O(1),O(n^1)) 8.09/2.34 ----------------------------------- 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime^#(s(0())) -> c_2() 8.09/2.34 , prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.34 Weak DPs: { divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.34 orient following rules strictly. 8.09/2.34 8.09/2.34 DPs: 8.09/2.34 { 1: prime^#(s(0())) -> c_2() } 8.09/2.34 8.09/2.34 Sub-proof: 8.09/2.34 ---------- 8.09/2.34 The following argument positions are usable: 8.09/2.34 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.34 8.09/2.34 TcT has computed the following constructor-based matrix 8.09/2.34 interpretation satisfying not(EDA). 8.09/2.34 8.09/2.34 [0] = [7] 8.09/2.34 8.09/2.34 [s](x1) = [0] 8.09/2.34 8.09/2.34 [prime^#](x1) = [1] 8.09/2.34 8.09/2.34 [c_2] = [0] 8.09/2.34 8.09/2.34 [c_3](x1) = [4] x1 + [1] 8.09/2.34 8.09/2.34 [prime1^#](x1, x2) = [0] 8.09/2.34 8.09/2.34 [c_6](x1, x2) = [4] x1 + [4] x2 + [0] 8.09/2.34 8.09/2.34 [divp^#](x1, x2) = [0] 8.09/2.34 8.09/2.34 [c_7](x1, x2) = [0] 8.09/2.34 8.09/2.34 The order satisfies the following ordering constraints: 8.09/2.34 8.09/2.34 [prime^#(s(0()))] = [1] 8.09/2.34 > [0] 8.09/2.34 = [c_2()] 8.09/2.34 8.09/2.34 [prime^#(s(s(x)))] = [1] 8.09/2.34 >= [1] 8.09/2.34 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.34 8.09/2.34 [prime1^#(x, s(s(y)))] = [0] 8.09/2.34 >= [0] 8.09/2.34 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.34 8.09/2.34 [divp^#(x, y)] = [0] 8.09/2.34 >= [0] 8.09/2.34 = [c_7(x, y)] 8.09/2.34 8.09/2.34 8.09/2.34 The strictly oriented rules are moved into the weak component. 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.34 Weak DPs: 8.09/2.34 { prime^#(s(0())) -> c_2() 8.09/2.34 , divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 The following weak DPs constitute a sub-graph of the DG that is 8.09/2.34 closed under successors. The DPs are removed. 8.09/2.34 8.09/2.34 { prime^#(s(0())) -> c_2() } 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.34 Weak DPs: { divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.34 orient following rules strictly. 8.09/2.34 8.09/2.34 DPs: 8.09/2.34 { 1: prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) } 8.09/2.34 8.09/2.34 Sub-proof: 8.09/2.34 ---------- 8.09/2.34 The following argument positions are usable: 8.09/2.34 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.34 8.09/2.34 TcT has computed the following constructor-based matrix 8.09/2.34 interpretation satisfying not(EDA). 8.09/2.34 8.09/2.34 [0] = [0] 8.09/2.34 8.09/2.34 [s](x1) = [0] 8.09/2.34 8.09/2.34 [prime^#](x1) = [7] 8.09/2.34 8.09/2.34 [c_2] = [0] 8.09/2.34 8.09/2.34 [c_3](x1) = [4] x1 + [1] 8.09/2.34 8.09/2.34 [prime1^#](x1, x2) = [0] 8.09/2.34 8.09/2.34 [c_6](x1, x2) = [4] x1 + [2] x2 + [0] 8.09/2.34 8.09/2.34 [divp^#](x1, x2) = [0] 8.09/2.34 8.09/2.34 [c_7](x1, x2) = [0] 8.09/2.34 8.09/2.34 The order satisfies the following ordering constraints: 8.09/2.34 8.09/2.34 [prime^#(s(s(x)))] = [7] 8.09/2.34 > [1] 8.09/2.34 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.34 8.09/2.34 [prime1^#(x, s(s(y)))] = [0] 8.09/2.34 >= [0] 8.09/2.34 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.34 8.09/2.34 [divp^#(x, y)] = [0] 8.09/2.34 >= [0] 8.09/2.34 = [c_7(x, y)] 8.09/2.34 8.09/2.34 8.09/2.34 The strictly oriented rules are moved into the weak component. 8.09/2.34 8.09/2.34 We are left with following problem, upon which TcT provides the 8.09/2.34 certificate YES(O(1),O(n^1)). 8.09/2.34 8.09/2.34 Strict DPs: 8.09/2.34 { prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.34 Weak DPs: 8.09/2.34 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.34 , divp^#(x, y) -> c_7(x, y) } 8.09/2.34 Obligation: 8.09/2.34 runtime complexity 8.09/2.34 Answer: 8.09/2.34 YES(O(1),O(n^1)) 8.09/2.34 8.09/2.34 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.34 orient following rules strictly. 8.09/2.34 8.09/2.34 DPs: 8.09/2.34 { 1: prime1^#(x, s(s(y))) -> 8.09/2.34 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.34 , 2: prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) } 8.09/2.34 8.09/2.34 Sub-proof: 8.09/2.34 ---------- 8.09/2.34 The following argument positions are usable: 8.09/2.34 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.34 8.09/2.34 TcT has computed the following constructor-based matrix 8.09/2.34 interpretation satisfying not(EDA). 8.09/2.34 8.09/2.34 [0] = [0] 8.09/2.34 8.09/2.34 [s](x1) = [1] x1 + [4] 8.09/2.34 8.09/2.34 [prime^#](x1) = [1] x1 + [7] 8.09/2.34 8.09/2.34 [c_2] = [0] 8.09/2.34 8.09/2.34 [c_3](x1) = [1] x1 + [7] 8.09/2.34 8.09/2.34 [prime1^#](x1, x2) = [1] x2 + [0] 8.09/2.34 8.09/2.34 [c_6](x1, x2) = [4] x1 + [1] x2 + [1] 8.09/2.34 8.09/2.34 [divp^#](x1, x2) = [0] 8.09/2.34 8.09/2.34 [c_7](x1, x2) = [0] 8.09/2.34 8.09/2.34 The order satisfies the following ordering constraints: 8.09/2.34 8.09/2.34 [prime^#(s(s(x)))] = [1] x + [15] 8.09/2.34 > [1] x + [11] 8.09/2.34 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.34 8.09/2.34 [prime1^#(x, s(s(y)))] = [1] y + [8] 8.09/2.34 > [1] y + [5] 8.09/2.34 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.35 8.09/2.35 [divp^#(x, y)] = [0] 8.09/2.35 >= [0] 8.09/2.35 = [c_7(x, y)] 8.09/2.35 8.09/2.35 8.09/2.35 The strictly oriented rules are moved into the weak component. 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(1)). 8.09/2.35 8.09/2.35 Weak DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(1)) 8.09/2.35 8.09/2.35 The following weak DPs constitute a sub-graph of the DG that is 8.09/2.35 closed under successors. The DPs are removed. 8.09/2.35 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(1)). 8.09/2.35 8.09/2.35 Rules: Empty 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(1)) 8.09/2.35 8.09/2.35 Empty rules are trivially bounded 8.09/2.35 8.09/2.35 * Path {3,7,6}->{4}: YES(O(1),O(n^1)) 8.09/2.35 ----------------------------------- 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(n^1)). 8.09/2.35 8.09/2.35 Strict DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, 0()) -> c_4() 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.35 Weak DPs: { divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(n^1)) 8.09/2.35 8.09/2.35 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.35 orient following rules strictly. 8.09/2.35 8.09/2.35 DPs: 8.09/2.35 { 2: prime1^#(x, 0()) -> c_4() } 8.09/2.35 8.09/2.35 Sub-proof: 8.09/2.35 ---------- 8.09/2.35 The following argument positions are usable: 8.09/2.35 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.35 8.09/2.35 TcT has computed the following constructor-based matrix 8.09/2.35 interpretation satisfying not(EDA). 8.09/2.35 8.09/2.35 [0] = [7] 8.09/2.35 8.09/2.35 [s](x1) = [0] 8.09/2.35 8.09/2.35 [prime^#](x1) = [7] 8.09/2.35 8.09/2.35 [c_3](x1) = [4] x1 + [3] 8.09/2.35 8.09/2.35 [prime1^#](x1, x2) = [1] 8.09/2.35 8.09/2.35 [c_4] = [0] 8.09/2.35 8.09/2.35 [c_6](x1, x2) = [4] x1 + [1] x2 + [0] 8.09/2.35 8.09/2.35 [divp^#](x1, x2) = [0] 8.09/2.35 8.09/2.35 [c_7](x1, x2) = [0] 8.09/2.35 8.09/2.35 The order satisfies the following ordering constraints: 8.09/2.35 8.09/2.35 [prime^#(s(s(x)))] = [7] 8.09/2.35 >= [7] 8.09/2.35 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.35 8.09/2.35 [prime1^#(x, 0())] = [1] 8.09/2.35 > [0] 8.09/2.35 = [c_4()] 8.09/2.35 8.09/2.35 [prime1^#(x, s(s(y)))] = [1] 8.09/2.35 >= [1] 8.09/2.35 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.35 8.09/2.35 [divp^#(x, y)] = [0] 8.09/2.35 >= [0] 8.09/2.35 = [c_7(x, y)] 8.09/2.35 8.09/2.35 8.09/2.35 The strictly oriented rules are moved into the weak component. 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(n^1)). 8.09/2.35 8.09/2.35 Strict DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.35 Weak DPs: 8.09/2.35 { prime1^#(x, 0()) -> c_4() 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(n^1)) 8.09/2.35 8.09/2.35 The following weak DPs constitute a sub-graph of the DG that is 8.09/2.35 closed under successors. The DPs are removed. 8.09/2.35 8.09/2.35 { prime1^#(x, 0()) -> c_4() } 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(n^1)). 8.09/2.35 8.09/2.35 Strict DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.35 Weak DPs: { divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(n^1)) 8.09/2.35 8.09/2.35 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.35 orient following rules strictly. 8.09/2.35 8.09/2.35 DPs: 8.09/2.35 { 1: prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) } 8.09/2.35 8.09/2.35 Sub-proof: 8.09/2.35 ---------- 8.09/2.35 The following argument positions are usable: 8.09/2.35 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.35 8.09/2.35 TcT has computed the following constructor-based matrix 8.09/2.35 interpretation satisfying not(EDA). 8.09/2.35 8.09/2.35 [0] = [0] 8.09/2.35 8.09/2.35 [s](x1) = [0] 8.09/2.35 8.09/2.35 [prime^#](x1) = [7] 8.09/2.35 8.09/2.35 [c_3](x1) = [4] x1 + [1] 8.09/2.35 8.09/2.35 [prime1^#](x1, x2) = [0] 8.09/2.35 8.09/2.35 [c_4] = [0] 8.09/2.35 8.09/2.35 [c_6](x1, x2) = [4] x1 + [2] x2 + [0] 8.09/2.35 8.09/2.35 [divp^#](x1, x2) = [0] 8.09/2.35 8.09/2.35 [c_7](x1, x2) = [0] 8.09/2.35 8.09/2.35 The order satisfies the following ordering constraints: 8.09/2.35 8.09/2.35 [prime^#(s(s(x)))] = [7] 8.09/2.35 > [1] 8.09/2.35 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.35 8.09/2.35 [prime1^#(x, s(s(y)))] = [0] 8.09/2.35 >= [0] 8.09/2.35 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.35 8.09/2.35 [divp^#(x, y)] = [0] 8.09/2.35 >= [0] 8.09/2.35 = [c_7(x, y)] 8.09/2.35 8.09/2.35 8.09/2.35 The strictly oriented rules are moved into the weak component. 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(n^1)). 8.09/2.35 8.09/2.35 Strict DPs: 8.09/2.35 { prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.35 Weak DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(n^1)) 8.09/2.35 8.09/2.35 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.35 orient following rules strictly. 8.09/2.35 8.09/2.35 DPs: 8.09/2.35 { 1: prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.35 , 2: prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) } 8.09/2.35 8.09/2.35 Sub-proof: 8.09/2.35 ---------- 8.09/2.35 The following argument positions are usable: 8.09/2.35 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.35 8.09/2.35 TcT has computed the following constructor-based matrix 8.09/2.35 interpretation satisfying not(EDA). 8.09/2.35 8.09/2.35 [0] = [0] 8.09/2.35 8.09/2.35 [s](x1) = [1] x1 + [4] 8.09/2.35 8.09/2.35 [prime^#](x1) = [1] x1 + [7] 8.09/2.35 8.09/2.35 [c_3](x1) = [1] x1 + [7] 8.09/2.35 8.09/2.35 [prime1^#](x1, x2) = [1] x2 + [0] 8.09/2.35 8.09/2.35 [c_4] = [0] 8.09/2.35 8.09/2.35 [c_6](x1, x2) = [4] x1 + [1] x2 + [1] 8.09/2.35 8.09/2.35 [divp^#](x1, x2) = [0] 8.09/2.35 8.09/2.35 [c_7](x1, x2) = [0] 8.09/2.35 8.09/2.35 The order satisfies the following ordering constraints: 8.09/2.35 8.09/2.35 [prime^#(s(s(x)))] = [1] x + [15] 8.09/2.35 > [1] x + [11] 8.09/2.35 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.35 8.09/2.35 [prime1^#(x, s(s(y)))] = [1] y + [8] 8.09/2.35 > [1] y + [5] 8.09/2.35 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.35 8.09/2.35 [divp^#(x, y)] = [0] 8.09/2.35 >= [0] 8.09/2.35 = [c_7(x, y)] 8.09/2.35 8.09/2.35 8.09/2.35 The strictly oriented rules are moved into the weak component. 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(1)). 8.09/2.35 8.09/2.35 Weak DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(1)) 8.09/2.35 8.09/2.35 The following weak DPs constitute a sub-graph of the DG that is 8.09/2.35 closed under successors. The DPs are removed. 8.09/2.35 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(1)). 8.09/2.35 8.09/2.35 Rules: Empty 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(1)) 8.09/2.35 8.09/2.35 Empty rules are trivially bounded 8.09/2.35 8.09/2.35 * Path {3,7,6}->{5}: YES(O(1),O(n^1)) 8.09/2.35 ----------------------------------- 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(n^1)). 8.09/2.35 8.09/2.35 Strict DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(0())) -> c_5() 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.35 Weak DPs: { divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(n^1)) 8.09/2.35 8.09/2.35 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.35 orient following rules strictly. 8.09/2.35 8.09/2.35 DPs: 8.09/2.35 { 1: prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , 2: prime1^#(x, s(0())) -> c_5() } 8.09/2.35 8.09/2.35 Sub-proof: 8.09/2.35 ---------- 8.09/2.35 The following argument positions are usable: 8.09/2.35 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.35 8.09/2.35 TcT has computed the following constructor-based matrix 8.09/2.35 interpretation satisfying not(EDA). 8.09/2.35 8.09/2.35 [0] = [7] 8.09/2.35 8.09/2.35 [s](x1) = [0] 8.09/2.35 8.09/2.35 [prime^#](x1) = [7] 8.09/2.35 8.09/2.35 [c_3](x1) = [1] x1 + [1] 8.09/2.35 8.09/2.35 [prime1^#](x1, x2) = [1] 8.09/2.35 8.09/2.35 [c_5] = [0] 8.09/2.35 8.09/2.35 [c_6](x1, x2) = [2] x1 + [1] x2 + [0] 8.09/2.35 8.09/2.35 [divp^#](x1, x2) = [0] 8.09/2.35 8.09/2.35 [c_7](x1, x2) = [0] 8.09/2.35 8.09/2.35 The order satisfies the following ordering constraints: 8.09/2.35 8.09/2.35 [prime^#(s(s(x)))] = [7] 8.09/2.35 > [2] 8.09/2.35 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.35 8.09/2.35 [prime1^#(x, s(0()))] = [1] 8.09/2.35 > [0] 8.09/2.35 = [c_5()] 8.09/2.35 8.09/2.35 [prime1^#(x, s(s(y)))] = [1] 8.09/2.35 >= [1] 8.09/2.35 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.35 8.09/2.35 [divp^#(x, y)] = [0] 8.09/2.35 >= [0] 8.09/2.35 = [c_7(x, y)] 8.09/2.35 8.09/2.35 8.09/2.35 The strictly oriented rules are moved into the weak component. 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(n^1)). 8.09/2.35 8.09/2.35 Strict DPs: 8.09/2.35 { prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.35 Weak DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(0())) -> c_5() 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(n^1)) 8.09/2.35 8.09/2.35 The following weak DPs constitute a sub-graph of the DG that is 8.09/2.35 closed under successors. The DPs are removed. 8.09/2.35 8.09/2.35 { prime1^#(x, s(0())) -> c_5() } 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(n^1)). 8.09/2.35 8.09/2.35 Strict DPs: 8.09/2.35 { prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) } 8.09/2.35 Weak DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(n^1)) 8.09/2.35 8.09/2.35 We use the processor 'matrix interpretation of dimension 1' to 8.09/2.35 orient following rules strictly. 8.09/2.35 8.09/2.35 DPs: 8.09/2.35 { 1: prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.35 , 2: prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) } 8.09/2.35 8.09/2.35 Sub-proof: 8.09/2.35 ---------- 8.09/2.35 The following argument positions are usable: 8.09/2.35 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2} 8.09/2.35 8.09/2.35 TcT has computed the following constructor-based matrix 8.09/2.35 interpretation satisfying not(EDA). 8.09/2.35 8.09/2.35 [0] = [0] 8.09/2.35 8.09/2.35 [s](x1) = [1] x1 + [4] 8.09/2.35 8.09/2.35 [prime^#](x1) = [1] x1 + [7] 8.09/2.35 8.09/2.35 [c_3](x1) = [1] x1 + [7] 8.09/2.35 8.09/2.35 [prime1^#](x1, x2) = [1] x2 + [0] 8.09/2.35 8.09/2.35 [c_5] = [0] 8.09/2.35 8.09/2.35 [c_6](x1, x2) = [4] x1 + [1] x2 + [1] 8.09/2.35 8.09/2.35 [divp^#](x1, x2) = [0] 8.09/2.35 8.09/2.35 [c_7](x1, x2) = [0] 8.09/2.35 8.09/2.35 The order satisfies the following ordering constraints: 8.09/2.35 8.09/2.35 [prime^#(s(s(x)))] = [1] x + [15] 8.09/2.35 > [1] x + [11] 8.09/2.35 = [c_3(prime1^#(s(s(x)), s(x)))] 8.09/2.35 8.09/2.35 [prime1^#(x, s(s(y)))] = [1] y + [8] 8.09/2.35 > [1] y + [5] 8.09/2.35 = [c_6(divp^#(s(s(y)), x), prime1^#(x, s(y)))] 8.09/2.35 8.09/2.35 [divp^#(x, y)] = [0] 8.09/2.35 >= [0] 8.09/2.35 = [c_7(x, y)] 8.09/2.35 8.09/2.35 8.09/2.35 The strictly oriented rules are moved into the weak component. 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(1)). 8.09/2.35 8.09/2.35 Weak DPs: 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(1)) 8.09/2.35 8.09/2.35 The following weak DPs constitute a sub-graph of the DG that is 8.09/2.35 closed under successors. The DPs are removed. 8.09/2.35 8.09/2.35 { prime^#(s(s(x))) -> c_3(prime1^#(s(s(x)), s(x))) 8.09/2.35 , prime1^#(x, s(s(y))) -> 8.09/2.35 c_6(divp^#(s(s(y)), x), prime1^#(x, s(y))) 8.09/2.35 , divp^#(x, y) -> c_7(x, y) } 8.09/2.35 8.09/2.35 We are left with following problem, upon which TcT provides the 8.09/2.35 certificate YES(O(1),O(1)). 8.09/2.35 8.09/2.35 Rules: Empty 8.09/2.35 Obligation: 8.09/2.35 runtime complexity 8.09/2.35 Answer: 8.09/2.35 YES(O(1),O(1)) 8.09/2.35 8.09/2.35 Empty rules are trivially bounded 8.09/2.35 8.09/2.35 Hurray, we answered YES(O(1),O(n^1)) 8.09/2.35 EOF