MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a__A() -> A() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__a() -> a() a__a() -> a__c() a__a() -> a__d() a__b() -> a__c() a__b() -> a__d() a__b() -> b() a__c() -> c() a__c() -> e() a__c() -> l() a__d() -> d() a__d() -> m() a__f(X) -> a__z(mark(X),X) a__f(X) -> f(X) a__g(X1,X2,X3) -> g(X1,X2,X3) a__g(d(),X,X) -> a__A() a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__h(X1,X2) -> h(X1,X2) a__k() -> k() a__k() -> l() a__k() -> m() a__z(X1,X2) -> z(X1,X2) a__z(e(),X) -> mark(X) mark(A()) -> a__A() mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(e()) -> e() mark(f(X)) -> a__f(mark(X)) mark(g(X1,X2,X3)) -> a__g(mark(X1),mark(X2),mark(X3)) mark(h(X1,X2)) -> a__h(mark(X1),mark(X2)) mark(k()) -> a__k() mark(l()) -> l() mark(m()) -> m() mark(z(X1,X2)) -> a__z(mark(X1),X2) - Signature: {a__A/0,a__a/0,a__b/0,a__c/0,a__d/0,a__f/1,a__g/3,a__h/2,a__k/0,a__z/2,mark/1} / {A/0,a/0,b/0,c/0,d/0,e/0 ,f/1,g/3,h/2,k/0,l/0,m/0,z/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__A,a__a,a__b,a__c,a__d,a__f,a__g,a__h,a__k,a__z ,mark} and constructors {A,a,b,c,d,e,f,g,h,k,l,m,z} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__A#() -> c_1() a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) a__a#() -> c_3() a__a#() -> c_4(a__c#()) a__a#() -> c_5(a__d#()) a__b#() -> c_6(a__c#()) a__b#() -> c_7(a__d#()) a__b#() -> c_8() a__c#() -> c_9() a__c#() -> c_10() a__c#() -> c_11() a__d#() -> c_12() a__d#() -> c_13() a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) a__f#(X) -> c_15() a__g#(X1,X2,X3) -> c_16() a__g#(d(),X,X) -> c_17(a__A#()) a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) a__h#(X1,X2) -> c_19() a__k#() -> c_20() a__k#() -> c_21() a__k#() -> c_22() a__z#(X1,X2) -> c_23() a__z#(e(),X) -> c_24(mark#(X)) mark#(A()) -> c_25(a__A#()) mark#(a()) -> c_26(a__a#()) mark#(b()) -> c_27(a__b#()) mark#(c()) -> c_28(a__c#()) mark#(d()) -> c_29(a__d#()) mark#(e()) -> c_30() mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(k()) -> c_34(a__k#()) mark#(l()) -> c_35() mark#(m()) -> c_36() mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__A#() -> c_1() a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) a__a#() -> c_3() a__a#() -> c_4(a__c#()) a__a#() -> c_5(a__d#()) a__b#() -> c_6(a__c#()) a__b#() -> c_7(a__d#()) a__b#() -> c_8() a__c#() -> c_9() a__c#() -> c_10() a__c#() -> c_11() a__d#() -> c_12() a__d#() -> c_13() a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) a__f#(X) -> c_15() a__g#(X1,X2,X3) -> c_16() a__g#(d(),X,X) -> c_17(a__A#()) a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) a__h#(X1,X2) -> c_19() a__k#() -> c_20() a__k#() -> c_21() a__k#() -> c_22() a__z#(X1,X2) -> c_23() a__z#(e(),X) -> c_24(mark#(X)) mark#(A()) -> c_25(a__A#()) mark#(a()) -> c_26(a__a#()) mark#(b()) -> c_27(a__b#()) mark#(c()) -> c_28(a__c#()) mark#(d()) -> c_29(a__d#()) mark#(e()) -> c_30() mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(k()) -> c_34(a__k#()) mark#(l()) -> c_35() mark#(m()) -> c_36() mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) - Weak TRS: a__A() -> A() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__a() -> a() a__a() -> a__c() a__a() -> a__d() a__b() -> a__c() a__b() -> a__d() a__b() -> b() a__c() -> c() a__c() -> e() a__c() -> l() a__d() -> d() a__d() -> m() a__f(X) -> a__z(mark(X),X) a__f(X) -> f(X) a__g(X1,X2,X3) -> g(X1,X2,X3) a__g(d(),X,X) -> a__A() a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__h(X1,X2) -> h(X1,X2) a__k() -> k() a__k() -> l() a__k() -> m() a__z(X1,X2) -> z(X1,X2) a__z(e(),X) -> mark(X) mark(A()) -> a__A() mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(e()) -> e() mark(f(X)) -> a__f(mark(X)) mark(g(X1,X2,X3)) -> a__g(mark(X1),mark(X2),mark(X3)) mark(h(X1,X2)) -> a__h(mark(X1),mark(X2)) mark(k()) -> a__k() mark(l()) -> l() mark(m()) -> m() mark(z(X1,X2)) -> a__z(mark(X1),X2) - Signature: {a__A/0,a__a/0,a__b/0,a__c/0,a__d/0,a__f/1,a__g/3,a__h/2,a__k/0,a__z/2,mark/1,a__A#/0,a__a#/0,a__b#/0 ,a__c#/0,a__d#/0,a__f#/1,a__g#/3,a__h#/2,a__k#/0,a__z#/2,mark#/1} / {A/0,a/0,b/0,c/0,d/0,e/0,f/1,g/3,h/2,k/0 ,l/0,m/0,z/2,c_1/0,c_2/5,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/2,c_15/0 ,c_16/0,c_17/1,c_18/5,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1,c_30/0 ,c_31/2,c_32/4,c_33/3,c_34/1,c_35/0,c_36/0,c_37/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__A#,a__a#,a__b#,a__c#,a__d#,a__f#,a__g#,a__h#,a__k# ,a__z#,mark#} and constructors {A,a,b,c,d,e,f,g,h,k,l,m,z} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,8,9,10,11,12,13,15,16,19,20,21,22,23,30,35,36} by application of Pre({1,3,8,9,10,11,12,13,15,16,19,20,21,22,23,30,35,36}) = {2,4,5,6,7,14,17,18,24,25,26,27,28,29,31,32,33 ,34,37}. Here rules are labelled as follows: 1: a__A#() -> c_1() 2: a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) 3: a__a#() -> c_3() 4: a__a#() -> c_4(a__c#()) 5: a__a#() -> c_5(a__d#()) 6: a__b#() -> c_6(a__c#()) 7: a__b#() -> c_7(a__d#()) 8: a__b#() -> c_8() 9: a__c#() -> c_9() 10: a__c#() -> c_10() 11: a__c#() -> c_11() 12: a__d#() -> c_12() 13: a__d#() -> c_13() 14: a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) 15: a__f#(X) -> c_15() 16: a__g#(X1,X2,X3) -> c_16() 17: a__g#(d(),X,X) -> c_17(a__A#()) 18: a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) 19: a__h#(X1,X2) -> c_19() 20: a__k#() -> c_20() 21: a__k#() -> c_21() 22: a__k#() -> c_22() 23: a__z#(X1,X2) -> c_23() 24: a__z#(e(),X) -> c_24(mark#(X)) 25: mark#(A()) -> c_25(a__A#()) 26: mark#(a()) -> c_26(a__a#()) 27: mark#(b()) -> c_27(a__b#()) 28: mark#(c()) -> c_28(a__c#()) 29: mark#(d()) -> c_29(a__d#()) 30: mark#(e()) -> c_30() 31: mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) 32: mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) 33: mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 34: mark#(k()) -> c_34(a__k#()) 35: mark#(l()) -> c_35() 36: mark#(m()) -> c_36() 37: mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) a__a#() -> c_4(a__c#()) a__a#() -> c_5(a__d#()) a__b#() -> c_6(a__c#()) a__b#() -> c_7(a__d#()) a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) a__g#(d(),X,X) -> c_17(a__A#()) a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) a__z#(e(),X) -> c_24(mark#(X)) mark#(A()) -> c_25(a__A#()) mark#(a()) -> c_26(a__a#()) mark#(b()) -> c_27(a__b#()) mark#(c()) -> c_28(a__c#()) mark#(d()) -> c_29(a__d#()) mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(k()) -> c_34(a__k#()) mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) - Weak DPs: a__A#() -> c_1() a__a#() -> c_3() a__b#() -> c_8() a__c#() -> c_9() a__c#() -> c_10() a__c#() -> c_11() a__d#() -> c_12() a__d#() -> c_13() a__f#(X) -> c_15() a__g#(X1,X2,X3) -> c_16() a__h#(X1,X2) -> c_19() a__k#() -> c_20() a__k#() -> c_21() a__k#() -> c_22() a__z#(X1,X2) -> c_23() mark#(e()) -> c_30() mark#(l()) -> c_35() mark#(m()) -> c_36() - Weak TRS: a__A() -> A() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__a() -> a() a__a() -> a__c() a__a() -> a__d() a__b() -> a__c() a__b() -> a__d() a__b() -> b() a__c() -> c() a__c() -> e() a__c() -> l() a__d() -> d() a__d() -> m() a__f(X) -> a__z(mark(X),X) a__f(X) -> f(X) a__g(X1,X2,X3) -> g(X1,X2,X3) a__g(d(),X,X) -> a__A() a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__h(X1,X2) -> h(X1,X2) a__k() -> k() a__k() -> l() a__k() -> m() a__z(X1,X2) -> z(X1,X2) a__z(e(),X) -> mark(X) mark(A()) -> a__A() mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(e()) -> e() mark(f(X)) -> a__f(mark(X)) mark(g(X1,X2,X3)) -> a__g(mark(X1),mark(X2),mark(X3)) mark(h(X1,X2)) -> a__h(mark(X1),mark(X2)) mark(k()) -> a__k() mark(l()) -> l() mark(m()) -> m() mark(z(X1,X2)) -> a__z(mark(X1),X2) - Signature: {a__A/0,a__a/0,a__b/0,a__c/0,a__d/0,a__f/1,a__g/3,a__h/2,a__k/0,a__z/2,mark/1,a__A#/0,a__a#/0,a__b#/0 ,a__c#/0,a__d#/0,a__f#/1,a__g#/3,a__h#/2,a__k#/0,a__z#/2,mark#/1} / {A/0,a/0,b/0,c/0,d/0,e/0,f/1,g/3,h/2,k/0 ,l/0,m/0,z/2,c_1/0,c_2/5,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/2,c_15/0 ,c_16/0,c_17/1,c_18/5,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1,c_30/0 ,c_31/2,c_32/4,c_33/3,c_34/1,c_35/0,c_36/0,c_37/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__A#,a__a#,a__b#,a__c#,a__d#,a__f#,a__g#,a__h#,a__k# ,a__z#,mark#} and constructors {A,a,b,c,d,e,f,g,h,k,l,m,z} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,4,5,13,14,18} by application of Pre({2,3,4,5,13,14,18}) = {1,6,8,9,11,12,15,16,17,19}. Here rules are labelled as follows: 1: a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) 2: a__a#() -> c_4(a__c#()) 3: a__a#() -> c_5(a__d#()) 4: a__b#() -> c_6(a__c#()) 5: a__b#() -> c_7(a__d#()) 6: a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) 7: a__g#(d(),X,X) -> c_17(a__A#()) 8: a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) 9: a__z#(e(),X) -> c_24(mark#(X)) 10: mark#(A()) -> c_25(a__A#()) 11: mark#(a()) -> c_26(a__a#()) 12: mark#(b()) -> c_27(a__b#()) 13: mark#(c()) -> c_28(a__c#()) 14: mark#(d()) -> c_29(a__d#()) 15: mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) 16: mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) 17: mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 18: mark#(k()) -> c_34(a__k#()) 19: mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) 20: a__A#() -> c_1() 21: a__a#() -> c_3() 22: a__b#() -> c_8() 23: a__c#() -> c_9() 24: a__c#() -> c_10() 25: a__c#() -> c_11() 26: a__d#() -> c_12() 27: a__d#() -> c_13() 28: a__f#(X) -> c_15() 29: a__g#(X1,X2,X3) -> c_16() 30: a__h#(X1,X2) -> c_19() 31: a__k#() -> c_20() 32: a__k#() -> c_21() 33: a__k#() -> c_22() 34: a__z#(X1,X2) -> c_23() 35: mark#(e()) -> c_30() 36: mark#(l()) -> c_35() 37: mark#(m()) -> c_36() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) a__g#(d(),X,X) -> c_17(a__A#()) a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) a__z#(e(),X) -> c_24(mark#(X)) mark#(A()) -> c_25(a__A#()) mark#(a()) -> c_26(a__a#()) mark#(b()) -> c_27(a__b#()) mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) - Weak DPs: a__A#() -> c_1() a__a#() -> c_3() a__a#() -> c_4(a__c#()) a__a#() -> c_5(a__d#()) a__b#() -> c_6(a__c#()) a__b#() -> c_7(a__d#()) a__b#() -> c_8() a__c#() -> c_9() a__c#() -> c_10() a__c#() -> c_11() a__d#() -> c_12() a__d#() -> c_13() a__f#(X) -> c_15() a__g#(X1,X2,X3) -> c_16() a__h#(X1,X2) -> c_19() a__k#() -> c_20() a__k#() -> c_21() a__k#() -> c_22() a__z#(X1,X2) -> c_23() mark#(c()) -> c_28(a__c#()) mark#(d()) -> c_29(a__d#()) mark#(e()) -> c_30() mark#(k()) -> c_34(a__k#()) mark#(l()) -> c_35() mark#(m()) -> c_36() - Weak TRS: a__A() -> A() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__a() -> a() a__a() -> a__c() a__a() -> a__d() a__b() -> a__c() a__b() -> a__d() a__b() -> b() a__c() -> c() a__c() -> e() a__c() -> l() a__d() -> d() a__d() -> m() a__f(X) -> a__z(mark(X),X) a__f(X) -> f(X) a__g(X1,X2,X3) -> g(X1,X2,X3) a__g(d(),X,X) -> a__A() a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__h(X1,X2) -> h(X1,X2) a__k() -> k() a__k() -> l() a__k() -> m() a__z(X1,X2) -> z(X1,X2) a__z(e(),X) -> mark(X) mark(A()) -> a__A() mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(e()) -> e() mark(f(X)) -> a__f(mark(X)) mark(g(X1,X2,X3)) -> a__g(mark(X1),mark(X2),mark(X3)) mark(h(X1,X2)) -> a__h(mark(X1),mark(X2)) mark(k()) -> a__k() mark(l()) -> l() mark(m()) -> m() mark(z(X1,X2)) -> a__z(mark(X1),X2) - Signature: {a__A/0,a__a/0,a__b/0,a__c/0,a__d/0,a__f/1,a__g/3,a__h/2,a__k/0,a__z/2,mark/1,a__A#/0,a__a#/0,a__b#/0 ,a__c#/0,a__d#/0,a__f#/1,a__g#/3,a__h#/2,a__k#/0,a__z#/2,mark#/1} / {A/0,a/0,b/0,c/0,d/0,e/0,f/1,g/3,h/2,k/0 ,l/0,m/0,z/2,c_1/0,c_2/5,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/2,c_15/0 ,c_16/0,c_17/1,c_18/5,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1,c_30/0 ,c_31/2,c_32/4,c_33/3,c_34/1,c_35/0,c_36/0,c_37/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__A#,a__a#,a__b#,a__c#,a__d#,a__f#,a__g#,a__h#,a__k# ,a__z#,mark#} and constructors {A,a,b,c,d,e,f,g,h,k,l,m,z} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {7,8} by application of Pre({7,8}) = {2,4,5,9,10,11,12}. Here rules are labelled as follows: 1: a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) 2: a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) 3: a__g#(d(),X,X) -> c_17(a__A#()) 4: a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) 5: a__z#(e(),X) -> c_24(mark#(X)) 6: mark#(A()) -> c_25(a__A#()) 7: mark#(a()) -> c_26(a__a#()) 8: mark#(b()) -> c_27(a__b#()) 9: mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) 10: mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) 11: mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 12: mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) 13: a__A#() -> c_1() 14: a__a#() -> c_3() 15: a__a#() -> c_4(a__c#()) 16: a__a#() -> c_5(a__d#()) 17: a__b#() -> c_6(a__c#()) 18: a__b#() -> c_7(a__d#()) 19: a__b#() -> c_8() 20: a__c#() -> c_9() 21: a__c#() -> c_10() 22: a__c#() -> c_11() 23: a__d#() -> c_12() 24: a__d#() -> c_13() 25: a__f#(X) -> c_15() 26: a__g#(X1,X2,X3) -> c_16() 27: a__h#(X1,X2) -> c_19() 28: a__k#() -> c_20() 29: a__k#() -> c_21() 30: a__k#() -> c_22() 31: a__z#(X1,X2) -> c_23() 32: mark#(c()) -> c_28(a__c#()) 33: mark#(d()) -> c_29(a__d#()) 34: mark#(e()) -> c_30() 35: mark#(k()) -> c_34(a__k#()) 36: mark#(l()) -> c_35() 37: mark#(m()) -> c_36() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) a__g#(d(),X,X) -> c_17(a__A#()) a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) a__z#(e(),X) -> c_24(mark#(X)) mark#(A()) -> c_25(a__A#()) mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) - Weak DPs: a__A#() -> c_1() a__a#() -> c_3() a__a#() -> c_4(a__c#()) a__a#() -> c_5(a__d#()) a__b#() -> c_6(a__c#()) a__b#() -> c_7(a__d#()) a__b#() -> c_8() a__c#() -> c_9() a__c#() -> c_10() a__c#() -> c_11() a__d#() -> c_12() a__d#() -> c_13() a__f#(X) -> c_15() a__g#(X1,X2,X3) -> c_16() a__h#(X1,X2) -> c_19() a__k#() -> c_20() a__k#() -> c_21() a__k#() -> c_22() a__z#(X1,X2) -> c_23() mark#(a()) -> c_26(a__a#()) mark#(b()) -> c_27(a__b#()) mark#(c()) -> c_28(a__c#()) mark#(d()) -> c_29(a__d#()) mark#(e()) -> c_30() mark#(k()) -> c_34(a__k#()) mark#(l()) -> c_35() mark#(m()) -> c_36() - Weak TRS: a__A() -> A() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__a() -> a() a__a() -> a__c() a__a() -> a__d() a__b() -> a__c() a__b() -> a__d() a__b() -> b() a__c() -> c() a__c() -> e() a__c() -> l() a__d() -> d() a__d() -> m() a__f(X) -> a__z(mark(X),X) a__f(X) -> f(X) a__g(X1,X2,X3) -> g(X1,X2,X3) a__g(d(),X,X) -> a__A() a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__h(X1,X2) -> h(X1,X2) a__k() -> k() a__k() -> l() a__k() -> m() a__z(X1,X2) -> z(X1,X2) a__z(e(),X) -> mark(X) mark(A()) -> a__A() mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(e()) -> e() mark(f(X)) -> a__f(mark(X)) mark(g(X1,X2,X3)) -> a__g(mark(X1),mark(X2),mark(X3)) mark(h(X1,X2)) -> a__h(mark(X1),mark(X2)) mark(k()) -> a__k() mark(l()) -> l() mark(m()) -> m() mark(z(X1,X2)) -> a__z(mark(X1),X2) - Signature: {a__A/0,a__a/0,a__b/0,a__c/0,a__d/0,a__f/1,a__g/3,a__h/2,a__k/0,a__z/2,mark/1,a__A#/0,a__a#/0,a__b#/0 ,a__c#/0,a__d#/0,a__f#/1,a__g#/3,a__h#/2,a__k#/0,a__z#/2,mark#/1} / {A/0,a/0,b/0,c/0,d/0,e/0,f/1,g/3,h/2,k/0 ,l/0,m/0,z/2,c_1/0,c_2/5,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/2,c_15/0 ,c_16/0,c_17/1,c_18/5,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1,c_30/0 ,c_31/2,c_32/4,c_33/3,c_34/1,c_35/0,c_36/0,c_37/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__A#,a__a#,a__b#,a__c#,a__d#,a__f#,a__g#,a__h#,a__k# ,a__z#,mark#} and constructors {A,a,b,c,d,e,f,g,h,k,l,m,z} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) -->_5 a__b#() -> c_7(a__d#()):16 -->_5 a__b#() -> c_6(a__c#()):15 -->_3 a__a#() -> c_5(a__d#()):14 -->_3 a__a#() -> c_4(a__c#()):13 -->_1 a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()):4 -->_4 a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)):2 -->_2 a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)):2 -->_1 a__h#(X1,X2) -> c_19():25 -->_4 a__f#(X) -> c_15():23 -->_2 a__f#(X) -> c_15():23 -->_5 a__b#() -> c_8():17 -->_3 a__a#() -> c_3():12 2:S:a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) -->_2 mark#(k()) -> c_34(a__k#()):35 -->_2 mark#(d()) -> c_29(a__d#()):33 -->_2 mark#(c()) -> c_28(a__c#()):32 -->_2 mark#(b()) -> c_27(a__b#()):31 -->_2 mark#(a()) -> c_26(a__a#()):30 -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__z#(e(),X) -> c_24(mark#(X)):5 -->_2 mark#(m()) -> c_36():37 -->_2 mark#(l()) -> c_35():36 -->_2 mark#(e()) -> c_30():34 -->_1 a__z#(X1,X2) -> c_23():29 3:S:a__g#(d(),X,X) -> c_17(a__A#()) -->_1 a__A#() -> c_1():11 -->_1 a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()):1 4:S:a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) -->_3 mark#(k()) -> c_34(a__k#()):35 -->_2 mark#(k()) -> c_34(a__k#()):35 -->_3 mark#(d()) -> c_29(a__d#()):33 -->_2 mark#(d()) -> c_29(a__d#()):33 -->_3 mark#(c()) -> c_28(a__c#()):32 -->_2 mark#(c()) -> c_28(a__c#()):32 -->_3 mark#(b()) -> c_27(a__b#()):31 -->_2 mark#(b()) -> c_27(a__b#()):31 -->_3 mark#(a()) -> c_26(a__a#()):30 -->_2 mark#(a()) -> c_26(a__a#()):30 -->_3 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_3 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_3 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_3 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_3 mark#(A()) -> c_25(a__A#()):6 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_3 mark#(m()) -> c_36():37 -->_2 mark#(m()) -> c_36():37 -->_3 mark#(l()) -> c_35():36 -->_2 mark#(l()) -> c_35():36 -->_3 mark#(e()) -> c_30():34 -->_2 mark#(e()) -> c_30():34 -->_5 a__k#() -> c_22():28 -->_5 a__k#() -> c_21():27 -->_5 a__k#() -> c_20():26 -->_1 a__g#(X1,X2,X3) -> c_16():24 -->_4 a__f#(X) -> c_15():23 -->_1 a__g#(d(),X,X) -> c_17(a__A#()):3 -->_4 a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)):2 5:S:a__z#(e(),X) -> c_24(mark#(X)) -->_1 mark#(k()) -> c_34(a__k#()):35 -->_1 mark#(d()) -> c_29(a__d#()):33 -->_1 mark#(c()) -> c_28(a__c#()):32 -->_1 mark#(b()) -> c_27(a__b#()):31 -->_1 mark#(a()) -> c_26(a__a#()):30 -->_1 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_1 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_1 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_1 mark#(A()) -> c_25(a__A#()):6 -->_1 mark#(m()) -> c_36():37 -->_1 mark#(l()) -> c_35():36 -->_1 mark#(e()) -> c_30():34 6:S:mark#(A()) -> c_25(a__A#()) -->_1 a__A#() -> c_1():11 -->_1 a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()):1 7:S:mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) -->_2 mark#(k()) -> c_34(a__k#()):35 -->_2 mark#(d()) -> c_29(a__d#()):33 -->_2 mark#(c()) -> c_28(a__c#()):32 -->_2 mark#(b()) -> c_27(a__b#()):31 -->_2 mark#(a()) -> c_26(a__a#()):30 -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(m()) -> c_36():37 -->_2 mark#(l()) -> c_35():36 -->_2 mark#(e()) -> c_30():34 -->_1 a__f#(X) -> c_15():23 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)):2 8:S:mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) -->_4 mark#(k()) -> c_34(a__k#()):35 -->_3 mark#(k()) -> c_34(a__k#()):35 -->_2 mark#(k()) -> c_34(a__k#()):35 -->_4 mark#(d()) -> c_29(a__d#()):33 -->_3 mark#(d()) -> c_29(a__d#()):33 -->_2 mark#(d()) -> c_29(a__d#()):33 -->_4 mark#(c()) -> c_28(a__c#()):32 -->_3 mark#(c()) -> c_28(a__c#()):32 -->_2 mark#(c()) -> c_28(a__c#()):32 -->_4 mark#(b()) -> c_27(a__b#()):31 -->_3 mark#(b()) -> c_27(a__b#()):31 -->_2 mark#(b()) -> c_27(a__b#()):31 -->_4 mark#(a()) -> c_26(a__a#()):30 -->_3 mark#(a()) -> c_26(a__a#()):30 -->_2 mark#(a()) -> c_26(a__a#()):30 -->_4 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_3 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_4 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_3 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_4 mark#(m()) -> c_36():37 -->_3 mark#(m()) -> c_36():37 -->_2 mark#(m()) -> c_36():37 -->_4 mark#(l()) -> c_35():36 -->_3 mark#(l()) -> c_35():36 -->_2 mark#(l()) -> c_35():36 -->_4 mark#(e()) -> c_30():34 -->_3 mark#(e()) -> c_30():34 -->_2 mark#(e()) -> c_30():34 -->_1 a__g#(X1,X2,X3) -> c_16():24 -->_4 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_3 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_4 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_3 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_4 mark#(A()) -> c_25(a__A#()):6 -->_3 mark#(A()) -> c_25(a__A#()):6 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__g#(d(),X,X) -> c_17(a__A#()):3 9:S:mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(k()) -> c_34(a__k#()):35 -->_2 mark#(k()) -> c_34(a__k#()):35 -->_3 mark#(d()) -> c_29(a__d#()):33 -->_2 mark#(d()) -> c_29(a__d#()):33 -->_3 mark#(c()) -> c_28(a__c#()):32 -->_2 mark#(c()) -> c_28(a__c#()):32 -->_3 mark#(b()) -> c_27(a__b#()):31 -->_2 mark#(b()) -> c_27(a__b#()):31 -->_3 mark#(a()) -> c_26(a__a#()):30 -->_2 mark#(a()) -> c_26(a__a#()):30 -->_3 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_3 mark#(m()) -> c_36():37 -->_2 mark#(m()) -> c_36():37 -->_3 mark#(l()) -> c_35():36 -->_2 mark#(l()) -> c_35():36 -->_3 mark#(e()) -> c_30():34 -->_2 mark#(e()) -> c_30():34 -->_1 a__h#(X1,X2) -> c_19():25 -->_3 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_3 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_3 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_3 mark#(A()) -> c_25(a__A#()):6 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()):4 10:S:mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) -->_2 mark#(k()) -> c_34(a__k#()):35 -->_2 mark#(d()) -> c_29(a__d#()):33 -->_2 mark#(c()) -> c_28(a__c#()):32 -->_2 mark#(b()) -> c_27(a__b#()):31 -->_2 mark#(a()) -> c_26(a__a#()):30 -->_2 mark#(m()) -> c_36():37 -->_2 mark#(l()) -> c_35():36 -->_2 mark#(e()) -> c_30():34 -->_1 a__z#(X1,X2) -> c_23():29 -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__z#(e(),X) -> c_24(mark#(X)):5 11:W:a__A#() -> c_1() 12:W:a__a#() -> c_3() 13:W:a__a#() -> c_4(a__c#()) -->_1 a__c#() -> c_11():20 -->_1 a__c#() -> c_10():19 -->_1 a__c#() -> c_9():18 14:W:a__a#() -> c_5(a__d#()) -->_1 a__d#() -> c_13():22 -->_1 a__d#() -> c_12():21 15:W:a__b#() -> c_6(a__c#()) -->_1 a__c#() -> c_11():20 -->_1 a__c#() -> c_10():19 -->_1 a__c#() -> c_9():18 16:W:a__b#() -> c_7(a__d#()) -->_1 a__d#() -> c_13():22 -->_1 a__d#() -> c_12():21 17:W:a__b#() -> c_8() 18:W:a__c#() -> c_9() 19:W:a__c#() -> c_10() 20:W:a__c#() -> c_11() 21:W:a__d#() -> c_12() 22:W:a__d#() -> c_13() 23:W:a__f#(X) -> c_15() 24:W:a__g#(X1,X2,X3) -> c_16() 25:W:a__h#(X1,X2) -> c_19() 26:W:a__k#() -> c_20() 27:W:a__k#() -> c_21() 28:W:a__k#() -> c_22() 29:W:a__z#(X1,X2) -> c_23() 30:W:mark#(a()) -> c_26(a__a#()) -->_1 a__a#() -> c_5(a__d#()):14 -->_1 a__a#() -> c_4(a__c#()):13 -->_1 a__a#() -> c_3():12 31:W:mark#(b()) -> c_27(a__b#()) -->_1 a__b#() -> c_8():17 -->_1 a__b#() -> c_7(a__d#()):16 -->_1 a__b#() -> c_6(a__c#()):15 32:W:mark#(c()) -> c_28(a__c#()) -->_1 a__c#() -> c_11():20 -->_1 a__c#() -> c_10():19 -->_1 a__c#() -> c_9():18 33:W:mark#(d()) -> c_29(a__d#()) -->_1 a__d#() -> c_13():22 -->_1 a__d#() -> c_12():21 34:W:mark#(e()) -> c_30() 35:W:mark#(k()) -> c_34(a__k#()) -->_1 a__k#() -> c_22():28 -->_1 a__k#() -> c_21():27 -->_1 a__k#() -> c_20():26 36:W:mark#(l()) -> c_35() 37:W:mark#(m()) -> c_36() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 11: a__A#() -> c_1() 23: a__f#(X) -> c_15() 24: a__g#(X1,X2,X3) -> c_16() 25: a__h#(X1,X2) -> c_19() 29: a__z#(X1,X2) -> c_23() 34: mark#(e()) -> c_30() 36: mark#(l()) -> c_35() 37: mark#(m()) -> c_36() 30: mark#(a()) -> c_26(a__a#()) 12: a__a#() -> c_3() 31: mark#(b()) -> c_27(a__b#()) 17: a__b#() -> c_8() 32: mark#(c()) -> c_28(a__c#()) 33: mark#(d()) -> c_29(a__d#()) 35: mark#(k()) -> c_34(a__k#()) 26: a__k#() -> c_20() 27: a__k#() -> c_21() 28: a__k#() -> c_22() 13: a__a#() -> c_4(a__c#()) 14: a__a#() -> c_5(a__d#()) 15: a__b#() -> c_6(a__c#()) 18: a__c#() -> c_9() 19: a__c#() -> c_10() 20: a__c#() -> c_11() 16: a__b#() -> c_7(a__d#()) 21: a__d#() -> c_12() 22: a__d#() -> c_13() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) a__g#(d(),X,X) -> c_17(a__A#()) a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) a__z#(e(),X) -> c_24(mark#(X)) mark#(A()) -> c_25(a__A#()) mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) - Weak TRS: a__A() -> A() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__a() -> a() a__a() -> a__c() a__a() -> a__d() a__b() -> a__c() a__b() -> a__d() a__b() -> b() a__c() -> c() a__c() -> e() a__c() -> l() a__d() -> d() a__d() -> m() a__f(X) -> a__z(mark(X),X) a__f(X) -> f(X) a__g(X1,X2,X3) -> g(X1,X2,X3) a__g(d(),X,X) -> a__A() a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__h(X1,X2) -> h(X1,X2) a__k() -> k() a__k() -> l() a__k() -> m() a__z(X1,X2) -> z(X1,X2) a__z(e(),X) -> mark(X) mark(A()) -> a__A() mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(e()) -> e() mark(f(X)) -> a__f(mark(X)) mark(g(X1,X2,X3)) -> a__g(mark(X1),mark(X2),mark(X3)) mark(h(X1,X2)) -> a__h(mark(X1),mark(X2)) mark(k()) -> a__k() mark(l()) -> l() mark(m()) -> m() mark(z(X1,X2)) -> a__z(mark(X1),X2) - Signature: {a__A/0,a__a/0,a__b/0,a__c/0,a__d/0,a__f/1,a__g/3,a__h/2,a__k/0,a__z/2,mark/1,a__A#/0,a__a#/0,a__b#/0 ,a__c#/0,a__d#/0,a__f#/1,a__g#/3,a__h#/2,a__k#/0,a__z#/2,mark#/1} / {A/0,a/0,b/0,c/0,d/0,e/0,f/1,g/3,h/2,k/0 ,l/0,m/0,z/2,c_1/0,c_2/5,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/2,c_15/0 ,c_16/0,c_17/1,c_18/5,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1,c_30/0 ,c_31/2,c_32/4,c_33/3,c_34/1,c_35/0,c_36/0,c_37/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__A#,a__a#,a__b#,a__c#,a__d#,a__f#,a__g#,a__h#,a__k# ,a__z#,mark#} and constructors {A,a,b,c,d,e,f,g,h,k,l,m,z} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()) -->_1 a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()):4 -->_4 a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)):2 -->_2 a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)):2 2:S:a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__z#(e(),X) -> c_24(mark#(X)):5 3:S:a__g#(d(),X,X) -> c_17(a__A#()) -->_1 a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()):1 4:S:a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()) -->_3 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_3 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_3 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_3 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_3 mark#(A()) -> c_25(a__A#()):6 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__g#(d(),X,X) -> c_17(a__A#()):3 -->_4 a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)):2 5:S:a__z#(e(),X) -> c_24(mark#(X)) -->_1 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_1 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_1 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_1 mark#(A()) -> c_25(a__A#()):6 6:S:mark#(A()) -> c_25(a__A#()) -->_1 a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__a#(),a__f#(a__b()),a__b#()):1 7:S:mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)):2 8:S:mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) -->_4 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_3 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_4 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_3 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_4 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_3 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_4 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_3 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_4 mark#(A()) -> c_25(a__A#()):6 -->_3 mark#(A()) -> c_25(a__A#()):6 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__g#(d(),X,X) -> c_17(a__A#()):3 9:S:mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_3 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_3 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_3 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_3 mark#(A()) -> c_25(a__A#()):6 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k()),a__k#()):4 10:S:mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) -->_2 mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)):10 -->_2 mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)):8 -->_2 mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)):7 -->_2 mark#(A()) -> c_25(a__A#()):6 -->_1 a__z#(e(),X) -> c_24(mark#(X)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__f#(a__b())) a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k())) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: a__A#() -> c_2(a__h#(a__f(a__a()),a__f(a__b())),a__f#(a__a()),a__f#(a__b())) a__f#(X) -> c_14(a__z#(mark(X),X),mark#(X)) a__g#(d(),X,X) -> c_17(a__A#()) a__h#(X,X) -> c_18(a__g#(mark(X),mark(X),a__f(a__k())),mark#(X),mark#(X),a__f#(a__k())) a__z#(e(),X) -> c_24(mark#(X)) mark#(A()) -> c_25(a__A#()) mark#(f(X)) -> c_31(a__f#(mark(X)),mark#(X)) mark#(g(X1,X2,X3)) -> c_32(a__g#(mark(X1),mark(X2),mark(X3)),mark#(X1),mark#(X2),mark#(X3)) mark#(h(X1,X2)) -> c_33(a__h#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(z(X1,X2)) -> c_37(a__z#(mark(X1),X2),mark#(X1)) - Weak TRS: a__A() -> A() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__a() -> a() a__a() -> a__c() a__a() -> a__d() a__b() -> a__c() a__b() -> a__d() a__b() -> b() a__c() -> c() a__c() -> e() a__c() -> l() a__d() -> d() a__d() -> m() a__f(X) -> a__z(mark(X),X) a__f(X) -> f(X) a__g(X1,X2,X3) -> g(X1,X2,X3) a__g(d(),X,X) -> a__A() a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__h(X1,X2) -> h(X1,X2) a__k() -> k() a__k() -> l() a__k() -> m() a__z(X1,X2) -> z(X1,X2) a__z(e(),X) -> mark(X) mark(A()) -> a__A() mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(e()) -> e() mark(f(X)) -> a__f(mark(X)) mark(g(X1,X2,X3)) -> a__g(mark(X1),mark(X2),mark(X3)) mark(h(X1,X2)) -> a__h(mark(X1),mark(X2)) mark(k()) -> a__k() mark(l()) -> l() mark(m()) -> m() mark(z(X1,X2)) -> a__z(mark(X1),X2) - Signature: {a__A/0,a__a/0,a__b/0,a__c/0,a__d/0,a__f/1,a__g/3,a__h/2,a__k/0,a__z/2,mark/1,a__A#/0,a__a#/0,a__b#/0 ,a__c#/0,a__d#/0,a__f#/1,a__g#/3,a__h#/2,a__k#/0,a__z#/2,mark#/1} / {A/0,a/0,b/0,c/0,d/0,e/0,f/1,g/3,h/2,k/0 ,l/0,m/0,z/2,c_1/0,c_2/3,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/2,c_15/0 ,c_16/0,c_17/1,c_18/4,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1,c_30/0 ,c_31/2,c_32/4,c_33/3,c_34/1,c_35/0,c_36/0,c_37/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__A#,a__a#,a__b#,a__c#,a__d#,a__f#,a__g#,a__h#,a__k# ,a__z#,mark#} and constructors {A,a,b,c,d,e,f,g,h,k,l,m,z} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE