MAYBE 567.63/155.61 MAYBE 567.63/155.61 567.63/155.61 We are left with following problem, upon which TcT provides the 567.63/155.61 certificate MAYBE. 567.63/155.61 567.63/155.61 Strict Trs: 567.63/155.61 { minus(x, 0()) -> x 567.63/155.61 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.61 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.61 , quot(0(), s(y)) -> 0() 567.63/155.61 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 567.63/155.61 , plus(0(), y) -> y 567.63/155.61 , plus(s(x), y) -> s(plus(x, y)) 567.63/155.61 , app(l, nil()) -> l 567.63/155.61 , app(nil(), k) -> k 567.63/155.61 , app(cons(x, l), k) -> cons(x, app(l, k)) 567.63/155.61 , sum(app(l, cons(x, cons(y, k)))) -> 567.63/155.61 sum(app(l, sum(cons(x, cons(y, k))))) 567.63/155.61 , sum(cons(x, nil())) -> cons(x, nil()) 567.63/155.61 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) } 567.63/155.61 Obligation: 567.63/155.61 innermost runtime complexity 567.63/155.61 Answer: 567.63/155.61 MAYBE 567.63/155.61 567.63/155.61 None of the processors succeeded. 567.63/155.61 567.63/155.61 Details of failed attempt(s): 567.63/155.61 ----------------------------- 567.63/155.61 1) 'empty' failed due to the following reason: 567.63/155.61 567.63/155.61 Empty strict component of the problem is NOT empty. 567.63/155.61 567.63/155.61 2) 'Best' failed due to the following reason: 567.63/155.61 567.63/155.61 None of the processors succeeded. 567.63/155.61 567.63/155.61 Details of failed attempt(s): 567.63/155.61 ----------------------------- 567.63/155.61 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 567.63/155.61 following reason: 567.63/155.61 567.63/155.61 We add the following dependency tuples: 567.63/155.61 567.63/155.61 Strict DPs: 567.63/155.61 { minus^#(x, 0()) -> c_1() 567.63/155.61 , minus^#(minus(x, y), z) -> 567.63/155.61 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.61 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.61 , plus^#(0(), y) -> c_6() 567.63/155.61 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.61 , quot^#(0(), s(y)) -> c_4() 567.63/155.61 , quot^#(s(x), s(y)) -> 567.63/155.61 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.61 , app^#(l, nil()) -> c_8() 567.63/155.61 , app^#(nil(), k) -> c_9() 567.63/155.61 , app^#(cons(x, l), k) -> c_10(app^#(l, k)) 567.63/155.61 , sum^#(app(l, cons(x, cons(y, k)))) -> 567.63/155.61 c_11(sum^#(app(l, sum(cons(x, cons(y, k))))), 567.63/155.61 app^#(l, sum(cons(x, cons(y, k)))), 567.63/155.61 sum^#(cons(x, cons(y, k)))) 567.63/155.61 , sum^#(cons(x, nil())) -> c_12() 567.63/155.61 , sum^#(cons(x, cons(y, l))) -> 567.63/155.61 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.61 567.63/155.61 and mark the set of starting terms. 567.63/155.61 567.63/155.61 We are left with following problem, upon which TcT provides the 567.63/155.61 certificate MAYBE. 567.63/155.61 567.63/155.61 Strict DPs: 567.63/155.61 { minus^#(x, 0()) -> c_1() 567.63/155.61 , minus^#(minus(x, y), z) -> 567.63/155.61 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.61 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.61 , plus^#(0(), y) -> c_6() 567.63/155.61 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.61 , quot^#(0(), s(y)) -> c_4() 567.63/155.61 , quot^#(s(x), s(y)) -> 567.63/155.61 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.61 , app^#(l, nil()) -> c_8() 567.63/155.61 , app^#(nil(), k) -> c_9() 567.63/155.61 , app^#(cons(x, l), k) -> c_10(app^#(l, k)) 567.63/155.61 , sum^#(app(l, cons(x, cons(y, k)))) -> 567.63/155.61 c_11(sum^#(app(l, sum(cons(x, cons(y, k))))), 567.63/155.61 app^#(l, sum(cons(x, cons(y, k)))), 567.63/155.61 sum^#(cons(x, cons(y, k)))) 567.63/155.61 , sum^#(cons(x, nil())) -> c_12() 567.63/155.61 , sum^#(cons(x, cons(y, l))) -> 567.63/155.61 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.61 Weak Trs: 567.63/155.61 { minus(x, 0()) -> x 567.63/155.61 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.61 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.61 , quot(0(), s(y)) -> 0() 567.63/155.61 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 567.63/155.61 , plus(0(), y) -> y 567.63/155.61 , plus(s(x), y) -> s(plus(x, y)) 567.63/155.61 , app(l, nil()) -> l 567.63/155.61 , app(nil(), k) -> k 567.63/155.61 , app(cons(x, l), k) -> cons(x, app(l, k)) 567.63/155.61 , sum(app(l, cons(x, cons(y, k)))) -> 567.63/155.61 sum(app(l, sum(cons(x, cons(y, k))))) 567.63/155.61 , sum(cons(x, nil())) -> cons(x, nil()) 567.63/155.61 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) } 567.63/155.61 Obligation: 567.63/155.61 innermost runtime complexity 567.63/155.61 Answer: 567.63/155.61 MAYBE 567.63/155.61 567.63/155.61 Consider the dependency graph: 567.63/155.61 567.63/155.61 1: minus^#(x, 0()) -> c_1() 567.63/155.61 567.63/155.61 2: minus^#(minus(x, y), z) -> 567.63/155.61 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.61 -->_2 plus^#(s(x), y) -> c_7(plus^#(x, y)) :5 567.63/155.61 -->_1 minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) :3 567.63/155.61 -->_1 minus^#(x, 0()) -> c_1() :1 567.63/155.61 567.63/155.61 3: minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.61 -->_1 minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) :3 567.63/155.61 -->_1 minus^#(minus(x, y), z) -> 567.63/155.61 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) :2 567.63/155.61 -->_1 minus^#(x, 0()) -> c_1() :1 567.63/155.61 567.63/155.61 4: plus^#(0(), y) -> c_6() 567.63/155.61 567.63/155.61 5: plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.61 -->_1 plus^#(s(x), y) -> c_7(plus^#(x, y)) :5 567.63/155.61 -->_1 plus^#(0(), y) -> c_6() :4 567.63/155.61 567.63/155.61 6: quot^#(0(), s(y)) -> c_4() 567.63/155.61 567.63/155.61 7: quot^#(s(x), s(y)) -> 567.63/155.61 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.61 -->_1 quot^#(s(x), s(y)) -> 567.63/155.61 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) :7 567.63/155.61 -->_1 quot^#(0(), s(y)) -> c_4() :6 567.63/155.61 -->_2 minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) :3 567.63/155.61 -->_2 minus^#(minus(x, y), z) -> 567.63/155.61 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) :2 567.63/155.61 -->_2 minus^#(x, 0()) -> c_1() :1 567.63/155.61 567.63/155.61 8: app^#(l, nil()) -> c_8() 567.63/155.61 567.63/155.61 9: app^#(nil(), k) -> c_9() 567.63/155.61 567.63/155.61 10: app^#(cons(x, l), k) -> c_10(app^#(l, k)) 567.63/155.61 -->_1 app^#(cons(x, l), k) -> c_10(app^#(l, k)) :10 567.63/155.61 -->_1 app^#(nil(), k) -> c_9() :9 567.63/155.61 -->_1 app^#(l, nil()) -> c_8() :8 567.63/155.61 567.63/155.61 11: sum^#(app(l, cons(x, cons(y, k)))) -> 567.63/155.61 c_11(sum^#(app(l, sum(cons(x, cons(y, k))))), 567.63/155.61 app^#(l, sum(cons(x, cons(y, k)))), 567.63/155.61 sum^#(cons(x, cons(y, k)))) 567.63/155.61 -->_3 sum^#(cons(x, cons(y, l))) -> 567.63/155.61 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :13 567.63/155.61 -->_1 sum^#(cons(x, cons(y, l))) -> 567.63/155.61 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :13 567.63/155.61 -->_1 sum^#(cons(x, nil())) -> c_12() :12 567.63/155.61 -->_1 sum^#(app(l, cons(x, cons(y, k)))) -> 567.63/155.61 c_11(sum^#(app(l, sum(cons(x, cons(y, k))))), 567.63/155.61 app^#(l, sum(cons(x, cons(y, k)))), 567.63/155.61 sum^#(cons(x, cons(y, k)))) :11 567.63/155.61 -->_2 app^#(l, nil()) -> c_8() :8 567.63/155.61 567.63/155.61 12: sum^#(cons(x, nil())) -> c_12() 567.63/155.61 567.63/155.61 13: sum^#(cons(x, cons(y, l))) -> 567.63/155.61 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 567.63/155.61 -->_1 sum^#(cons(x, cons(y, l))) -> 567.63/155.61 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :13 567.63/155.61 -->_1 sum^#(cons(x, nil())) -> c_12() :12 567.63/155.61 -->_2 plus^#(s(x), y) -> c_7(plus^#(x, y)) :5 567.63/155.61 -->_2 plus^#(0(), y) -> c_6() :4 567.63/155.61 567.63/155.61 567.63/155.61 Only the nodes {1,3,2,5,4,6,7,8,9,10,12,13} are reachable from 567.63/155.61 nodes {1,3,4,5,6,7,8,9,10,12,13} that start derivation from marked 567.63/155.61 basic terms. The nodes not reachable are removed from the problem. 567.63/155.61 567.63/155.61 We are left with following problem, upon which TcT provides the 567.63/155.61 certificate MAYBE. 567.63/155.61 567.63/155.61 Strict DPs: 567.63/155.61 { minus^#(x, 0()) -> c_1() 567.63/155.61 , minus^#(minus(x, y), z) -> 567.63/155.61 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.61 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.61 , plus^#(0(), y) -> c_6() 567.63/155.61 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.61 , quot^#(0(), s(y)) -> c_4() 567.63/155.61 , quot^#(s(x), s(y)) -> 567.63/155.61 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.61 , app^#(l, nil()) -> c_8() 567.63/155.61 , app^#(nil(), k) -> c_9() 567.63/155.61 , app^#(cons(x, l), k) -> c_10(app^#(l, k)) 567.63/155.61 , sum^#(cons(x, nil())) -> c_12() 567.63/155.61 , sum^#(cons(x, cons(y, l))) -> 567.63/155.61 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.61 Weak Trs: 567.63/155.61 { minus(x, 0()) -> x 567.63/155.61 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.61 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.61 , quot(0(), s(y)) -> 0() 567.63/155.61 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 567.63/155.61 , plus(0(), y) -> y 567.63/155.61 , plus(s(x), y) -> s(plus(x, y)) 567.63/155.61 , app(l, nil()) -> l 567.63/155.61 , app(nil(), k) -> k 567.63/155.61 , app(cons(x, l), k) -> cons(x, app(l, k)) 567.63/155.61 , sum(app(l, cons(x, cons(y, k)))) -> 567.63/155.61 sum(app(l, sum(cons(x, cons(y, k))))) 567.63/155.62 , sum(cons(x, nil())) -> cons(x, nil()) 567.63/155.62 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 MAYBE 567.63/155.62 567.63/155.62 We estimate the number of application of {1,4,6,8,9,11} by 567.63/155.62 applications of Pre({1,4,6,8,9,11}) = {2,3,5,7,10,12}. Here rules 567.63/155.62 are labeled as follows: 567.63/155.62 567.63/155.62 DPs: 567.63/155.62 { 1: minus^#(x, 0()) -> c_1() 567.63/155.62 , 2: minus^#(minus(x, y), z) -> 567.63/155.62 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.62 , 3: minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.62 , 4: plus^#(0(), y) -> c_6() 567.63/155.62 , 5: plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.62 , 6: quot^#(0(), s(y)) -> c_4() 567.63/155.62 , 7: quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , 8: app^#(l, nil()) -> c_8() 567.63/155.62 , 9: app^#(nil(), k) -> c_9() 567.63/155.62 , 10: app^#(cons(x, l), k) -> c_10(app^#(l, k)) 567.63/155.62 , 11: sum^#(cons(x, nil())) -> c_12() 567.63/155.62 , 12: sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate MAYBE. 567.63/155.62 567.63/155.62 Strict DPs: 567.63/155.62 { minus^#(minus(x, y), z) -> 567.63/155.62 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.62 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.62 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.62 , quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , app^#(cons(x, l), k) -> c_10(app^#(l, k)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 Weak DPs: 567.63/155.62 { minus^#(x, 0()) -> c_1() 567.63/155.62 , plus^#(0(), y) -> c_6() 567.63/155.62 , quot^#(0(), s(y)) -> c_4() 567.63/155.62 , app^#(l, nil()) -> c_8() 567.63/155.62 , app^#(nil(), k) -> c_9() 567.63/155.62 , sum^#(cons(x, nil())) -> c_12() } 567.63/155.62 Weak Trs: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , quot(0(), s(y)) -> 0() 567.63/155.62 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) 567.63/155.62 , app(l, nil()) -> l 567.63/155.62 , app(nil(), k) -> k 567.63/155.62 , app(cons(x, l), k) -> cons(x, app(l, k)) 567.63/155.62 , sum(app(l, cons(x, cons(y, k)))) -> 567.63/155.62 sum(app(l, sum(cons(x, cons(y, k))))) 567.63/155.62 , sum(cons(x, nil())) -> cons(x, nil()) 567.63/155.62 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 MAYBE 567.63/155.62 567.63/155.62 The following weak DPs constitute a sub-graph of the DG that is 567.63/155.62 closed under successors. The DPs are removed. 567.63/155.62 567.63/155.62 { minus^#(x, 0()) -> c_1() 567.63/155.62 , plus^#(0(), y) -> c_6() 567.63/155.62 , quot^#(0(), s(y)) -> c_4() 567.63/155.62 , app^#(l, nil()) -> c_8() 567.63/155.62 , app^#(nil(), k) -> c_9() 567.63/155.62 , sum^#(cons(x, nil())) -> c_12() } 567.63/155.62 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate MAYBE. 567.63/155.62 567.63/155.62 Strict DPs: 567.63/155.62 { minus^#(minus(x, y), z) -> 567.63/155.62 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.62 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.62 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.62 , quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , app^#(cons(x, l), k) -> c_10(app^#(l, k)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 Weak Trs: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , quot(0(), s(y)) -> 0() 567.63/155.62 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) 567.63/155.62 , app(l, nil()) -> l 567.63/155.62 , app(nil(), k) -> k 567.63/155.62 , app(cons(x, l), k) -> cons(x, app(l, k)) 567.63/155.62 , sum(app(l, cons(x, cons(y, k)))) -> 567.63/155.62 sum(app(l, sum(cons(x, cons(y, k))))) 567.63/155.62 , sum(cons(x, nil())) -> cons(x, nil()) 567.63/155.62 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 MAYBE 567.63/155.62 567.63/155.62 We replace rewrite rules by usable rules: 567.63/155.62 567.63/155.62 Weak Usable Rules: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.62 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate MAYBE. 567.63/155.62 567.63/155.62 Strict DPs: 567.63/155.62 { minus^#(minus(x, y), z) -> 567.63/155.62 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.62 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.62 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.62 , quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , app^#(cons(x, l), k) -> c_10(app^#(l, k)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 Weak Trs: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 MAYBE 567.63/155.62 567.63/155.62 None of the processors succeeded. 567.63/155.62 567.63/155.62 Details of failed attempt(s): 567.63/155.62 ----------------------------- 567.63/155.62 1) 'empty' failed due to the following reason: 567.63/155.62 567.63/155.62 Empty strict component of the problem is NOT empty. 567.63/155.62 567.63/155.62 2) 'With Problem ...' failed due to the following reason: 567.63/155.62 567.63/155.62 We use the processor 'matrix interpretation of dimension 1' to 567.63/155.62 orient following rules strictly. 567.63/155.62 567.63/155.62 DPs: 567.63/155.62 { 5: app^#(cons(x, l), k) -> c_10(app^#(l, k)) } 567.63/155.62 567.63/155.62 Sub-proof: 567.63/155.62 ---------- 567.63/155.62 The following argument positions are usable: 567.63/155.62 Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, 567.63/155.62 Uargs(c_7) = {1}, Uargs(c_10) = {1}, Uargs(c_13) = {1, 2} 567.63/155.62 567.63/155.62 TcT has computed the following constructor-based matrix 567.63/155.62 interpretation satisfying not(EDA). 567.63/155.62 567.63/155.62 [minus](x1, x2) = [0] 567.63/155.62 567.63/155.62 [0] = [0] 567.63/155.62 567.63/155.62 [s](x1) = [0] 567.63/155.62 567.63/155.62 [plus](x1, x2) = [0] 567.63/155.62 567.63/155.62 [cons](x1, x2) = [1] x2 + [2] 567.63/155.62 567.63/155.62 [minus^#](x1, x2) = [0] 567.63/155.62 567.63/155.62 [c_2](x1, x2) = [2] x1 + [4] x2 + [0] 567.63/155.62 567.63/155.62 [plus^#](x1, x2) = [0] 567.63/155.62 567.63/155.62 [c_3](x1) = [1] x1 + [0] 567.63/155.62 567.63/155.62 [quot^#](x1, x2) = [0] 567.63/155.62 567.63/155.62 [c_5](x1, x2) = [2] x1 + [4] x2 + [0] 567.63/155.62 567.63/155.62 [c_7](x1) = [2] x1 + [0] 567.63/155.62 567.63/155.62 [app^#](x1, x2) = [4] x1 + [7] x2 + [1] 567.63/155.62 567.63/155.62 [c_10](x1) = [1] x1 + [5] 567.63/155.62 567.63/155.62 [sum^#](x1) = [0] 567.63/155.62 567.63/155.62 [c_13](x1, x2) = [2] x1 + [2] x2 + [0] 567.63/155.62 567.63/155.62 The order satisfies the following ordering constraints: 567.63/155.62 567.63/155.62 [minus(x, 0())] = [0] 567.63/155.62 ? [1] x + [0] 567.63/155.62 = [x] 567.63/155.62 567.63/155.62 [minus(minus(x, y), z)] = [0] 567.63/155.62 >= [0] 567.63/155.62 = [minus(x, plus(y, z))] 567.63/155.62 567.63/155.62 [minus(s(x), s(y))] = [0] 567.63/155.62 >= [0] 567.63/155.62 = [minus(x, y)] 567.63/155.62 567.63/155.62 [plus(0(), y)] = [0] 567.63/155.62 ? [1] y + [0] 567.63/155.62 = [y] 567.63/155.62 567.63/155.62 [plus(s(x), y)] = [0] 567.63/155.62 >= [0] 567.63/155.62 = [s(plus(x, y))] 567.63/155.62 567.63/155.62 [minus^#(minus(x, y), z)] = [0] 567.63/155.62 >= [0] 567.63/155.62 = [c_2(minus^#(x, plus(y, z)), plus^#(y, z))] 567.63/155.62 567.63/155.62 [minus^#(s(x), s(y))] = [0] 567.63/155.62 >= [0] 567.63/155.62 = [c_3(minus^#(x, y))] 567.63/155.62 567.63/155.62 [plus^#(s(x), y)] = [0] 567.63/155.62 >= [0] 567.63/155.62 = [c_7(plus^#(x, y))] 567.63/155.62 567.63/155.62 [quot^#(s(x), s(y))] = [0] 567.63/155.62 >= [0] 567.63/155.62 = [c_5(quot^#(minus(x, y), s(y)), minus^#(x, y))] 567.63/155.62 567.63/155.62 [app^#(cons(x, l), k)] = [7] k + [4] l + [9] 567.63/155.62 > [7] k + [4] l + [6] 567.63/155.62 = [c_10(app^#(l, k))] 567.63/155.62 567.63/155.62 [sum^#(cons(x, cons(y, l)))] = [0] 567.63/155.62 >= [0] 567.63/155.62 = [c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y))] 567.63/155.62 567.63/155.62 567.63/155.62 The strictly oriented rules are moved into the weak component. 567.63/155.62 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate MAYBE. 567.63/155.62 567.63/155.62 Strict DPs: 567.63/155.62 { minus^#(minus(x, y), z) -> 567.63/155.62 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.62 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.62 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.62 , quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 Weak DPs: { app^#(cons(x, l), k) -> c_10(app^#(l, k)) } 567.63/155.62 Weak Trs: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 MAYBE 567.63/155.62 567.63/155.62 The following weak DPs constitute a sub-graph of the DG that is 567.63/155.62 closed under successors. The DPs are removed. 567.63/155.62 567.63/155.62 { app^#(cons(x, l), k) -> c_10(app^#(l, k)) } 567.63/155.62 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate MAYBE. 567.63/155.62 567.63/155.62 Strict DPs: 567.63/155.62 { minus^#(minus(x, y), z) -> 567.63/155.62 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.62 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.62 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 567.63/155.62 , quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 Weak Trs: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 MAYBE 567.63/155.62 567.63/155.62 We decompose the input problem according to the dependency graph 567.63/155.62 into the upper component 567.63/155.62 567.63/155.62 { quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 567.63/155.62 and lower component 567.63/155.62 567.63/155.62 { minus^#(minus(x, y), z) -> 567.63/155.62 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.62 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.62 , plus^#(s(x), y) -> c_7(plus^#(x, y)) } 567.63/155.62 567.63/155.62 Further, following extension rules are added to the lower 567.63/155.62 component. 567.63/155.62 567.63/155.62 { quot^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.62 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) } 567.63/155.62 567.63/155.62 TcT solves the upper component with certificate YES(O(1),O(n^1)). 567.63/155.62 567.63/155.62 Sub-proof: 567.63/155.62 ---------- 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate YES(O(1),O(n^1)). 567.63/155.62 567.63/155.62 Strict DPs: 567.63/155.62 { quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 Weak Trs: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 YES(O(1),O(n^1)) 567.63/155.62 567.63/155.62 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 567.63/155.62 to orient following rules strictly. 567.63/155.62 567.63/155.62 DPs: 567.63/155.62 { 1: quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , 2: sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 Trs: 567.63/155.62 { minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , plus(0(), y) -> y } 567.63/155.62 567.63/155.62 Sub-proof: 567.63/155.62 ---------- 567.63/155.62 The input was oriented with the instance of 'Small Polynomial Path 567.63/155.62 Order (PS,1-bounded)' as induced by the safe mapping 567.63/155.62 567.63/155.62 safe(minus) = {1, 2}, safe(0) = {}, safe(s) = {1}, 567.63/155.62 safe(plus) = {1}, safe(cons) = {1, 2}, safe(minus^#) = {}, 567.63/155.62 safe(plus^#) = {}, safe(quot^#) = {2}, safe(c_5) = {}, 567.63/155.62 safe(sum^#) = {}, safe(c_13) = {} 567.63/155.62 567.63/155.62 and precedence 567.63/155.62 567.63/155.62 plus ~ quot^#, plus ~ sum^#, quot^# ~ sum^# . 567.63/155.62 567.63/155.62 Following symbols are considered recursive: 567.63/155.62 567.63/155.62 {plus, quot^#, sum^#} 567.63/155.62 567.63/155.62 The recursion depth is 1. 567.63/155.62 567.63/155.62 Further, following argument filtering is employed: 567.63/155.62 567.63/155.62 pi(minus) = 1, pi(0) = [], pi(s) = [1], pi(plus) = [1, 2], 567.63/155.62 pi(cons) = [2], pi(minus^#) = [], pi(plus^#) = [], 567.63/155.62 pi(quot^#) = [1], pi(c_5) = [1, 2], pi(sum^#) = [1], 567.63/155.62 pi(c_13) = [1, 2] 567.63/155.62 567.63/155.62 Usable defined function symbols are a subset of: 567.63/155.62 567.63/155.62 {minus, minus^#, plus^#, quot^#, sum^#} 567.63/155.62 567.63/155.62 For your convenience, here are the satisfied ordering constraints: 567.63/155.62 567.63/155.62 pi(quot^#(s(x), s(y))) = quot^#(s(; x);) 567.63/155.62 > c_5(quot^#(x;), minus^#();) 567.63/155.62 = pi(c_5(quot^#(minus(x, y), s(y)), minus^#(x, y))) 567.63/155.62 567.63/155.62 pi(sum^#(cons(x, cons(y, l)))) = sum^#(cons(; cons(; l));) 567.63/155.62 > c_13(sum^#(cons(; l);), plus^#();) 567.63/155.62 = pi(c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y))) 567.63/155.62 567.63/155.62 pi(minus(x, 0())) = x 567.63/155.62 >= x 567.63/155.62 = pi(x) 567.63/155.62 567.63/155.62 pi(minus(minus(x, y), z)) = x 567.63/155.62 >= x 567.63/155.62 = pi(minus(x, plus(y, z))) 567.63/155.62 567.63/155.62 pi(minus(s(x), s(y))) = s(; x) 567.63/155.62 > x 567.63/155.62 = pi(minus(x, y)) 567.63/155.62 567.63/155.62 567.63/155.62 The strictly oriented rules are moved into the weak component. 567.63/155.62 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate YES(O(1),O(1)). 567.63/155.62 567.63/155.62 Weak DPs: 567.63/155.62 { quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 Weak Trs: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 YES(O(1),O(1)) 567.63/155.62 567.63/155.62 The following weak DPs constitute a sub-graph of the DG that is 567.63/155.62 closed under successors. The DPs are removed. 567.63/155.62 567.63/155.62 { quot^#(s(x), s(y)) -> 567.63/155.62 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> 567.63/155.62 c_13(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 567.63/155.62 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate YES(O(1),O(1)). 567.63/155.62 567.63/155.62 Weak Trs: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 YES(O(1),O(1)) 567.63/155.62 567.63/155.62 No rule is usable, rules are removed from the input problem. 567.63/155.62 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate YES(O(1),O(1)). 567.63/155.62 567.63/155.62 Rules: Empty 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 YES(O(1),O(1)) 567.63/155.62 567.63/155.62 Empty rules are trivially bounded 567.63/155.62 567.63/155.62 We return to the main proof. 567.63/155.62 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.62 certificate MAYBE. 567.63/155.62 567.63/155.62 Strict DPs: 567.63/155.62 { minus^#(minus(x, y), z) -> 567.63/155.62 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.62 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.62 , plus^#(s(x), y) -> c_7(plus^#(x, y)) } 567.63/155.62 Weak DPs: 567.63/155.62 { quot^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.62 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) } 567.63/155.62 Weak Trs: 567.63/155.62 { minus(x, 0()) -> x 567.63/155.62 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.62 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.62 , plus(0(), y) -> y 567.63/155.62 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.62 Obligation: 567.63/155.62 innermost runtime complexity 567.63/155.62 Answer: 567.63/155.62 MAYBE 567.63/155.62 567.63/155.62 We decompose the input problem according to the dependency graph 567.63/155.62 into the upper component 567.63/155.62 567.63/155.62 { minus^#(minus(x, y), z) -> 567.63/155.62 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.62 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.62 , quot^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.62 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) } 567.63/155.62 567.63/155.62 and lower component 567.63/155.62 567.63/155.62 { plus^#(s(x), y) -> c_7(plus^#(x, y)) } 567.63/155.62 567.63/155.62 Further, following extension rules are added to the lower 567.63/155.62 component. 567.63/155.62 567.63/155.62 { minus^#(minus(x, y), z) -> minus^#(x, plus(y, z)) 567.63/155.62 , minus^#(minus(x, y), z) -> plus^#(y, z) 567.63/155.62 , minus^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.62 , quot^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.62 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 567.63/155.62 , sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) } 567.63/155.62 567.63/155.62 TcT solves the upper component with certificate YES(O(1),O(n^1)). 567.63/155.62 567.63/155.62 Sub-proof: 567.63/155.62 ---------- 567.63/155.62 We are left with following problem, upon which TcT provides the 567.63/155.63 certificate YES(O(1),O(n^1)). 567.63/155.63 567.63/155.63 Strict DPs: 567.63/155.63 { minus^#(minus(x, y), z) -> 567.63/155.63 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.63 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.63 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) } 567.63/155.63 Weak DPs: 567.63/155.63 { quot^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.63 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 567.63/155.63 , sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) } 567.63/155.63 Weak Trs: 567.63/155.63 { minus(x, 0()) -> x 567.63/155.63 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.63 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.63 , plus(0(), y) -> y 567.63/155.63 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.63 Obligation: 567.63/155.63 innermost runtime complexity 567.63/155.63 Answer: 567.63/155.63 YES(O(1),O(n^1)) 567.63/155.63 567.63/155.63 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 567.63/155.63 to orient following rules strictly. 567.63/155.63 567.63/155.63 DPs: 567.63/155.63 { 1: minus^#(minus(x, y), z) -> 567.63/155.63 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.63 , 2: minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.63 , 3: sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 567.63/155.63 , 4: quot^#(s(x), s(y)) -> minus^#(x, y) } 567.63/155.63 Trs: 567.63/155.63 { minus(x, 0()) -> x 567.63/155.63 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.63 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.63 , plus(0(), y) -> y } 567.63/155.63 567.63/155.63 Sub-proof: 567.63/155.63 ---------- 567.63/155.63 The input was oriented with the instance of 'Small Polynomial Path 567.63/155.63 Order (PS,1-bounded)' as induced by the safe mapping 567.63/155.63 567.63/155.63 safe(minus) = {1, 2}, safe(0) = {}, safe(s) = {1}, safe(plus) = {}, 567.63/155.63 safe(cons) = {1, 2}, safe(minus^#) = {2}, safe(c_2) = {}, 567.63/155.63 safe(plus^#) = {}, safe(c_3) = {}, safe(quot^#) = {}, 567.63/155.63 safe(sum^#) = {} 567.63/155.63 567.63/155.63 and precedence 567.63/155.63 567.63/155.63 minus^# > plus, quot^# > plus, quot^# > minus^#, sum^# > plus, 567.63/155.63 quot^# ~ sum^# . 567.63/155.63 567.63/155.63 Following symbols are considered recursive: 567.63/155.63 567.63/155.63 {minus^#, sum^#} 567.63/155.63 567.63/155.63 The recursion depth is 1. 567.63/155.63 567.63/155.63 Further, following argument filtering is employed: 567.63/155.63 567.63/155.63 pi(minus) = [1], pi(0) = [], pi(s) = [1], pi(plus) = [2], 567.63/155.63 pi(cons) = [], pi(minus^#) = [1], pi(c_2) = [1, 2], 567.63/155.63 pi(plus^#) = [], pi(c_3) = [1], pi(quot^#) = [1], pi(sum^#) = [] 567.63/155.63 567.63/155.63 Usable defined function symbols are a subset of: 567.63/155.63 567.63/155.63 {minus, minus^#, plus^#, quot^#, sum^#} 567.63/155.63 567.63/155.63 For your convenience, here are the satisfied ordering constraints: 567.63/155.63 567.63/155.63 pi(minus^#(minus(x, y), z)) = minus^#(minus(; x);) 567.63/155.63 > c_2(minus^#(x;), plus^#();) 567.63/155.63 = pi(c_2(minus^#(x, plus(y, z)), plus^#(y, z))) 567.63/155.63 567.63/155.63 pi(minus^#(s(x), s(y))) = minus^#(s(; x);) 567.63/155.63 > c_3(minus^#(x;);) 567.63/155.63 = pi(c_3(minus^#(x, y))) 567.63/155.63 567.63/155.63 pi(quot^#(s(x), s(y))) = quot^#(s(; x);) 567.63/155.63 > minus^#(x;) 567.63/155.63 = pi(minus^#(x, y)) 567.63/155.63 567.63/155.63 pi(quot^#(s(x), s(y))) = quot^#(s(; x);) 567.63/155.63 >= quot^#(minus(; x);) 567.63/155.63 = pi(quot^#(minus(x, y), s(y))) 567.63/155.63 567.63/155.63 pi(sum^#(cons(x, cons(y, l)))) = sum^#() 567.63/155.63 > plus^#() 567.63/155.63 = pi(plus^#(x, y)) 567.63/155.63 567.63/155.63 pi(sum^#(cons(x, cons(y, l)))) = sum^#() 567.63/155.63 >= sum^#() 567.63/155.63 = pi(sum^#(cons(plus(x, y), l))) 567.63/155.63 567.63/155.63 pi(minus(x, 0())) = minus(; x) 567.63/155.63 > x 567.63/155.63 = pi(x) 567.63/155.63 567.63/155.63 pi(minus(minus(x, y), z)) = minus(; minus(; x)) 567.63/155.63 > minus(; x) 567.63/155.63 = pi(minus(x, plus(y, z))) 567.63/155.63 567.63/155.63 pi(minus(s(x), s(y))) = minus(; s(; x)) 567.63/155.63 > minus(; x) 567.63/155.63 = pi(minus(x, y)) 567.63/155.63 567.63/155.63 567.63/155.63 The strictly oriented rules are moved into the weak component. 567.63/155.63 567.63/155.63 We are left with following problem, upon which TcT provides the 567.63/155.63 certificate YES(O(1),O(1)). 567.63/155.63 567.63/155.63 Weak DPs: 567.63/155.63 { minus^#(minus(x, y), z) -> 567.63/155.63 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.63 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.63 , quot^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.63 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 567.63/155.63 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 567.63/155.63 , sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) } 567.63/155.63 Weak Trs: 567.63/155.63 { minus(x, 0()) -> x 567.63/155.63 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.63 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.63 , plus(0(), y) -> y 567.63/155.63 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.63 Obligation: 567.63/155.63 innermost runtime complexity 567.63/155.63 Answer: 567.63/155.63 YES(O(1),O(1)) 567.63/155.63 567.63/155.63 The following weak DPs constitute a sub-graph of the DG that is 567.63/155.63 closed under successors. The DPs are removed. 567.63/155.63 567.63/155.63 { minus^#(minus(x, y), z) -> 567.63/155.63 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 567.63/155.63 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 567.63/155.63 , quot^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.63 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 567.63/155.63 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 567.63/155.63 , sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) } 567.63/155.63 567.63/155.63 We are left with following problem, upon which TcT provides the 567.63/155.63 certificate YES(O(1),O(1)). 567.63/155.63 567.63/155.63 Weak Trs: 567.63/155.63 { minus(x, 0()) -> x 567.63/155.63 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.63 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.63 , plus(0(), y) -> y 567.63/155.63 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.63 Obligation: 567.63/155.63 innermost runtime complexity 567.63/155.63 Answer: 567.63/155.63 YES(O(1),O(1)) 567.63/155.63 567.63/155.63 No rule is usable, rules are removed from the input problem. 567.63/155.63 567.63/155.63 We are left with following problem, upon which TcT provides the 567.63/155.63 certificate YES(O(1),O(1)). 567.63/155.63 567.63/155.63 Rules: Empty 567.63/155.63 Obligation: 567.63/155.63 innermost runtime complexity 567.63/155.63 Answer: 567.63/155.63 YES(O(1),O(1)) 567.63/155.63 567.63/155.63 Empty rules are trivially bounded 567.63/155.63 567.63/155.63 We return to the main proof. 567.63/155.63 567.63/155.63 We are left with following problem, upon which TcT provides the 567.63/155.63 certificate MAYBE. 567.63/155.63 567.63/155.63 Strict DPs: { plus^#(s(x), y) -> c_7(plus^#(x, y)) } 567.63/155.63 Weak DPs: 567.63/155.63 { minus^#(minus(x, y), z) -> minus^#(x, plus(y, z)) 567.63/155.63 , minus^#(minus(x, y), z) -> plus^#(y, z) 567.63/155.63 , minus^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.63 , quot^#(s(x), s(y)) -> minus^#(x, y) 567.63/155.63 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 567.63/155.63 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 567.63/155.63 , sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) } 567.63/155.63 Weak Trs: 567.63/155.63 { minus(x, 0()) -> x 567.63/155.63 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 567.63/155.63 , minus(s(x), s(y)) -> minus(x, y) 567.63/155.63 , plus(0(), y) -> y 567.63/155.63 , plus(s(x), y) -> s(plus(x, y)) } 567.63/155.63 Obligation: 567.63/155.63 innermost runtime complexity 567.63/155.63 Answer: 567.63/155.63 MAYBE 567.63/155.63 567.63/155.63 None of the processors succeeded. 567.63/155.63 567.63/155.63 Details of failed attempt(s): 567.63/155.63 ----------------------------- 567.63/155.63 1) 'empty' failed due to the following reason: 567.63/155.63 567.63/155.63 Empty strict component of the problem is NOT empty. 567.63/155.63 567.63/155.63 2) 'Fastest' failed due to the following reason: 567.63/155.63 567.63/155.63 None of the processors succeeded. 567.63/155.63 567.63/155.63 Details of failed attempt(s): 567.63/155.63 ----------------------------- 567.63/155.63 1) 'With Problem ...' failed due to the following reason: 567.63/155.63 567.63/155.63 None of the processors succeeded. 567.63/155.63 567.63/155.63 Details of failed attempt(s): 567.63/155.63 ----------------------------- 567.63/155.63 1) 'empty' failed due to the following reason: 567.63/155.63 567.63/155.63 Empty strict component of the problem is NOT empty. 567.63/155.63 567.63/155.63 2) 'Polynomial Path Order (PS)' failed due to the following reason: 567.63/155.63 567.63/155.63 The input cannot be shown compatible 567.63/155.63 567.63/155.63 567.63/155.63 2) 'Polynomial Path Order (PS)' failed due to the following reason: 567.63/155.63 567.63/155.63 The input cannot be shown compatible 567.63/155.63 567.63/155.63 3) 'Fastest (timeout of 24 seconds)' failed due to the following 567.63/155.63 reason: 567.63/155.63 567.63/155.63 None of the processors succeeded. 567.63/155.63 567.63/155.63 Details of failed attempt(s): 567.63/155.63 ----------------------------- 567.63/155.63 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 567.63/155.63 failed due to the following reason: 567.63/155.63 567.63/155.63 match-boundness of the problem could not be verified. 567.63/155.63 567.63/155.63 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 567.63/155.63 failed due to the following reason: 567.63/155.63 567.63/155.63 match-boundness of the problem could not be verified. 567.63/155.63 567.63/155.63 567.63/155.63 567.63/155.63 567.63/155.63 567.63/155.63 2) 'Best' failed due to the following reason: 567.63/155.63 567.63/155.63 None of the processors succeeded. 567.63/155.63 567.63/155.63 Details of failed attempt(s): 567.63/155.63 ----------------------------- 567.63/155.63 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 567.63/155.63 seconds)' failed due to the following reason: 567.63/155.63 567.63/155.63 Computation stopped due to timeout after 148.0 seconds. 567.63/155.63 567.63/155.63 2) 'Best' failed due to the following reason: 567.63/155.63 567.63/155.63 None of the processors succeeded. 567.63/155.63 567.63/155.63 Details of failed attempt(s): 567.63/155.63 ----------------------------- 567.63/155.63 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 567.63/155.63 following reason: 567.63/155.63 567.63/155.63 The input cannot be shown compatible 567.63/155.63 567.63/155.63 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 567.63/155.63 to the following reason: 567.63/155.63 567.63/155.63 The input cannot be shown compatible 567.63/155.63 567.63/155.63 567.63/155.63 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 567.63/155.63 failed due to the following reason: 567.63/155.63 567.63/155.63 None of the processors succeeded. 567.63/155.63 567.63/155.63 Details of failed attempt(s): 567.63/155.63 ----------------------------- 567.63/155.63 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 567.63/155.63 failed due to the following reason: 567.63/155.63 567.63/155.63 match-boundness of the problem could not be verified. 567.63/155.63 567.63/155.63 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 567.63/155.63 failed due to the following reason: 567.63/155.63 567.63/155.63 match-boundness of the problem could not be verified. 567.63/155.63 567.63/155.63 567.63/155.63 567.63/155.63 567.63/155.63 567.63/155.63 Arrrr.. 567.99/155.95 EOF