* Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: e1(x1,x1,x,y,z) -> e5(x1,x,y,z) e1(h1(),h2(),x,y,z) -> e2(x,x,y,z,z) e2(x,x,y,z,z) -> e6(x,y,z) e2(f1(),x,y,z,f2()) -> e3(x,y,x,y,y,z,y,z,x,y,z) e2(i(),x,y,z,i()) -> e6(x,y,z) e3(x,y,x,y,y,z,y,z,x,y,z) -> e6(x,y,z) e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) e4(x,x,x,x,x,x,x,x,x,x,x) -> e6(x,x,x) e4(g1(),x1,g2(),x1,g1(),x1,g2(),x1,x,y,z) -> e1(x1,x1,x,y,z) e4(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> e5(x1,x,y,z) e5(i(),x,y,z) -> e6(x,y,z) f1() -> g1() f1() -> g2() f2() -> g1() f2() -> g2() g1() -> h1() g1() -> h2() g2() -> h1() g2() -> h2() h1() -> i() h2() -> i() - Signature: {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0} / {e6/3,i/0} - Obligation: innermost runtime complexity wrt. defined symbols {e1,e2,e3,e4,e5,f1,f2,g1,g2,h1,h2} and constructors {e6,i} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: InnermostRuleRemoval WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: e1(x1,x1,x,y,z) -> e5(x1,x,y,z) e1(h1(),h2(),x,y,z) -> e2(x,x,y,z,z) e2(x,x,y,z,z) -> e6(x,y,z) e2(f1(),x,y,z,f2()) -> e3(x,y,x,y,y,z,y,z,x,y,z) e2(i(),x,y,z,i()) -> e6(x,y,z) e3(x,y,x,y,y,z,y,z,x,y,z) -> e6(x,y,z) e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) e4(x,x,x,x,x,x,x,x,x,x,x) -> e6(x,x,x) e4(g1(),x1,g2(),x1,g1(),x1,g2(),x1,x,y,z) -> e1(x1,x1,x,y,z) e4(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> e5(x1,x,y,z) e5(i(),x,y,z) -> e6(x,y,z) f1() -> g1() f1() -> g2() f2() -> g1() f2() -> g2() g1() -> h1() g1() -> h2() g2() -> h1() g2() -> h2() h1() -> i() h2() -> i() - Signature: {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0} / {e6/3,i/0} - Obligation: innermost runtime complexity wrt. defined symbols {e1,e2,e3,e4,e5,f1,f2,g1,g2,h1,h2} and constructors {e6,i} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. e1(h1(),h2(),x,y,z) -> e2(x,x,y,z,z) e2(f1(),x,y,z,f2()) -> e3(x,y,x,y,y,z,y,z,x,y,z) e4(g1(),x1,g2(),x1,g1(),x1,g2(),x1,x,y,z) -> e1(x1,x1,x,y,z) All above mentioned rules can be savely removed. * Step 3: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: e1(x1,x1,x,y,z) -> e5(x1,x,y,z) e2(x,x,y,z,z) -> e6(x,y,z) e2(i(),x,y,z,i()) -> e6(x,y,z) e3(x,y,x,y,y,z,y,z,x,y,z) -> e6(x,y,z) e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) e4(x,x,x,x,x,x,x,x,x,x,x) -> e6(x,x,x) e4(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> e5(x1,x,y,z) e5(i(),x,y,z) -> e6(x,y,z) f1() -> g1() f1() -> g2() f2() -> g1() f2() -> g2() g1() -> h1() g1() -> h2() g2() -> h1() g2() -> h2() h1() -> i() h2() -> i() - Signature: {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0} / {e6/3,i/0} - Obligation: innermost runtime complexity wrt. defined symbols {e1,e2,e3,e4,e5,f1,f2,g1,g2,h1,h2} and constructors {e6,i} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z)) e2#(x,x,y,z,z) -> c_2() e2#(i(),x,y,z,i()) -> c_3() e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4() e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z)) e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6() e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z)) e5#(i(),x,y,z) -> c_8() f1#() -> c_9(g1#()) f1#() -> c_10(g2#()) f2#() -> c_11(g1#()) f2#() -> c_12(g2#()) g1#() -> c_13(h1#()) g1#() -> c_14(h2#()) g2#() -> c_15(h1#()) g2#() -> c_16(h2#()) h1#() -> c_17() h2#() -> c_18() Weak DPs and mark the set of starting terms. * Step 4: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z)) e2#(x,x,y,z,z) -> c_2() e2#(i(),x,y,z,i()) -> c_3() e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4() e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z)) e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6() e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z)) e5#(i(),x,y,z) -> c_8() f1#() -> c_9(g1#()) f1#() -> c_10(g2#()) f2#() -> c_11(g1#()) f2#() -> c_12(g2#()) g1#() -> c_13(h1#()) g1#() -> c_14(h2#()) g2#() -> c_15(h1#()) g2#() -> c_16(h2#()) h1#() -> c_17() h2#() -> c_18() - Weak TRS: e1(x1,x1,x,y,z) -> e5(x1,x,y,z) e2(x,x,y,z,z) -> e6(x,y,z) e2(i(),x,y,z,i()) -> e6(x,y,z) e3(x,y,x,y,y,z,y,z,x,y,z) -> e6(x,y,z) e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) e4(x,x,x,x,x,x,x,x,x,x,x) -> e6(x,x,x) e4(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> e5(x1,x,y,z) e5(i(),x,y,z) -> e6(x,y,z) f1() -> g1() f1() -> g2() f2() -> g1() f2() -> g2() g1() -> h1() g1() -> h2() g2() -> h1() g2() -> h2() h1() -> i() h2() -> i() - Signature: {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0,e1#/5,e2#/5,e3#/11,e4#/11,e5#/4,f1#/0,f2#/0,g1#/0 ,g2#/0,h1#/0,h2#/0} / {e6/3,i/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1 ,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0} - Obligation: innermost runtime complexity wrt. defined symbols {e1#,e2#,e3#,e4#,e5#,f1#,f2#,g1#,g2#,h1# ,h2#} and constructors {e6,i} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z)) e2#(x,x,y,z,z) -> c_2() e2#(i(),x,y,z,i()) -> c_3() e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4() e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z)) e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6() e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z)) e5#(i(),x,y,z) -> c_8() f1#() -> c_9(g1#()) f1#() -> c_10(g2#()) f2#() -> c_11(g1#()) f2#() -> c_12(g2#()) g1#() -> c_13(h1#()) g1#() -> c_14(h2#()) g2#() -> c_15(h1#()) g2#() -> c_16(h2#()) h1#() -> c_17() h2#() -> c_18() * Step 5: Trivial WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z)) e2#(x,x,y,z,z) -> c_2() e2#(i(),x,y,z,i()) -> c_3() e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4() e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z)) e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6() e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z)) e5#(i(),x,y,z) -> c_8() f1#() -> c_9(g1#()) f1#() -> c_10(g2#()) f2#() -> c_11(g1#()) f2#() -> c_12(g2#()) g1#() -> c_13(h1#()) g1#() -> c_14(h2#()) g2#() -> c_15(h1#()) g2#() -> c_16(h2#()) h1#() -> c_17() h2#() -> c_18() - Signature: {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0,e1#/5,e2#/5,e3#/11,e4#/11,e5#/4,f1#/0,f2#/0,g1#/0 ,g2#/0,h1#/0,h2#/0} / {e6/3,i/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1 ,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0} - Obligation: innermost runtime complexity wrt. defined symbols {e1#,e2#,e3#,e4#,e5#,f1#,f2#,g1#,g2#,h1# ,h2#} and constructors {e6,i} + Applied Processor: Trivial + Details: Consider the dependency graph 1:S:e1#(x1,x1,x,y,z) -> c_1(e5#(x1,x,y,z)) -->_1 e5#(i(),x,y,z) -> c_8():8 2:S:e2#(x,x,y,z,z) -> c_2() 3:S:e2#(i(),x,y,z,i()) -> c_3() 4:S:e3#(x,y,x,y,y,z,y,z,x,y,z) -> c_4() 5:S:e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z)) -->_1 e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z)):7 -->_1 e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6():6 6:S:e4#(x,x,x,x,x,x,x,x,x,x,x) -> c_6() 7:S:e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z) -> c_7(e5#(x1,x,y,z)) -->_1 e5#(i(),x,y,z) -> c_8():8 8:S:e5#(i(),x,y,z) -> c_8() 9:S:f1#() -> c_9(g1#()) -->_1 g1#() -> c_14(h2#()):14 -->_1 g1#() -> c_13(h1#()):13 10:S:f1#() -> c_10(g2#()) -->_1 g2#() -> c_16(h2#()):16 -->_1 g2#() -> c_15(h1#()):15 11:S:f2#() -> c_11(g1#()) -->_1 g1#() -> c_14(h2#()):14 -->_1 g1#() -> c_13(h1#()):13 12:S:f2#() -> c_12(g2#()) -->_1 g2#() -> c_16(h2#()):16 -->_1 g2#() -> c_15(h1#()):15 13:S:g1#() -> c_13(h1#()) -->_1 h1#() -> c_17():17 14:S:g1#() -> c_14(h2#()) -->_1 h2#() -> c_18():18 15:S:g2#() -> c_15(h1#()) -->_1 h1#() -> c_17():17 16:S:g2#() -> c_16(h2#()) -->_1 h2#() -> c_18():18 17:S:h1#() -> c_17() 18:S:h2#() -> c_18() The dependency graph contains no loops, we remove all dependency pairs. * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {e1/5,e2/5,e3/11,e4/11,e5/4,f1/0,f2/0,g1/0,g2/0,h1/0,h2/0,e1#/5,e2#/5,e3#/11,e4#/11,e5#/4,f1#/0,f2#/0,g1#/0 ,g2#/0,h1#/0,h2#/0} / {e6/3,i/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1 ,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0} - Obligation: innermost runtime complexity wrt. defined symbols {e1#,e2#,e3#,e4#,e5#,f1#,f2#,g1#,g2#,h1# ,h2#} and constructors {e6,i} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))