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