YES(O(1),O(n^2)) 26.59/6.94 YES(O(1),O(n^2)) 26.59/6.94 26.59/6.94 We are left with following problem, upon which TcT provides the 26.59/6.94 certificate YES(O(1),O(n^2)). 26.59/6.94 26.59/6.94 Strict Trs: 26.59/6.94 { strmatch(patstr, str) -> domatch(patstr, str, Nil()) 26.59/6.94 , prefix(Nil(), cs) -> True() 26.59/6.94 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.94 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.94 , notEmpty(Nil()) -> False() 26.59/6.94 , notEmpty(Cons(x, xs)) -> True() 26.59/6.94 , eqNatList(Nil(), Nil()) -> True() 26.59/6.94 , eqNatList(Nil(), Cons(y, ys)) -> False() 26.59/6.94 , eqNatList(Cons(x, xs), Nil()) -> False() 26.59/6.94 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 26.59/6.94 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) 26.59/6.94 , domatch(patcs, Cons(x, xs), n) -> 26.59/6.94 domatch[Ite][True][Ite](prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n) 26.59/6.94 , domatch(Nil(), Nil(), n) -> Cons(n, Nil()) 26.59/6.94 , domatch(Cons(x, xs), Nil(), n) -> Nil() } 26.59/6.94 Weak Trs: 26.59/6.94 { domatch[Ite][True][Ite](True(), patcs, Cons(x, xs), n) -> 26.59/6.94 Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , domatch[Ite][True][Ite](False(), patcs, Cons(x, xs), n) -> 26.59/6.94 domatch(patcs, xs, Cons(n, Cons(Nil(), Nil()))) 26.59/6.94 , and(True(), True()) -> True() 26.59/6.94 , and(True(), False()) -> False() 26.59/6.94 , and(False(), True()) -> False() 26.59/6.94 , and(False(), False()) -> False() 26.59/6.94 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.94 , !EQ(S(x), 0()) -> False() 26.59/6.94 , !EQ(0(), S(y)) -> False() 26.59/6.94 , !EQ(0(), 0()) -> True() } 26.59/6.94 Obligation: 26.59/6.94 innermost runtime complexity 26.59/6.94 Answer: 26.59/6.94 YES(O(1),O(n^2)) 26.59/6.94 26.59/6.94 We add the following weak dependency pairs: 26.59/6.94 26.59/6.94 Strict DPs: 26.59/6.94 { strmatch^#(patstr, str) -> c_1(domatch^#(patstr, str, Nil())) 26.59/6.94 , domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) 26.59/6.94 , domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.94 , domatch^#(Cons(x, xs), Nil(), n) -> c_13() 26.59/6.94 , prefix^#(Nil(), cs) -> c_2() 26.59/6.94 , prefix^#(Cons(x, xs), Nil()) -> c_3() 26.59/6.94 , prefix^#(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 c_4(and^#(!EQ(x', x), prefix(xs', xs))) 26.59/6.94 , notEmpty^#(Nil()) -> c_5() 26.59/6.94 , notEmpty^#(Cons(x, xs)) -> c_6() 26.59/6.94 , eqNatList^#(Nil(), Nil()) -> c_7() 26.59/6.94 , eqNatList^#(Nil(), Cons(y, ys)) -> c_8() 26.59/6.94 , eqNatList^#(Cons(x, xs), Nil()) -> c_9() 26.59/6.94 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_10(!EQ^#(x, y)) } 26.59/6.94 Weak DPs: 26.59/6.94 { and^#(True(), True()) -> c_16() 26.59/6.94 , and^#(True(), False()) -> c_17() 26.59/6.94 , and^#(False(), True()) -> c_18() 26.59/6.94 , and^#(False(), False()) -> c_19() 26.59/6.94 , !EQ^#(S(x), S(y)) -> c_20(!EQ^#(x, y)) 26.59/6.94 , !EQ^#(S(x), 0()) -> c_21() 26.59/6.94 , !EQ^#(0(), S(y)) -> c_22() 26.59/6.94 , !EQ^#(0(), 0()) -> c_23() 26.59/6.94 , domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.94 26.59/6.94 and mark the set of starting terms. 26.59/6.94 26.59/6.94 We are left with following problem, upon which TcT provides the 26.59/6.94 certificate YES(O(1),O(n^2)). 26.59/6.94 26.59/6.94 Strict DPs: 26.59/6.94 { strmatch^#(patstr, str) -> c_1(domatch^#(patstr, str, Nil())) 26.59/6.94 , domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) 26.59/6.94 , domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.94 , domatch^#(Cons(x, xs), Nil(), n) -> c_13() 26.59/6.94 , prefix^#(Nil(), cs) -> c_2() 26.59/6.94 , prefix^#(Cons(x, xs), Nil()) -> c_3() 26.59/6.94 , prefix^#(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 c_4(and^#(!EQ(x', x), prefix(xs', xs))) 26.59/6.94 , notEmpty^#(Nil()) -> c_5() 26.59/6.94 , notEmpty^#(Cons(x, xs)) -> c_6() 26.59/6.94 , eqNatList^#(Nil(), Nil()) -> c_7() 26.59/6.94 , eqNatList^#(Nil(), Cons(y, ys)) -> c_8() 26.59/6.94 , eqNatList^#(Cons(x, xs), Nil()) -> c_9() 26.59/6.94 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_10(!EQ^#(x, y)) } 26.59/6.94 Strict Trs: 26.59/6.94 { strmatch(patstr, str) -> domatch(patstr, str, Nil()) 26.59/6.94 , prefix(Nil(), cs) -> True() 26.59/6.94 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.94 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.94 , notEmpty(Nil()) -> False() 26.59/6.94 , notEmpty(Cons(x, xs)) -> True() 26.59/6.94 , eqNatList(Nil(), Nil()) -> True() 26.59/6.94 , eqNatList(Nil(), Cons(y, ys)) -> False() 26.59/6.94 , eqNatList(Cons(x, xs), Nil()) -> False() 26.59/6.94 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 26.59/6.94 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) 26.59/6.94 , domatch(patcs, Cons(x, xs), n) -> 26.59/6.94 domatch[Ite][True][Ite](prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n) 26.59/6.94 , domatch(Nil(), Nil(), n) -> Cons(n, Nil()) 26.59/6.94 , domatch(Cons(x, xs), Nil(), n) -> Nil() } 26.59/6.94 Weak DPs: 26.59/6.94 { and^#(True(), True()) -> c_16() 26.59/6.94 , and^#(True(), False()) -> c_17() 26.59/6.94 , and^#(False(), True()) -> c_18() 26.59/6.94 , and^#(False(), False()) -> c_19() 26.59/6.94 , !EQ^#(S(x), S(y)) -> c_20(!EQ^#(x, y)) 26.59/6.94 , !EQ^#(S(x), 0()) -> c_21() 26.59/6.94 , !EQ^#(0(), S(y)) -> c_22() 26.59/6.94 , !EQ^#(0(), 0()) -> c_23() 26.59/6.94 , domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.94 Weak Trs: 26.59/6.94 { domatch[Ite][True][Ite](True(), patcs, Cons(x, xs), n) -> 26.59/6.94 Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , domatch[Ite][True][Ite](False(), patcs, Cons(x, xs), n) -> 26.59/6.94 domatch(patcs, xs, Cons(n, Cons(Nil(), Nil()))) 26.59/6.94 , and(True(), True()) -> True() 26.59/6.94 , and(True(), False()) -> False() 26.59/6.94 , and(False(), True()) -> False() 26.59/6.94 , and(False(), False()) -> False() 26.59/6.94 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.94 , !EQ(S(x), 0()) -> False() 26.59/6.94 , !EQ(0(), S(y)) -> False() 26.59/6.94 , !EQ(0(), 0()) -> True() } 26.59/6.94 Obligation: 26.59/6.94 innermost runtime complexity 26.59/6.94 Answer: 26.59/6.94 YES(O(1),O(n^2)) 26.59/6.94 26.59/6.94 We replace rewrite rules by usable rules: 26.59/6.94 26.59/6.94 Strict Usable Rules: 26.59/6.94 { prefix(Nil(), cs) -> True() 26.59/6.94 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.94 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 and(!EQ(x', x), prefix(xs', xs)) } 26.59/6.94 Weak Usable Rules: 26.59/6.94 { and(True(), True()) -> True() 26.59/6.94 , and(True(), False()) -> False() 26.59/6.94 , and(False(), True()) -> False() 26.59/6.94 , and(False(), False()) -> False() 26.59/6.94 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.94 , !EQ(S(x), 0()) -> False() 26.59/6.94 , !EQ(0(), S(y)) -> False() 26.59/6.94 , !EQ(0(), 0()) -> True() } 26.59/6.94 26.59/6.94 We are left with following problem, upon which TcT provides the 26.59/6.94 certificate YES(O(1),O(n^2)). 26.59/6.94 26.59/6.94 Strict DPs: 26.59/6.94 { strmatch^#(patstr, str) -> c_1(domatch^#(patstr, str, Nil())) 26.59/6.94 , domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) 26.59/6.94 , domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.94 , domatch^#(Cons(x, xs), Nil(), n) -> c_13() 26.59/6.94 , prefix^#(Nil(), cs) -> c_2() 26.59/6.94 , prefix^#(Cons(x, xs), Nil()) -> c_3() 26.59/6.94 , prefix^#(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 c_4(and^#(!EQ(x', x), prefix(xs', xs))) 26.59/6.94 , notEmpty^#(Nil()) -> c_5() 26.59/6.94 , notEmpty^#(Cons(x, xs)) -> c_6() 26.59/6.94 , eqNatList^#(Nil(), Nil()) -> c_7() 26.59/6.94 , eqNatList^#(Nil(), Cons(y, ys)) -> c_8() 26.59/6.94 , eqNatList^#(Cons(x, xs), Nil()) -> c_9() 26.59/6.94 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_10(!EQ^#(x, y)) } 26.59/6.94 Strict Trs: 26.59/6.94 { prefix(Nil(), cs) -> True() 26.59/6.94 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.94 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 and(!EQ(x', x), prefix(xs', xs)) } 26.59/6.94 Weak DPs: 26.59/6.94 { and^#(True(), True()) -> c_16() 26.59/6.94 , and^#(True(), False()) -> c_17() 26.59/6.94 , and^#(False(), True()) -> c_18() 26.59/6.94 , and^#(False(), False()) -> c_19() 26.59/6.94 , !EQ^#(S(x), S(y)) -> c_20(!EQ^#(x, y)) 26.59/6.94 , !EQ^#(S(x), 0()) -> c_21() 26.59/6.94 , !EQ^#(0(), S(y)) -> c_22() 26.59/6.94 , !EQ^#(0(), 0()) -> c_23() 26.59/6.94 , domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.94 Weak Trs: 26.59/6.94 { and(True(), True()) -> True() 26.59/6.94 , and(True(), False()) -> False() 26.59/6.94 , and(False(), True()) -> False() 26.59/6.94 , and(False(), False()) -> False() 26.59/6.94 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.94 , !EQ(S(x), 0()) -> False() 26.59/6.94 , !EQ(0(), S(y)) -> False() 26.59/6.94 , !EQ(0(), 0()) -> True() } 26.59/6.94 Obligation: 26.59/6.94 innermost runtime complexity 26.59/6.94 Answer: 26.59/6.94 YES(O(1),O(n^2)) 26.59/6.94 26.59/6.94 The weightgap principle applies (using the following constant 26.59/6.94 growth matrix-interpretation) 26.59/6.94 26.59/6.94 The following argument positions are usable: 26.59/6.94 Uargs(and) = {1, 2}, Uargs(c_1) = {1}, Uargs(c_4) = {1}, 26.59/6.94 Uargs(and^#) = {1, 2}, Uargs(c_10) = {1}, Uargs(c_11) = {1}, 26.59/6.94 Uargs(domatch[Ite][True][Ite]^#) = {1}, Uargs(c_14) = {1}, 26.59/6.94 Uargs(c_15) = {1}, Uargs(c_20) = {1} 26.59/6.94 26.59/6.94 TcT has computed the following constructor-restricted matrix 26.59/6.94 interpretation. 26.59/6.94 26.59/6.94 [True] = [0] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [prefix](x1, x2) = [0 0] x1 + [0 26.59/6.94 1] x2 + [2] 26.59/6.94 [2 0] [2 26.59/6.94 0] [0] 26.59/6.94 26.59/6.94 [Nil] = [0] 26.59/6.94 [2] 26.59/6.94 26.59/6.94 [and](x1, x2) = [2 0] x1 + [1 26.59/6.94 0] x2 + [0] 26.59/6.94 [0 0] [0 26.59/6.94 0] [0] 26.59/6.94 26.59/6.94 [!EQ](x1, x2) = [0] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [S](x1) = [1 0] x1 + [0] 26.59/6.94 [0 0] [0] 26.59/6.94 26.59/6.94 [Cons](x1, x2) = [1 2] x2 + [0] 26.59/6.94 [0 1] [1] 26.59/6.94 26.59/6.94 [0] = [0] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [False] = [0] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [strmatch^#](x1, x2) = [1 1] x1 + [2 26.59/6.94 2] x2 + [1] 26.59/6.94 [2 2] [1 26.59/6.94 1] [1] 26.59/6.94 26.59/6.94 [c_1](x1) = [1 0] x1 + [2] 26.59/6.94 [0 1] [2] 26.59/6.94 26.59/6.94 [domatch^#](x1, x2, x3) = [1 2] x2 + [0] 26.59/6.94 [0 0] [0] 26.59/6.94 26.59/6.94 [prefix^#](x1, x2) = [2 0] x2 + [0] 26.59/6.94 [0 0] [0] 26.59/6.94 26.59/6.94 [c_2] = [1] 26.59/6.94 [1] 26.59/6.94 26.59/6.94 [c_3] = [1] 26.59/6.94 [1] 26.59/6.94 26.59/6.94 [c_4](x1) = [1 0] x1 + [1] 26.59/6.94 [0 1] [2] 26.59/6.94 26.59/6.94 [and^#](x1, x2) = [1 0] x1 + [1 26.59/6.94 0] x2 + [1] 26.59/6.94 [0 0] [0 26.59/6.94 0] [0] 26.59/6.94 26.59/6.94 [notEmpty^#](x1) = [1 1] x1 + [1] 26.59/6.94 [2 1] [1] 26.59/6.94 26.59/6.94 [c_5] = [1] 26.59/6.94 [1] 26.59/6.94 26.59/6.94 [c_6] = [1] 26.59/6.94 [1] 26.59/6.94 26.59/6.94 [eqNatList^#](x1, x2) = [0] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [c_7] = [1] 26.59/6.94 [1] 26.59/6.94 26.59/6.94 [c_8] = [1] 26.59/6.94 [1] 26.59/6.94 26.59/6.94 [c_9] = [1] 26.59/6.94 [1] 26.59/6.94 26.59/6.94 [c_10](x1) = [1 0] x1 + [2] 26.59/6.94 [0 1] [2] 26.59/6.94 26.59/6.94 [!EQ^#](x1, x2) = [0] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [c_11](x1) = [1 0] x1 + [1] 26.59/6.94 [0 1] [2] 26.59/6.94 26.59/6.94 [domatch[Ite][True][Ite]^#](x1, x2, x3, x4) = [2 0] x1 + [1 26.59/6.94 0] x3 + [0 0] x4 + [0] 26.59/6.94 [0 0] [0 26.59/6.94 0] [1 1] [0] 26.59/6.94 26.59/6.94 [c_12] = [1] 26.59/6.94 [1] 26.59/6.94 26.59/6.94 [c_13] = [1] 26.59/6.94 [2] 26.59/6.94 26.59/6.94 [c_14](x1) = [1 0] x1 + [0] 26.59/6.94 [0 1] [0] 26.59/6.94 26.59/6.94 [c_15](x1) = [1 0] x1 + [0] 26.59/6.94 [0 1] [0] 26.59/6.94 26.59/6.94 [c_16] = [1] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [c_17] = [1] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [c_18] = [1] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [c_19] = [1] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [c_20](x1) = [1 0] x1 + [0] 26.59/6.94 [0 1] [0] 26.59/6.94 26.59/6.94 [c_21] = [0] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [c_22] = [0] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 [c_23] = [0] 26.59/6.94 [0] 26.59/6.94 26.59/6.94 The order satisfies the following ordering constraints: 26.59/6.94 26.59/6.94 [prefix(Nil(), cs)] = [0 1] cs + [2] 26.59/6.94 [2 0] [0] 26.59/6.94 > [0] 26.59/6.94 [0] 26.59/6.94 = [True()] 26.59/6.94 26.59/6.94 [prefix(Cons(x, xs), Nil())] = [0 0] xs + [4] 26.59/6.94 [2 4] [0] 26.59/6.94 > [0] 26.59/6.94 [0] 26.59/6.94 = [False()] 26.59/6.94 26.59/6.94 [prefix(Cons(x', xs'), Cons(x, xs))] = [0 0] xs' + [0 1] xs + [3] 26.59/6.94 [2 4] [2 4] [0] 26.59/6.94 > [0 1] xs + [2] 26.59/6.94 [0 0] [0] 26.59/6.94 = [and(!EQ(x', x), prefix(xs', xs))] 26.59/6.94 26.59/6.94 [and(True(), True())] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [True()] 26.59/6.94 26.59/6.94 [and(True(), False())] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [False()] 26.59/6.94 26.59/6.94 [and(False(), True())] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [False()] 26.59/6.94 26.59/6.94 [and(False(), False())] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [False()] 26.59/6.94 26.59/6.94 [!EQ(S(x), S(y))] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [!EQ(x, y)] 26.59/6.94 26.59/6.94 [!EQ(S(x), 0())] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [False()] 26.59/6.94 26.59/6.94 [!EQ(0(), S(y))] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [False()] 26.59/6.94 26.59/6.94 [!EQ(0(), 0())] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [True()] 26.59/6.94 26.59/6.94 [strmatch^#(patstr, str)] = [1 1] patstr + [2 2] str + [1] 26.59/6.94 [2 2] [1 1] [1] 26.59/6.94 ? [1 2] str + [2] 26.59/6.94 [0 0] [2] 26.59/6.94 = [c_1(domatch^#(patstr, str, Nil()))] 26.59/6.94 26.59/6.94 [domatch^#(patcs, Cons(x, xs), n)] = [1 4] xs + [2] 26.59/6.94 [0 0] [0] 26.59/6.94 ? [1 4] xs + [0 0] n + [7] 26.59/6.94 [0 0] [1 1] [2] 26.59/6.94 = [c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n))] 26.59/6.94 26.59/6.94 [domatch^#(Nil(), Nil(), n)] = [4] 26.59/6.94 [0] 26.59/6.94 ? [1] 26.59/6.94 [1] 26.59/6.94 = [c_12()] 26.59/6.94 26.59/6.94 [domatch^#(Cons(x, xs), Nil(), n)] = [4] 26.59/6.94 [0] 26.59/6.94 ? [1] 26.59/6.94 [2] 26.59/6.94 = [c_13()] 26.59/6.94 26.59/6.94 [prefix^#(Nil(), cs)] = [2 0] cs + [0] 26.59/6.94 [0 0] [0] 26.59/6.94 ? [1] 26.59/6.94 [1] 26.59/6.94 = [c_2()] 26.59/6.94 26.59/6.94 [prefix^#(Cons(x, xs), Nil())] = [0] 26.59/6.94 [0] 26.59/6.94 ? [1] 26.59/6.94 [1] 26.59/6.94 = [c_3()] 26.59/6.94 26.59/6.94 [prefix^#(Cons(x', xs'), Cons(x, xs))] = [2 4] xs + [0] 26.59/6.94 [0 0] [0] 26.59/6.94 ? [0 1] xs + [4] 26.59/6.94 [0 0] [2] 26.59/6.94 = [c_4(and^#(!EQ(x', x), prefix(xs', xs)))] 26.59/6.94 26.59/6.94 [and^#(True(), True())] = [1] 26.59/6.94 [0] 26.59/6.94 >= [1] 26.59/6.94 [0] 26.59/6.94 = [c_16()] 26.59/6.94 26.59/6.94 [and^#(True(), False())] = [1] 26.59/6.94 [0] 26.59/6.94 >= [1] 26.59/6.94 [0] 26.59/6.94 = [c_17()] 26.59/6.94 26.59/6.94 [and^#(False(), True())] = [1] 26.59/6.94 [0] 26.59/6.94 >= [1] 26.59/6.94 [0] 26.59/6.94 = [c_18()] 26.59/6.94 26.59/6.94 [and^#(False(), False())] = [1] 26.59/6.94 [0] 26.59/6.94 >= [1] 26.59/6.94 [0] 26.59/6.94 = [c_19()] 26.59/6.94 26.59/6.94 [notEmpty^#(Nil())] = [3] 26.59/6.94 [3] 26.59/6.94 > [1] 26.59/6.94 [1] 26.59/6.94 = [c_5()] 26.59/6.94 26.59/6.94 [notEmpty^#(Cons(x, xs))] = [1 3] xs + [2] 26.59/6.94 [2 5] [2] 26.59/6.94 > [1] 26.59/6.94 [1] 26.59/6.94 = [c_6()] 26.59/6.94 26.59/6.94 [eqNatList^#(Nil(), Nil())] = [0] 26.59/6.94 [0] 26.59/6.94 ? [1] 26.59/6.94 [1] 26.59/6.94 = [c_7()] 26.59/6.94 26.59/6.94 [eqNatList^#(Nil(), Cons(y, ys))] = [0] 26.59/6.94 [0] 26.59/6.94 ? [1] 26.59/6.94 [1] 26.59/6.94 = [c_8()] 26.59/6.94 26.59/6.94 [eqNatList^#(Cons(x, xs), Nil())] = [0] 26.59/6.94 [0] 26.59/6.94 ? [1] 26.59/6.94 [1] 26.59/6.94 = [c_9()] 26.59/6.94 26.59/6.94 [eqNatList^#(Cons(x, xs), Cons(y, ys))] = [0] 26.59/6.94 [0] 26.59/6.94 ? [2] 26.59/6.94 [2] 26.59/6.94 = [c_10(!EQ^#(x, y))] 26.59/6.94 26.59/6.94 [!EQ^#(S(x), S(y))] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [c_20(!EQ^#(x, y))] 26.59/6.94 26.59/6.94 [!EQ^#(S(x), 0())] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [c_21()] 26.59/6.94 26.59/6.94 [!EQ^#(0(), S(y))] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [c_22()] 26.59/6.94 26.59/6.94 [!EQ^#(0(), 0())] = [0] 26.59/6.94 [0] 26.59/6.94 >= [0] 26.59/6.94 [0] 26.59/6.94 = [c_23()] 26.59/6.94 26.59/6.94 [domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n)] = [1 2] xs + [0 0] n + [0] 26.59/6.94 [0 0] [1 1] [0] 26.59/6.94 >= [1 2] xs + [0] 26.59/6.94 [0 0] [0] 26.59/6.94 = [c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil()))))] 26.59/6.94 26.59/6.94 [domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n)] = [1 2] xs + [0 0] n + [0] 26.59/6.94 [0 0] [1 1] [0] 26.59/6.94 >= [1 2] xs + [0] 26.59/6.94 [0 0] [0] 26.59/6.94 = [c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil()))))] 26.59/6.94 26.59/6.94 26.59/6.94 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 26.59/6.94 26.59/6.94 We are left with following problem, upon which TcT provides the 26.59/6.94 certificate YES(O(1),O(n^1)). 26.59/6.94 26.59/6.94 Strict DPs: 26.59/6.94 { strmatch^#(patstr, str) -> c_1(domatch^#(patstr, str, Nil())) 26.59/6.94 , domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) 26.59/6.94 , domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.94 , domatch^#(Cons(x, xs), Nil(), n) -> c_13() 26.59/6.94 , prefix^#(Nil(), cs) -> c_2() 26.59/6.94 , prefix^#(Cons(x, xs), Nil()) -> c_3() 26.59/6.94 , prefix^#(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 c_4(and^#(!EQ(x', x), prefix(xs', xs))) 26.59/6.94 , eqNatList^#(Nil(), Nil()) -> c_7() 26.59/6.94 , eqNatList^#(Nil(), Cons(y, ys)) -> c_8() 26.59/6.94 , eqNatList^#(Cons(x, xs), Nil()) -> c_9() 26.59/6.94 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_10(!EQ^#(x, y)) } 26.59/6.94 Weak DPs: 26.59/6.94 { and^#(True(), True()) -> c_16() 26.59/6.94 , and^#(True(), False()) -> c_17() 26.59/6.94 , and^#(False(), True()) -> c_18() 26.59/6.94 , and^#(False(), False()) -> c_19() 26.59/6.94 , notEmpty^#(Nil()) -> c_5() 26.59/6.94 , notEmpty^#(Cons(x, xs)) -> c_6() 26.59/6.94 , !EQ^#(S(x), S(y)) -> c_20(!EQ^#(x, y)) 26.59/6.94 , !EQ^#(S(x), 0()) -> c_21() 26.59/6.94 , !EQ^#(0(), S(y)) -> c_22() 26.59/6.94 , !EQ^#(0(), 0()) -> c_23() 26.59/6.94 , domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.94 Weak Trs: 26.59/6.94 { prefix(Nil(), cs) -> True() 26.59/6.94 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.94 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.94 , and(True(), True()) -> True() 26.59/6.94 , and(True(), False()) -> False() 26.59/6.94 , and(False(), True()) -> False() 26.59/6.94 , and(False(), False()) -> False() 26.59/6.94 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.94 , !EQ(S(x), 0()) -> False() 26.59/6.94 , !EQ(0(), S(y)) -> False() 26.59/6.94 , !EQ(0(), 0()) -> True() } 26.59/6.94 Obligation: 26.59/6.94 innermost runtime complexity 26.59/6.94 Answer: 26.59/6.94 YES(O(1),O(n^1)) 26.59/6.94 26.59/6.94 We estimate the number of application of {5,6,7,8,9,10,11} by 26.59/6.94 applications of Pre({5,6,7,8,9,10,11}) = {}. Here rules are labeled 26.59/6.94 as follows: 26.59/6.94 26.59/6.94 DPs: 26.59/6.94 { 1: strmatch^#(patstr, str) -> c_1(domatch^#(patstr, str, Nil())) 26.59/6.94 , 2: domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) 26.59/6.94 , 3: domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.94 , 4: domatch^#(Cons(x, xs), Nil(), n) -> c_13() 26.59/6.94 , 5: prefix^#(Nil(), cs) -> c_2() 26.59/6.94 , 6: prefix^#(Cons(x, xs), Nil()) -> c_3() 26.59/6.94 , 7: prefix^#(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 c_4(and^#(!EQ(x', x), prefix(xs', xs))) 26.59/6.94 , 8: eqNatList^#(Nil(), Nil()) -> c_7() 26.59/6.94 , 9: eqNatList^#(Nil(), Cons(y, ys)) -> c_8() 26.59/6.94 , 10: eqNatList^#(Cons(x, xs), Nil()) -> c_9() 26.59/6.94 , 11: eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_10(!EQ^#(x, y)) 26.59/6.94 , 12: and^#(True(), True()) -> c_16() 26.59/6.94 , 13: and^#(True(), False()) -> c_17() 26.59/6.94 , 14: and^#(False(), True()) -> c_18() 26.59/6.94 , 15: and^#(False(), False()) -> c_19() 26.59/6.94 , 16: notEmpty^#(Nil()) -> c_5() 26.59/6.94 , 17: notEmpty^#(Cons(x, xs)) -> c_6() 26.59/6.94 , 18: !EQ^#(S(x), S(y)) -> c_20(!EQ^#(x, y)) 26.59/6.94 , 19: !EQ^#(S(x), 0()) -> c_21() 26.59/6.94 , 20: !EQ^#(0(), S(y)) -> c_22() 26.59/6.94 , 21: !EQ^#(0(), 0()) -> c_23() 26.59/6.94 , 22: domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , 23: domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.94 26.59/6.94 We are left with following problem, upon which TcT provides the 26.59/6.94 certificate YES(O(1),O(n^1)). 26.59/6.94 26.59/6.94 Strict DPs: 26.59/6.94 { strmatch^#(patstr, str) -> c_1(domatch^#(patstr, str, Nil())) 26.59/6.94 , domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) 26.59/6.94 , domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.94 , domatch^#(Cons(x, xs), Nil(), n) -> c_13() } 26.59/6.94 Weak DPs: 26.59/6.94 { prefix^#(Nil(), cs) -> c_2() 26.59/6.94 , prefix^#(Cons(x, xs), Nil()) -> c_3() 26.59/6.94 , prefix^#(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 c_4(and^#(!EQ(x', x), prefix(xs', xs))) 26.59/6.94 , and^#(True(), True()) -> c_16() 26.59/6.94 , and^#(True(), False()) -> c_17() 26.59/6.94 , and^#(False(), True()) -> c_18() 26.59/6.94 , and^#(False(), False()) -> c_19() 26.59/6.94 , notEmpty^#(Nil()) -> c_5() 26.59/6.94 , notEmpty^#(Cons(x, xs)) -> c_6() 26.59/6.94 , eqNatList^#(Nil(), Nil()) -> c_7() 26.59/6.94 , eqNatList^#(Nil(), Cons(y, ys)) -> c_8() 26.59/6.94 , eqNatList^#(Cons(x, xs), Nil()) -> c_9() 26.59/6.94 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_10(!EQ^#(x, y)) 26.59/6.94 , !EQ^#(S(x), S(y)) -> c_20(!EQ^#(x, y)) 26.59/6.94 , !EQ^#(S(x), 0()) -> c_21() 26.59/6.94 , !EQ^#(0(), S(y)) -> c_22() 26.59/6.94 , !EQ^#(0(), 0()) -> c_23() 26.59/6.94 , domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.94 Weak Trs: 26.59/6.94 { prefix(Nil(), cs) -> True() 26.59/6.94 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.94 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.94 , and(True(), True()) -> True() 26.59/6.94 , and(True(), False()) -> False() 26.59/6.94 , and(False(), True()) -> False() 26.59/6.94 , and(False(), False()) -> False() 26.59/6.94 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.94 , !EQ(S(x), 0()) -> False() 26.59/6.94 , !EQ(0(), S(y)) -> False() 26.59/6.94 , !EQ(0(), 0()) -> True() } 26.59/6.94 Obligation: 26.59/6.94 innermost runtime complexity 26.59/6.94 Answer: 26.59/6.94 YES(O(1),O(n^1)) 26.59/6.94 26.59/6.94 The following weak DPs constitute a sub-graph of the DG that is 26.59/6.94 closed under successors. The DPs are removed. 26.59/6.94 26.59/6.94 { prefix^#(Nil(), cs) -> c_2() 26.59/6.94 , prefix^#(Cons(x, xs), Nil()) -> c_3() 26.59/6.94 , prefix^#(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 c_4(and^#(!EQ(x', x), prefix(xs', xs))) 26.59/6.94 , and^#(True(), True()) -> c_16() 26.59/6.94 , and^#(True(), False()) -> c_17() 26.59/6.94 , and^#(False(), True()) -> c_18() 26.59/6.94 , and^#(False(), False()) -> c_19() 26.59/6.94 , notEmpty^#(Nil()) -> c_5() 26.59/6.94 , notEmpty^#(Cons(x, xs)) -> c_6() 26.59/6.94 , eqNatList^#(Nil(), Nil()) -> c_7() 26.59/6.94 , eqNatList^#(Nil(), Cons(y, ys)) -> c_8() 26.59/6.94 , eqNatList^#(Cons(x, xs), Nil()) -> c_9() 26.59/6.94 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_10(!EQ^#(x, y)) 26.59/6.94 , !EQ^#(S(x), S(y)) -> c_20(!EQ^#(x, y)) 26.59/6.94 , !EQ^#(S(x), 0()) -> c_21() 26.59/6.94 , !EQ^#(0(), S(y)) -> c_22() 26.59/6.94 , !EQ^#(0(), 0()) -> c_23() } 26.59/6.94 26.59/6.94 We are left with following problem, upon which TcT provides the 26.59/6.94 certificate YES(O(1),O(n^1)). 26.59/6.94 26.59/6.94 Strict DPs: 26.59/6.94 { strmatch^#(patstr, str) -> c_1(domatch^#(patstr, str, Nil())) 26.59/6.94 , domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) 26.59/6.94 , domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.94 , domatch^#(Cons(x, xs), Nil(), n) -> c_13() } 26.59/6.94 Weak DPs: 26.59/6.94 { domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.94 Weak Trs: 26.59/6.94 { prefix(Nil(), cs) -> True() 26.59/6.94 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.94 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.94 , and(True(), True()) -> True() 26.59/6.94 , and(True(), False()) -> False() 26.59/6.94 , and(False(), True()) -> False() 26.59/6.94 , and(False(), False()) -> False() 26.59/6.94 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.94 , !EQ(S(x), 0()) -> False() 26.59/6.94 , !EQ(0(), S(y)) -> False() 26.59/6.94 , !EQ(0(), 0()) -> True() } 26.59/6.94 Obligation: 26.59/6.94 innermost runtime complexity 26.59/6.94 Answer: 26.59/6.94 YES(O(1),O(n^1)) 26.59/6.94 26.59/6.94 Consider the dependency graph 26.59/6.94 26.59/6.94 1: strmatch^#(patstr, str) -> c_1(domatch^#(patstr, str, Nil())) 26.59/6.94 -->_1 domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) :2 26.59/6.94 -->_1 domatch^#(Cons(x, xs), Nil(), n) -> c_13() :4 26.59/6.94 -->_1 domatch^#(Nil(), Nil(), n) -> c_12() :3 26.59/6.94 26.59/6.94 2: domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) 26.59/6.94 -->_1 domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) :6 26.59/6.94 -->_1 domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) :5 26.59/6.94 26.59/6.94 3: domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.94 26.59/6.94 4: domatch^#(Cons(x, xs), Nil(), n) -> c_13() 26.59/6.94 26.59/6.94 5: domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 -->_1 domatch^#(Cons(x, xs), Nil(), n) -> c_13() :4 26.59/6.94 -->_1 domatch^#(Nil(), Nil(), n) -> c_12() :3 26.59/6.94 -->_1 domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) :2 26.59/6.94 26.59/6.94 6: domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 -->_1 domatch^#(Cons(x, xs), Nil(), n) -> c_13() :4 26.59/6.94 -->_1 domatch^#(Nil(), Nil(), n) -> c_12() :3 26.59/6.94 -->_1 domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) :2 26.59/6.94 26.59/6.94 26.59/6.94 Following roots of the dependency graph are removed, as the 26.59/6.94 considered set of starting terms is closed under reduction with 26.59/6.94 respect to these rules (modulo compound contexts). 26.59/6.94 26.59/6.94 { strmatch^#(patstr, str) -> c_1(domatch^#(patstr, str, Nil())) } 26.59/6.94 26.59/6.94 26.59/6.94 We are left with following problem, upon which TcT provides the 26.59/6.94 certificate YES(O(1),O(n^1)). 26.59/6.94 26.59/6.94 Strict DPs: 26.59/6.94 { domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.94 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.94 patcs, 26.59/6.94 Cons(x, xs), 26.59/6.94 n)) 26.59/6.94 , domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.94 , domatch^#(Cons(x, xs), Nil(), n) -> c_13() } 26.59/6.94 Weak DPs: 26.59/6.94 { domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.94 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.94 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.94 Weak Trs: 26.59/6.94 { prefix(Nil(), cs) -> True() 26.59/6.94 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.94 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.94 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.94 , and(True(), True()) -> True() 26.59/6.94 , and(True(), False()) -> False() 26.59/6.94 , and(False(), True()) -> False() 26.59/6.94 , and(False(), False()) -> False() 26.59/6.94 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.94 , !EQ(S(x), 0()) -> False() 26.59/6.94 , !EQ(0(), S(y)) -> False() 26.59/6.94 , !EQ(0(), 0()) -> True() } 26.59/6.94 Obligation: 26.59/6.94 innermost runtime complexity 26.59/6.95 Answer: 26.59/6.95 YES(O(1),O(n^1)) 26.59/6.95 26.59/6.95 We use the processor 'matrix interpretation of dimension 1' to 26.59/6.95 orient following rules strictly. 26.59/6.95 26.59/6.95 DPs: 26.59/6.95 { 2: domatch^#(Nil(), Nil(), n) -> c_12() } 26.59/6.95 26.59/6.95 Sub-proof: 26.59/6.95 ---------- 26.59/6.95 The following argument positions are usable: 26.59/6.95 Uargs(c_11) = {1}, Uargs(c_14) = {1}, Uargs(c_15) = {1} 26.59/6.95 26.59/6.95 TcT has computed the following constructor-based matrix 26.59/6.95 interpretation satisfying not(EDA). 26.59/6.95 26.59/6.95 [True] = [0] 26.59/6.95 26.59/6.95 [prefix](x1, x2) = [0] 26.59/6.95 26.59/6.95 [Nil] = [2] 26.59/6.95 26.59/6.95 [and](x1, x2) = [0] 26.59/6.95 26.59/6.95 [!EQ](x1, x2) = [0] 26.59/6.95 26.59/6.95 [S](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 [Cons](x1, x2) = [0] 26.59/6.95 26.59/6.95 [0] = [0] 26.59/6.95 26.59/6.95 [False] = [0] 26.59/6.95 26.59/6.95 [domatch^#](x1, x2, x3) = [4] x1 + [0] 26.59/6.95 26.59/6.95 [c_11](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 [domatch[Ite][True][Ite]^#](x1, x2, x3, x4) = [4] x2 + [0] 26.59/6.95 26.59/6.95 [c_12] = [6] 26.59/6.95 26.59/6.95 [c_13] = [0] 26.59/6.95 26.59/6.95 [c_14](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 [c_15](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 The order satisfies the following ordering constraints: 26.59/6.95 26.59/6.95 [prefix(Nil(), cs)] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [True()] 26.59/6.95 26.59/6.95 [prefix(Cons(x, xs), Nil())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [prefix(Cons(x', xs'), Cons(x, xs))] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [and(!EQ(x', x), prefix(xs', xs))] 26.59/6.95 26.59/6.95 [and(True(), True())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [True()] 26.59/6.95 26.59/6.95 [and(True(), False())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [and(False(), True())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [and(False(), False())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [!EQ(S(x), S(y))] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [!EQ(x, y)] 26.59/6.95 26.59/6.95 [!EQ(S(x), 0())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [!EQ(0(), S(y))] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [!EQ(0(), 0())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [True()] 26.59/6.95 26.59/6.95 [domatch^#(patcs, Cons(x, xs), n)] = [4] patcs + [0] 26.59/6.95 >= [4] patcs + [0] 26.59/6.95 = [c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n))] 26.59/6.95 26.59/6.95 [domatch^#(Nil(), Nil(), n)] = [8] 26.59/6.95 > [6] 26.59/6.95 = [c_12()] 26.59/6.95 26.59/6.95 [domatch^#(Cons(x, xs), Nil(), n)] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [c_13()] 26.59/6.95 26.59/6.95 [domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n)] = [4] patcs + [0] 26.59/6.95 >= [4] patcs + [0] 26.59/6.95 = [c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil()))))] 26.59/6.95 26.59/6.95 [domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n)] = [4] patcs + [0] 26.59/6.95 >= [4] patcs + [0] 26.59/6.95 = [c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil()))))] 26.59/6.95 26.59/6.95 26.59/6.95 The strictly oriented rules are moved into the weak component. 26.59/6.95 26.59/6.95 We are left with following problem, upon which TcT provides the 26.59/6.95 certificate YES(O(1),O(n^1)). 26.59/6.95 26.59/6.95 Strict DPs: 26.59/6.95 { domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.95 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n)) 26.59/6.95 , domatch^#(Cons(x, xs), Nil(), n) -> c_13() } 26.59/6.95 Weak DPs: 26.59/6.95 { domatch^#(Nil(), Nil(), n) -> c_12() 26.59/6.95 , domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.95 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.95 Weak Trs: 26.59/6.95 { prefix(Nil(), cs) -> True() 26.59/6.95 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.95 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.95 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.95 , and(True(), True()) -> True() 26.59/6.95 , and(True(), False()) -> False() 26.59/6.95 , and(False(), True()) -> False() 26.59/6.95 , and(False(), False()) -> False() 26.59/6.95 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.95 , !EQ(S(x), 0()) -> False() 26.59/6.95 , !EQ(0(), S(y)) -> False() 26.59/6.95 , !EQ(0(), 0()) -> True() } 26.59/6.95 Obligation: 26.59/6.95 innermost runtime complexity 26.59/6.95 Answer: 26.59/6.95 YES(O(1),O(n^1)) 26.59/6.95 26.59/6.95 The following weak DPs constitute a sub-graph of the DG that is 26.59/6.95 closed under successors. The DPs are removed. 26.59/6.95 26.59/6.95 { domatch^#(Nil(), Nil(), n) -> c_12() } 26.59/6.95 26.59/6.95 We are left with following problem, upon which TcT provides the 26.59/6.95 certificate YES(O(1),O(n^1)). 26.59/6.95 26.59/6.95 Strict DPs: 26.59/6.95 { domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.95 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n)) 26.59/6.95 , domatch^#(Cons(x, xs), Nil(), n) -> c_13() } 26.59/6.95 Weak DPs: 26.59/6.95 { domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.95 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.95 Weak Trs: 26.59/6.95 { prefix(Nil(), cs) -> True() 26.59/6.95 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.95 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.95 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.95 , and(True(), True()) -> True() 26.59/6.95 , and(True(), False()) -> False() 26.59/6.95 , and(False(), True()) -> False() 26.59/6.95 , and(False(), False()) -> False() 26.59/6.95 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.95 , !EQ(S(x), 0()) -> False() 26.59/6.95 , !EQ(0(), S(y)) -> False() 26.59/6.95 , !EQ(0(), 0()) -> True() } 26.59/6.95 Obligation: 26.59/6.95 innermost runtime complexity 26.59/6.95 Answer: 26.59/6.95 YES(O(1),O(n^1)) 26.59/6.95 26.59/6.95 We use the processor 'matrix interpretation of dimension 1' to 26.59/6.95 orient following rules strictly. 26.59/6.95 26.59/6.95 DPs: 26.59/6.95 { 2: domatch^#(Cons(x, xs), Nil(), n) -> c_13() } 26.59/6.95 26.59/6.95 Sub-proof: 26.59/6.95 ---------- 26.59/6.95 The following argument positions are usable: 26.59/6.95 Uargs(c_11) = {1}, Uargs(c_14) = {1}, Uargs(c_15) = {1} 26.59/6.95 26.59/6.95 TcT has computed the following constructor-restricted matrix 26.59/6.95 interpretation. Note that the diagonal of the component-wise maxima 26.59/6.95 of interpretation-entries (of constructors) contains no more than 0 26.59/6.95 non-zero entries. 26.59/6.95 26.59/6.95 [True] = [0] 26.59/6.95 26.59/6.95 [prefix](x1, x2) = [0] 26.59/6.95 26.59/6.95 [Nil] = [0] 26.59/6.95 26.59/6.95 [and](x1, x2) = [0] 26.59/6.95 26.59/6.95 [!EQ](x1, x2) = [0] 26.59/6.95 26.59/6.95 [S](x1) = [0] 26.59/6.95 26.59/6.95 [Cons](x1, x2) = [2] 26.59/6.95 26.59/6.95 [0] = [0] 26.59/6.95 26.59/6.95 [False] = [0] 26.59/6.95 26.59/6.95 [domatch^#](x1, x2, x3) = [4] x1 + [0] 26.59/6.95 26.59/6.95 [c_11](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 [domatch[Ite][True][Ite]^#](x1, x2, x3, x4) = [4] x2 + [0] 26.59/6.95 26.59/6.95 [c_12] = [0] 26.59/6.95 26.59/6.95 [c_13] = [6] 26.59/6.95 26.59/6.95 [c_14](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 [c_15](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 The order satisfies the following ordering constraints: 26.59/6.95 26.59/6.95 [prefix(Nil(), cs)] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [True()] 26.59/6.95 26.59/6.95 [prefix(Cons(x, xs), Nil())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [prefix(Cons(x', xs'), Cons(x, xs))] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [and(!EQ(x', x), prefix(xs', xs))] 26.59/6.95 26.59/6.95 [and(True(), True())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [True()] 26.59/6.95 26.59/6.95 [and(True(), False())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [and(False(), True())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [and(False(), False())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [!EQ(S(x), S(y))] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [!EQ(x, y)] 26.59/6.95 26.59/6.95 [!EQ(S(x), 0())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [!EQ(0(), S(y))] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [!EQ(0(), 0())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [True()] 26.59/6.95 26.59/6.95 [domatch^#(patcs, Cons(x, xs), n)] = [4] patcs + [0] 26.59/6.95 >= [4] patcs + [0] 26.59/6.95 = [c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n))] 26.59/6.95 26.59/6.95 [domatch^#(Cons(x, xs), Nil(), n)] = [8] 26.59/6.95 > [6] 26.59/6.95 = [c_13()] 26.59/6.95 26.59/6.95 [domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n)] = [4] patcs + [0] 26.59/6.95 >= [4] patcs + [0] 26.59/6.95 = [c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil()))))] 26.59/6.95 26.59/6.95 [domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n)] = [4] patcs + [0] 26.59/6.95 >= [4] patcs + [0] 26.59/6.95 = [c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil()))))] 26.59/6.95 26.59/6.95 26.59/6.95 The strictly oriented rules are moved into the weak component. 26.59/6.95 26.59/6.95 We are left with following problem, upon which TcT provides the 26.59/6.95 certificate YES(O(1),O(n^1)). 26.59/6.95 26.59/6.95 Strict DPs: 26.59/6.95 { domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.95 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n)) } 26.59/6.95 Weak DPs: 26.59/6.95 { domatch^#(Cons(x, xs), Nil(), n) -> c_13() 26.59/6.95 , domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.95 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.95 Weak Trs: 26.59/6.95 { prefix(Nil(), cs) -> True() 26.59/6.95 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.95 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.95 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.95 , and(True(), True()) -> True() 26.59/6.95 , and(True(), False()) -> False() 26.59/6.95 , and(False(), True()) -> False() 26.59/6.95 , and(False(), False()) -> False() 26.59/6.95 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.95 , !EQ(S(x), 0()) -> False() 26.59/6.95 , !EQ(0(), S(y)) -> False() 26.59/6.95 , !EQ(0(), 0()) -> True() } 26.59/6.95 Obligation: 26.59/6.95 innermost runtime complexity 26.59/6.95 Answer: 26.59/6.95 YES(O(1),O(n^1)) 26.59/6.95 26.59/6.95 The following weak DPs constitute a sub-graph of the DG that is 26.59/6.95 closed under successors. The DPs are removed. 26.59/6.95 26.59/6.95 { domatch^#(Cons(x, xs), Nil(), n) -> c_13() } 26.59/6.95 26.59/6.95 We are left with following problem, upon which TcT provides the 26.59/6.95 certificate YES(O(1),O(n^1)). 26.59/6.95 26.59/6.95 Strict DPs: 26.59/6.95 { domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.95 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n)) } 26.59/6.95 Weak DPs: 26.59/6.95 { domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.95 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.95 Weak Trs: 26.59/6.95 { prefix(Nil(), cs) -> True() 26.59/6.95 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.95 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.95 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.95 , and(True(), True()) -> True() 26.59/6.95 , and(True(), False()) -> False() 26.59/6.95 , and(False(), True()) -> False() 26.59/6.95 , and(False(), False()) -> False() 26.59/6.95 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.95 , !EQ(S(x), 0()) -> False() 26.59/6.95 , !EQ(0(), S(y)) -> False() 26.59/6.95 , !EQ(0(), 0()) -> True() } 26.59/6.95 Obligation: 26.59/6.95 innermost runtime complexity 26.59/6.95 Answer: 26.59/6.95 YES(O(1),O(n^1)) 26.59/6.95 26.59/6.95 We use the processor 'matrix interpretation of dimension 1' to 26.59/6.95 orient following rules strictly. 26.59/6.95 26.59/6.95 DPs: 26.59/6.95 { 2: domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.95 , 3: domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.95 26.59/6.95 Sub-proof: 26.59/6.95 ---------- 26.59/6.95 The following argument positions are usable: 26.59/6.95 Uargs(c_11) = {1}, Uargs(c_14) = {1}, Uargs(c_15) = {1} 26.59/6.95 26.59/6.95 TcT has computed the following constructor-based matrix 26.59/6.95 interpretation satisfying not(EDA). 26.59/6.95 26.59/6.95 [True] = [0] 26.59/6.95 26.59/6.95 [prefix](x1, x2) = [0] 26.59/6.95 26.59/6.95 [Nil] = [0] 26.59/6.95 26.59/6.95 [and](x1, x2) = [0] 26.59/6.95 26.59/6.95 [!EQ](x1, x2) = [0] 26.59/6.95 26.59/6.95 [S](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 [Cons](x1, x2) = [1] x2 + [1] 26.59/6.95 26.59/6.95 [0] = [0] 26.59/6.95 26.59/6.95 [False] = [0] 26.59/6.95 26.59/6.95 [domatch^#](x1, x2, x3) = [1] x2 + [0] 26.59/6.95 26.59/6.95 [c_11](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 [domatch[Ite][True][Ite]^#](x1, x2, x3, x4) = [1] x3 + [0] 26.59/6.95 26.59/6.95 [c_12] = [0] 26.59/6.95 26.59/6.95 [c_13] = [0] 26.59/6.95 26.59/6.95 [c_14](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 [c_15](x1) = [1] x1 + [0] 26.59/6.95 26.59/6.95 The order satisfies the following ordering constraints: 26.59/6.95 26.59/6.95 [prefix(Nil(), cs)] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [True()] 26.59/6.95 26.59/6.95 [prefix(Cons(x, xs), Nil())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [prefix(Cons(x', xs'), Cons(x, xs))] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [and(!EQ(x', x), prefix(xs', xs))] 26.59/6.95 26.59/6.95 [and(True(), True())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [True()] 26.59/6.95 26.59/6.95 [and(True(), False())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [and(False(), True())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [and(False(), False())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [!EQ(S(x), S(y))] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [!EQ(x, y)] 26.59/6.95 26.59/6.95 [!EQ(S(x), 0())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [!EQ(0(), S(y))] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [False()] 26.59/6.95 26.59/6.95 [!EQ(0(), 0())] = [0] 26.59/6.95 >= [0] 26.59/6.95 = [True()] 26.59/6.95 26.59/6.95 [domatch^#(patcs, Cons(x, xs), n)] = [1] xs + [1] 26.59/6.95 >= [1] xs + [1] 26.59/6.95 = [c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n))] 26.59/6.95 26.59/6.95 [domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n)] = [1] xs + [1] 26.59/6.95 > [1] xs + [0] 26.59/6.95 = [c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil()))))] 26.59/6.95 26.59/6.95 [domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n)] = [1] xs + [1] 26.59/6.95 > [1] xs + [0] 26.59/6.95 = [c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil()))))] 26.59/6.95 26.59/6.95 26.59/6.95 We return to the main proof. Consider the set of all dependency 26.59/6.95 pairs 26.59/6.95 26.59/6.95 : 26.59/6.95 { 1: domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.95 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n)) 26.59/6.95 , 2: domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.95 , 3: domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.95 26.59/6.95 Processor 'matrix interpretation of dimension 1' induces the 26.59/6.95 complexity certificate YES(?,O(n^1)) on application of dependency 26.59/6.95 pairs {2,3}. These cover all (indirect) predecessors of dependency 26.59/6.95 pairs {1,2,3}, their number of application is equally bounded. The 26.59/6.95 dependency pairs are shifted into the weak component. 26.59/6.95 26.59/6.95 We are left with following problem, upon which TcT provides the 26.59/6.95 certificate YES(O(1),O(1)). 26.59/6.95 26.59/6.95 Weak DPs: 26.59/6.95 { domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.95 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n)) 26.59/6.95 , domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.95 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.95 Weak Trs: 26.59/6.95 { prefix(Nil(), cs) -> True() 26.59/6.95 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.95 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.95 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.95 , and(True(), True()) -> True() 26.59/6.95 , and(True(), False()) -> False() 26.59/6.95 , and(False(), True()) -> False() 26.59/6.95 , and(False(), False()) -> False() 26.59/6.95 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.95 , !EQ(S(x), 0()) -> False() 26.59/6.95 , !EQ(0(), S(y)) -> False() 26.59/6.95 , !EQ(0(), 0()) -> True() } 26.59/6.95 Obligation: 26.59/6.95 innermost runtime complexity 26.59/6.95 Answer: 26.59/6.95 YES(O(1),O(1)) 26.59/6.95 26.59/6.95 The following weak DPs constitute a sub-graph of the DG that is 26.59/6.95 closed under successors. The DPs are removed. 26.59/6.95 26.59/6.95 { domatch^#(patcs, Cons(x, xs), n) -> 26.59/6.95 c_11(domatch[Ite][True][Ite]^#(prefix(patcs, Cons(x, xs)), 26.59/6.95 patcs, 26.59/6.95 Cons(x, xs), 26.59/6.95 n)) 26.59/6.95 , domatch[Ite][True][Ite]^#(True(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_14(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) 26.59/6.95 , domatch[Ite][True][Ite]^#(False(), patcs, Cons(x, xs), n) -> 26.59/6.95 c_15(domatch^#(patcs, xs, Cons(n, Cons(Nil(), Nil())))) } 26.59/6.95 26.59/6.95 We are left with following problem, upon which TcT provides the 26.59/6.95 certificate YES(O(1),O(1)). 26.59/6.95 26.59/6.95 Weak Trs: 26.59/6.95 { prefix(Nil(), cs) -> True() 26.59/6.95 , prefix(Cons(x, xs), Nil()) -> False() 26.59/6.95 , prefix(Cons(x', xs'), Cons(x, xs)) -> 26.59/6.95 and(!EQ(x', x), prefix(xs', xs)) 26.59/6.95 , and(True(), True()) -> True() 26.59/6.95 , and(True(), False()) -> False() 26.59/6.95 , and(False(), True()) -> False() 26.59/6.95 , and(False(), False()) -> False() 26.59/6.95 , !EQ(S(x), S(y)) -> !EQ(x, y) 26.59/6.95 , !EQ(S(x), 0()) -> False() 26.59/6.95 , !EQ(0(), S(y)) -> False() 26.59/6.95 , !EQ(0(), 0()) -> True() } 26.59/6.95 Obligation: 26.59/6.95 innermost runtime complexity 26.59/6.95 Answer: 26.59/6.95 YES(O(1),O(1)) 26.59/6.95 26.59/6.95 No rule is usable, rules are removed from the input problem. 26.59/6.95 26.59/6.95 We are left with following problem, upon which TcT provides the 26.59/6.95 certificate YES(O(1),O(1)). 26.59/6.95 26.59/6.95 Rules: Empty 26.59/6.95 Obligation: 26.59/6.95 innermost runtime complexity 26.59/6.95 Answer: 26.59/6.95 YES(O(1),O(1)) 26.59/6.95 26.59/6.95 Empty rules are trivially bounded 26.59/6.95 26.59/6.95 Hurray, we answered YES(O(1),O(n^2)) 26.59/6.95 EOF