MAYBE 168.50/78.10 MAYBE 168.50/78.10 168.50/78.10 We are left with following problem, upon which TcT provides the 168.50/78.10 certificate MAYBE. 168.50/78.10 168.50/78.10 Strict Trs: 168.50/78.10 { subsets(Cons(x, xs)) -> 168.50/78.10 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.50/78.10 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.50/78.10 , mapconsapp(x', Cons(x, xs), rest) -> 168.50/78.10 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.50/78.10 , mapconsapp(x, Nil(), rest) -> rest 168.50/78.10 , notEmpty(Cons(x, xs)) -> True() 168.50/78.10 , notEmpty(Nil()) -> False() 168.50/78.10 , goal(xs) -> subsets(xs) } 168.50/78.10 Weak Trs: 168.50/78.10 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.50/78.10 mapconsapp(x, subs, subs) } 168.50/78.10 Obligation: 168.50/78.10 innermost runtime complexity 168.50/78.10 Answer: 168.50/78.10 MAYBE 168.50/78.10 168.50/78.10 None of the processors succeeded. 168.50/78.10 168.50/78.10 Details of failed attempt(s): 168.50/78.10 ----------------------------- 168.50/78.10 1) 'empty' failed due to the following reason: 168.50/78.10 168.50/78.10 Empty strict component of the problem is NOT empty. 168.50/78.10 168.50/78.10 2) 'Best' failed due to the following reason: 168.50/78.10 168.50/78.10 None of the processors succeeded. 168.50/78.10 168.50/78.10 Details of failed attempt(s): 168.50/78.10 ----------------------------- 168.50/78.10 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 168.50/78.10 following reason: 168.50/78.10 168.50/78.10 We add the following dependency tuples: 168.50/78.10 168.50/78.10 Strict DPs: 168.50/78.10 { subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) 168.50/78.10 , subsets^#(Nil()) -> c_2() 168.50/78.10 , mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) 168.50/78.10 , mapconsapp^#(x, Nil(), rest) -> c_4() 168.50/78.10 , notEmpty^#(Cons(x, xs)) -> c_5() 168.50/78.10 , notEmpty^#(Nil()) -> c_6() 168.50/78.10 , goal^#(xs) -> c_7(subsets^#(xs)) } 168.50/78.10 Weak DPs: 168.50/78.10 { subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.50/78.10 c_8(mapconsapp^#(x, subs, subs)) } 168.50/78.10 168.50/78.10 and mark the set of starting terms. 168.50/78.10 168.50/78.10 We are left with following problem, upon which TcT provides the 168.50/78.10 certificate MAYBE. 168.50/78.10 168.50/78.10 Strict DPs: 168.50/78.10 { subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) 168.50/78.10 , subsets^#(Nil()) -> c_2() 168.50/78.10 , mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) 168.50/78.10 , mapconsapp^#(x, Nil(), rest) -> c_4() 168.50/78.10 , notEmpty^#(Cons(x, xs)) -> c_5() 168.50/78.10 , notEmpty^#(Nil()) -> c_6() 168.50/78.10 , goal^#(xs) -> c_7(subsets^#(xs)) } 168.50/78.10 Weak DPs: 168.50/78.10 { subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.50/78.10 c_8(mapconsapp^#(x, subs, subs)) } 168.50/78.10 Weak Trs: 168.50/78.10 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.50/78.10 mapconsapp(x, subs, subs) 168.50/78.10 , subsets(Cons(x, xs)) -> 168.50/78.10 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.50/78.10 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.50/78.10 , mapconsapp(x', Cons(x, xs), rest) -> 168.50/78.10 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.50/78.10 , mapconsapp(x, Nil(), rest) -> rest 168.50/78.10 , notEmpty(Cons(x, xs)) -> True() 168.50/78.10 , notEmpty(Nil()) -> False() 168.50/78.10 , goal(xs) -> subsets(xs) } 168.50/78.10 Obligation: 168.50/78.10 innermost runtime complexity 168.50/78.10 Answer: 168.50/78.10 MAYBE 168.50/78.10 168.50/78.10 We estimate the number of application of {2,5,6} by applications of 168.50/78.10 Pre({2,5,6}) = {1,7}. Here rules are labeled as follows: 168.50/78.10 168.50/78.10 DPs: 168.50/78.10 { 1: subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) 168.50/78.10 , 2: subsets^#(Nil()) -> c_2() 168.50/78.10 , 3: mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) 168.50/78.10 , 4: mapconsapp^#(x, Nil(), rest) -> c_4() 168.50/78.10 , 5: notEmpty^#(Cons(x, xs)) -> c_5() 168.50/78.10 , 6: notEmpty^#(Nil()) -> c_6() 168.50/78.10 , 7: goal^#(xs) -> c_7(subsets^#(xs)) 168.50/78.10 , 8: subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.50/78.10 c_8(mapconsapp^#(x, subs, subs)) } 168.50/78.10 168.50/78.10 We are left with following problem, upon which TcT provides the 168.50/78.10 certificate MAYBE. 168.50/78.10 168.50/78.10 Strict DPs: 168.50/78.10 { subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) 168.50/78.10 , mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) 168.50/78.10 , mapconsapp^#(x, Nil(), rest) -> c_4() 168.50/78.10 , goal^#(xs) -> c_7(subsets^#(xs)) } 168.50/78.10 Weak DPs: 168.50/78.10 { subsets^#(Nil()) -> c_2() 168.50/78.10 , subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.50/78.10 c_8(mapconsapp^#(x, subs, subs)) 168.50/78.10 , notEmpty^#(Cons(x, xs)) -> c_5() 168.50/78.10 , notEmpty^#(Nil()) -> c_6() } 168.50/78.10 Weak Trs: 168.50/78.10 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.50/78.10 mapconsapp(x, subs, subs) 168.50/78.10 , subsets(Cons(x, xs)) -> 168.50/78.10 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.50/78.10 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.50/78.10 , mapconsapp(x', Cons(x, xs), rest) -> 168.50/78.10 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.50/78.10 , mapconsapp(x, Nil(), rest) -> rest 168.50/78.10 , notEmpty(Cons(x, xs)) -> True() 168.50/78.10 , notEmpty(Nil()) -> False() 168.50/78.10 , goal(xs) -> subsets(xs) } 168.50/78.10 Obligation: 168.50/78.10 innermost runtime complexity 168.50/78.10 Answer: 168.50/78.10 MAYBE 168.50/78.10 168.50/78.10 The following weak DPs constitute a sub-graph of the DG that is 168.50/78.10 closed under successors. The DPs are removed. 168.50/78.10 168.50/78.10 { subsets^#(Nil()) -> c_2() 168.50/78.10 , notEmpty^#(Cons(x, xs)) -> c_5() 168.50/78.10 , notEmpty^#(Nil()) -> c_6() } 168.50/78.10 168.50/78.10 We are left with following problem, upon which TcT provides the 168.50/78.10 certificate MAYBE. 168.50/78.10 168.50/78.10 Strict DPs: 168.50/78.10 { subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) 168.50/78.10 , mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) 168.50/78.10 , mapconsapp^#(x, Nil(), rest) -> c_4() 168.50/78.10 , goal^#(xs) -> c_7(subsets^#(xs)) } 168.50/78.10 Weak DPs: 168.50/78.10 { subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.50/78.10 c_8(mapconsapp^#(x, subs, subs)) } 168.50/78.10 Weak Trs: 168.50/78.10 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.50/78.10 mapconsapp(x, subs, subs) 168.50/78.10 , subsets(Cons(x, xs)) -> 168.50/78.10 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.50/78.10 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.50/78.10 , mapconsapp(x', Cons(x, xs), rest) -> 168.50/78.10 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.50/78.10 , mapconsapp(x, Nil(), rest) -> rest 168.50/78.10 , notEmpty(Cons(x, xs)) -> True() 168.50/78.10 , notEmpty(Nil()) -> False() 168.50/78.10 , goal(xs) -> subsets(xs) } 168.50/78.10 Obligation: 168.50/78.10 innermost runtime complexity 168.50/78.10 Answer: 168.50/78.10 MAYBE 168.50/78.10 168.50/78.10 Consider the dependency graph 168.50/78.10 168.50/78.10 1: subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) 168.50/78.10 -->_1 subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.50/78.10 c_8(mapconsapp^#(x, subs, subs)) :5 168.50/78.10 -->_2 subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) :1 168.50/78.10 168.50/78.10 2: mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) 168.50/78.10 -->_1 mapconsapp^#(x, Nil(), rest) -> c_4() :3 168.50/78.10 -->_1 mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) :2 168.50/78.10 168.50/78.10 3: mapconsapp^#(x, Nil(), rest) -> c_4() 168.50/78.10 168.50/78.10 4: goal^#(xs) -> c_7(subsets^#(xs)) 168.50/78.10 -->_1 subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) :1 168.50/78.10 168.50/78.10 5: subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.50/78.10 c_8(mapconsapp^#(x, subs, subs)) 168.50/78.10 -->_1 mapconsapp^#(x, Nil(), rest) -> c_4() :3 168.50/78.10 -->_1 mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) :2 168.50/78.10 168.50/78.10 168.50/78.10 Following roots of the dependency graph are removed, as the 168.50/78.10 considered set of starting terms is closed under reduction with 168.50/78.10 respect to these rules (modulo compound contexts). 168.50/78.10 168.50/78.10 { goal^#(xs) -> c_7(subsets^#(xs)) } 168.50/78.10 168.50/78.10 168.50/78.10 We are left with following problem, upon which TcT provides the 168.50/78.10 certificate MAYBE. 168.50/78.10 168.50/78.10 Strict DPs: 168.50/78.10 { subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) 168.50/78.10 , mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) 168.50/78.10 , mapconsapp^#(x, Nil(), rest) -> c_4() } 168.50/78.10 Weak DPs: 168.50/78.10 { subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.50/78.10 c_8(mapconsapp^#(x, subs, subs)) } 168.50/78.10 Weak Trs: 168.50/78.10 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.50/78.10 mapconsapp(x, subs, subs) 168.50/78.10 , subsets(Cons(x, xs)) -> 168.50/78.10 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.50/78.10 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.50/78.10 , mapconsapp(x', Cons(x, xs), rest) -> 168.50/78.10 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.50/78.10 , mapconsapp(x, Nil(), rest) -> rest 168.50/78.10 , notEmpty(Cons(x, xs)) -> True() 168.50/78.10 , notEmpty(Nil()) -> False() 168.50/78.10 , goal(xs) -> subsets(xs) } 168.50/78.10 Obligation: 168.50/78.10 innermost runtime complexity 168.50/78.10 Answer: 168.50/78.10 MAYBE 168.50/78.10 168.50/78.10 We replace rewrite rules by usable rules: 168.50/78.10 168.50/78.10 Weak Usable Rules: 168.50/78.10 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.50/78.10 mapconsapp(x, subs, subs) 168.50/78.10 , subsets(Cons(x, xs)) -> 168.50/78.10 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.50/78.10 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.50/78.10 , mapconsapp(x', Cons(x, xs), rest) -> 168.50/78.10 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.50/78.10 , mapconsapp(x, Nil(), rest) -> rest } 168.50/78.10 168.50/78.10 We are left with following problem, upon which TcT provides the 168.50/78.10 certificate MAYBE. 168.50/78.10 168.50/78.10 Strict DPs: 168.50/78.10 { subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) 168.50/78.10 , mapconsapp^#(x', Cons(x, xs), rest) -> 168.50/78.10 c_3(mapconsapp^#(x', xs, rest)) 168.50/78.10 , mapconsapp^#(x, Nil(), rest) -> c_4() } 168.50/78.10 Weak DPs: 168.50/78.10 { subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.50/78.10 c_8(mapconsapp^#(x, subs, subs)) } 168.50/78.10 Weak Trs: 168.50/78.10 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.50/78.10 mapconsapp(x, subs, subs) 168.50/78.10 , subsets(Cons(x, xs)) -> 168.50/78.10 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.50/78.10 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.50/78.10 , mapconsapp(x', Cons(x, xs), rest) -> 168.50/78.10 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.50/78.10 , mapconsapp(x, Nil(), rest) -> rest } 168.50/78.10 Obligation: 168.50/78.10 innermost runtime complexity 168.50/78.10 Answer: 168.50/78.10 MAYBE 168.50/78.10 168.50/78.10 None of the processors succeeded. 168.50/78.10 168.50/78.10 Details of failed attempt(s): 168.50/78.10 ----------------------------- 168.50/78.10 1) 'empty' failed due to the following reason: 168.50/78.10 168.50/78.10 Empty strict component of the problem is NOT empty. 168.50/78.10 168.50/78.10 2) 'With Problem ...' failed due to the following reason: 168.50/78.10 168.50/78.10 We use the processor 'matrix interpretation of dimension 1' to 168.50/78.10 orient following rules strictly. 168.50/78.10 168.50/78.10 DPs: 168.50/78.10 { 1: subsets^#(Cons(x, xs)) -> 168.50/78.10 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs)) 168.50/78.10 , 3: mapconsapp^#(x, Nil(), rest) -> c_4() } 168.50/78.10 168.50/78.10 Sub-proof: 168.50/78.10 ---------- 168.50/78.10 The following argument positions are usable: 168.50/78.10 Uargs(c_1) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_8) = {1} 168.50/78.10 168.50/78.10 TcT has computed the following constructor-based matrix 168.50/78.10 interpretation satisfying not(EDA). 168.50/78.10 168.50/78.10 [subsets[Ite][True][Let]](x1, x2) = [0] 168.50/78.10 168.50/78.10 [subsets](x1) = [0] 168.50/78.10 168.50/78.10 [Cons](x1, x2) = [1] x2 + [1] 168.50/78.10 168.50/78.10 [Nil] = [0] 168.50/78.10 168.50/78.10 [mapconsapp](x1, x2, x3) = [4] x1 + [1] x3 + [0] 168.50/78.10 168.50/78.10 [subsets^#](x1) = [6] x1 + [2] 168.50/78.10 168.50/78.10 [c_1](x1, x2) = [4] x1 + [1] x2 + [1] 168.50/78.10 168.50/78.10 [subsets[Ite][True][Let]^#](x1, x2) = [1] 168.50/78.10 168.50/78.10 [mapconsapp^#](x1, x2, x3) = [1] 168.50/78.10 168.50/78.10 [c_3](x1) = [1] x1 + [0] 168.50/78.10 168.50/78.10 [c_4] = [0] 168.50/78.10 168.50/78.10 [c_8](x1) = [1] x1 + [0] 168.50/78.10 168.50/78.10 The order satisfies the following ordering constraints: 168.50/78.10 168.50/78.10 [subsets[Ite][True][Let](Cons(x, xs), subs)] = [0] 168.50/78.10 ? [4] x + [1] subs + [0] 168.50/78.10 = [mapconsapp(x, subs, subs)] 168.50/78.10 168.50/78.10 [subsets(Cons(x, xs))] = [0] 168.50/78.10 >= [0] 168.50/78.10 = [subsets[Ite][True][Let](Cons(x, xs), subsets(xs))] 168.50/78.10 168.50/78.10 [subsets(Nil())] = [0] 168.50/78.10 ? [1] 168.50/78.10 = [Cons(Nil(), Nil())] 168.50/78.10 168.50/78.10 [mapconsapp(x', Cons(x, xs), rest)] = [4] x' + [1] rest + [0] 168.50/78.10 ? [4] x' + [1] rest + [1] 168.50/78.10 = [Cons(Cons(x', x), mapconsapp(x', xs, rest))] 168.50/78.10 168.50/78.10 [mapconsapp(x, Nil(), rest)] = [4] x + [1] rest + [0] 168.50/78.10 >= [1] rest + [0] 168.50/78.10 = [rest] 168.50/78.10 168.50/78.10 [subsets^#(Cons(x, xs))] = [6] xs + [8] 168.50/78.10 > [6] xs + [7] 168.50/78.10 = [c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.50/78.10 subsets^#(xs))] 168.71/78.11 168.71/78.11 [subsets[Ite][True][Let]^#(Cons(x, xs), subs)] = [1] 168.71/78.11 >= [1] 168.71/78.11 = [c_8(mapconsapp^#(x, subs, subs))] 168.71/78.11 168.71/78.11 [mapconsapp^#(x', Cons(x, xs), rest)] = [1] 168.71/78.11 >= [1] 168.71/78.11 = [c_3(mapconsapp^#(x', xs, rest))] 168.71/78.11 168.71/78.11 [mapconsapp^#(x, Nil(), rest)] = [1] 168.71/78.11 > [0] 168.71/78.11 = [c_4()] 168.71/78.11 168.71/78.11 168.71/78.11 We return to the main proof. Consider the set of all dependency 168.71/78.11 pairs 168.71/78.11 168.71/78.11 : 168.71/78.11 { 1: subsets^#(Cons(x, xs)) -> 168.71/78.11 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.71/78.11 subsets^#(xs)) 168.71/78.11 , 2: mapconsapp^#(x', Cons(x, xs), rest) -> 168.71/78.11 c_3(mapconsapp^#(x', xs, rest)) 168.71/78.11 , 3: mapconsapp^#(x, Nil(), rest) -> c_4() 168.71/78.11 , 4: subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.71/78.11 c_8(mapconsapp^#(x, subs, subs)) } 168.71/78.11 168.71/78.11 Processor 'matrix interpretation of dimension 1' induces the 168.71/78.11 complexity certificate YES(?,O(n^1)) on application of dependency 168.71/78.11 pairs {1,3}. These cover all (indirect) predecessors of dependency 168.71/78.11 pairs {1,3,4}, their number of application is equally bounded. The 168.71/78.11 dependency pairs are shifted into the weak component. 168.71/78.11 168.71/78.11 We are left with following problem, upon which TcT provides the 168.71/78.11 certificate MAYBE. 168.71/78.11 168.71/78.11 Strict DPs: 168.71/78.11 { mapconsapp^#(x', Cons(x, xs), rest) -> 168.71/78.11 c_3(mapconsapp^#(x', xs, rest)) } 168.71/78.11 Weak DPs: 168.71/78.11 { subsets^#(Cons(x, xs)) -> 168.71/78.11 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.71/78.11 subsets^#(xs)) 168.71/78.11 , subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.71/78.11 c_8(mapconsapp^#(x, subs, subs)) 168.71/78.11 , mapconsapp^#(x, Nil(), rest) -> c_4() } 168.71/78.11 Weak Trs: 168.71/78.11 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.11 mapconsapp(x, subs, subs) 168.71/78.11 , subsets(Cons(x, xs)) -> 168.71/78.11 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.11 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.11 , mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.11 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.71/78.11 , mapconsapp(x, Nil(), rest) -> rest } 168.71/78.11 Obligation: 168.71/78.11 innermost runtime complexity 168.71/78.11 Answer: 168.71/78.11 MAYBE 168.71/78.11 168.71/78.11 The following weak DPs constitute a sub-graph of the DG that is 168.71/78.11 closed under successors. The DPs are removed. 168.71/78.11 168.71/78.11 { mapconsapp^#(x, Nil(), rest) -> c_4() } 168.71/78.11 168.71/78.11 We are left with following problem, upon which TcT provides the 168.71/78.11 certificate MAYBE. 168.71/78.11 168.71/78.11 Strict DPs: 168.71/78.11 { mapconsapp^#(x', Cons(x, xs), rest) -> 168.71/78.11 c_3(mapconsapp^#(x', xs, rest)) } 168.71/78.11 Weak DPs: 168.71/78.11 { subsets^#(Cons(x, xs)) -> 168.71/78.11 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.71/78.11 subsets^#(xs)) 168.71/78.11 , subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.71/78.11 c_8(mapconsapp^#(x, subs, subs)) } 168.71/78.11 Weak Trs: 168.71/78.11 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.11 mapconsapp(x, subs, subs) 168.71/78.11 , subsets(Cons(x, xs)) -> 168.71/78.11 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.11 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.11 , mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.11 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.71/78.11 , mapconsapp(x, Nil(), rest) -> rest } 168.71/78.11 Obligation: 168.71/78.11 innermost runtime complexity 168.71/78.11 Answer: 168.71/78.11 MAYBE 168.71/78.11 168.71/78.11 We decompose the input problem according to the dependency graph 168.71/78.11 into the upper component 168.71/78.11 168.71/78.11 { subsets^#(Cons(x, xs)) -> 168.71/78.11 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.71/78.11 subsets^#(xs)) } 168.71/78.11 168.71/78.11 and lower component 168.71/78.11 168.71/78.11 { subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.71/78.11 c_8(mapconsapp^#(x, subs, subs)) 168.71/78.11 , mapconsapp^#(x', Cons(x, xs), rest) -> 168.71/78.11 c_3(mapconsapp^#(x', xs, rest)) } 168.71/78.11 168.71/78.11 Further, following extension rules are added to the lower 168.71/78.11 component. 168.71/78.11 168.71/78.11 { subsets^#(Cons(x, xs)) -> subsets^#(xs) 168.71/78.11 , subsets^#(Cons(x, xs)) -> 168.71/78.11 subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)) } 168.71/78.11 168.71/78.11 TcT solves the upper component with certificate YES(O(1),O(n^1)). 168.71/78.11 168.71/78.11 Sub-proof: 168.71/78.11 ---------- 168.71/78.11 We are left with following problem, upon which TcT provides the 168.71/78.11 certificate YES(O(1),O(n^1)). 168.71/78.11 168.71/78.11 Strict DPs: 168.71/78.11 { subsets^#(Cons(x, xs)) -> 168.71/78.11 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.71/78.11 subsets^#(xs)) } 168.71/78.11 Weak Trs: 168.71/78.11 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.11 mapconsapp(x, subs, subs) 168.71/78.11 , subsets(Cons(x, xs)) -> 168.71/78.11 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.11 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.11 , mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.11 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.71/78.11 , mapconsapp(x, Nil(), rest) -> rest } 168.71/78.11 Obligation: 168.71/78.11 innermost runtime complexity 168.71/78.11 Answer: 168.71/78.11 YES(O(1),O(n^1)) 168.71/78.11 168.71/78.11 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 168.71/78.11 to orient following rules strictly. 168.71/78.11 168.71/78.11 DPs: 168.71/78.11 { 1: subsets^#(Cons(x, xs)) -> 168.71/78.11 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.71/78.11 subsets^#(xs)) } 168.71/78.11 Trs: { mapconsapp(x, Nil(), rest) -> rest } 168.71/78.11 168.71/78.11 Sub-proof: 168.71/78.11 ---------- 168.71/78.11 The input was oriented with the instance of 'Small Polynomial Path 168.71/78.11 Order (PS,1-bounded)' as induced by the safe mapping 168.71/78.11 168.71/78.11 safe(subsets[Ite][True][Let]) = {1}, safe(subsets) = {}, 168.71/78.11 safe(Cons) = {1, 2}, safe(Nil) = {}, safe(mapconsapp) = {2, 3}, 168.71/78.11 safe(subsets^#) = {}, safe(c_1) = {}, 168.71/78.11 safe(subsets[Ite][True][Let]^#) = {} 168.71/78.11 168.71/78.11 and precedence 168.71/78.11 168.71/78.11 subsets^# > subsets[Ite][True][Let] . 168.71/78.11 168.71/78.11 Following symbols are considered recursive: 168.71/78.11 168.71/78.11 {subsets^#} 168.71/78.11 168.71/78.11 The recursion depth is 1. 168.71/78.11 168.71/78.11 Further, following argument filtering is employed: 168.71/78.11 168.71/78.11 pi(subsets[Ite][True][Let]) = [1], pi(subsets) = [], 168.71/78.11 pi(Cons) = [1, 2], pi(Nil) = [], pi(mapconsapp) = [2, 3], 168.71/78.11 pi(subsets^#) = [1], pi(c_1) = [1, 2], 168.71/78.11 pi(subsets[Ite][True][Let]^#) = [] 168.71/78.11 168.71/78.11 Usable defined function symbols are a subset of: 168.71/78.11 168.71/78.11 {subsets^#, subsets[Ite][True][Let]^#} 168.71/78.11 168.71/78.11 For your convenience, here are the satisfied ordering constraints: 168.71/78.11 168.71/78.11 pi(subsets^#(Cons(x, xs))) = subsets^#(Cons(; x, xs);) 168.71/78.11 > c_1(subsets[Ite][True][Let]^#(), subsets^#(xs;);) 168.71/78.11 = pi(c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.71/78.11 subsets^#(xs))) 168.71/78.11 168.71/78.11 168.71/78.11 The strictly oriented rules are moved into the weak component. 168.71/78.11 168.71/78.11 We are left with following problem, upon which TcT provides the 168.71/78.11 certificate YES(O(1),O(1)). 168.71/78.11 168.71/78.11 Weak DPs: 168.71/78.11 { subsets^#(Cons(x, xs)) -> 168.71/78.11 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.71/78.11 subsets^#(xs)) } 168.71/78.11 Weak Trs: 168.71/78.11 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.11 mapconsapp(x, subs, subs) 168.71/78.11 , subsets(Cons(x, xs)) -> 168.71/78.11 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.11 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.11 , mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.11 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.71/78.11 , mapconsapp(x, Nil(), rest) -> rest } 168.71/78.11 Obligation: 168.71/78.11 innermost runtime complexity 168.71/78.11 Answer: 168.71/78.11 YES(O(1),O(1)) 168.71/78.11 168.71/78.11 The following weak DPs constitute a sub-graph of the DG that is 168.71/78.11 closed under successors. The DPs are removed. 168.71/78.11 168.71/78.11 { subsets^#(Cons(x, xs)) -> 168.71/78.11 c_1(subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)), 168.71/78.11 subsets^#(xs)) } 168.71/78.11 168.71/78.11 We are left with following problem, upon which TcT provides the 168.71/78.11 certificate YES(O(1),O(1)). 168.71/78.11 168.71/78.11 Weak Trs: 168.71/78.11 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.11 mapconsapp(x, subs, subs) 168.71/78.11 , subsets(Cons(x, xs)) -> 168.71/78.11 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.11 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.11 , mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.11 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.71/78.11 , mapconsapp(x, Nil(), rest) -> rest } 168.71/78.11 Obligation: 168.71/78.11 innermost runtime complexity 168.71/78.11 Answer: 168.71/78.11 YES(O(1),O(1)) 168.71/78.11 168.71/78.11 No rule is usable, rules are removed from the input problem. 168.71/78.11 168.71/78.11 We are left with following problem, upon which TcT provides the 168.71/78.11 certificate YES(O(1),O(1)). 168.71/78.11 168.71/78.11 Rules: Empty 168.71/78.11 Obligation: 168.71/78.11 innermost runtime complexity 168.71/78.11 Answer: 168.71/78.11 YES(O(1),O(1)) 168.71/78.11 168.71/78.11 Empty rules are trivially bounded 168.71/78.11 168.71/78.11 We return to the main proof. 168.71/78.11 168.71/78.11 We are left with following problem, upon which TcT provides the 168.71/78.11 certificate MAYBE. 168.71/78.11 168.71/78.11 Strict DPs: 168.71/78.11 { mapconsapp^#(x', Cons(x, xs), rest) -> 168.71/78.11 c_3(mapconsapp^#(x', xs, rest)) } 168.71/78.11 Weak DPs: 168.71/78.11 { subsets^#(Cons(x, xs)) -> subsets^#(xs) 168.71/78.11 , subsets^#(Cons(x, xs)) -> 168.71/78.11 subsets[Ite][True][Let]^#(Cons(x, xs), subsets(xs)) 168.71/78.11 , subsets[Ite][True][Let]^#(Cons(x, xs), subs) -> 168.71/78.11 c_8(mapconsapp^#(x, subs, subs)) } 168.71/78.11 Weak Trs: 168.71/78.11 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.11 mapconsapp(x, subs, subs) 168.71/78.11 , subsets(Cons(x, xs)) -> 168.71/78.11 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.11 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.11 , mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.11 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.71/78.11 , mapconsapp(x, Nil(), rest) -> rest } 168.71/78.11 Obligation: 168.71/78.11 innermost runtime complexity 168.71/78.11 Answer: 168.71/78.11 MAYBE 168.71/78.11 168.71/78.11 None of the processors succeeded. 168.71/78.11 168.71/78.11 Details of failed attempt(s): 168.71/78.11 ----------------------------- 168.71/78.11 1) 'empty' failed due to the following reason: 168.71/78.11 168.71/78.11 Empty strict component of the problem is NOT empty. 168.71/78.11 168.71/78.11 2) 'Fastest' failed due to the following reason: 168.71/78.11 168.71/78.11 None of the processors succeeded. 168.71/78.11 168.71/78.11 Details of failed attempt(s): 168.71/78.11 ----------------------------- 168.71/78.11 1) 'With Problem ...' failed due to the following reason: 168.71/78.11 168.71/78.11 None of the processors succeeded. 168.71/78.11 168.71/78.11 Details of failed attempt(s): 168.71/78.11 ----------------------------- 168.71/78.11 1) 'empty' failed due to the following reason: 168.71/78.11 168.71/78.11 Empty strict component of the problem is NOT empty. 168.71/78.11 168.71/78.11 2) 'Polynomial Path Order (PS)' failed due to the following reason: 168.71/78.11 168.71/78.11 The input cannot be shown compatible 168.71/78.11 168.71/78.11 168.71/78.11 2) 'Polynomial Path Order (PS)' failed due to the following reason: 168.71/78.11 168.71/78.11 The input cannot be shown compatible 168.71/78.11 168.71/78.11 3) 'Fastest (timeout of 24 seconds)' failed due to the following 168.71/78.11 reason: 168.71/78.11 168.71/78.11 None of the processors succeeded. 168.71/78.11 168.71/78.11 Details of failed attempt(s): 168.71/78.11 ----------------------------- 168.71/78.11 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 168.71/78.11 failed due to the following reason: 168.71/78.11 168.71/78.11 match-boundness of the problem could not be verified. 168.71/78.11 168.71/78.11 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 168.71/78.11 failed due to the following reason: 168.71/78.11 168.71/78.11 match-boundness of the problem could not be verified. 168.71/78.11 168.71/78.11 168.71/78.11 168.71/78.11 168.71/78.11 168.71/78.11 2) 'Best' failed due to the following reason: 168.71/78.11 168.71/78.11 None of the processors succeeded. 168.71/78.11 168.71/78.11 Details of failed attempt(s): 168.71/78.11 ----------------------------- 168.71/78.11 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 168.71/78.11 seconds)' failed due to the following reason: 168.71/78.11 168.71/78.11 The weightgap principle applies (using the following nonconstant 168.71/78.11 growth matrix-interpretation) 168.71/78.11 168.71/78.11 The following argument positions are usable: 168.71/78.11 Uargs(subsets[Ite][True][Let]) = {2}, Uargs(Cons) = {2} 168.71/78.11 168.71/78.11 TcT has computed the following matrix interpretation satisfying 168.71/78.11 not(EDA) and not(IDA(1)). 168.71/78.11 168.71/78.11 [subsets[Ite][True][Let]](x1, x2) = [1] x2 + [7] 168.71/78.11 168.71/78.11 [True] = [5] 168.71/78.11 168.71/78.11 [subsets](x1) = [1] x1 + [7] 168.71/78.11 168.71/78.11 [Cons](x1, x2) = [1] x2 + [7] 168.71/78.11 168.71/78.11 [Nil] = [7] 168.71/78.11 168.71/78.11 [mapconsapp](x1, x2, x3) = [1] x3 + [7] 168.71/78.11 168.71/78.11 [notEmpty](x1) = [1] x1 + [7] 168.71/78.11 168.71/78.11 [goal](x1) = [1] x1 + [7] 168.71/78.11 168.71/78.11 [False] = [5] 168.71/78.11 168.71/78.11 The order satisfies the following ordering constraints: 168.71/78.11 168.71/78.11 [subsets[Ite][True][Let](Cons(x, xs), subs)] = [1] subs + [7] 168.71/78.11 >= [1] subs + [7] 168.71/78.11 = [mapconsapp(x, subs, subs)] 168.71/78.11 168.71/78.11 [subsets(Cons(x, xs))] = [1] xs + [14] 168.71/78.11 >= [1] xs + [14] 168.71/78.11 = [subsets[Ite][True][Let](Cons(x, xs), subsets(xs))] 168.71/78.11 168.71/78.11 [subsets(Nil())] = [14] 168.71/78.11 >= [14] 168.71/78.11 = [Cons(Nil(), Nil())] 168.71/78.11 168.71/78.11 [mapconsapp(x', Cons(x, xs), rest)] = [1] rest + [7] 168.71/78.11 ? [1] rest + [14] 168.71/78.11 = [Cons(Cons(x', x), mapconsapp(x', xs, rest))] 168.71/78.11 168.71/78.11 [mapconsapp(x, Nil(), rest)] = [1] rest + [7] 168.71/78.11 > [1] rest + [0] 168.71/78.11 = [rest] 168.71/78.11 168.71/78.11 [notEmpty(Cons(x, xs))] = [1] xs + [14] 168.71/78.11 > [5] 168.71/78.11 = [True()] 168.71/78.11 168.71/78.11 [notEmpty(Nil())] = [14] 168.71/78.11 > [5] 168.71/78.11 = [False()] 168.71/78.11 168.71/78.11 [goal(xs)] = [1] xs + [7] 168.71/78.11 >= [1] xs + [7] 168.71/78.11 = [subsets(xs)] 168.71/78.11 168.71/78.11 168.71/78.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 168.71/78.11 168.71/78.11 We are left with following problem, upon which TcT provides the 168.71/78.11 certificate MAYBE. 168.71/78.11 168.71/78.11 Strict Trs: 168.71/78.11 { subsets(Cons(x, xs)) -> 168.71/78.11 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.11 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.11 , mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.11 Cons(Cons(x', x), mapconsapp(x', xs, rest)) 168.71/78.11 , goal(xs) -> subsets(xs) } 168.71/78.11 Weak Trs: 168.71/78.11 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.11 mapconsapp(x, subs, subs) 168.71/78.11 , mapconsapp(x, Nil(), rest) -> rest 168.71/78.11 , notEmpty(Cons(x, xs)) -> True() 168.71/78.11 , notEmpty(Nil()) -> False() } 168.71/78.11 Obligation: 168.71/78.11 innermost runtime complexity 168.71/78.11 Answer: 168.71/78.11 MAYBE 168.71/78.11 168.71/78.11 The weightgap principle applies (using the following nonconstant 168.71/78.11 growth matrix-interpretation) 168.71/78.11 168.71/78.11 The following argument positions are usable: 168.71/78.11 Uargs(subsets[Ite][True][Let]) = {2}, Uargs(Cons) = {2} 168.71/78.11 168.71/78.11 TcT has computed the following matrix interpretation satisfying 168.71/78.11 not(EDA) and not(IDA(1)). 168.71/78.11 168.71/78.11 [subsets[Ite][True][Let]](x1, x2) = [1] x2 + [0] 168.71/78.11 168.71/78.11 [True] = [7] 168.71/78.11 168.71/78.11 [subsets](x1) = [0] 168.71/78.11 168.71/78.11 [Cons](x1, x2) = [1] x2 + [0] 168.71/78.11 168.71/78.11 [Nil] = [0] 168.71/78.11 168.71/78.11 [mapconsapp](x1, x2, x3) = [1] x3 + [0] 168.71/78.11 168.71/78.11 [notEmpty](x1) = [1] x1 + [7] 168.71/78.11 168.71/78.11 [goal](x1) = [1] x1 + [7] 168.71/78.11 168.71/78.11 [False] = [7] 168.71/78.11 168.71/78.11 The order satisfies the following ordering constraints: 168.71/78.11 168.71/78.11 [subsets[Ite][True][Let](Cons(x, xs), subs)] = [1] subs + [0] 168.71/78.11 >= [1] subs + [0] 168.71/78.11 = [mapconsapp(x, subs, subs)] 168.71/78.11 168.71/78.11 [subsets(Cons(x, xs))] = [0] 168.71/78.11 >= [0] 168.71/78.11 = [subsets[Ite][True][Let](Cons(x, xs), subsets(xs))] 168.71/78.11 168.71/78.11 [subsets(Nil())] = [0] 168.71/78.11 >= [0] 168.71/78.11 = [Cons(Nil(), Nil())] 168.71/78.11 168.71/78.11 [mapconsapp(x', Cons(x, xs), rest)] = [1] rest + [0] 168.71/78.11 >= [1] rest + [0] 168.71/78.11 = [Cons(Cons(x', x), mapconsapp(x', xs, rest))] 168.71/78.11 168.71/78.11 [mapconsapp(x, Nil(), rest)] = [1] rest + [0] 168.71/78.11 >= [1] rest + [0] 168.71/78.11 = [rest] 168.71/78.11 168.71/78.11 [notEmpty(Cons(x, xs))] = [1] xs + [7] 168.71/78.12 >= [7] 168.71/78.12 = [True()] 168.71/78.12 168.71/78.12 [notEmpty(Nil())] = [7] 168.71/78.12 >= [7] 168.71/78.12 = [False()] 168.71/78.12 168.71/78.12 [goal(xs)] = [1] xs + [7] 168.71/78.12 > [0] 168.71/78.12 = [subsets(xs)] 168.71/78.12 168.71/78.12 168.71/78.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 168.71/78.12 168.71/78.12 We are left with following problem, upon which TcT provides the 168.71/78.12 certificate MAYBE. 168.71/78.12 168.71/78.12 Strict Trs: 168.71/78.12 { subsets(Cons(x, xs)) -> 168.71/78.12 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.12 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.12 , mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.12 Cons(Cons(x', x), mapconsapp(x', xs, rest)) } 168.71/78.12 Weak Trs: 168.71/78.12 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.12 mapconsapp(x, subs, subs) 168.71/78.12 , mapconsapp(x, Nil(), rest) -> rest 168.71/78.12 , notEmpty(Cons(x, xs)) -> True() 168.71/78.12 , notEmpty(Nil()) -> False() 168.71/78.12 , goal(xs) -> subsets(xs) } 168.71/78.12 Obligation: 168.71/78.12 innermost runtime complexity 168.71/78.12 Answer: 168.71/78.12 MAYBE 168.71/78.12 168.71/78.12 The weightgap principle applies (using the following nonconstant 168.71/78.12 growth matrix-interpretation) 168.71/78.12 168.71/78.12 The following argument positions are usable: 168.71/78.12 Uargs(subsets[Ite][True][Let]) = {2}, Uargs(Cons) = {2} 168.71/78.12 168.71/78.12 TcT has computed the following matrix interpretation satisfying 168.71/78.12 not(EDA) and not(IDA(1)). 168.71/78.12 168.71/78.12 [subsets[Ite][True][Let]](x1, x2) = [1] x2 + [0] 168.71/78.12 168.71/78.12 [True] = [7] 168.71/78.12 168.71/78.12 [subsets](x1) = [1] 168.71/78.12 168.71/78.12 [Cons](x1, x2) = [1] x2 + [0] 168.71/78.12 168.71/78.12 [Nil] = [0] 168.71/78.12 168.71/78.12 [mapconsapp](x1, x2, x3) = [1] x3 + [0] 168.71/78.12 168.71/78.12 [notEmpty](x1) = [1] x1 + [7] 168.71/78.12 168.71/78.12 [goal](x1) = [1] x1 + [7] 168.71/78.12 168.71/78.12 [False] = [7] 168.71/78.12 168.71/78.12 The order satisfies the following ordering constraints: 168.71/78.12 168.71/78.12 [subsets[Ite][True][Let](Cons(x, xs), subs)] = [1] subs + [0] 168.71/78.12 >= [1] subs + [0] 168.71/78.12 = [mapconsapp(x, subs, subs)] 168.71/78.12 168.71/78.12 [subsets(Cons(x, xs))] = [1] 168.71/78.12 >= [1] 168.71/78.12 = [subsets[Ite][True][Let](Cons(x, xs), subsets(xs))] 168.71/78.12 168.71/78.12 [subsets(Nil())] = [1] 168.71/78.12 > [0] 168.71/78.12 = [Cons(Nil(), Nil())] 168.71/78.12 168.71/78.12 [mapconsapp(x', Cons(x, xs), rest)] = [1] rest + [0] 168.71/78.12 >= [1] rest + [0] 168.71/78.12 = [Cons(Cons(x', x), mapconsapp(x', xs, rest))] 168.71/78.12 168.71/78.12 [mapconsapp(x, Nil(), rest)] = [1] rest + [0] 168.71/78.12 >= [1] rest + [0] 168.71/78.12 = [rest] 168.71/78.12 168.71/78.12 [notEmpty(Cons(x, xs))] = [1] xs + [7] 168.71/78.12 >= [7] 168.71/78.12 = [True()] 168.71/78.12 168.71/78.12 [notEmpty(Nil())] = [7] 168.71/78.12 >= [7] 168.71/78.12 = [False()] 168.71/78.12 168.71/78.12 [goal(xs)] = [1] xs + [7] 168.71/78.12 > [1] 168.71/78.12 = [subsets(xs)] 168.71/78.12 168.71/78.12 168.71/78.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 168.71/78.12 168.71/78.12 We are left with following problem, upon which TcT provides the 168.71/78.12 certificate MAYBE. 168.71/78.12 168.71/78.12 Strict Trs: 168.71/78.12 { subsets(Cons(x, xs)) -> 168.71/78.12 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.12 , mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.12 Cons(Cons(x', x), mapconsapp(x', xs, rest)) } 168.71/78.12 Weak Trs: 168.71/78.12 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.12 mapconsapp(x, subs, subs) 168.71/78.12 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.12 , mapconsapp(x, Nil(), rest) -> rest 168.71/78.12 , notEmpty(Cons(x, xs)) -> True() 168.71/78.12 , notEmpty(Nil()) -> False() 168.71/78.12 , goal(xs) -> subsets(xs) } 168.71/78.12 Obligation: 168.71/78.12 innermost runtime complexity 168.71/78.12 Answer: 168.71/78.12 MAYBE 168.71/78.12 168.71/78.12 The weightgap principle applies (using the following nonconstant 168.71/78.12 growth matrix-interpretation) 168.71/78.12 168.71/78.12 The following argument positions are usable: 168.71/78.12 Uargs(subsets[Ite][True][Let]) = {2}, Uargs(Cons) = {2} 168.71/78.12 168.71/78.12 TcT has computed the following matrix interpretation satisfying 168.71/78.12 not(EDA) and not(IDA(1)). 168.71/78.12 168.71/78.12 [subsets[Ite][True][Let]](x1, x2) = [1] x2 + [2] 168.71/78.12 168.71/78.12 [True] = [3] 168.71/78.12 168.71/78.12 [subsets](x1) = [1] x1 + [6] 168.71/78.12 168.71/78.12 [Cons](x1, x2) = [1] x2 + [6] 168.71/78.12 168.71/78.12 [Nil] = [5] 168.71/78.12 168.71/78.12 [mapconsapp](x1, x2, x3) = [1] x3 + [2] 168.71/78.12 168.71/78.12 [notEmpty](x1) = [1] x1 + [5] 168.71/78.12 168.71/78.12 [goal](x1) = [1] x1 + [7] 168.71/78.12 168.71/78.12 [False] = [1] 168.71/78.12 168.71/78.12 The order satisfies the following ordering constraints: 168.71/78.12 168.71/78.12 [subsets[Ite][True][Let](Cons(x, xs), subs)] = [1] subs + [2] 168.71/78.12 >= [1] subs + [2] 168.71/78.12 = [mapconsapp(x, subs, subs)] 168.71/78.12 168.71/78.12 [subsets(Cons(x, xs))] = [1] xs + [12] 168.71/78.12 > [1] xs + [8] 168.71/78.12 = [subsets[Ite][True][Let](Cons(x, xs), subsets(xs))] 168.71/78.12 168.71/78.12 [subsets(Nil())] = [11] 168.71/78.12 >= [11] 168.71/78.12 = [Cons(Nil(), Nil())] 168.71/78.12 168.71/78.12 [mapconsapp(x', Cons(x, xs), rest)] = [1] rest + [2] 168.71/78.12 ? [1] rest + [8] 168.71/78.12 = [Cons(Cons(x', x), mapconsapp(x', xs, rest))] 168.71/78.12 168.71/78.12 [mapconsapp(x, Nil(), rest)] = [1] rest + [2] 168.71/78.12 > [1] rest + [0] 168.71/78.12 = [rest] 168.71/78.12 168.71/78.12 [notEmpty(Cons(x, xs))] = [1] xs + [11] 168.71/78.12 > [3] 168.71/78.12 = [True()] 168.71/78.12 168.71/78.12 [notEmpty(Nil())] = [10] 168.71/78.12 > [1] 168.71/78.12 = [False()] 168.71/78.12 168.71/78.12 [goal(xs)] = [1] xs + [7] 168.71/78.12 > [1] xs + [6] 168.71/78.12 = [subsets(xs)] 168.71/78.12 168.71/78.12 168.71/78.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 168.71/78.12 168.71/78.12 We are left with following problem, upon which TcT provides the 168.71/78.12 certificate MAYBE. 168.71/78.12 168.71/78.12 Strict Trs: 168.71/78.12 { mapconsapp(x', Cons(x, xs), rest) -> 168.71/78.12 Cons(Cons(x', x), mapconsapp(x', xs, rest)) } 168.71/78.12 Weak Trs: 168.71/78.12 { subsets[Ite][True][Let](Cons(x, xs), subs) -> 168.71/78.12 mapconsapp(x, subs, subs) 168.71/78.12 , subsets(Cons(x, xs)) -> 168.71/78.12 subsets[Ite][True][Let](Cons(x, xs), subsets(xs)) 168.71/78.12 , subsets(Nil()) -> Cons(Nil(), Nil()) 168.71/78.12 , mapconsapp(x, Nil(), rest) -> rest 168.71/78.12 , notEmpty(Cons(x, xs)) -> True() 168.71/78.12 , notEmpty(Nil()) -> False() 168.71/78.12 , goal(xs) -> subsets(xs) } 168.71/78.12 Obligation: 168.71/78.12 innermost runtime complexity 168.71/78.12 Answer: 168.71/78.12 MAYBE 168.71/78.12 168.71/78.12 None of the processors succeeded. 168.71/78.12 168.71/78.12 Details of failed attempt(s): 168.71/78.12 ----------------------------- 168.71/78.12 1) 'empty' failed due to the following reason: 168.71/78.12 168.71/78.12 Empty strict component of the problem is NOT empty. 168.71/78.12 168.71/78.12 2) 'With Problem ...' failed due to the following reason: 168.71/78.12 168.71/78.12 None of the processors succeeded. 168.71/78.12 168.71/78.12 Details of failed attempt(s): 168.71/78.12 ----------------------------- 168.71/78.12 1) 'empty' failed due to the following reason: 168.71/78.12 168.71/78.12 Empty strict component of the problem is NOT empty. 168.71/78.12 168.71/78.12 2) 'Fastest' failed due to the following reason: 168.71/78.12 168.71/78.12 None of the processors succeeded. 168.71/78.12 168.71/78.12 Details of failed attempt(s): 168.71/78.12 ----------------------------- 168.71/78.12 1) 'With Problem ...' failed due to the following reason: 168.71/78.12 168.71/78.12 None of the processors succeeded. 168.71/78.12 168.71/78.12 Details of failed attempt(s): 168.71/78.12 ----------------------------- 168.71/78.12 1) 'empty' failed due to the following reason: 168.71/78.12 168.71/78.12 Empty strict component of the problem is NOT empty. 168.71/78.12 168.71/78.12 2) 'With Problem ...' failed due to the following reason: 168.71/78.12 168.71/78.12 None of the processors succeeded. 168.71/78.12 168.71/78.12 Details of failed attempt(s): 168.71/78.12 ----------------------------- 168.71/78.12 1) 'empty' failed due to the following reason: 168.71/78.12 168.71/78.12 Empty strict component of the problem is NOT empty. 168.71/78.12 168.71/78.12 2) 'With Problem ...' failed due to the following reason: 168.71/78.12 168.71/78.12 None of the processors succeeded. 168.71/78.12 168.71/78.12 Details of failed attempt(s): 168.71/78.12 ----------------------------- 168.71/78.12 1) 'empty' failed due to the following reason: 168.71/78.12 168.71/78.12 Empty strict component of the problem is NOT empty. 168.71/78.12 168.71/78.12 2) 'With Problem ...' failed due to the following reason: 168.71/78.12 168.71/78.12 Empty strict component of the problem is NOT empty. 168.71/78.12 168.71/78.12 168.71/78.12 168.71/78.12 168.71/78.12 2) 'With Problem ...' failed due to the following reason: 168.71/78.12 168.71/78.12 None of the processors succeeded. 168.71/78.12 168.71/78.12 Details of failed attempt(s): 168.71/78.12 ----------------------------- 168.71/78.12 1) 'empty' failed due to the following reason: 168.71/78.12 168.71/78.12 Empty strict component of the problem is NOT empty. 168.71/78.12 168.71/78.12 2) 'With Problem ...' failed due to the following reason: 168.71/78.12 168.71/78.12 Empty strict component of the problem is NOT empty. 168.71/78.12 168.71/78.12 168.71/78.12 168.71/78.12 168.71/78.12 168.71/78.12 2) 'Best' failed due to the following reason: 168.71/78.12 168.71/78.12 None of the processors succeeded. 168.71/78.12 168.71/78.12 Details of failed attempt(s): 168.71/78.12 ----------------------------- 168.71/78.12 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 168.71/78.12 to the following reason: 168.71/78.12 168.71/78.12 The input cannot be shown compatible 168.71/78.12 168.71/78.12 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 168.71/78.12 following reason: 168.71/78.12 168.71/78.12 The input cannot be shown compatible 168.71/78.12 168.71/78.12 168.71/78.12 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 168.71/78.12 failed due to the following reason: 168.71/78.12 168.71/78.12 None of the processors succeeded. 168.71/78.12 168.71/78.12 Details of failed attempt(s): 168.71/78.12 ----------------------------- 168.71/78.12 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 168.71/78.12 failed due to the following reason: 168.71/78.12 168.71/78.12 match-boundness of the problem could not be verified. 168.71/78.12 168.71/78.12 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 168.71/78.12 failed due to the following reason: 168.71/78.12 168.71/78.12 match-boundness of the problem could not be verified. 168.71/78.12 168.71/78.12 168.71/78.12 168.71/78.12 168.71/78.12 168.71/78.12 Arrrr.. 168.83/78.21 EOF