MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, 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: { minus^#(x, 0()) -> c_1() , minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , plus^#(0(), y) -> c_6() , plus^#(s(x), y) -> c_7(plus^#(x, y)) , quot^#(0(), s(y)) -> c_4() , quot^#(s(x), s(y)) -> c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(x, 0()) -> c_1() , minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , plus^#(0(), y) -> c_6() , plus^#(s(x), y) -> c_7(plus^#(x, y)) , quot^#(0(), s(y)) -> c_4() , quot^#(s(x), s(y)) -> c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,4,6} by applications of Pre({1,4,6}) = {2,3,5,7}. Here rules are labeled as follows: DPs: { 1: minus^#(x, 0()) -> c_1() , 2: minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , 3: minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , 4: plus^#(0(), y) -> c_6() , 5: plus^#(s(x), y) -> c_7(plus^#(x, y)) , 6: quot^#(0(), s(y)) -> c_4() , 7: quot^#(s(x), s(y)) -> c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , plus^#(s(x), y) -> c_7(plus^#(x, y)) , quot^#(s(x), s(y)) -> c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak DPs: { minus^#(x, 0()) -> c_1() , plus^#(0(), y) -> c_6() , quot^#(0(), s(y)) -> c_4() } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, 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. { minus^#(x, 0()) -> c_1() , plus^#(0(), y) -> c_6() , quot^#(0(), s(y)) -> c_4() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , plus^#(s(x), y) -> c_7(plus^#(x, y)) , quot^#(s(x), s(y)) -> c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , plus^#(s(x), y) -> c_7(plus^#(x, y)) , quot^#(s(x), s(y)) -> c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, 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) '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_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } and lower component { minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , plus^#(s(x), y) -> c_7(plus^#(x, y)) } Further, following extension rules are added to the lower component. { quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(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_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } 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_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Trs: { minus(s(x), s(y)) -> minus(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(minus) = {1, 2}, safe(0) = {}, safe(s) = {1}, safe(quot) = {}, safe(plus) = {1}, safe(minus^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(plus^#) = {}, safe(c_3) = {}, safe(quot^#) = {2}, safe(c_4) = {}, safe(c_5) = {}, 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(minus) = 1, pi(0) = [], pi(s) = [1], pi(quot) = [], pi(plus) = 2, pi(minus^#) = [], pi(c_1) = [], pi(c_2) = [], pi(plus^#) = [], pi(c_3) = [], pi(quot^#) = [1], pi(c_4) = [], pi(c_5) = [1, 2], pi(c_6) = [], pi(c_7) = [] Usable defined function symbols are a subset of: {minus, minus^#, plus^#, quot^#} For your convenience, here are the satisfied ordering constraints: pi(quot^#(s(x), s(y))) = quot^#(s(; x);) > c_5(quot^#(x;), minus^#();) = pi(c_5(quot^#(minus(x, y), s(y)), minus^#(x, y))) pi(minus(x, 0())) = x >= x = pi(x) pi(minus(minus(x, y), z)) = x >= x = pi(minus(x, plus(y, z))) pi(minus(s(x), s(y))) = s(; x) > x = pi(minus(x, y)) 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_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } 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_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } 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: { minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , plus^#(s(x), y) -> c_7(plus^#(x, y)) } Weak DPs: { quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: MAYBE We decompose the input problem according to the dependency graph into the upper component { minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } and lower component { plus^#(s(x), y) -> c_7(plus^#(x, y)) } Further, following extension rules are added to the lower component. { minus^#(minus(x, y), z) -> minus^#(x, plus(y, z)) , minus^#(minus(x, y), z) -> plus^#(y, z) , minus^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(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: { minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) } Weak DPs: { quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } 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: minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , 2: minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , 3: quot^#(s(x), s(y)) -> minus^#(x, y) } Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> 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(minus) = {1, 2}, safe(0) = {}, safe(s) = {1}, safe(quot) = {}, safe(plus) = {2}, safe(minus^#) = {2}, safe(c_1) = {}, safe(c_2) = {}, safe(plus^#) = {}, safe(c_3) = {}, safe(quot^#) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(c_7) = {} and precedence quot^# > plus, quot^# > minus^#, plus ~ minus^# . Following symbols are considered recursive: {minus^#} The recursion depth is 1. Further, following argument filtering is employed: pi(minus) = [1], pi(0) = [], pi(s) = [1], pi(quot) = [], pi(plus) = [1, 2], pi(minus^#) = [1], pi(c_1) = [], pi(c_2) = [1, 2], pi(plus^#) = [], pi(c_3) = [1], pi(quot^#) = [1], pi(c_4) = [], pi(c_5) = [], pi(c_6) = [], pi(c_7) = [] Usable defined function symbols are a subset of: {minus, minus^#, plus^#, quot^#} For your convenience, here are the satisfied ordering constraints: pi(minus^#(minus(x, y), z)) = minus^#(minus(; x);) > c_2(minus^#(x;), plus^#();) = pi(c_2(minus^#(x, plus(y, z)), plus^#(y, z))) pi(minus^#(s(x), s(y))) = minus^#(s(; x);) > c_3(minus^#(x;);) = pi(c_3(minus^#(x, y))) pi(quot^#(s(x), s(y))) = quot^#(s(; x);) > minus^#(x;) = pi(minus^#(x, y)) pi(quot^#(s(x), s(y))) = quot^#(s(; x);) >= quot^#(minus(; x);) = pi(quot^#(minus(x, y), s(y))) pi(minus(x, 0())) = minus(; x) > x = pi(x) pi(minus(minus(x, y), z)) = minus(; minus(; x)) > minus(; x) = pi(minus(x, plus(y, z))) pi(minus(s(x), s(y))) = minus(; s(; x)) > minus(; x) = pi(minus(x, y)) 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: { minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } 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. { minus^#(minus(x, y), z) -> c_2(minus^#(x, plus(y, z)), plus^#(y, z)) , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) , quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } 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_7(plus^#(x, y)) } Weak DPs: { minus^#(minus(x, y), z) -> minus^#(x, plus(y, z)) , minus^#(minus(x, y), z) -> plus^#(y, z) , minus^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } Weak Trs: { minus(x, 0()) -> x , minus(minus(x, y), z) -> minus(x, plus(y, z)) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, 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) '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 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. 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) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'bsearch-popstar (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 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. Arrrr..