WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^2)) + Considered Problem: - Strict TRS: F(0(),z0) -> c3() F(S(z0),0()) -> c2() F(S(z0),S(z1)) -> c(H(g(z0,S(z1)),f(S(S(z0)),z1)),G(z0,S(z1))) F(S(z0),S(z1)) -> c1(H(g(z0,S(z1)),f(S(S(z0)),z1)),F(S(S(z0)),z1)) G(0(),z0) -> c10() G(S(z0),0()) -> c9() G(S(z0),S(z1)) -> c7(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),F(S(z0),S(z1))) G(S(z0),S(z1)) -> c8(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),G(z0,S(S(z1)))) H(0(),0()) -> c5() H(0(),S(z0)) -> c4(H(0(),z0)) H(S(z0),z1) -> c6(H(z0,z1)) - Weak TRS: f(0(),z0) -> 0() f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),0()) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {F,G,H,f,g,h} and constructors {0,S,c,c1,c10,c2,c3,c4,c5 ,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: F(0(),z0) -> c3() F(S(z0),0()) -> c2() F(S(z0),S(z1)) -> c(H(g(z0,S(z1)),f(S(S(z0)),z1)),G(z0,S(z1))) F(S(z0),S(z1)) -> c1(H(g(z0,S(z1)),f(S(S(z0)),z1)),F(S(S(z0)),z1)) G(0(),z0) -> c10() G(S(z0),0()) -> c9() G(S(z0),S(z1)) -> c7(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),F(S(z0),S(z1))) G(S(z0),S(z1)) -> c8(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),G(z0,S(S(z1)))) H(0(),0()) -> c5() H(0(),S(z0)) -> c4(H(0(),z0)) H(S(z0),z1) -> c6(H(z0,z1)) - Weak TRS: f(0(),z0) -> 0() f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),0()) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {F,G,H,f,g,h} and constructors {0,S,c,c1,c10,c2,c3,c4,c5 ,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: F(0(),z0) -> c3() F(S(z0),0()) -> c2() F(S(z0),S(z1)) -> c(H(g(z0,S(z1)),f(S(S(z0)),z1)),G(z0,S(z1))) F(S(z0),S(z1)) -> c1(H(g(z0,S(z1)),f(S(S(z0)),z1)),F(S(S(z0)),z1)) G(0(),z0) -> c10() G(S(z0),0()) -> c9() G(S(z0),S(z1)) -> c7(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),F(S(z0),S(z1))) G(S(z0),S(z1)) -> c8(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),G(z0,S(S(z1)))) H(0(),0()) -> c5() H(0(),S(z0)) -> c4(H(0(),z0)) H(S(z0),z1) -> c6(H(z0,z1)) - Weak TRS: f(0(),z0) -> 0() f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),0()) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {F,G,H,f,g,h} and constructors {0,S,c,c1,c10,c2,c3,c4,c5 ,c6,c7,c8,c9} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: F(S(x),y){y -> S(y)} = F(S(x),S(y)) ->^+ c1(H(g(x,S(y)),f(S(S(x)),y)),F(S(S(x)),y)) = C[F(S(S(x)),y) = F(S(x),y){x -> S(x)}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: F(0(),z0) -> c3() F(S(z0),0()) -> c2() F(S(z0),S(z1)) -> c(H(g(z0,S(z1)),f(S(S(z0)),z1)),G(z0,S(z1))) F(S(z0),S(z1)) -> c1(H(g(z0,S(z1)),f(S(S(z0)),z1)),F(S(S(z0)),z1)) G(0(),z0) -> c10() G(S(z0),0()) -> c9() G(S(z0),S(z1)) -> c7(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),F(S(z0),S(z1))) G(S(z0),S(z1)) -> c8(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),G(z0,S(S(z1)))) H(0(),0()) -> c5() H(0(),S(z0)) -> c4(H(0(),z0)) H(S(z0),z1) -> c6(H(z0,z1)) - Weak TRS: f(0(),z0) -> 0() f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),0()) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {F,G,H,f,g,h} and constructors {0,S,c,c1,c10,c2,c3,c4,c5 ,c6,c7,c8,c9} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs F#(0(),z0) -> c_1() F#(S(z0),0()) -> c_2() F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(0(),z0) -> c_5() G#(S(z0),0()) -> c_6() G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(0(),0()) -> c_9() H#(0(),S(z0)) -> c_10(H#(0(),z0)) H#(S(z0),z1) -> c_11(H#(z0,z1)) Weak DPs f#(0(),z0) -> c_12() f#(S(z0),0()) -> c_13() f#(S(z0),S(z1)) -> c_14(h#(g(z0,S(z1)),f(S(S(z0)),z1))) g#(0(),z0) -> c_15() g#(S(z0),0()) -> c_16() g#(S(z0),S(z1)) -> c_17(h#(f(S(z0),S(z1)),g(z0,S(S(z1))))) h#(0(),0()) -> c_18() h#(0(),S(z0)) -> c_19(h#(0(),z0)) h#(S(z0),z1) -> c_20(h#(z0,z1)) and mark the set of starting terms. ** Step 1.b:2: UsableRules. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(0(),z0) -> c_1() F#(S(z0),0()) -> c_2() F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(0(),z0) -> c_5() G#(S(z0),0()) -> c_6() G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(0(),0()) -> c_9() H#(0(),S(z0)) -> c_10(H#(0(),z0)) H#(S(z0),z1) -> c_11(H#(z0,z1)) - Strict TRS: F(0(),z0) -> c3() F(S(z0),0()) -> c2() F(S(z0),S(z1)) -> c(H(g(z0,S(z1)),f(S(S(z0)),z1)),G(z0,S(z1))) F(S(z0),S(z1)) -> c1(H(g(z0,S(z1)),f(S(S(z0)),z1)),F(S(S(z0)),z1)) G(0(),z0) -> c10() G(S(z0),0()) -> c9() G(S(z0),S(z1)) -> c7(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),F(S(z0),S(z1))) G(S(z0),S(z1)) -> c8(H(f(S(z0),S(z1)),g(z0,S(S(z1)))),G(z0,S(S(z1)))) H(0(),0()) -> c5() H(0(),S(z0)) -> c4(H(0(),z0)) H(S(z0),z1) -> c6(H(z0,z1)) - Weak DPs: f#(0(),z0) -> c_12() f#(S(z0),0()) -> c_13() f#(S(z0),S(z1)) -> c_14(h#(g(z0,S(z1)),f(S(S(z0)),z1))) g#(0(),z0) -> c_15() g#(S(z0),0()) -> c_16() g#(S(z0),S(z1)) -> c_17(h#(f(S(z0),S(z1)),g(z0,S(S(z1))))) h#(0(),0()) -> c_18() h#(0(),S(z0)) -> c_19(h#(0(),z0)) h#(S(z0),z1) -> c_20(h#(z0,z1)) - Weak TRS: f(0(),z0) -> 0() f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),0()) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) F#(0(),z0) -> c_1() F#(S(z0),0()) -> c_2() F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(0(),z0) -> c_5() G#(S(z0),0()) -> c_6() G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(0(),0()) -> c_9() H#(0(),S(z0)) -> c_10(H#(0(),z0)) H#(S(z0),z1) -> c_11(H#(z0,z1)) f#(0(),z0) -> c_12() f#(S(z0),0()) -> c_13() f#(S(z0),S(z1)) -> c_14(h#(g(z0,S(z1)),f(S(S(z0)),z1))) g#(0(),z0) -> c_15() g#(S(z0),0()) -> c_16() g#(S(z0),S(z1)) -> c_17(h#(f(S(z0),S(z1)),g(z0,S(S(z1))))) h#(0(),0()) -> c_18() h#(0(),S(z0)) -> c_19(h#(0(),z0)) h#(S(z0),z1) -> c_20(h#(z0,z1)) ** Step 1.b:3: PredecessorEstimation. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(0(),z0) -> c_1() F#(S(z0),0()) -> c_2() F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(0(),z0) -> c_5() G#(S(z0),0()) -> c_6() G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(0(),0()) -> c_9() H#(0(),S(z0)) -> c_10(H#(0(),z0)) H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak DPs: f#(0(),z0) -> c_12() f#(S(z0),0()) -> c_13() f#(S(z0),S(z1)) -> c_14(h#(g(z0,S(z1)),f(S(S(z0)),z1))) g#(0(),z0) -> c_15() g#(S(z0),0()) -> c_16() g#(S(z0),S(z1)) -> c_17(h#(f(S(z0),S(z1)),g(z0,S(S(z1))))) h#(0(),0()) -> c_18() h#(0(),S(z0)) -> c_19(h#(0(),z0)) h#(S(z0),z1) -> c_20(h#(z0,z1)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,5,6,9} by application of Pre({1,2,5,6,9}) = {3,4,7,8,10,11}. Here rules are labelled as follows: 1: F#(0(),z0) -> c_1() 2: F#(S(z0),0()) -> c_2() 3: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) 4: F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) 5: G#(0(),z0) -> c_5() 6: G#(S(z0),0()) -> c_6() 7: G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) 8: G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) 9: H#(0(),0()) -> c_9() 10: H#(0(),S(z0)) -> c_10(H#(0(),z0)) 11: H#(S(z0),z1) -> c_11(H#(z0,z1)) 12: f#(0(),z0) -> c_12() 13: f#(S(z0),0()) -> c_13() 14: f#(S(z0),S(z1)) -> c_14(h#(g(z0,S(z1)),f(S(S(z0)),z1))) 15: g#(0(),z0) -> c_15() 16: g#(S(z0),0()) -> c_16() 17: g#(S(z0),S(z1)) -> c_17(h#(f(S(z0),S(z1)),g(z0,S(S(z1))))) 18: h#(0(),0()) -> c_18() 19: h#(0(),S(z0)) -> c_19(h#(0(),z0)) 20: h#(S(z0),z1) -> c_20(h#(z0,z1)) ** Step 1.b:4: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(0(),S(z0)) -> c_10(H#(0(),z0)) H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak DPs: F#(0(),z0) -> c_1() F#(S(z0),0()) -> c_2() G#(0(),z0) -> c_5() G#(S(z0),0()) -> c_6() H#(0(),0()) -> c_9() f#(0(),z0) -> c_12() f#(S(z0),0()) -> c_13() f#(S(z0),S(z1)) -> c_14(h#(g(z0,S(z1)),f(S(S(z0)),z1))) g#(0(),z0) -> c_15() g#(S(z0),0()) -> c_16() g#(S(z0),S(z1)) -> c_17(h#(f(S(z0),S(z1)),g(z0,S(S(z1))))) h#(0(),0()) -> c_18() h#(0(),S(z0)) -> c_19(h#(0(),z0)) h#(S(z0),z1) -> c_20(h#(z0,z1)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):6 -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):5 -->_2 G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))):4 -->_2 G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))):3 -->_1 H#(0(),0()) -> c_9():11 -->_2 G#(0(),z0) -> c_5():9 2:S:F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):6 -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):5 -->_1 H#(0(),0()) -> c_9():11 -->_2 F#(S(z0),0()) -> c_2():8 -->_2 F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)):2 -->_2 F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))):1 3:S:G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):6 -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):5 -->_1 H#(0(),0()) -> c_9():11 -->_2 F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)):2 -->_2 F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))):1 4:S:G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):6 -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):5 -->_1 H#(0(),0()) -> c_9():11 -->_2 G#(0(),z0) -> c_5():9 -->_2 G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))):4 -->_2 G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))):3 5:S:H#(0(),S(z0)) -> c_10(H#(0(),z0)) -->_1 H#(0(),0()) -> c_9():11 -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):5 6:S:H#(S(z0),z1) -> c_11(H#(z0,z1)) -->_1 H#(0(),0()) -> c_9():11 -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):6 -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):5 7:W:F#(0(),z0) -> c_1() 8:W:F#(S(z0),0()) -> c_2() 9:W:G#(0(),z0) -> c_5() 10:W:G#(S(z0),0()) -> c_6() 11:W:H#(0(),0()) -> c_9() 12:W:f#(0(),z0) -> c_12() 13:W:f#(S(z0),0()) -> c_13() 14:W:f#(S(z0),S(z1)) -> c_14(h#(g(z0,S(z1)),f(S(S(z0)),z1))) -->_1 h#(S(z0),z1) -> c_20(h#(z0,z1)):20 -->_1 h#(0(),S(z0)) -> c_19(h#(0(),z0)):19 -->_1 h#(0(),0()) -> c_18():18 15:W:g#(0(),z0) -> c_15() 16:W:g#(S(z0),0()) -> c_16() 17:W:g#(S(z0),S(z1)) -> c_17(h#(f(S(z0),S(z1)),g(z0,S(S(z1))))) -->_1 h#(S(z0),z1) -> c_20(h#(z0,z1)):20 -->_1 h#(0(),S(z0)) -> c_19(h#(0(),z0)):19 -->_1 h#(0(),0()) -> c_18():18 18:W:h#(0(),0()) -> c_18() 19:W:h#(0(),S(z0)) -> c_19(h#(0(),z0)) -->_1 h#(0(),S(z0)) -> c_19(h#(0(),z0)):19 -->_1 h#(0(),0()) -> c_18():18 20:W:h#(S(z0),z1) -> c_20(h#(z0,z1)) -->_1 h#(S(z0),z1) -> c_20(h#(z0,z1)):20 -->_1 h#(0(),S(z0)) -> c_19(h#(0(),z0)):19 -->_1 h#(0(),0()) -> c_18():18 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 17: g#(S(z0),S(z1)) -> c_17(h#(f(S(z0),S(z1)),g(z0,S(S(z1))))) 16: g#(S(z0),0()) -> c_16() 15: g#(0(),z0) -> c_15() 14: f#(S(z0),S(z1)) -> c_14(h#(g(z0,S(z1)),f(S(S(z0)),z1))) 20: h#(S(z0),z1) -> c_20(h#(z0,z1)) 19: h#(0(),S(z0)) -> c_19(h#(0(),z0)) 18: h#(0(),0()) -> c_18() 13: f#(S(z0),0()) -> c_13() 12: f#(0(),z0) -> c_12() 10: G#(S(z0),0()) -> c_6() 7: F#(0(),z0) -> c_1() 8: F#(S(z0),0()) -> c_2() 9: G#(0(),z0) -> c_5() 11: H#(0(),0()) -> c_9() ** Step 1.b:5: PredecessorEstimationCP. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(0(),S(z0)) -> c_10(H#(0(),z0)) H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 5: H#(0(),S(z0)) -> c_10(H#(0(),z0)) The strictly oriented rules are moved into the weak component. *** Step 1.b:5.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(0(),S(z0)) -> c_10(H#(0(),z0)) H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1,2}, uargs(c_4) = {1,2}, uargs(c_7) = {1,2}, uargs(c_8) = {1,2}, uargs(c_10) = {1}, uargs(c_11) = {1} Following symbols are considered usable: {f,g,h,F#,G#,H#,f#,g#,h#} TcT has computed the following interpretation: p(0) = [0] p(F) = [4] x1 + [2] x2 + [4] p(G) = [1] p(H) = [2] x2 + [1] p(S) = [1] x1 + [4] p(c) = [1] x1 + [0] p(c1) = [1] p(c10) = [1] p(c2) = [0] p(c3) = [4] p(c4) = [2] p(c5) = [0] p(c6) = [0] p(c7) = [1] x2 + [0] p(c8) = [1] x1 + [1] x2 + [4] p(c9) = [1] p(f) = [0] p(g) = [0] p(h) = [0] p(F#) = [0] p(G#) = [0] p(H#) = [2] x2 + [0] p(f#) = [1] x1 + [0] p(g#) = [0] p(h#) = [1] x1 + [1] x2 + [4] p(c_1) = [2] p(c_2) = [1] p(c_3) = [1] x1 + [1] x2 + [0] p(c_4) = [4] x1 + [2] x2 + [0] p(c_5) = [1] p(c_6) = [4] p(c_7) = [2] x1 + [2] x2 + [0] p(c_8) = [4] x1 + [4] x2 + [0] p(c_9) = [1] p(c_10) = [1] x1 + [4] p(c_11) = [1] x1 + [0] p(c_12) = [4] p(c_13) = [0] p(c_14) = [2] x1 + [2] p(c_15) = [4] p(c_16) = [1] p(c_17) = [0] p(c_18) = [1] p(c_19) = [1] x1 + [0] p(c_20) = [1] Following rules are strictly oriented: H#(0(),S(z0)) = [2] z0 + [8] > [2] z0 + [4] = c_10(H#(0(),z0)) Following rules are (at-least) weakly oriented: F#(S(z0),S(z1)) = [0] >= [0] = c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) = [0] >= [0] = c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) = [0] >= [0] = c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) = [0] >= [0] = c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(S(z0),z1) = [2] z1 + [0] >= [2] z1 + [0] = c_11(H#(z0,z1)) f(S(z0),0()) = [0] >= [0] = 0() f(S(z0),S(z1)) = [0] >= [0] = h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) = [0] >= [0] = 0() g(S(z0),S(z1)) = [0] >= [0] = h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) = [0] >= [0] = 0() h(0(),S(z0)) = [0] >= [0] = h(0(),z0) h(S(z0),z1) = [0] >= [0] = h(z0,z1) *** Step 1.b:5.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak DPs: H#(0(),S(z0)) -> c_10(H#(0(),z0)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () *** Step 1.b:5.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak DPs: H#(0(),S(z0)) -> c_10(H#(0(),z0)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):6 -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 -->_2 G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))):4 -->_2 G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))):3 2:S:F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):6 -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 -->_2 F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)):2 -->_2 F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))):1 3:S:G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):6 -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 -->_2 F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)):2 -->_2 F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))):1 4:S:G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):6 -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 -->_2 G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))):4 -->_2 G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))):3 5:S:H#(S(z0),z1) -> c_11(H#(z0,z1)) -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):6 -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 6:W:H#(0(),S(z0)) -> c_10(H#(0(),z0)) -->_1 H#(0(),S(z0)) -> c_10(H#(0(),z0)):6 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: H#(0(),S(z0)) -> c_10(H#(0(),z0)) *** Step 1.b:5.b:2: PredecessorEstimationCP. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 5: H#(S(z0),z1) -> c_11(H#(z0,z1)) The strictly oriented rules are moved into the weak component. **** Step 1.b:5.b:2.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1,2}, uargs(c_4) = {1,2}, uargs(c_7) = {1,2}, uargs(c_8) = {1,2}, uargs(c_11) = {1} Following symbols are considered usable: {f,g,h,F#,G#,H#,f#,g#,h#} TcT has computed the following interpretation: p(0) = [0] p(F) = [0] p(G) = [0] p(H) = [0] p(S) = [1] x1 + [4] p(c) = [1] x1 + [1] x2 + [0] p(c1) = [1] x1 + [1] x2 + [0] p(c10) = [0] p(c2) = [0] p(c3) = [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [1] x1 + [0] p(c7) = [1] x1 + [1] x2 + [0] p(c8) = [1] x1 + [1] x2 + [0] p(c9) = [0] p(f) = [0] p(g) = [0] p(h) = [0] p(F#) = [0] p(G#) = [0] p(H#) = [1] x1 + [0] p(f#) = [0] p(g#) = [0] p(h#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [4] x2 + [0] p(c_4) = [4] x1 + [1] x2 + [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [4] x1 + [1] x2 + [0] p(c_9) = [2] p(c_10) = [0] p(c_11) = [1] x1 + [2] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [1] x1 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] Following rules are strictly oriented: H#(S(z0),z1) = [1] z0 + [4] > [1] z0 + [2] = c_11(H#(z0,z1)) Following rules are (at-least) weakly oriented: F#(S(z0),S(z1)) = [0] >= [0] = c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) = [0] >= [0] = c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) = [0] >= [0] = c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) = [0] >= [0] = c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) f(S(z0),0()) = [0] >= [0] = 0() f(S(z0),S(z1)) = [0] >= [0] = h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) = [0] >= [0] = 0() g(S(z0),S(z1)) = [0] >= [0] = h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) = [0] >= [0] = 0() h(0(),S(z0)) = [0] >= [0] = h(0(),z0) h(S(z0),z1) = [0] >= [0] = h(z0,z1) **** Step 1.b:5.b:2.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) - Weak DPs: H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () **** Step 1.b:5.b:2.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) - Weak DPs: H#(S(z0),z1) -> c_11(H#(z0,z1)) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 -->_2 G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))):4 -->_2 G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))):3 2:S:F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 -->_2 F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)):2 -->_2 F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))):1 3:S:G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 -->_2 F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)):2 -->_2 F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))):1 4:S:G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 -->_2 G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))):4 -->_2 G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))):3 5:W:H#(S(z0),z1) -> c_11(H#(z0,z1)) -->_1 H#(S(z0),z1) -> c_11(H#(z0,z1)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: H#(S(z0),z1) -> c_11(H#(z0,z1)) **** Step 1.b:5.b:2.b:2: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/2,c_4/2,c_5/0,c_6/0,c_7/2,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))) -->_2 G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))):4 -->_2 G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))):3 2:S:F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)) -->_2 F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)):2 -->_2 F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))):1 3:S:G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))) -->_2 F#(S(z0),S(z1)) -> c_4(H#(g(z0,S(z1)),f(S(S(z0)),z1)),F#(S(S(z0)),z1)):2 -->_2 F#(S(z0),S(z1)) -> c_3(H#(g(z0,S(z1)),f(S(S(z0)),z1)),G#(z0,S(z1))):1 4:S:G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))) -->_2 G#(S(z0),S(z1)) -> c_8(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),G#(z0,S(S(z1)))):4 -->_2 G#(S(z0),S(z1)) -> c_7(H#(f(S(z0),S(z1)),g(z0,S(S(z1)))),F#(S(z0),S(z1))):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) **** Step 1.b:5.b:2.b:3: UsableRules. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Weak TRS: f(S(z0),0()) -> 0() f(S(z0),S(z1)) -> h(g(z0,S(z1)),f(S(S(z0)),z1)) g(0(),z0) -> 0() g(S(z0),S(z1)) -> h(f(S(z0),S(z1)),g(z0,S(S(z1)))) h(0(),0()) -> 0() h(0(),S(z0)) -> h(0(),z0) h(S(z0),z1) -> h(z0,z1) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) **** Step 1.b:5.b:2.b:4: PredecessorEstimationCP. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) The strictly oriented rules are moved into the weak component. ***** Step 1.b:5.b:2.b:4.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {F#,G#,H#,f#,g#,h#} TcT has computed the following interpretation: p(0) = [2] p(F) = [1] x1 + [1] x2 + [4] p(G) = [1] x1 + [2] p(H) = [0] p(S) = [1] x1 + [2] p(c) = [1] x1 + [1] x2 + [0] p(c1) = [1] x1 + [1] x2 + [1] p(c10) = [1] p(c2) = [1] p(c3) = [1] p(c4) = [0] p(c5) = [0] p(c6) = [1] p(c7) = [1] x1 + [1] x2 + [1] p(c8) = [1] p(c9) = [0] p(f) = [2] x1 + [2] x2 + [0] p(g) = [0] p(h) = [1] x2 + [1] p(F#) = [4] x1 + [4] x2 + [4] p(G#) = [4] x1 + [4] x2 + [8] p(H#) = [4] x1 + [1] x2 + [4] p(f#) = [4] x1 + [1] p(g#) = [1] x1 + [2] x2 + [1] p(h#) = [4] x1 + [0] p(c_1) = [0] p(c_2) = [2] p(c_3) = [1] x1 + [2] p(c_4) = [1] x1 + [0] p(c_5) = [1] p(c_6) = [2] p(c_7) = [1] x1 + [4] p(c_8) = [1] x1 + [0] p(c_9) = [1] p(c_10) = [1] x1 + [0] p(c_11) = [1] p(c_12) = [1] p(c_13) = [0] p(c_14) = [1] x1 + [0] p(c_15) = [4] p(c_16) = [0] p(c_17) = [4] x1 + [1] p(c_18) = [1] p(c_19) = [1] x1 + [1] p(c_20) = [2] Following rules are strictly oriented: F#(S(z0),S(z1)) = [4] z0 + [4] z1 + [20] > [4] z0 + [4] z1 + [18] = c_3(G#(z0,S(z1))) Following rules are (at-least) weakly oriented: F#(S(z0),S(z1)) = [4] z0 + [4] z1 + [20] >= [4] z0 + [4] z1 + [20] = c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) = [4] z0 + [4] z1 + [24] >= [4] z0 + [4] z1 + [24] = c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) = [4] z0 + [4] z1 + [24] >= [4] z0 + [4] z1 + [24] = c_8(G#(z0,S(S(z1)))) ***** Step 1.b:5.b:2.b:4.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ***** Step 1.b:5.b:2.b:4.b:1: PredecessorEstimationCP. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) The strictly oriented rules are moved into the weak component. ****** Step 1.b:5.b:2.b:4.b:1.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {F#,G#,H#,f#,g#,h#} TcT has computed the following interpretation: p(0) = [1] p(F) = [2] p(G) = [2] x2 + [8] p(H) = [1] x1 + [2] x2 + [1] p(S) = [1] x1 + [2] p(c) = [1] x2 + [0] p(c1) = [0] p(c10) = [0] p(c2) = [0] p(c3) = [1] p(c4) = [0] p(c5) = [2] p(c6) = [1] x1 + [1] p(c7) = [2] p(c8) = [1] x1 + [0] p(c9) = [1] p(f) = [1] x1 + [0] p(g) = [4] p(h) = [0] p(F#) = [1] x1 + [1] x2 + [0] p(G#) = [1] x1 + [1] x2 + [1] p(H#) = [1] x1 + [0] p(f#) = [1] x2 + [2] p(g#) = [1] x1 + [1] x2 + [0] p(h#) = [8] x1 + [1] x2 + [0] p(c_1) = [4] p(c_2) = [0] p(c_3) = [1] x1 + [1] p(c_4) = [1] x1 + [0] p(c_5) = [2] p(c_6) = [2] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [0] p(c_9) = [2] p(c_10) = [0] p(c_11) = [2] x1 + [1] p(c_12) = [1] p(c_13) = [0] p(c_14) = [1] p(c_15) = [1] p(c_16) = [4] p(c_17) = [1] p(c_18) = [1] p(c_19) = [0] p(c_20) = [1] x1 + [1] Following rules are strictly oriented: G#(S(z0),S(z1)) = [1] z0 + [1] z1 + [5] > [1] z0 + [1] z1 + [4] = c_7(F#(S(z0),S(z1))) Following rules are (at-least) weakly oriented: F#(S(z0),S(z1)) = [1] z0 + [1] z1 + [4] >= [1] z0 + [1] z1 + [4] = c_3(G#(z0,S(z1))) F#(S(z0),S(z1)) = [1] z0 + [1] z1 + [4] >= [1] z0 + [1] z1 + [4] = c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) = [1] z0 + [1] z1 + [5] >= [1] z0 + [1] z1 + [5] = c_8(G#(z0,S(S(z1)))) ****** Step 1.b:5.b:2.b:4.b:1.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ****** Step 1.b:5.b:2.b:4.b:1.b:1: PredecessorEstimationCP. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) The strictly oriented rules are moved into the weak component. ******* Step 1.b:5.b:2.b:4.b:1.b:1.a:1: NaturalPI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {F#,G#,H#,f#,g#,h#} TcT has computed the following interpretation: p(0) = 1 p(F) = x1 + x2^2 p(G) = 1 + 4*x1 + 2*x1*x2 p(H) = 1 + 4*x2 p(S) = 1 + x1 p(c) = x1 p(c1) = 4 + x2 p(c10) = 0 p(c2) = 1 p(c3) = 1 p(c4) = x1 p(c5) = 1 p(c6) = 1 p(c7) = x2 p(c8) = x1 + x2 p(c9) = 0 p(f) = 4*x1 + 4*x2 p(g) = 1 + 2*x1 + 2*x1*x2 + 4*x1^2 + 2*x2 + x2^2 p(h) = 1 + x1 + 2*x2 + x2^2 p(F#) = 6*x1*x2 + 3*x1^2 + 3*x2^2 p(G#) = 2*x1 + 6*x1*x2 + 3*x1^2 + x2 + 3*x2^2 p(H#) = x1 + 2*x1^2 + x2^2 p(f#) = 1 + x1 + x1^2 + 2*x2 + x2^2 p(g#) = 1 + x1^2 + 2*x2 p(h#) = 1 + x2 + 4*x2^2 p(c_1) = 0 p(c_2) = 0 p(c_3) = 2 + x1 p(c_4) = x1 p(c_5) = 4 p(c_6) = 0 p(c_7) = x1 p(c_8) = x1 p(c_9) = 1 p(c_10) = x1 p(c_11) = 0 p(c_12) = 1 p(c_13) = 4 p(c_14) = 1 p(c_15) = 1 p(c_16) = 1 p(c_17) = 4 p(c_18) = 2 p(c_19) = 4 + x1 p(c_20) = 1 Following rules are strictly oriented: G#(S(z0),S(z1)) = 15 + 14*z0 + 6*z0*z1 + 3*z0^2 + 13*z1 + 3*z1^2 > 14 + 14*z0 + 6*z0*z1 + 3*z0^2 + 13*z1 + 3*z1^2 = c_8(G#(z0,S(S(z1)))) Following rules are (at-least) weakly oriented: F#(S(z0),S(z1)) = 12 + 12*z0 + 6*z0*z1 + 3*z0^2 + 12*z1 + 3*z1^2 >= 6 + 8*z0 + 6*z0*z1 + 3*z0^2 + 7*z1 + 3*z1^2 = c_3(G#(z0,S(z1))) F#(S(z0),S(z1)) = 12 + 12*z0 + 6*z0*z1 + 3*z0^2 + 12*z1 + 3*z1^2 >= 12 + 12*z0 + 6*z0*z1 + 3*z0^2 + 12*z1 + 3*z1^2 = c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) = 15 + 14*z0 + 6*z0*z1 + 3*z0^2 + 13*z1 + 3*z1^2 >= 12 + 12*z0 + 6*z0*z1 + 3*z0^2 + 12*z1 + 3*z1^2 = c_7(F#(S(z0),S(z1))) ******* Step 1.b:5.b:2.b:4.b:1.b:1.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ******* Step 1.b:5.b:2.b:4.b:1.b:1.b:1: PredecessorEstimationCP. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) The strictly oriented rules are moved into the weak component. ******** Step 1.b:5.b:2.b:4.b:1.b:1.b:1.a:1: NaturalPI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {F#,G#,H#,f#,g#,h#} TcT has computed the following interpretation: p(0) = 1 p(F) = 4 + 4*x1 p(G) = x1*x2 + 2*x2 p(H) = 1 + 2*x1*x2 + x1^2 + 4*x2^2 p(S) = 1 + x1 p(c) = 0 p(c1) = 2 p(c10) = 0 p(c2) = 1 p(c3) = 0 p(c4) = 0 p(c5) = 4 p(c6) = 4 p(c7) = 1 + x2 p(c8) = 0 p(c9) = 1 p(f) = 4 + x1 + 2*x1^2 + x2^2 p(g) = 1 + 4*x2 p(h) = 1 + x1*x2 + 4*x2 + x2^2 p(F#) = 4*x1*x2 + 2*x1^2 + x2 + 2*x2^2 p(G#) = 3*x1 + 4*x1*x2 + 2*x1^2 + 2*x2 + 2*x2^2 p(H#) = x1 + x1*x2 + x1^2 + 4*x2^2 p(f#) = 1 + x1 + 4*x1^2 + x2 + x2^2 p(g#) = 1 + 2*x2 + x2^2 p(h#) = 1 + x1^2 + 4*x2 + 4*x2^2 p(c_1) = 1 p(c_2) = 1 p(c_3) = 2 + x1 p(c_4) = x1 p(c_5) = 2 p(c_6) = 4 p(c_7) = 1 + x1 p(c_8) = x1 p(c_9) = 1 p(c_10) = 0 p(c_11) = 4 p(c_12) = 0 p(c_13) = 1 p(c_14) = 1 p(c_15) = 1 p(c_16) = 0 p(c_17) = x1 p(c_18) = 0 p(c_19) = 4 + x1 p(c_20) = 0 Following rules are strictly oriented: F#(S(z0),S(z1)) = 9 + 8*z0 + 4*z0*z1 + 2*z0^2 + 9*z1 + 2*z1^2 > 8 + 8*z0 + 4*z0*z1 + 2*z0^2 + 9*z1 + 2*z1^2 = c_4(F#(S(S(z0)),z1)) Following rules are (at-least) weakly oriented: F#(S(z0),S(z1)) = 9 + 8*z0 + 4*z0*z1 + 2*z0^2 + 9*z1 + 2*z1^2 >= 6 + 7*z0 + 4*z0*z1 + 2*z0^2 + 6*z1 + 2*z1^2 = c_3(G#(z0,S(z1))) G#(S(z0),S(z1)) = 13 + 11*z0 + 4*z0*z1 + 2*z0^2 + 10*z1 + 2*z1^2 >= 10 + 8*z0 + 4*z0*z1 + 2*z0^2 + 9*z1 + 2*z1^2 = c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) = 13 + 11*z0 + 4*z0*z1 + 2*z0^2 + 10*z1 + 2*z1^2 >= 12 + 11*z0 + 4*z0*z1 + 2*z0^2 + 10*z1 + 2*z1^2 = c_8(G#(z0,S(S(z1)))) ******** Step 1.b:5.b:2.b:4.b:1.b:1.b:1.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ******** Step 1.b:5.b:2.b:4.b:1.b:1.b:1.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) -->_1 G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))):4 -->_1 G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))):3 2:W:F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) -->_1 F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)):2 -->_1 F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))):1 3:W:G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) -->_1 F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)):2 -->_1 F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))):1 4:W:G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) -->_1 G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))):4 -->_1 G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: F#(S(z0),S(z1)) -> c_3(G#(z0,S(z1))) 3: G#(S(z0),S(z1)) -> c_7(F#(S(z0),S(z1))) 4: G#(S(z0),S(z1)) -> c_8(G#(z0,S(S(z1)))) 2: F#(S(z0),S(z1)) -> c_4(F#(S(S(z0)),z1)) ******** Step 1.b:5.b:2.b:4.b:1.b:1.b:1.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Signature: {F/2,G/2,H/2,f/2,g/2,h/2,F#/2,G#/2,H#/2,f#/2,g#/2,h#/2} / {0/0,S/1,c/2,c1/2,c10/0,c2/0,c3/0,c4/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {F#,G#,H#,f#,g#,h#} and constructors {0,S,c,c1,c10,c2,c3 ,c4,c5,c6,c7,c8,c9} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^2))