MAYBE 196.20/102.67 MAYBE 196.20/102.67 196.20/102.67 We are left with following problem, upon which TcT provides the 196.20/102.67 certificate MAYBE. 196.20/102.67 196.20/102.67 Strict Trs: 196.20/102.67 { pred(s(x)) -> x 196.20/102.67 , minus(x, s(y)) -> pred(minus(x, y)) 196.20/102.67 , minus(x, 0()) -> x 196.20/102.67 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 196.20/102.67 , quot(0(), s(y)) -> 0() } 196.20/102.67 Obligation: 196.20/102.67 runtime complexity 196.20/102.67 Answer: 196.20/102.67 MAYBE 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'Best' failed due to the following reason: 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 196.20/102.67 seconds)' failed due to the following reason: 196.20/102.67 196.20/102.67 The weightgap principle applies (using the following nonconstant 196.20/102.67 growth matrix-interpretation) 196.20/102.67 196.20/102.67 The following argument positions are usable: 196.20/102.67 Uargs(pred) = {1}, Uargs(s) = {1}, Uargs(minus) = {1}, 196.20/102.67 Uargs(quot) = {1} 196.20/102.67 196.20/102.67 TcT has computed the following matrix interpretation satisfying 196.20/102.67 not(EDA) and not(IDA(1)). 196.20/102.67 196.20/102.67 [pred](x1) = [1] x1 + [7] 196.20/102.67 196.20/102.67 [s](x1) = [1] x1 + [0] 196.20/102.67 196.20/102.67 [minus](x1, x2) = [1] x1 + [0] 196.20/102.67 196.20/102.67 [0] = [7] 196.20/102.67 196.20/102.67 [quot](x1, x2) = [1] x1 + [0] 196.20/102.67 196.20/102.67 The order satisfies the following ordering constraints: 196.20/102.67 196.20/102.67 [pred(s(x))] = [1] x + [7] 196.20/102.67 > [1] x + [0] 196.20/102.67 = [x] 196.20/102.67 196.20/102.67 [minus(x, s(y))] = [1] x + [0] 196.20/102.67 ? [1] x + [7] 196.20/102.67 = [pred(minus(x, y))] 196.20/102.67 196.20/102.67 [minus(x, 0())] = [1] x + [0] 196.20/102.67 >= [1] x + [0] 196.20/102.67 = [x] 196.20/102.67 196.20/102.67 [quot(s(x), s(y))] = [1] x + [0] 196.20/102.67 >= [1] x + [0] 196.20/102.67 = [s(quot(minus(x, y), s(y)))] 196.20/102.67 196.20/102.67 [quot(0(), s(y))] = [7] 196.20/102.67 >= [7] 196.20/102.67 = [0()] 196.20/102.67 196.20/102.67 196.20/102.67 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 196.20/102.67 196.20/102.67 We are left with following problem, upon which TcT provides the 196.20/102.67 certificate MAYBE. 196.20/102.67 196.20/102.67 Strict Trs: 196.20/102.67 { minus(x, s(y)) -> pred(minus(x, y)) 196.20/102.67 , minus(x, 0()) -> x 196.20/102.67 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 196.20/102.67 , quot(0(), s(y)) -> 0() } 196.20/102.67 Weak Trs: { pred(s(x)) -> x } 196.20/102.67 Obligation: 196.20/102.67 runtime complexity 196.20/102.67 Answer: 196.20/102.67 MAYBE 196.20/102.67 196.20/102.67 The weightgap principle applies (using the following nonconstant 196.20/102.67 growth matrix-interpretation) 196.20/102.67 196.20/102.67 The following argument positions are usable: 196.20/102.67 Uargs(pred) = {1}, Uargs(s) = {1}, Uargs(minus) = {1}, 196.20/102.67 Uargs(quot) = {1} 196.20/102.67 196.20/102.67 TcT has computed the following matrix interpretation satisfying 196.20/102.67 not(EDA) and not(IDA(1)). 196.20/102.67 196.20/102.67 [pred](x1) = [1] x1 + [5] 196.20/102.67 196.20/102.67 [s](x1) = [1] x1 + [0] 196.20/102.67 196.20/102.67 [minus](x1, x2) = [1] x1 + [1] 196.20/102.67 196.20/102.67 [0] = [0] 196.20/102.67 196.20/102.67 [quot](x1, x2) = [1] x1 + [0] 196.20/102.67 196.20/102.67 The order satisfies the following ordering constraints: 196.20/102.67 196.20/102.67 [pred(s(x))] = [1] x + [5] 196.20/102.67 > [1] x + [0] 196.20/102.67 = [x] 196.20/102.67 196.20/102.67 [minus(x, s(y))] = [1] x + [1] 196.20/102.67 ? [1] x + [6] 196.20/102.67 = [pred(minus(x, y))] 196.20/102.67 196.20/102.67 [minus(x, 0())] = [1] x + [1] 196.20/102.67 > [1] x + [0] 196.20/102.67 = [x] 196.20/102.67 196.20/102.67 [quot(s(x), s(y))] = [1] x + [0] 196.20/102.67 ? [1] x + [1] 196.20/102.67 = [s(quot(minus(x, y), s(y)))] 196.20/102.67 196.20/102.67 [quot(0(), s(y))] = [0] 196.20/102.67 >= [0] 196.20/102.67 = [0()] 196.20/102.67 196.20/102.67 196.20/102.67 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 196.20/102.67 196.20/102.67 We are left with following problem, upon which TcT provides the 196.20/102.67 certificate MAYBE. 196.20/102.67 196.20/102.67 Strict Trs: 196.20/102.67 { minus(x, s(y)) -> pred(minus(x, y)) 196.20/102.67 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 196.20/102.67 , quot(0(), s(y)) -> 0() } 196.20/102.67 Weak Trs: 196.20/102.67 { pred(s(x)) -> x 196.20/102.67 , minus(x, 0()) -> x } 196.20/102.67 Obligation: 196.20/102.67 runtime complexity 196.20/102.67 Answer: 196.20/102.67 MAYBE 196.20/102.67 196.20/102.67 The weightgap principle applies (using the following nonconstant 196.20/102.67 growth matrix-interpretation) 196.20/102.67 196.20/102.67 The following argument positions are usable: 196.20/102.67 Uargs(pred) = {1}, Uargs(s) = {1}, Uargs(minus) = {1}, 196.20/102.67 Uargs(quot) = {1} 196.20/102.67 196.20/102.67 TcT has computed the following matrix interpretation satisfying 196.20/102.67 not(EDA) and not(IDA(1)). 196.20/102.67 196.20/102.67 [pred](x1) = [1] x1 + [3] 196.20/102.67 196.20/102.67 [s](x1) = [1] x1 + [0] 196.20/102.67 196.20/102.67 [minus](x1, x2) = [1] x1 + [4] 196.20/102.67 196.20/102.67 [0] = [0] 196.20/102.67 196.20/102.67 [quot](x1, x2) = [1] x1 + [4] 196.20/102.67 196.20/102.67 The order satisfies the following ordering constraints: 196.20/102.67 196.20/102.67 [pred(s(x))] = [1] x + [3] 196.20/102.67 > [1] x + [0] 196.20/102.67 = [x] 196.20/102.67 196.20/102.67 [minus(x, s(y))] = [1] x + [4] 196.20/102.67 ? [1] x + [7] 196.20/102.67 = [pred(minus(x, y))] 196.20/102.67 196.20/102.67 [minus(x, 0())] = [1] x + [4] 196.20/102.67 > [1] x + [0] 196.20/102.67 = [x] 196.20/102.67 196.20/102.67 [quot(s(x), s(y))] = [1] x + [4] 196.20/102.67 ? [1] x + [8] 196.20/102.67 = [s(quot(minus(x, y), s(y)))] 196.20/102.67 196.20/102.67 [quot(0(), s(y))] = [4] 196.20/102.67 > [0] 196.20/102.67 = [0()] 196.20/102.67 196.20/102.67 196.20/102.67 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 196.20/102.67 196.20/102.67 We are left with following problem, upon which TcT provides the 196.20/102.67 certificate MAYBE. 196.20/102.67 196.20/102.67 Strict Trs: 196.20/102.67 { minus(x, s(y)) -> pred(minus(x, y)) 196.20/102.67 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 196.20/102.67 Weak Trs: 196.20/102.67 { pred(s(x)) -> x 196.20/102.67 , minus(x, 0()) -> x 196.20/102.67 , quot(0(), s(y)) -> 0() } 196.20/102.67 Obligation: 196.20/102.67 runtime complexity 196.20/102.67 Answer: 196.20/102.67 MAYBE 196.20/102.67 196.20/102.67 We use the processor 'matrix interpretation of dimension 1' to 196.20/102.67 orient following rules strictly. 196.20/102.67 196.20/102.67 Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 196.20/102.67 196.20/102.67 The induced complexity on above rules (modulo remaining rules) is 196.20/102.67 YES(?,O(n^1)) . These rules are moved into the corresponding weak 196.20/102.67 component(s). 196.20/102.67 196.20/102.67 Sub-proof: 196.20/102.67 ---------- 196.20/102.67 The following argument positions are usable: 196.20/102.67 Uargs(pred) = {1}, Uargs(s) = {1}, Uargs(minus) = {1}, 196.20/102.67 Uargs(quot) = {1} 196.20/102.67 196.20/102.67 TcT has computed the following constructor-based matrix 196.20/102.67 interpretation satisfying not(EDA). 196.20/102.67 196.20/102.67 [pred](x1) = [1] x1 + [0] 196.20/102.67 196.20/102.67 [s](x1) = [1] x1 + [4] 196.20/102.67 196.20/102.67 [minus](x1, x2) = [1] x1 + [0] 196.20/102.67 196.20/102.67 [0] = [4] 196.20/102.67 196.20/102.67 [quot](x1, x2) = [2] x1 + [0] 196.20/102.67 196.20/102.67 The order satisfies the following ordering constraints: 196.20/102.67 196.20/102.67 [pred(s(x))] = [1] x + [4] 196.20/102.67 > [1] x + [0] 196.20/102.67 = [x] 196.20/102.67 196.20/102.67 [minus(x, s(y))] = [1] x + [0] 196.20/102.67 >= [1] x + [0] 196.20/102.67 = [pred(minus(x, y))] 196.20/102.67 196.20/102.67 [minus(x, 0())] = [1] x + [0] 196.20/102.67 >= [1] x + [0] 196.20/102.67 = [x] 196.20/102.67 196.20/102.67 [quot(s(x), s(y))] = [2] x + [8] 196.20/102.67 > [2] x + [4] 196.20/102.67 = [s(quot(minus(x, y), s(y)))] 196.20/102.67 196.20/102.67 [quot(0(), s(y))] = [8] 196.20/102.67 > [4] 196.20/102.67 = [0()] 196.20/102.67 196.20/102.67 196.20/102.67 We return to the main proof. 196.20/102.67 196.20/102.67 We are left with following problem, upon which TcT provides the 196.20/102.67 certificate MAYBE. 196.20/102.67 196.20/102.67 Strict Trs: { minus(x, s(y)) -> pred(minus(x, y)) } 196.20/102.67 Weak Trs: 196.20/102.67 { pred(s(x)) -> x 196.20/102.67 , minus(x, 0()) -> x 196.20/102.67 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 196.20/102.67 , quot(0(), s(y)) -> 0() } 196.20/102.67 Obligation: 196.20/102.67 runtime complexity 196.20/102.67 Answer: 196.20/102.67 MAYBE 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'empty' failed due to the following reason: 196.20/102.67 196.20/102.67 Empty strict component of the problem is NOT empty. 196.20/102.67 196.20/102.67 2) 'With Problem ...' failed due to the following reason: 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'empty' failed due to the following reason: 196.20/102.67 196.20/102.67 Empty strict component of the problem is NOT empty. 196.20/102.67 196.20/102.67 2) 'Fastest' failed due to the following reason: 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'With Problem ...' failed due to the following reason: 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'empty' failed due to the following reason: 196.20/102.67 196.20/102.67 Empty strict component of the problem is NOT empty. 196.20/102.67 196.20/102.67 2) 'With Problem ...' failed due to the following reason: 196.20/102.67 196.20/102.67 Empty strict component of the problem is NOT empty. 196.20/102.67 196.20/102.67 196.20/102.67 2) 'With Problem ...' failed due to the following reason: 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'empty' failed due to the following reason: 196.20/102.67 196.20/102.67 Empty strict component of the problem is NOT empty. 196.20/102.67 196.20/102.67 2) 'With Problem ...' failed due to the following reason: 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'empty' failed due to the following reason: 196.20/102.67 196.20/102.67 Empty strict component of the problem is NOT empty. 196.20/102.67 196.20/102.67 2) 'With Problem ...' failed due to the following reason: 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'empty' failed due to the following reason: 196.20/102.67 196.20/102.67 Empty strict component of the problem is NOT empty. 196.20/102.67 196.20/102.67 2) 'With Problem ...' failed due to the following reason: 196.20/102.67 196.20/102.67 Empty strict component of the problem is NOT empty. 196.20/102.67 196.20/102.67 196.20/102.67 196.20/102.67 196.20/102.67 196.20/102.67 196.20/102.67 196.20/102.67 2) 'Best' failed due to the following reason: 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 196.20/102.67 to the following reason: 196.20/102.67 196.20/102.67 The processor is inapplicable, reason: 196.20/102.67 Processor only applicable for innermost runtime complexity analysis 196.20/102.67 196.20/102.67 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 196.20/102.67 following reason: 196.20/102.67 196.20/102.67 The processor is inapplicable, reason: 196.20/102.67 Processor only applicable for innermost runtime complexity analysis 196.20/102.67 196.20/102.67 196.20/102.67 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 196.20/102.67 failed due to the following reason: 196.20/102.67 196.20/102.67 None of the processors succeeded. 196.20/102.67 196.20/102.67 Details of failed attempt(s): 196.20/102.67 ----------------------------- 196.20/102.67 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 196.20/102.67 failed due to the following reason: 196.20/102.67 196.20/102.67 match-boundness of the problem could not be verified. 196.20/102.67 196.20/102.67 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 196.20/102.67 failed due to the following reason: 196.20/102.67 196.20/102.67 match-boundness of the problem could not be verified. 196.20/102.67 196.20/102.67 196.20/102.67 196.20/102.67 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 196.20/102.67 the following reason: 196.20/102.67 196.20/102.67 We add the following weak dependency pairs: 196.20/102.67 196.20/102.67 Strict DPs: 196.20/102.67 { pred^#(s(x)) -> c_1(x) 196.20/102.67 , minus^#(x, s(y)) -> c_2(pred^#(minus(x, y))) 196.20/102.67 , minus^#(x, 0()) -> c_3(x) 196.20/102.67 , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) 196.20/102.67 , quot^#(0(), s(y)) -> c_5() } 196.20/102.67 196.20/102.67 and mark the set of starting terms. 196.20/102.67 196.20/102.67 We are left with following problem, upon which TcT provides the 196.20/102.67 certificate MAYBE. 196.20/102.67 196.20/102.67 Strict DPs: 196.20/102.67 { pred^#(s(x)) -> c_1(x) 196.20/102.67 , minus^#(x, s(y)) -> c_2(pred^#(minus(x, y))) 196.20/102.67 , minus^#(x, 0()) -> c_3(x) 196.20/102.67 , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) 196.20/102.67 , quot^#(0(), s(y)) -> c_5() } 196.20/102.67 Strict Trs: 196.20/102.67 { pred(s(x)) -> x 196.20/102.67 , minus(x, s(y)) -> pred(minus(x, y)) 196.20/102.67 , minus(x, 0()) -> x 196.20/102.67 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 196.20/102.67 , quot(0(), s(y)) -> 0() } 196.20/102.67 Obligation: 196.20/102.67 runtime complexity 196.20/102.67 Answer: 196.20/102.67 MAYBE 196.20/102.67 196.20/102.67 We estimate the number of application of {5} by applications of 196.20/102.67 Pre({5}) = {1,3,4}. Here rules are labeled as follows: 196.20/102.67 196.20/102.67 DPs: 196.20/102.67 { 1: pred^#(s(x)) -> c_1(x) 196.20/102.67 , 2: minus^#(x, s(y)) -> c_2(pred^#(minus(x, y))) 196.20/102.67 , 3: minus^#(x, 0()) -> c_3(x) 196.20/102.67 , 4: quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) 196.20/102.67 , 5: quot^#(0(), s(y)) -> c_5() } 196.20/102.67 196.20/102.67 We are left with following problem, upon which TcT provides the 196.20/102.67 certificate MAYBE. 196.20/102.67 196.20/102.67 Strict DPs: 196.20/102.67 { pred^#(s(x)) -> c_1(x) 196.20/102.67 , minus^#(x, s(y)) -> c_2(pred^#(minus(x, y))) 196.20/102.67 , minus^#(x, 0()) -> c_3(x) 196.20/102.67 , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) } 196.20/102.67 Strict Trs: 196.20/102.67 { pred(s(x)) -> x 196.20/102.67 , minus(x, s(y)) -> pred(minus(x, y)) 196.20/102.67 , minus(x, 0()) -> x 196.20/102.67 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 196.20/102.67 , quot(0(), s(y)) -> 0() } 196.20/102.67 Weak DPs: { quot^#(0(), s(y)) -> c_5() } 196.20/102.67 Obligation: 196.20/102.67 runtime complexity 196.20/102.67 Answer: 196.20/102.67 MAYBE 196.20/102.67 196.20/102.67 Empty strict component of the problem is NOT empty. 196.20/102.67 196.20/102.67 196.20/102.67 Arrrr.. 196.46/102.86 EOF