WORST_CASE(?,O(1)) * Step 1: Sum. WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: F(z0,z1,z2) -> c(G(<=(z0,z1),z0,z1,z2)) G(false(),z0,z1,z2) -> c2(F(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)),F(p(z0),z1,z2),P(z0)) G(false(),z0,z1,z2) -> c3(F(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)),F(p(z1),z2,z0),P(z1)) G(false(),z0,z1,z2) -> c4(F(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)),F(p(z2),z0,z1),P(z2)) G(true(),z0,z1,z2) -> c1() P(0()) -> c5() P(s(z0)) -> c6() - Weak TRS: f(z0,z1,z2) -> g(<=(z0,z1),z0,z1,z2) g(false(),z0,z1,z2) -> f(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) g(true(),z0,z1,z2) -> z2 p(0()) -> 0() p(s(z0)) -> z0 - Signature: {F/3,G/4,P/1,f/3,g/4,p/1} / {0/0,<=/2,c/1,c1/0,c2/3,c3/3,c4/3,c5/0,c6/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {F,G,P,f,g,p} and constructors {0,<=,c,c1,c2,c3,c4,c5,c6 ,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs. WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: F(z0,z1,z2) -> c(G(<=(z0,z1),z0,z1,z2)) G(false(),z0,z1,z2) -> c2(F(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)),F(p(z0),z1,z2),P(z0)) G(false(),z0,z1,z2) -> c3(F(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)),F(p(z1),z2,z0),P(z1)) G(false(),z0,z1,z2) -> c4(F(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)),F(p(z2),z0,z1),P(z2)) G(true(),z0,z1,z2) -> c1() P(0()) -> c5() P(s(z0)) -> c6() - Weak TRS: f(z0,z1,z2) -> g(<=(z0,z1),z0,z1,z2) g(false(),z0,z1,z2) -> f(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) g(true(),z0,z1,z2) -> z2 p(0()) -> 0() p(s(z0)) -> z0 - Signature: {F/3,G/4,P/1,f/3,g/4,p/1} / {0/0,<=/2,c/1,c1/0,c2/3,c3/3,c4/3,c5/0,c6/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {F,G,P,f,g,p} and constructors {0,<=,c,c1,c2,c3,c4,c5,c6 ,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)) G#(false(),z0,z1,z2) -> c_2(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z0),z1,z2) ,p#(z0) ,P#(z0)) G#(false(),z0,z1,z2) -> c_3(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z1),z2,z0) ,p#(z1) ,P#(z1)) G#(false(),z0,z1,z2) -> c_4(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z2),z0,z1) ,p#(z2) ,P#(z2)) G#(true(),z0,z1,z2) -> c_5() P#(0()) -> c_6() P#(s(z0)) -> c_7() Weak DPs f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)) g#(false(),z0,z1,z2) -> c_9(f#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2)) g#(true(),z0,z1,z2) -> c_10() p#(0()) -> c_11() p#(s(z0)) -> c_12() and mark the set of starting terms. * Step 3: UsableRules. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)) G#(false(),z0,z1,z2) -> c_2(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z0),z1,z2) ,p#(z0) ,P#(z0)) G#(false(),z0,z1,z2) -> c_3(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z1),z2,z0) ,p#(z1) ,P#(z1)) G#(false(),z0,z1,z2) -> c_4(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z2),z0,z1) ,p#(z2) ,P#(z2)) G#(true(),z0,z1,z2) -> c_5() P#(0()) -> c_6() P#(s(z0)) -> c_7() - Weak DPs: f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)) g#(false(),z0,z1,z2) -> c_9(f#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2)) g#(true(),z0,z1,z2) -> c_10() p#(0()) -> c_11() p#(s(z0)) -> c_12() - Weak TRS: F(z0,z1,z2) -> c(G(<=(z0,z1),z0,z1,z2)) G(false(),z0,z1,z2) -> c2(F(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)),F(p(z0),z1,z2),P(z0)) G(false(),z0,z1,z2) -> c3(F(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)),F(p(z1),z2,z0),P(z1)) G(false(),z0,z1,z2) -> c4(F(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)),F(p(z2),z0,z1),P(z2)) G(true(),z0,z1,z2) -> c1() P(0()) -> c5() P(s(z0)) -> c6() f(z0,z1,z2) -> g(<=(z0,z1),z0,z1,z2) g(false(),z0,z1,z2) -> f(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) g(true(),z0,z1,z2) -> z2 p(0()) -> 0() p(s(z0)) -> z0 - Signature: {F/3,G/4,P/1,f/3,g/4,p/1,F#/3,G#/4,P#/1,f#/3,g#/4,p#/1} / {0/0,<=/2,c/1,c1/0,c2/3,c3/3,c4/3,c5/0,c6/0 ,false/0,s/1,true/0,c_1/1,c_2/10,c_3/10,c_4/10,c_5/0,c_6/0,c_7/0,c_8/1,c_9/7,c_10/0,c_11/0,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,P#,f#,g#,p#} and constructors {0,<=,c,c1,c2,c3,c4 ,c5,c6,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: f(z0,z1,z2) -> g(<=(z0,z1),z0,z1,z2) p(0()) -> 0() p(s(z0)) -> z0 F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)) G#(false(),z0,z1,z2) -> c_2(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z0),z1,z2) ,p#(z0) ,P#(z0)) G#(false(),z0,z1,z2) -> c_3(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z1),z2,z0) ,p#(z1) ,P#(z1)) G#(false(),z0,z1,z2) -> c_4(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z2),z0,z1) ,p#(z2) ,P#(z2)) G#(true(),z0,z1,z2) -> c_5() P#(0()) -> c_6() P#(s(z0)) -> c_7() f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)) g#(false(),z0,z1,z2) -> c_9(f#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2)) g#(true(),z0,z1,z2) -> c_10() p#(0()) -> c_11() p#(s(z0)) -> c_12() * Step 4: Trivial. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)) G#(false(),z0,z1,z2) -> c_2(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z0),z1,z2) ,p#(z0) ,P#(z0)) G#(false(),z0,z1,z2) -> c_3(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z1),z2,z0) ,p#(z1) ,P#(z1)) G#(false(),z0,z1,z2) -> c_4(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z2),z0,z1) ,p#(z2) ,P#(z2)) G#(true(),z0,z1,z2) -> c_5() P#(0()) -> c_6() P#(s(z0)) -> c_7() - Weak DPs: f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)) g#(false(),z0,z1,z2) -> c_9(f#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2)) g#(true(),z0,z1,z2) -> c_10() p#(0()) -> c_11() p#(s(z0)) -> c_12() - Weak TRS: f(z0,z1,z2) -> g(<=(z0,z1),z0,z1,z2) p(0()) -> 0() p(s(z0)) -> z0 - Signature: {F/3,G/4,P/1,f/3,g/4,p/1,F#/3,G#/4,P#/1,f#/3,g#/4,p#/1} / {0/0,<=/2,c/1,c1/0,c2/3,c3/3,c4/3,c5/0,c6/0 ,false/0,s/1,true/0,c_1/1,c_2/10,c_3/10,c_4/10,c_5/0,c_6/0,c_7/0,c_8/1,c_9/7,c_10/0,c_11/0,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,P#,f#,g#,p#} and constructors {0,<=,c,c1,c2,c3,c4 ,c5,c6,false,s,true} + Applied Processor: Trivial + Details: Consider the dependency graph 1:S:F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)) 2:S:G#(false(),z0,z1,z2) -> c_2(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z0),z1,z2) ,p#(z0) ,P#(z0)) -->_9 p#(s(z0)) -> c_12():12 -->_7 p#(s(z0)) -> c_12():12 -->_5 p#(s(z0)) -> c_12():12 -->_3 p#(s(z0)) -> c_12():12 -->_9 p#(0()) -> c_11():11 -->_7 p#(0()) -> c_11():11 -->_5 p#(0()) -> c_11():11 -->_3 p#(0()) -> c_11():11 -->_6 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_4 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_2 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_10 P#(s(z0)) -> c_7():7 -->_10 P#(0()) -> c_6():6 -->_8 F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)):1 -->_1 F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)):1 3:S:G#(false(),z0,z1,z2) -> c_3(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z1),z2,z0) ,p#(z1) ,P#(z1)) -->_9 p#(s(z0)) -> c_12():12 -->_7 p#(s(z0)) -> c_12():12 -->_5 p#(s(z0)) -> c_12():12 -->_3 p#(s(z0)) -> c_12():12 -->_9 p#(0()) -> c_11():11 -->_7 p#(0()) -> c_11():11 -->_5 p#(0()) -> c_11():11 -->_3 p#(0()) -> c_11():11 -->_6 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_4 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_2 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_10 P#(s(z0)) -> c_7():7 -->_10 P#(0()) -> c_6():6 -->_8 F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)):1 -->_1 F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)):1 4:S:G#(false(),z0,z1,z2) -> c_4(F#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2) ,F#(p(z2),z0,z1) ,p#(z2) ,P#(z2)) -->_9 p#(s(z0)) -> c_12():12 -->_7 p#(s(z0)) -> c_12():12 -->_5 p#(s(z0)) -> c_12():12 -->_3 p#(s(z0)) -> c_12():12 -->_9 p#(0()) -> c_11():11 -->_7 p#(0()) -> c_11():11 -->_5 p#(0()) -> c_11():11 -->_3 p#(0()) -> c_11():11 -->_6 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_4 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_2 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_10 P#(s(z0)) -> c_7():7 -->_10 P#(0()) -> c_6():6 -->_8 F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)):1 -->_1 F#(z0,z1,z2) -> c_1(G#(<=(z0,z1),z0,z1,z2)):1 5:S:G#(true(),z0,z1,z2) -> c_5() 6:S:P#(0()) -> c_6() 7:S:P#(s(z0)) -> c_7() 8:W:f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)) 9:W:g#(false(),z0,z1,z2) -> c_9(f#(f(p(z0),z1,z2),f(p(z1),z2,z0),f(p(z2),z0,z1)) ,f#(p(z0),z1,z2) ,p#(z0) ,f#(p(z1),z2,z0) ,p#(z1) ,f#(p(z2),z0,z1) ,p#(z2)) -->_7 p#(s(z0)) -> c_12():12 -->_5 p#(s(z0)) -> c_12():12 -->_3 p#(s(z0)) -> c_12():12 -->_7 p#(0()) -> c_11():11 -->_5 p#(0()) -> c_11():11 -->_3 p#(0()) -> c_11():11 -->_6 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_4 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_2 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 -->_1 f#(z0,z1,z2) -> c_8(g#(<=(z0,z1),z0,z1,z2)):8 10:W:g#(true(),z0,z1,z2) -> c_10() 11:W:p#(0()) -> c_11() 12:W:p#(s(z0)) -> c_12() The dependency graph contains no loops, we remove all dependency pairs. * Step 5: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: f(z0,z1,z2) -> g(<=(z0,z1),z0,z1,z2) p(0()) -> 0() p(s(z0)) -> z0 - Signature: {F/3,G/4,P/1,f/3,g/4,p/1,F#/3,G#/4,P#/1,f#/3,g#/4,p#/1} / {0/0,<=/2,c/1,c1/0,c2/3,c3/3,c4/3,c5/0,c6/0 ,false/0,s/1,true/0,c_1/1,c_2/10,c_3/10,c_4/10,c_5/0,c_6/0,c_7/0,c_8/1,c_9/7,c_10/0,c_11/0,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,P#,f#,g#,p#} and constructors {0,<=,c,c1,c2,c3,c4 ,c5,c6,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))