YES(O(1),O(n^1)) 71.27/32.35 YES(O(1),O(n^1)) 71.27/32.35 71.27/32.35 We are left with following problem, upon which TcT provides the 71.27/32.35 certificate YES(O(1),O(n^1)). 71.27/32.35 71.27/32.35 Strict Trs: 71.27/32.35 { flatten(flatten(x)) -> flatten(x) 71.27/32.35 , flatten(nil()) -> nil() 71.27/32.35 , flatten(unit(x)) -> flatten(x) 71.27/32.35 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , ++(x, nil()) -> x 71.27/32.35 , ++(nil(), y) -> y 71.27/32.35 , ++(++(x, y), z) -> ++(x, ++(y, z)) 71.27/32.35 , rev(nil()) -> nil() 71.27/32.35 , rev(unit(x)) -> unit(x) 71.27/32.35 , rev(++(x, y)) -> ++(rev(y), rev(x)) 71.27/32.35 , rev(rev(x)) -> x } 71.27/32.35 Obligation: 71.27/32.35 innermost runtime complexity 71.27/32.35 Answer: 71.27/32.35 YES(O(1),O(n^1)) 71.27/32.35 71.27/32.35 We add the following dependency tuples: 71.27/32.35 71.27/32.35 Strict DPs: 71.27/32.35 { flatten^#(flatten(x)) -> c_1(flatten^#(x)) 71.27/32.35 , flatten^#(nil()) -> c_2() 71.27/32.35 , flatten^#(unit(x)) -> c_3(flatten^#(x)) 71.27/32.35 , flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , ++^#(x, nil()) -> c_6() 71.27/32.35 , ++^#(nil(), y) -> c_7() 71.27/32.35 , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) 71.27/32.35 , rev^#(nil()) -> c_9() 71.27/32.35 , rev^#(unit(x)) -> c_10() 71.27/32.35 , rev^#(++(x, y)) -> c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x)) 71.27/32.35 , rev^#(rev(x)) -> c_12() } 71.27/32.35 71.27/32.35 and mark the set of starting terms. 71.27/32.35 71.27/32.35 We are left with following problem, upon which TcT provides the 71.27/32.35 certificate YES(O(1),O(n^1)). 71.27/32.35 71.27/32.35 Strict DPs: 71.27/32.35 { flatten^#(flatten(x)) -> c_1(flatten^#(x)) 71.27/32.35 , flatten^#(nil()) -> c_2() 71.27/32.35 , flatten^#(unit(x)) -> c_3(flatten^#(x)) 71.27/32.35 , flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , ++^#(x, nil()) -> c_6() 71.27/32.35 , ++^#(nil(), y) -> c_7() 71.27/32.35 , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) 71.27/32.35 , rev^#(nil()) -> c_9() 71.27/32.35 , rev^#(unit(x)) -> c_10() 71.27/32.35 , rev^#(++(x, y)) -> c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x)) 71.27/32.35 , rev^#(rev(x)) -> c_12() } 71.27/32.35 Weak Trs: 71.27/32.35 { flatten(flatten(x)) -> flatten(x) 71.27/32.35 , flatten(nil()) -> nil() 71.27/32.35 , flatten(unit(x)) -> flatten(x) 71.27/32.35 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , ++(x, nil()) -> x 71.27/32.35 , ++(nil(), y) -> y 71.27/32.35 , ++(++(x, y), z) -> ++(x, ++(y, z)) 71.27/32.35 , rev(nil()) -> nil() 71.27/32.35 , rev(unit(x)) -> unit(x) 71.27/32.35 , rev(++(x, y)) -> ++(rev(y), rev(x)) 71.27/32.35 , rev(rev(x)) -> x } 71.27/32.35 Obligation: 71.27/32.35 innermost runtime complexity 71.27/32.35 Answer: 71.27/32.35 YES(O(1),O(n^1)) 71.27/32.35 71.27/32.35 Consider the dependency graph: 71.27/32.35 71.27/32.35 1: flatten^#(flatten(x)) -> c_1(flatten^#(x)) 71.27/32.35 71.27/32.35 2: flatten^#(nil()) -> c_2() 71.27/32.35 71.27/32.35 3: flatten^#(unit(x)) -> c_3(flatten^#(x)) 71.27/32.35 -->_1 flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5 71.27/32.35 -->_1 flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4 71.27/32.35 -->_1 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3 71.27/32.35 -->_1 flatten^#(nil()) -> c_2() :2 71.27/32.35 -->_1 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1 71.27/32.35 71.27/32.35 4: flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 -->_1 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8 71.27/32.35 -->_3 flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5 71.27/32.35 -->_1 ++^#(nil(), y) -> c_7() :7 71.27/32.35 -->_1 ++^#(x, nil()) -> c_6() :6 71.27/32.35 -->_3 flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4 71.27/32.35 -->_3 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3 71.27/32.35 -->_2 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3 71.27/32.35 -->_3 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1 71.27/32.35 -->_2 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1 71.27/32.35 71.27/32.35 5: flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 -->_1 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8 71.27/32.35 -->_1 ++^#(nil(), y) -> c_7() :7 71.27/32.35 -->_1 ++^#(x, nil()) -> c_6() :6 71.27/32.35 -->_3 flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5 71.27/32.35 -->_2 flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5 71.27/32.35 -->_3 flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4 71.27/32.35 -->_2 flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4 71.27/32.35 -->_3 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3 71.27/32.35 -->_2 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3 71.27/32.35 -->_2 flatten^#(nil()) -> c_2() :2 71.27/32.35 -->_3 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1 71.27/32.35 -->_2 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1 71.27/32.35 71.27/32.35 6: ++^#(x, nil()) -> c_6() 71.27/32.35 71.27/32.35 7: ++^#(nil(), y) -> c_7() 71.27/32.35 71.27/32.35 8: ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) 71.27/32.35 -->_2 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8 71.27/32.35 -->_2 ++^#(x, nil()) -> c_6() :6 71.27/32.35 -->_1 ++^#(x, nil()) -> c_6() :6 71.27/32.35 71.27/32.35 9: rev^#(nil()) -> c_9() 71.27/32.35 71.27/32.35 10: rev^#(unit(x)) -> c_10() 71.27/32.35 71.27/32.35 11: rev^#(++(x, y)) -> 71.27/32.35 c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x)) 71.27/32.35 -->_3 rev^#(rev(x)) -> c_12() :12 71.27/32.35 -->_2 rev^#(rev(x)) -> c_12() :12 71.27/32.35 -->_2 rev^#(++(x, y)) -> 71.27/32.35 c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x)) :11 71.27/32.35 -->_3 rev^#(unit(x)) -> c_10() :10 71.27/32.35 -->_2 rev^#(unit(x)) -> c_10() :10 71.27/32.35 -->_1 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8 71.27/32.35 -->_1 ++^#(nil(), y) -> c_7() :7 71.27/32.35 -->_1 ++^#(x, nil()) -> c_6() :6 71.27/32.35 71.27/32.35 12: rev^#(rev(x)) -> c_12() 71.27/32.35 71.27/32.35 71.27/32.35 Only the nodes {2,3,5,8,6,7,4,1,9,10} are reachable from nodes 71.27/32.35 {2,3,6,7,9,10} that start derivation from marked basic terms. The 71.27/32.35 nodes not reachable are removed from the problem. 71.27/32.35 71.27/32.35 We are left with following problem, upon which TcT provides the 71.27/32.35 certificate YES(O(1),O(n^1)). 71.27/32.35 71.27/32.35 Strict DPs: 71.27/32.35 { flatten^#(flatten(x)) -> c_1(flatten^#(x)) 71.27/32.35 , flatten^#(nil()) -> c_2() 71.27/32.35 , flatten^#(unit(x)) -> c_3(flatten^#(x)) 71.27/32.35 , flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , ++^#(x, nil()) -> c_6() 71.27/32.35 , ++^#(nil(), y) -> c_7() 71.27/32.35 , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) 71.27/32.35 , rev^#(nil()) -> c_9() 71.27/32.35 , rev^#(unit(x)) -> c_10() } 71.27/32.35 Weak Trs: 71.27/32.35 { flatten(flatten(x)) -> flatten(x) 71.27/32.35 , flatten(nil()) -> nil() 71.27/32.35 , flatten(unit(x)) -> flatten(x) 71.27/32.35 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , ++(x, nil()) -> x 71.27/32.35 , ++(nil(), y) -> y 71.27/32.35 , ++(++(x, y), z) -> ++(x, ++(y, z)) 71.27/32.35 , rev(nil()) -> nil() 71.27/32.35 , rev(unit(x)) -> unit(x) 71.27/32.35 , rev(++(x, y)) -> ++(rev(y), rev(x)) 71.27/32.35 , rev(rev(x)) -> x } 71.27/32.35 Obligation: 71.27/32.35 innermost runtime complexity 71.27/32.35 Answer: 71.27/32.35 YES(O(1),O(n^1)) 71.27/32.35 71.27/32.35 We estimate the number of application of {1,2,6,7,9,10} by 71.27/32.35 applications of Pre({1,2,6,7,9,10}) = {3,4,5,8}. Here rules are 71.27/32.35 labeled as follows: 71.27/32.35 71.27/32.35 DPs: 71.27/32.35 { 1: flatten^#(flatten(x)) -> c_1(flatten^#(x)) 71.27/32.35 , 2: flatten^#(nil()) -> c_2() 71.27/32.35 , 3: flatten^#(unit(x)) -> c_3(flatten^#(x)) 71.27/32.35 , 4: flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , 5: flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , 6: ++^#(x, nil()) -> c_6() 71.27/32.35 , 7: ++^#(nil(), y) -> c_7() 71.27/32.35 , 8: ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) 71.27/32.35 , 9: rev^#(nil()) -> c_9() 71.27/32.35 , 10: rev^#(unit(x)) -> c_10() } 71.27/32.35 71.27/32.35 We are left with following problem, upon which TcT provides the 71.27/32.35 certificate YES(O(1),O(n^1)). 71.27/32.35 71.27/32.35 Strict DPs: 71.27/32.35 { flatten^#(unit(x)) -> c_3(flatten^#(x)) 71.27/32.35 , flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) } 71.27/32.35 Weak DPs: 71.27/32.35 { flatten^#(flatten(x)) -> c_1(flatten^#(x)) 71.27/32.35 , flatten^#(nil()) -> c_2() 71.27/32.35 , ++^#(x, nil()) -> c_6() 71.27/32.35 , ++^#(nil(), y) -> c_7() 71.27/32.35 , rev^#(nil()) -> c_9() 71.27/32.35 , rev^#(unit(x)) -> c_10() } 71.27/32.35 Weak Trs: 71.27/32.35 { flatten(flatten(x)) -> flatten(x) 71.27/32.35 , flatten(nil()) -> nil() 71.27/32.35 , flatten(unit(x)) -> flatten(x) 71.27/32.35 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , ++(x, nil()) -> x 71.27/32.35 , ++(nil(), y) -> y 71.27/32.35 , ++(++(x, y), z) -> ++(x, ++(y, z)) 71.27/32.35 , rev(nil()) -> nil() 71.27/32.35 , rev(unit(x)) -> unit(x) 71.27/32.35 , rev(++(x, y)) -> ++(rev(y), rev(x)) 71.27/32.35 , rev(rev(x)) -> x } 71.27/32.35 Obligation: 71.27/32.35 innermost runtime complexity 71.27/32.35 Answer: 71.27/32.35 YES(O(1),O(n^1)) 71.27/32.35 71.27/32.35 The following weak DPs constitute a sub-graph of the DG that is 71.27/32.35 closed under successors. The DPs are removed. 71.27/32.35 71.27/32.35 { flatten^#(flatten(x)) -> c_1(flatten^#(x)) 71.27/32.35 , flatten^#(nil()) -> c_2() 71.27/32.35 , ++^#(x, nil()) -> c_6() 71.27/32.35 , ++^#(nil(), y) -> c_7() 71.27/32.35 , rev^#(nil()) -> c_9() 71.27/32.35 , rev^#(unit(x)) -> c_10() } 71.27/32.35 71.27/32.35 We are left with following problem, upon which TcT provides the 71.27/32.35 certificate YES(O(1),O(n^1)). 71.27/32.35 71.27/32.35 Strict DPs: 71.27/32.35 { flatten^#(unit(x)) -> c_3(flatten^#(x)) 71.27/32.35 , flatten^#(++(x, y)) -> 71.27/32.35 c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , flatten^#(++(unit(x), y)) -> 71.27/32.35 c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) } 71.27/32.35 Weak Trs: 71.27/32.35 { flatten(flatten(x)) -> flatten(x) 71.27/32.35 , flatten(nil()) -> nil() 71.27/32.35 , flatten(unit(x)) -> flatten(x) 71.27/32.35 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , ++(x, nil()) -> x 71.27/32.35 , ++(nil(), y) -> y 71.27/32.35 , ++(++(x, y), z) -> ++(x, ++(y, z)) 71.27/32.35 , rev(nil()) -> nil() 71.27/32.35 , rev(unit(x)) -> unit(x) 71.27/32.35 , rev(++(x, y)) -> ++(rev(y), rev(x)) 71.27/32.35 , rev(rev(x)) -> x } 71.27/32.35 Obligation: 71.27/32.35 innermost runtime complexity 71.27/32.35 Answer: 71.27/32.35 YES(O(1),O(n^1)) 71.27/32.35 71.27/32.35 Due to missing edges in the dependency-graph, the right-hand sides 71.27/32.35 of following rules could be simplified: 71.27/32.35 71.27/32.35 { ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) } 71.27/32.35 71.27/32.35 We are left with following problem, upon which TcT provides the 71.27/32.35 certificate YES(O(1),O(n^1)). 71.27/32.35 71.27/32.35 Strict DPs: 71.27/32.35 { flatten^#(unit(x)) -> c_1(flatten^#(x)) 71.27/32.35 , flatten^#(++(x, y)) -> 71.27/32.35 c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , flatten^#(++(unit(x), y)) -> 71.27/32.35 c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , ++^#(++(x, y), z) -> c_4(++^#(y, z)) } 71.27/32.35 Weak Trs: 71.27/32.35 { flatten(flatten(x)) -> flatten(x) 71.27/32.35 , flatten(nil()) -> nil() 71.27/32.35 , flatten(unit(x)) -> flatten(x) 71.27/32.35 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , ++(x, nil()) -> x 71.27/32.35 , ++(nil(), y) -> y 71.27/32.35 , ++(++(x, y), z) -> ++(x, ++(y, z)) 71.27/32.35 , rev(nil()) -> nil() 71.27/32.35 , rev(unit(x)) -> unit(x) 71.27/32.35 , rev(++(x, y)) -> ++(rev(y), rev(x)) 71.27/32.35 , rev(rev(x)) -> x } 71.27/32.35 Obligation: 71.27/32.35 innermost runtime complexity 71.27/32.35 Answer: 71.27/32.35 YES(O(1),O(n^1)) 71.27/32.35 71.27/32.35 We replace rewrite rules by usable rules: 71.27/32.35 71.27/32.35 Weak Usable Rules: 71.27/32.35 { flatten(flatten(x)) -> flatten(x) 71.27/32.35 , flatten(nil()) -> nil() 71.27/32.35 , flatten(unit(x)) -> flatten(x) 71.27/32.35 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , ++(x, nil()) -> x 71.27/32.35 , ++(nil(), y) -> y 71.27/32.35 , ++(++(x, y), z) -> ++(x, ++(y, z)) } 71.27/32.35 71.27/32.35 We are left with following problem, upon which TcT provides the 71.27/32.35 certificate YES(O(1),O(n^1)). 71.27/32.35 71.27/32.35 Strict DPs: 71.27/32.35 { flatten^#(unit(x)) -> c_1(flatten^#(x)) 71.27/32.35 , flatten^#(++(x, y)) -> 71.27/32.35 c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , flatten^#(++(unit(x), y)) -> 71.27/32.35 c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.35 , ++^#(++(x, y), z) -> c_4(++^#(y, z)) } 71.27/32.35 Weak Trs: 71.27/32.35 { flatten(flatten(x)) -> flatten(x) 71.27/32.35 , flatten(nil()) -> nil() 71.27/32.35 , flatten(unit(x)) -> flatten(x) 71.27/32.35 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.35 , ++(x, nil()) -> x 71.27/32.35 , ++(nil(), y) -> y 71.27/32.35 , ++(++(x, y), z) -> ++(x, ++(y, z)) } 71.27/32.35 Obligation: 71.27/32.35 innermost runtime complexity 71.27/32.35 Answer: 71.27/32.35 YES(O(1),O(n^1)) 71.27/32.35 71.27/32.35 We use the processor 'matrix interpretation of dimension 1' to 71.27/32.35 orient following rules strictly. 71.27/32.35 71.27/32.35 DPs: 71.27/32.35 { 4: ++^#(++(x, y), z) -> c_4(++^#(y, z)) } 71.27/32.35 Trs: 71.27/32.35 { ++(x, nil()) -> x 71.27/32.35 , ++(nil(), y) -> y 71.27/32.35 , ++(++(x, y), z) -> ++(x, ++(y, z)) } 71.27/32.35 71.27/32.35 Sub-proof: 71.27/32.35 ---------- 71.27/32.35 The following argument positions are usable: 71.27/32.35 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2, 3}, Uargs(c_3) = {1, 2, 3}, 71.27/32.35 Uargs(c_4) = {1} 71.27/32.35 71.27/32.35 TcT has computed the following constructor-based matrix 71.27/32.35 interpretation satisfying not(EDA). 71.27/32.35 71.27/32.35 [flatten](x1) = [1] x1 + [0] 71.27/32.35 71.27/32.35 [nil] = [0] 71.27/32.35 71.27/32.35 [unit](x1) = [1] x1 + [0] 71.27/32.35 71.27/32.35 [++](x1, x2) = [3] x1 + [1] x2 + [1] 71.27/32.35 71.27/32.35 [flatten^#](x1) = [2] x1 + [0] 71.27/32.35 71.27/32.35 [++^#](x1, x2) = [4] x1 + [0] 71.27/32.35 71.27/32.35 [c_1](x1) = [1] x1 + [0] 71.27/32.35 71.27/32.35 [c_2](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] 71.27/32.35 71.27/32.35 [c_3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] 71.27/32.35 71.27/32.35 [c_4](x1) = [1] x1 + [1] 71.27/32.35 71.27/32.35 The order satisfies the following ordering constraints: 71.27/32.35 71.27/32.35 [flatten(flatten(x))] = [1] x + [0] 71.27/32.35 >= [1] x + [0] 71.27/32.35 = [flatten(x)] 71.27/32.35 71.27/32.35 [flatten(nil())] = [0] 71.27/32.35 >= [0] 71.27/32.35 = [nil()] 71.27/32.35 71.27/32.35 [flatten(unit(x))] = [1] x + [0] 71.27/32.35 >= [1] x + [0] 71.27/32.35 = [flatten(x)] 71.27/32.35 71.27/32.35 [flatten(++(x, y))] = [3] x + [1] y + [1] 71.27/32.35 >= [3] x + [1] y + [1] 71.27/32.35 = [++(flatten(x), flatten(y))] 71.27/32.35 71.27/32.35 [flatten(++(unit(x), y))] = [3] x + [1] y + [1] 71.27/32.35 >= [3] x + [1] y + [1] 71.27/32.35 = [++(flatten(x), flatten(y))] 71.27/32.35 71.27/32.35 [++(x, nil())] = [3] x + [1] 71.27/32.35 > [1] x + [0] 71.27/32.35 = [x] 71.27/32.35 71.27/32.35 [++(nil(), y)] = [1] y + [1] 71.27/32.35 > [1] y + [0] 71.27/32.35 = [y] 71.27/32.36 71.27/32.36 [++(++(x, y), z)] = [9] x + [3] y + [1] z + [4] 71.27/32.36 > [3] x + [3] y + [1] z + [2] 71.27/32.36 = [++(x, ++(y, z))] 71.27/32.36 71.27/32.36 [flatten^#(unit(x))] = [2] x + [0] 71.27/32.36 >= [2] x + [0] 71.27/32.36 = [c_1(flatten^#(x))] 71.27/32.36 71.27/32.36 [flatten^#(++(x, y))] = [6] x + [2] y + [2] 71.27/32.36 >= [6] x + [2] y + [2] 71.27/32.36 = [c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))] 71.27/32.36 71.27/32.36 [flatten^#(++(unit(x), y))] = [6] x + [2] y + [2] 71.27/32.36 >= [6] x + [2] y + [2] 71.27/32.36 = [c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))] 71.27/32.36 71.27/32.36 [++^#(++(x, y), z)] = [12] x + [4] y + [4] 71.27/32.36 > [4] y + [1] 71.27/32.36 = [c_4(++^#(y, z))] 71.27/32.36 71.27/32.36 71.27/32.36 The strictly oriented rules are moved into the weak component. 71.27/32.36 71.27/32.36 We are left with following problem, upon which TcT provides the 71.27/32.36 certificate YES(O(1),O(n^1)). 71.27/32.36 71.27/32.36 Strict DPs: 71.27/32.36 { flatten^#(unit(x)) -> c_1(flatten^#(x)) 71.27/32.36 , flatten^#(++(x, y)) -> 71.27/32.36 c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.36 , flatten^#(++(unit(x), y)) -> 71.27/32.36 c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) } 71.27/32.36 Weak DPs: { ++^#(++(x, y), z) -> c_4(++^#(y, z)) } 71.27/32.36 Weak Trs: 71.27/32.36 { flatten(flatten(x)) -> flatten(x) 71.27/32.36 , flatten(nil()) -> nil() 71.27/32.36 , flatten(unit(x)) -> flatten(x) 71.27/32.36 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.36 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.36 , ++(x, nil()) -> x 71.27/32.36 , ++(nil(), y) -> y 71.27/32.36 , ++(++(x, y), z) -> ++(x, ++(y, z)) } 71.27/32.36 Obligation: 71.27/32.36 innermost runtime complexity 71.27/32.36 Answer: 71.27/32.36 YES(O(1),O(n^1)) 71.27/32.36 71.27/32.36 The following weak DPs constitute a sub-graph of the DG that is 71.27/32.36 closed under successors. The DPs are removed. 71.27/32.36 71.27/32.36 { ++^#(++(x, y), z) -> c_4(++^#(y, z)) } 71.27/32.36 71.27/32.36 We are left with following problem, upon which TcT provides the 71.27/32.36 certificate YES(O(1),O(n^1)). 71.27/32.36 71.27/32.36 Strict DPs: 71.27/32.36 { flatten^#(unit(x)) -> c_1(flatten^#(x)) 71.27/32.36 , flatten^#(++(x, y)) -> 71.27/32.36 c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.36 , flatten^#(++(unit(x), y)) -> 71.27/32.36 c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) } 71.27/32.36 Weak Trs: 71.27/32.36 { flatten(flatten(x)) -> flatten(x) 71.27/32.36 , flatten(nil()) -> nil() 71.27/32.36 , flatten(unit(x)) -> flatten(x) 71.27/32.36 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.36 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.36 , ++(x, nil()) -> x 71.27/32.36 , ++(nil(), y) -> y 71.27/32.36 , ++(++(x, y), z) -> ++(x, ++(y, z)) } 71.27/32.36 Obligation: 71.27/32.36 innermost runtime complexity 71.27/32.36 Answer: 71.27/32.36 YES(O(1),O(n^1)) 71.27/32.36 71.27/32.36 Due to missing edges in the dependency-graph, the right-hand sides 71.27/32.36 of following rules could be simplified: 71.27/32.36 71.27/32.36 { flatten^#(++(x, y)) -> 71.27/32.36 c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) 71.27/32.36 , flatten^#(++(unit(x), y)) -> 71.27/32.36 c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) } 71.27/32.36 71.27/32.36 We are left with following problem, upon which TcT provides the 71.27/32.36 certificate YES(O(1),O(n^1)). 71.27/32.36 71.27/32.36 Strict DPs: 71.27/32.36 { flatten^#(unit(x)) -> c_1(flatten^#(x)) 71.27/32.36 , flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y)) 71.27/32.36 , flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) } 71.27/32.36 Weak Trs: 71.27/32.36 { flatten(flatten(x)) -> flatten(x) 71.27/32.36 , flatten(nil()) -> nil() 71.27/32.36 , flatten(unit(x)) -> flatten(x) 71.27/32.36 , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) 71.27/32.36 , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) 71.27/32.36 , ++(x, nil()) -> x 71.27/32.36 , ++(nil(), y) -> y 71.27/32.36 , ++(++(x, y), z) -> ++(x, ++(y, z)) } 71.27/32.36 Obligation: 71.27/32.36 innermost runtime complexity 71.27/32.36 Answer: 71.27/32.36 YES(O(1),O(n^1)) 71.27/32.36 71.27/32.36 No rule is usable, rules are removed from the input problem. 71.27/32.36 71.27/32.36 We are left with following problem, upon which TcT provides the 71.27/32.36 certificate YES(O(1),O(n^1)). 71.27/32.36 71.27/32.36 Strict DPs: 71.27/32.36 { flatten^#(unit(x)) -> c_1(flatten^#(x)) 71.27/32.36 , flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y)) 71.27/32.36 , flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) } 71.27/32.36 Obligation: 71.27/32.36 innermost runtime complexity 71.27/32.36 Answer: 71.27/32.36 YES(O(1),O(n^1)) 71.27/32.36 71.27/32.36 We use the processor 'matrix interpretation of dimension 1' to 71.27/32.36 orient following rules strictly. 71.27/32.36 71.27/32.36 DPs: 71.27/32.36 { 2: flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y)) 71.27/32.36 , 3: flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) } 71.27/32.36 71.27/32.36 Sub-proof: 71.27/32.36 ---------- 71.27/32.36 The following argument positions are usable: 71.27/32.36 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2} 71.27/32.36 71.27/32.36 TcT has computed the following constructor-based matrix 71.27/32.36 interpretation satisfying not(EDA). 71.27/32.36 71.27/32.36 [flatten](x1) = [7] x1 + [0] 71.27/32.36 71.27/32.36 [nil] = [0] 71.27/32.36 71.27/32.36 [unit](x1) = [1] x1 + [0] 71.27/32.36 71.27/32.36 [++](x1, x2) = [4] x1 + [4] x2 + [4] 71.27/32.36 71.27/32.36 [flatten^#](x1) = [2] x1 + [0] 71.27/32.36 71.27/32.36 [++^#](x1, x2) = [7] x1 + [7] x2 + [0] 71.27/32.36 71.27/32.36 [c_1](x1) = [7] x1 + [0] 71.27/32.36 71.27/32.36 [c_2](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 71.27/32.36 71.27/32.36 [c_3](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 71.27/32.36 71.27/32.36 [c_4](x1) = [7] x1 + [0] 71.27/32.36 71.27/32.36 [c] = [0] 71.27/32.36 71.27/32.36 [c_1](x1) = [1] x1 + [0] 71.27/32.36 71.27/32.36 [c_2](x1, x2) = [4] x1 + [4] x2 + [7] 71.27/32.36 71.27/32.36 [c_3](x1, x2) = [1] x1 + [1] x2 + [5] 71.27/32.36 71.27/32.36 The order satisfies the following ordering constraints: 71.27/32.36 71.27/32.36 [flatten^#(unit(x))] = [2] x + [0] 71.27/32.36 >= [2] x + [0] 71.27/32.36 = [c_1(flatten^#(x))] 71.27/32.36 71.27/32.36 [flatten^#(++(x, y))] = [8] x + [8] y + [8] 71.27/32.36 > [8] x + [8] y + [7] 71.27/32.36 = [c_2(flatten^#(x), flatten^#(y))] 71.27/32.36 71.27/32.36 [flatten^#(++(unit(x), y))] = [8] x + [8] y + [8] 71.27/32.36 > [2] x + [2] y + [5] 71.27/32.36 = [c_3(flatten^#(x), flatten^#(y))] 71.27/32.36 71.27/32.36 71.27/32.36 The strictly oriented rules are moved into the weak component. 71.27/32.36 71.27/32.36 We are left with following problem, upon which TcT provides the 71.27/32.36 certificate YES(O(1),O(n^1)). 71.27/32.36 71.27/32.36 Strict DPs: { flatten^#(unit(x)) -> c_1(flatten^#(x)) } 71.27/32.36 Weak DPs: 71.27/32.36 { flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y)) 71.27/32.36 , flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) } 71.27/32.36 Obligation: 71.27/32.36 innermost runtime complexity 71.27/32.36 Answer: 71.27/32.36 YES(O(1),O(n^1)) 71.27/32.36 71.27/32.36 We use the processor 'matrix interpretation of dimension 1' to 71.27/32.36 orient following rules strictly. 71.27/32.36 71.27/32.36 DPs: 71.27/32.36 { 1: flatten^#(unit(x)) -> c_1(flatten^#(x)) 71.27/32.36 , 3: flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) } 71.27/32.36 71.27/32.36 Sub-proof: 71.27/32.36 ---------- 71.27/32.36 The following argument positions are usable: 71.27/32.36 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2} 71.27/32.36 71.27/32.36 TcT has computed the following constructor-based matrix 71.27/32.36 interpretation satisfying not(EDA). 71.27/32.36 71.27/32.36 [flatten](x1) = [7] x1 + [0] 71.27/32.36 71.27/32.36 [nil] = [0] 71.27/32.36 71.27/32.36 [unit](x1) = [1] x1 + [2] 71.27/32.36 71.27/32.36 [++](x1, x2) = [1] x1 + [1] x2 + [0] 71.27/32.36 71.27/32.36 [flatten^#](x1) = [4] x1 + [0] 71.27/32.36 71.27/32.36 [++^#](x1, x2) = [7] x1 + [7] x2 + [0] 71.27/32.36 71.27/32.36 [c_1](x1) = [7] x1 + [0] 71.27/32.36 71.27/32.36 [c_2](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 71.27/32.36 71.27/32.36 [c_3](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 71.27/32.36 71.27/32.36 [c_4](x1) = [7] x1 + [0] 71.27/32.36 71.27/32.36 [c] = [0] 71.27/32.36 71.27/32.36 [c_1](x1) = [1] x1 + [5] 71.27/32.36 71.27/32.36 [c_2](x1, x2) = [1] x1 + [1] x2 + [0] 71.27/32.36 71.27/32.36 [c_3](x1, x2) = [1] x1 + [1] x2 + [7] 71.27/32.36 71.27/32.36 The order satisfies the following ordering constraints: 71.27/32.36 71.27/32.36 [flatten^#(unit(x))] = [4] x + [8] 71.27/32.36 > [4] x + [5] 71.27/32.36 = [c_1(flatten^#(x))] 71.27/32.36 71.27/32.36 [flatten^#(++(x, y))] = [4] x + [4] y + [0] 71.27/32.36 >= [4] x + [4] y + [0] 71.27/32.36 = [c_2(flatten^#(x), flatten^#(y))] 71.27/32.36 71.27/32.36 [flatten^#(++(unit(x), y))] = [4] x + [4] y + [8] 71.27/32.36 > [4] x + [4] y + [7] 71.27/32.36 = [c_3(flatten^#(x), flatten^#(y))] 71.27/32.36 71.27/32.36 71.27/32.36 The strictly oriented rules are moved into the weak component. 71.27/32.36 71.27/32.36 We are left with following problem, upon which TcT provides the 71.27/32.36 certificate YES(O(1),O(1)). 71.27/32.36 71.27/32.36 Weak DPs: 71.27/32.36 { flatten^#(unit(x)) -> c_1(flatten^#(x)) 71.27/32.36 , flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y)) 71.27/32.36 , flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) } 71.27/32.36 Obligation: 71.27/32.36 innermost runtime complexity 71.27/32.36 Answer: 71.27/32.36 YES(O(1),O(1)) 71.27/32.36 71.27/32.36 The following weak DPs constitute a sub-graph of the DG that is 71.27/32.36 closed under successors. The DPs are removed. 71.27/32.36 71.27/32.36 { flatten^#(unit(x)) -> c_1(flatten^#(x)) 71.27/32.36 , flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y)) 71.27/32.36 , flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) } 71.27/32.36 71.27/32.36 We are left with following problem, upon which TcT provides the 71.27/32.36 certificate YES(O(1),O(1)). 71.27/32.36 71.27/32.36 Rules: Empty 71.27/32.36 Obligation: 71.27/32.36 innermost runtime complexity 71.27/32.36 Answer: 71.27/32.36 YES(O(1),O(1)) 71.27/32.36 71.27/32.36 Empty rules are trivially bounded 71.27/32.36 71.27/32.36 Hurray, we answered YES(O(1),O(n^1)) 71.53/32.41 EOF