MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) , quot(0(), s(Y)) -> 0() , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: We add the following dependency tuples: Strict DPs: { plus^#(0(), Y) -> c_1() , plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , min^#(X, 0()) -> c_3() , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , quot^#(0(), s(Y)) -> c_6() , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(0(), Y) -> c_1() , plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , min^#(X, 0()) -> c_3() , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , quot^#(0(), s(Y)) -> c_6() , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) , quot(0(), s(Y)) -> 0() , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,3,6} by applications of Pre({1,3,6}) = {2,4,5,7}. Here rules are labeled as follows: DPs: { 1: plus^#(0(), Y) -> c_1() , 2: plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , 3: min^#(X, 0()) -> c_3() , 4: min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , 5: min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , 6: quot^#(0(), s(Y)) -> c_6() , 7: quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } Weak DPs: { plus^#(0(), Y) -> c_1() , min^#(X, 0()) -> c_3() , quot^#(0(), s(Y)) -> c_6() } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) , quot(0(), s(Y)) -> 0() , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { plus^#(0(), Y) -> c_1() , min^#(X, 0()) -> c_3() , quot^#(0(), s(Y)) -> c_6() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) , quot(0(), s(Y)) -> 0() , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: We decompose the input problem according to the dependency graph into the upper component { quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } and lower component { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) } Further, following extension rules are added to the lower component. { quot^#(s(X), s(Y)) -> min^#(X, Y) , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. DPs: { 1: quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } Trs: { min(s(X), s(Y)) -> min(X, Y) } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(plus) = {1}, safe(0) = {}, safe(s) = {1}, safe(min) = {1, 2}, safe(Z) = {}, safe(quot) = {}, safe(plus^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(min^#) = {}, safe(c_3) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(quot^#) = {}, safe(c_6) = {}, safe(c_7) = {} and precedence empty . Following symbols are considered recursive: {plus, quot^#} The recursion depth is 1. Further, following argument filtering is employed: pi(plus) = 2, pi(0) = [], pi(s) = [1], pi(min) = 1, pi(Z) = [], pi(quot) = [], pi(plus^#) = [], pi(c_1) = [], pi(c_2) = [], pi(min^#) = [], pi(c_3) = [], pi(c_4) = [], pi(c_5) = [], pi(quot^#) = [1, 2], pi(c_6) = [], pi(c_7) = [1, 2] Usable defined function symbols are a subset of: {min, plus^#, min^#, quot^#} For your convenience, here are the satisfied ordering constraints: pi(quot^#(s(X), s(Y))) = quot^#(s(; X), s(; Y);) > c_7(quot^#(X, s(; Y);), min^#();) = pi(c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y))) pi(min(X, 0())) = X >= X = pi(X) pi(min(s(X), s(Y))) = s(; X) > X = pi(min(X, Y)) pi(min(min(X, Y), Z())) = X >= X = pi(min(X, plus(Y, Z()))) The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y)), min^#(X, Y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) , min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) } Weak DPs: { quot^#(s(X), s(Y)) -> min^#(X, Y) , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Obligation: innermost runtime complexity Answer: MAYBE We decompose the input problem according to the dependency graph into the upper component { min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , quot^#(s(X), s(Y)) -> min^#(X, Y) , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } and lower component { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) } Further, following extension rules are added to the lower component. { min^#(s(X), s(Y)) -> min^#(X, Y) , min^#(min(X, Y), Z()) -> plus^#(Y, Z()) , min^#(min(X, Y), Z()) -> min^#(X, plus(Y, Z())) , quot^#(s(X), s(Y)) -> min^#(X, Y) , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) } Weak DPs: { quot^#(s(X), s(Y)) -> min^#(X, Y) , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. DPs: { 1: min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , 2: min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , 3: quot^#(s(X), s(Y)) -> min^#(X, Y) } Trs: { min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(plus) = {}, safe(0) = {}, safe(s) = {1}, safe(min) = {1, 2}, safe(Z) = {}, safe(quot) = {}, safe(plus^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(min^#) = {2}, safe(c_3) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(quot^#) = {}, safe(c_6) = {}, safe(c_7) = {} and precedence quot^# > plus, quot^# > min^#, plus ~ min^# . Following symbols are considered recursive: {min^#} The recursion depth is 1. Further, following argument filtering is employed: pi(plus) = [], pi(0) = [], pi(s) = [1], pi(min) = [1], pi(Z) = [], pi(quot) = [], pi(plus^#) = [2], pi(c_1) = [], pi(c_2) = [], pi(min^#) = [1], pi(c_3) = [], pi(c_4) = [1], pi(c_5) = [1, 2], pi(quot^#) = [1], pi(c_6) = [], pi(c_7) = [] Usable defined function symbols are a subset of: {min, plus^#, min^#, quot^#} For your convenience, here are the satisfied ordering constraints: pi(min^#(s(X), s(Y))) = min^#(s(; X);) > c_4(min^#(X;);) = pi(c_4(min^#(X, Y))) pi(min^#(min(X, Y), Z())) = min^#(min(; X);) > c_5(min^#(X;), plus^#(Z(););) = pi(c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z()))) pi(quot^#(s(X), s(Y))) = quot^#(s(; X);) > min^#(X;) = pi(min^#(X, Y)) pi(quot^#(s(X), s(Y))) = quot^#(s(; X);) >= quot^#(min(; X);) = pi(quot^#(min(X, Y), s(Y))) pi(min(X, 0())) = min(; X) > X = pi(X) pi(min(s(X), s(Y))) = min(; s(; X)) > min(; X) = pi(min(X, Y)) pi(min(min(X, Y), Z())) = min(; min(; X)) > min(; X) = pi(min(X, plus(Y, Z()))) The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , quot^#(s(X), s(Y)) -> min^#(X, Y) , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { min^#(s(X), s(Y)) -> c_4(min^#(X, Y)) , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())), plus^#(Y, Z())) , quot^#(s(X), s(Y)) -> min^#(X, Y) , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(s(X), Y) -> c_2(plus^#(X, Y)) } Weak DPs: { min^#(s(X), s(Y)) -> min^#(X, Y) , min^#(min(X, Y), Z()) -> plus^#(Y, Z()) , min^#(min(X, Y), Z()) -> min^#(X, plus(Y, Z())) , quot^#(s(X), s(Y)) -> min^#(X, Y) , quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y)) } Weak Trs: { plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , min(X, 0()) -> X , min(s(X), s(Y)) -> min(X, Y) , min(min(X, Y), Z()) -> min(X, plus(Y, Z())) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 3) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..