WORST_CASE(Omega(n^1),O(n^3)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^3)) + Considered Problem: - Strict TRS: -'(z0,0()) -> c() -'(s(z0),s(z1)) -> c1(-'(z0,z1)) F(z0,s(z1)) -> c5(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(z0,s(z1))),-'(z0,s(z1))) F(z0,s(z1)) -> c6(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(s(z1),z0)),-'(s(z1),z0)) F(s(z0),z1) -> c3(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(s(z0),z1)),-'(s(z0),z1)) F(s(z0),z1) -> c4(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(z1,s(z0))),-'(z1,s(z0))) P(s(z0)) -> c2() - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) f(z0,s(z1)) -> f(p(-(z0,s(z1))),p(-(s(z1),z0))) f(s(z0),z1) -> f(p(-(s(z0),z1)),p(-(z1,s(z0)))) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',F,P,f,p} and constructors {0,c,c1,c2,c3,c4,c5,c6,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: -'(z0,0()) -> c() -'(s(z0),s(z1)) -> c1(-'(z0,z1)) F(z0,s(z1)) -> c5(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(z0,s(z1))),-'(z0,s(z1))) F(z0,s(z1)) -> c6(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(s(z1),z0)),-'(s(z1),z0)) F(s(z0),z1) -> c3(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(s(z0),z1)),-'(s(z0),z1)) F(s(z0),z1) -> c4(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(z1,s(z0))),-'(z1,s(z0))) P(s(z0)) -> c2() - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) f(z0,s(z1)) -> f(p(-(z0,s(z1))),p(-(s(z1),z0))) f(s(z0),z1) -> f(p(-(s(z0),z1)),p(-(z1,s(z0)))) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',F,P,f,p} and constructors {0,c,c1,c2,c3,c4,c5,c6,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: -'(z0,0()) -> c() -'(s(z0),s(z1)) -> c1(-'(z0,z1)) F(z0,s(z1)) -> c5(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(z0,s(z1))),-'(z0,s(z1))) F(z0,s(z1)) -> c6(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(s(z1),z0)),-'(s(z1),z0)) F(s(z0),z1) -> c3(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(s(z0),z1)),-'(s(z0),z1)) F(s(z0),z1) -> c4(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(z1,s(z0))),-'(z1,s(z0))) P(s(z0)) -> c2() - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) f(z0,s(z1)) -> f(p(-(z0,s(z1))),p(-(s(z1),z0))) f(s(z0),z1) -> f(p(-(s(z0),z1)),p(-(z1,s(z0)))) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',F,P,f,p} and constructors {0,c,c1,c2,c3,c4,c5,c6,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: -'(x,y){x -> s(x),y -> s(y)} = -'(s(x),s(y)) ->^+ c1(-'(x,y)) = C[-'(x,y) = -'(x,y){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: -'(z0,0()) -> c() -'(s(z0),s(z1)) -> c1(-'(z0,z1)) F(z0,s(z1)) -> c5(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(z0,s(z1))),-'(z0,s(z1))) F(z0,s(z1)) -> c6(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(s(z1),z0)),-'(s(z1),z0)) F(s(z0),z1) -> c3(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(s(z0),z1)),-'(s(z0),z1)) F(s(z0),z1) -> c4(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(z1,s(z0))),-'(z1,s(z0))) P(s(z0)) -> c2() - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) f(z0,s(z1)) -> f(p(-(z0,s(z1))),p(-(s(z1),z0))) f(s(z0),z1) -> f(p(-(s(z0),z1)),p(-(z1,s(z0)))) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',F,P,f,p} and constructors {0,c,c1,c2,c3,c4,c5,c6,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs -'#(z0,0()) -> c_1() -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))) P#(s(z0)) -> c_7() Weak DPs -#(z0,0()) -> c_8() -#(s(z0),s(z1)) -> c_9(-#(z0,z1)) f#(z0,s(z1)) -> c_10(f#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0)) f#(s(z0),z1) -> c_11(f#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0))) p#(s(z0)) -> c_12() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: -'#(z0,0()) -> c_1() -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))) P#(s(z0)) -> c_7() - Weak DPs: -#(z0,0()) -> c_8() -#(s(z0),s(z1)) -> c_9(-#(z0,z1)) f#(z0,s(z1)) -> c_10(f#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0)) f#(s(z0),z1) -> c_11(f#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0))) p#(s(z0)) -> c_12() - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) -'(z0,0()) -> c() -'(s(z0),s(z1)) -> c1(-'(z0,z1)) F(z0,s(z1)) -> c5(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(z0,s(z1))),-'(z0,s(z1))) F(z0,s(z1)) -> c6(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(s(z1),z0)),-'(s(z1),z0)) F(s(z0),z1) -> c3(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(s(z0),z1)),-'(s(z0),z1)) F(s(z0),z1) -> c4(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(z1,s(z0))),-'(z1,s(z0))) P(s(z0)) -> c2() f(z0,s(z1)) -> f(p(-(z0,s(z1))),p(-(s(z1),z0))) f(s(z0),z1) -> f(p(-(s(z0),z1)),p(-(z1,s(z0)))) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/8,c_4/8,c_5/8,c_6/8,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,7} by application of Pre({1,7}) = {2,3,4,5,6}. Here rules are labelled as follows: 1: -'#(z0,0()) -> c_1() 2: -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) 3: F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))) 4: F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)) 5: F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)) 6: F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))) 7: P#(s(z0)) -> c_7() 8: -#(z0,0()) -> c_8() 9: -#(s(z0),s(z1)) -> c_9(-#(z0,z1)) 10: f#(z0,s(z1)) -> c_10(f#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0)) 11: f#(s(z0),z1) -> c_11(f#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0))) 12: p#(s(z0)) -> c_12() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))) - Weak DPs: -#(z0,0()) -> c_8() -#(s(z0),s(z1)) -> c_9(-#(z0,z1)) -'#(z0,0()) -> c_1() P#(s(z0)) -> c_7() f#(z0,s(z1)) -> c_10(f#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0)) f#(s(z0),z1) -> c_11(f#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0))) p#(s(z0)) -> c_12() - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) -'(z0,0()) -> c() -'(s(z0),s(z1)) -> c1(-'(z0,z1)) F(z0,s(z1)) -> c5(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(z0,s(z1))),-'(z0,s(z1))) F(z0,s(z1)) -> c6(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(s(z1),z0)),-'(s(z1),z0)) F(s(z0),z1) -> c3(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(s(z0),z1)),-'(s(z0),z1)) F(s(z0),z1) -> c4(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(z1,s(z0))),-'(z1,s(z0))) P(s(z0)) -> c2() f(z0,s(z1)) -> f(p(-(z0,s(z1))),p(-(s(z1),z0))) f(s(z0),z1) -> f(p(-(s(z0),z1)),p(-(z1,s(z0)))) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/8,c_4/8,c_5/8,c_6/8,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:-'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) -->_1 -'#(z0,0()) -> c_1():8 -->_1 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 2:S:F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))) -->_7 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_5 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_3 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))):5 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)):4 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)):3 -->_4 p#(s(z0)) -> c_12():12 -->_2 p#(s(z0)) -> c_12():12 -->_6 P#(s(z0)) -> c_7():9 -->_5 -#(z0,0()) -> c_8():6 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))):2 -->_8 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 3:S:F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)) -->_7 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_5 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_3 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))):5 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)):4 -->_4 p#(s(z0)) -> c_12():12 -->_2 p#(s(z0)) -> c_12():12 -->_6 P#(s(z0)) -> c_7():9 -->_8 -'#(z0,0()) -> c_1():8 -->_7 -#(z0,0()) -> c_8():6 -->_5 -#(z0,0()) -> c_8():6 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)):3 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))):2 -->_8 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 4:S:F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)) -->_7 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_5 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_3 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))):5 -->_4 p#(s(z0)) -> c_12():12 -->_2 p#(s(z0)) -> c_12():12 -->_6 P#(s(z0)) -> c_7():9 -->_8 -'#(z0,0()) -> c_1():8 -->_7 -#(z0,0()) -> c_8():6 -->_3 -#(z0,0()) -> c_8():6 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)):4 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)):3 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))):2 -->_8 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 5:S:F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))) -->_7 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_5 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_3 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_4 p#(s(z0)) -> c_12():12 -->_2 p#(s(z0)) -> c_12():12 -->_6 P#(s(z0)) -> c_7():9 -->_3 -#(z0,0()) -> c_8():6 -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))):5 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)):4 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)):3 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))):2 -->_8 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 6:W:-#(z0,0()) -> c_8() 7:W:-#(s(z0),s(z1)) -> c_9(-#(z0,z1)) -->_1 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_1 -#(z0,0()) -> c_8():6 8:W:-'#(z0,0()) -> c_1() 9:W:P#(s(z0)) -> c_7() 10:W:f#(z0,s(z1)) -> c_10(f#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0)) -->_1 f#(s(z0),z1) -> c_11(f#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0))):11 -->_4 p#(s(z0)) -> c_12():12 -->_2 p#(s(z0)) -> c_12():12 -->_1 f#(z0,s(z1)) -> c_10(f#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0)):10 -->_5 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_3 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_5 -#(z0,0()) -> c_8():6 11:W:f#(s(z0),z1) -> c_11(f#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0))) -->_4 p#(s(z0)) -> c_12():12 -->_2 p#(s(z0)) -> c_12():12 -->_1 f#(s(z0),z1) -> c_11(f#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0))):11 -->_1 f#(z0,s(z1)) -> c_10(f#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0)):10 -->_5 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_3 -#(s(z0),s(z1)) -> c_9(-#(z0,z1)):7 -->_3 -#(z0,0()) -> c_8():6 12:W:p#(s(z0)) -> c_12() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: f#(z0,s(z1)) -> c_10(f#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0)) 11: f#(s(z0),z1) -> c_11(f#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0))) 9: P#(s(z0)) -> c_7() 12: p#(s(z0)) -> c_12() 7: -#(s(z0),s(z1)) -> c_9(-#(z0,z1)) 6: -#(z0,0()) -> c_8() 8: -'#(z0,0()) -> c_1() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) -'(z0,0()) -> c() -'(s(z0),s(z1)) -> c1(-'(z0,z1)) F(z0,s(z1)) -> c5(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(z0,s(z1))),-'(z0,s(z1))) F(z0,s(z1)) -> c6(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(s(z1),z0)),-'(s(z1),z0)) F(s(z0),z1) -> c3(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(s(z0),z1)),-'(s(z0),z1)) F(s(z0),z1) -> c4(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(z1,s(z0))),-'(z1,s(z0))) P(s(z0)) -> c2() f(z0,s(z1)) -> f(p(-(z0,s(z1))),p(-(s(z1),z0))) f(s(z0),z1) -> f(p(-(s(z0),z1)),p(-(z1,s(z0)))) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/8,c_4/8,c_5/8,c_6/8,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:-'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) -->_1 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 2:S:F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))) -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))):5 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)):4 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)):3 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))):2 -->_8 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 3:S:F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)) -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))):5 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)):4 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)):3 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))):2 -->_8 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 4:S:F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)) -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))):5 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)):4 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)):3 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))):2 -->_8 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 5:S:F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))) -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(z1,s(z0))) ,-#(z1,s(z0)) ,-'#(z1,s(z0))):5 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) ,p#(-(s(z0),z1)) ,-#(s(z0),z1) ,p#(-(z1,s(z0))) ,-#(z1,s(z0)) ,P#(-(s(z0),z1)) ,-#(s(z0),z1) ,-'#(s(z0),z1)):4 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(s(z1),z0)) ,-#(s(z1),z0) ,-'#(s(z1),z0)):3 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))) ,p#(-(z0,s(z1))) ,-#(z0,s(z1)) ,p#(-(s(z1),z0)) ,-#(s(z1),z0) ,P#(-(z0,s(z1))) ,-#(z0,s(z1)) ,-'#(z0,s(z1))):2 -->_8 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) -'(z0,0()) -> c() -'(s(z0),s(z1)) -> c1(-'(z0,z1)) F(z0,s(z1)) -> c5(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(z0,s(z1))),-'(z0,s(z1))) F(z0,s(z1)) -> c6(F(p(-(z0,s(z1))),p(-(s(z1),z0))),P(-(s(z1),z0)),-'(s(z1),z0)) F(s(z0),z1) -> c3(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(s(z0),z1)),-'(s(z0),z1)) F(s(z0),z1) -> c4(F(p(-(s(z0),z1)),p(-(z1,s(z0)))),P(-(z1,s(z0))),-'(z1,s(z0))) P(s(z0)) -> c2() f(z0,s(z1)) -> f(p(-(z0,s(z1))),p(-(s(z1),z0))) f(s(z0),z1) -> f(p(-(s(z0),z1)),p(-(z1,s(z0)))) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/2,c_4/2,c_5/2,c_6/2,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) p(s(z0)) -> z0 -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))) ** Step 1.b:6: DecomposeDG. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/2,c_4/2,c_5/2,c_6/2,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))) and a lower component -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) Further, following extension rules are added to the lower component. F#(z0,s(z1)) -> -'#(z0,s(z1)) F#(z0,s(z1)) -> -'#(s(z1),z0) F#(z0,s(z1)) -> F#(p(-(z0,s(z1))),p(-(s(z1),z0))) F#(s(z0),z1) -> -'#(z1,s(z0)) F#(s(z0),z1) -> -'#(s(z0),z1) F#(s(z0),z1) -> F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) *** Step 1.b:6.a:1: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/2,c_4/2,c_5/2,c_6/2,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))) -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))):4 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)):3 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)):2 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))):1 2:S:F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)) -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))):4 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)):3 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)):2 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))):1 3:S:F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)) -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))):4 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)):3 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)):2 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))):1 4:S:F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))) -->_1 F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(z1,s(z0))):4 -->_1 F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0)))),-'#(s(z0),z1)):3 -->_1 F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(s(z1),z0)):2 -->_1 F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0))),-'#(z0,s(z1))):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0)))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0)))) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0))))) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0))))) *** Step 1.b:6.a:2: Ara. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0)))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0)))) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0))))) F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0))))) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "-") :: ["A"(2, 3) x "A"(0, 0)] -(0)-> "A"(2, 3) F (TrsFun "0") :: [] -(0)-> "A"(0, 0) F (TrsFun "p") :: ["A"(2, 3)] -(0)-> "A"(5, 3) F (TrsFun "s") :: ["A"(8, 3)] -(5)-> "A"(5, 3) F (TrsFun "s") :: ["A"(6, 3)] -(3)-> "A"(3, 3) F (TrsFun "s") :: ["A"(5, 3)] -(2)-> "A"(2, 3) F (TrsFun "s") :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (TrsFun "s") :: ["A"(1, 0)] -(1)-> "A"(1, 0) F (DpFun "F") :: ["A"(3, 3) x "A"(5, 3)] -(0)-> "A"(0, 0) F (ComFun 3) :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (ComFun 4) :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (ComFun 5) :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (ComFun 6) :: ["A"(0, 0)] -(0)-> "A"(0, 0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0)))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0)))) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0))))) 2. Weak: F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0))))) *** Step 1.b:6.a:3: Ara. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0))))) - Weak DPs: F#(z0,s(z1)) -> c_3(F#(p(-(z0,s(z1))),p(-(s(z1),z0)))) F#(z0,s(z1)) -> c_4(F#(p(-(z0,s(z1))),p(-(s(z1),z0)))) F#(s(z0),z1) -> c_5(F#(p(-(s(z0),z1)),p(-(z1,s(z0))))) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "-") :: ["A"(4, 3) x "A"(0, 0)] -(0)-> "A"(3, 3) F (TrsFun "0") :: [] -(0)-> "A"(0, 0) F (TrsFun "p") :: ["A"(3, 3)] -(0)-> "A"(6, 3) F (TrsFun "s") :: ["A"(9, 3)] -(6)-> "A"(6, 3) F (TrsFun "s") :: ["A"(7, 3)] -(4)-> "A"(4, 3) F (TrsFun "s") :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (TrsFun "s") :: ["A"(6, 3)] -(3)-> "A"(3, 3) F (TrsFun "s") :: ["A"(1, 0)] -(1)-> "A"(1, 0) F (DpFun "F") :: ["A"(6, 3) x "A"(4, 3)] -(0)-> "A"(0, 0) F (ComFun 3) :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (ComFun 4) :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (ComFun 5) :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (ComFun 6) :: ["A"(0, 0)] -(0)-> "A"(0, 0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: F#(s(z0),z1) -> c_6(F#(p(-(s(z0),z1)),p(-(z1,s(z0))))) 2. Weak: *** Step 1.b:6.b:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) - Weak DPs: F#(z0,s(z1)) -> -'#(z0,s(z1)) F#(z0,s(z1)) -> -'#(s(z1),z0) F#(z0,s(z1)) -> F#(p(-(z0,s(z1))),p(-(s(z1),z0))) F#(s(z0),z1) -> -'#(z1,s(z0)) F#(s(z0),z1) -> -'#(s(z0),z1) F#(s(z0),z1) -> F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/2,c_4/2,c_5/2,c_6/2,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1} Following symbols are considered usable: {-,p,-#,-'#,F#,P#,f#,p#} TcT has computed the following interpretation: p(-) = [1] x1 + [0] p(-') = [1] x1 + [1] p(0) = [1] p(F) = [1] x1 + [4] x2 + [1] p(P) = [1] x1 + [0] p(c) = [4] p(c1) = [0] p(c2) = [1] p(c3) = [1] x2 + [0] p(c4) = [0] p(c5) = [1] x1 + [0] p(c6) = [1] x3 + [1] p(f) = [1] x1 + [1] x2 + [0] p(p) = [1] x1 + [0] p(s) = [1] x1 + [8] p(-#) = [4] x1 + [1] x2 + [1] p(-'#) = [1] x2 + [0] p(F#) = [2] x1 + [2] x2 + [4] p(P#) = [4] p(f#) = [4] x1 + [1] x2 + [1] p(p#) = [0] p(c_1) = [2] p(c_2) = [1] x1 + [7] p(c_3) = [2] x1 + [1] x2 + [4] p(c_4) = [1] x1 + [2] p(c_5) = [1] x2 + [2] p(c_6) = [1] x1 + [1] p(c_7) = [1] p(c_8) = [1] p(c_9) = [1] p(c_10) = [1] x1 + [2] x2 + [2] x3 + [1] x5 + [1] p(c_11) = [1] x1 + [1] x3 + [2] x4 + [1] x5 + [1] p(c_12) = [1] Following rules are strictly oriented: -'#(s(z0),s(z1)) = [1] z1 + [8] > [1] z1 + [7] = c_2(-'#(z0,z1)) Following rules are (at-least) weakly oriented: F#(z0,s(z1)) = [2] z0 + [2] z1 + [20] >= [1] z1 + [8] = -'#(z0,s(z1)) F#(z0,s(z1)) = [2] z0 + [2] z1 + [20] >= [1] z0 + [0] = -'#(s(z1),z0) F#(z0,s(z1)) = [2] z0 + [2] z1 + [20] >= [2] z0 + [2] z1 + [20] = F#(p(-(z0,s(z1))),p(-(s(z1),z0))) F#(s(z0),z1) = [2] z0 + [2] z1 + [20] >= [1] z0 + [8] = -'#(z1,s(z0)) F#(s(z0),z1) = [2] z0 + [2] z1 + [20] >= [1] z1 + [0] = -'#(s(z0),z1) F#(s(z0),z1) = [2] z0 + [2] z1 + [20] >= [2] z0 + [2] z1 + [20] = F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) -(z0,0()) = [1] z0 + [0] >= [1] z0 + [0] = z0 -(s(z0),s(z1)) = [1] z0 + [8] >= [1] z0 + [0] = -(z0,z1) p(s(z0)) = [1] z0 + [8] >= [1] z0 + [0] = z0 *** Step 1.b:6.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: -'#(s(z0),s(z1)) -> c_2(-'#(z0,z1)) F#(z0,s(z1)) -> -'#(z0,s(z1)) F#(z0,s(z1)) -> -'#(s(z1),z0) F#(z0,s(z1)) -> F#(p(-(z0,s(z1))),p(-(s(z1),z0))) F#(s(z0),z1) -> -'#(z1,s(z0)) F#(s(z0),z1) -> -'#(s(z0),z1) F#(s(z0),z1) -> F#(p(-(s(z0),z1)),p(-(z1,s(z0)))) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) p(s(z0)) -> z0 - Signature: {-/2,-'/2,F/2,P/1,f/2,p/1,-#/2,-'#/2,F#/2,P#/1,f#/2,p#/1} / {0/0,c/0,c1/1,c2/0,c3/3,c4/3,c5/3,c6/3,s/1,c_1/0 ,c_2/1,c_3/2,c_4/2,c_5/2,c_6/2,c_7/0,c_8/0,c_9/1,c_10/5,c_11/5,c_12/0} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,F#,P#,f#,p#} and constructors {0,c,c1,c2,c3,c4,c5 ,c6,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^3))