MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
active(cons(X1,X2)) -> cons(active(X1),X2)
active(f(X)) -> f(active(X))
active(f(X)) -> mark(cons(X,f(g(X))))
active(g(X)) -> g(active(X))
active(g(0())) -> mark(s(0()))
active(g(s(X))) -> mark(s(s(g(X))))
active(s(X)) -> s(active(X))
active(sel(X1,X2)) -> sel(X1,active(X2))
active(sel(X1,X2)) -> sel(active(X1),X2)
active(sel(0(),cons(X,Y))) -> mark(X)
active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
f(mark(X)) -> mark(f(X))
f(ok(X)) -> ok(f(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
proper(s(X)) -> s(proper(X))
proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
sel(X1,mark(X2)) -> mark(sel(X1,X2))
sel(mark(X1),X2) -> mark(sel(X1,X2))
sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
- Signature:
{active/1,cons/2,f/1,g/1,proper/1,s/1,sel/2,top/1} / {0/0,mark/1,ok/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {active,cons,f,g,proper,s,sel,top} and constructors {0
,mark,ok}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1))
active#(f(X)) -> c_2(f#(active(X)),active#(X))
active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X))
active#(g(X)) -> c_4(g#(active(X)),active#(X))
active#(g(0())) -> c_5(s#(0()))
active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X))
active#(s(X)) -> c_7(s#(active(X)),active#(X))
active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2))
active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1))
active#(sel(0(),cons(X,Y))) -> c_10()
active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z))
cons#(mark(X1),X2) -> c_12(cons#(X1,X2))
cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2))
f#(mark(X)) -> c_14(f#(X))
f#(ok(X)) -> c_15(f#(X))
g#(mark(X)) -> c_16(g#(X))
g#(ok(X)) -> c_17(g#(X))
proper#(0()) -> c_18()
proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
proper#(f(X)) -> c_20(f#(proper(X)),proper#(X))
proper#(g(X)) -> c_21(g#(proper(X)),proper#(X))
proper#(s(X)) -> c_22(s#(proper(X)),proper#(X))
proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
s#(mark(X)) -> c_24(s#(X))
s#(ok(X)) -> c_25(s#(X))
sel#(X1,mark(X2)) -> c_26(sel#(X1,X2))
sel#(mark(X1),X2) -> c_27(sel#(X1,X2))
sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2))
top#(mark(X)) -> c_29(top#(proper(X)),proper#(X))
top#(ok(X)) -> c_30(top#(active(X)),active#(X))
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1))
active#(f(X)) -> c_2(f#(active(X)),active#(X))
active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X))
active#(g(X)) -> c_4(g#(active(X)),active#(X))
active#(g(0())) -> c_5(s#(0()))
active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X))
active#(s(X)) -> c_7(s#(active(X)),active#(X))
active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2))
active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1))
active#(sel(0(),cons(X,Y))) -> c_10()
active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z))
cons#(mark(X1),X2) -> c_12(cons#(X1,X2))
cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2))
f#(mark(X)) -> c_14(f#(X))
f#(ok(X)) -> c_15(f#(X))
g#(mark(X)) -> c_16(g#(X))
g#(ok(X)) -> c_17(g#(X))
proper#(0()) -> c_18()
proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
proper#(f(X)) -> c_20(f#(proper(X)),proper#(X))
proper#(g(X)) -> c_21(g#(proper(X)),proper#(X))
proper#(s(X)) -> c_22(s#(proper(X)),proper#(X))
proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
s#(mark(X)) -> c_24(s#(X))
s#(ok(X)) -> c_25(s#(X))
sel#(X1,mark(X2)) -> c_26(sel#(X1,X2))
sel#(mark(X1),X2) -> c_27(sel#(X1,X2))
sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2))
top#(mark(X)) -> c_29(top#(proper(X)),proper#(X))
top#(ok(X)) -> c_30(top#(active(X)),active#(X))
- Weak TRS:
active(cons(X1,X2)) -> cons(active(X1),X2)
active(f(X)) -> f(active(X))
active(f(X)) -> mark(cons(X,f(g(X))))
active(g(X)) -> g(active(X))
active(g(0())) -> mark(s(0()))
active(g(s(X))) -> mark(s(s(g(X))))
active(s(X)) -> s(active(X))
active(sel(X1,X2)) -> sel(X1,active(X2))
active(sel(X1,X2)) -> sel(active(X1),X2)
active(sel(0(),cons(X,Y))) -> mark(X)
active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
f(mark(X)) -> mark(f(X))
f(ok(X)) -> ok(f(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
proper(s(X)) -> s(proper(X))
proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
sel(X1,mark(X2)) -> mark(sel(X1,X2))
sel(mark(X1),X2) -> mark(sel(X1,X2))
sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
- Signature:
{active/1,cons/2,f/1,g/1,proper/1,s/1,sel/2,top/1,active#/1,cons#/2,f#/1,g#/1,proper#/1,s#/1,sel#/2
,top#/1} / {0/0,mark/1,ok/1,c_1/2,c_2/2,c_3/3,c_4/2,c_5/1,c_6/3,c_7/2,c_8/2,c_9/2,c_10/0,c_11/1,c_12/1
,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/0,c_19/3,c_20/2,c_21/2,c_22/2,c_23/3,c_24/1,c_25/1,c_26/1,c_27/1
,c_28/1,c_29/2,c_30/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {active#,cons#,f#,g#,proper#,s#,sel#
,top#} and constructors {0,mark,ok}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
active(cons(X1,X2)) -> cons(active(X1),X2)
active(f(X)) -> f(active(X))
active(f(X)) -> mark(cons(X,f(g(X))))
active(g(X)) -> g(active(X))
active(g(0())) -> mark(s(0()))
active(g(s(X))) -> mark(s(s(g(X))))
active(s(X)) -> s(active(X))
active(sel(X1,X2)) -> sel(X1,active(X2))
active(sel(X1,X2)) -> sel(active(X1),X2)
active(sel(0(),cons(X,Y))) -> mark(X)
active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
f(mark(X)) -> mark(f(X))
f(ok(X)) -> ok(f(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
proper(s(X)) -> s(proper(X))
proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
sel(X1,mark(X2)) -> mark(sel(X1,X2))
sel(mark(X1),X2) -> mark(sel(X1,X2))
sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1))
active#(f(X)) -> c_2(f#(active(X)),active#(X))
active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X))
active#(g(X)) -> c_4(g#(active(X)),active#(X))
active#(g(0())) -> c_5(s#(0()))
active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X))
active#(s(X)) -> c_7(s#(active(X)),active#(X))
active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2))
active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1))
active#(sel(0(),cons(X,Y))) -> c_10()
active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z))
cons#(mark(X1),X2) -> c_12(cons#(X1,X2))
cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2))
f#(mark(X)) -> c_14(f#(X))
f#(ok(X)) -> c_15(f#(X))
g#(mark(X)) -> c_16(g#(X))
g#(ok(X)) -> c_17(g#(X))
proper#(0()) -> c_18()
proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
proper#(f(X)) -> c_20(f#(proper(X)),proper#(X))
proper#(g(X)) -> c_21(g#(proper(X)),proper#(X))
proper#(s(X)) -> c_22(s#(proper(X)),proper#(X))
proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
s#(mark(X)) -> c_24(s#(X))
s#(ok(X)) -> c_25(s#(X))
sel#(X1,mark(X2)) -> c_26(sel#(X1,X2))
sel#(mark(X1),X2) -> c_27(sel#(X1,X2))
sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2))
top#(mark(X)) -> c_29(top#(proper(X)),proper#(X))
top#(ok(X)) -> c_30(top#(active(X)),active#(X))
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1))
active#(f(X)) -> c_2(f#(active(X)),active#(X))
active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X))
active#(g(X)) -> c_4(g#(active(X)),active#(X))
active#(g(0())) -> c_5(s#(0()))
active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X))
active#(s(X)) -> c_7(s#(active(X)),active#(X))
active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2))
active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1))
active#(sel(0(),cons(X,Y))) -> c_10()
active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z))
cons#(mark(X1),X2) -> c_12(cons#(X1,X2))
cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2))
f#(mark(X)) -> c_14(f#(X))
f#(ok(X)) -> c_15(f#(X))
g#(mark(X)) -> c_16(g#(X))
g#(ok(X)) -> c_17(g#(X))
proper#(0()) -> c_18()
proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
proper#(f(X)) -> c_20(f#(proper(X)),proper#(X))
proper#(g(X)) -> c_21(g#(proper(X)),proper#(X))
proper#(s(X)) -> c_22(s#(proper(X)),proper#(X))
proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
s#(mark(X)) -> c_24(s#(X))
s#(ok(X)) -> c_25(s#(X))
sel#(X1,mark(X2)) -> c_26(sel#(X1,X2))
sel#(mark(X1),X2) -> c_27(sel#(X1,X2))
sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2))
top#(mark(X)) -> c_29(top#(proper(X)),proper#(X))
top#(ok(X)) -> c_30(top#(active(X)),active#(X))
- Weak TRS:
active(cons(X1,X2)) -> cons(active(X1),X2)
active(f(X)) -> f(active(X))
active(f(X)) -> mark(cons(X,f(g(X))))
active(g(X)) -> g(active(X))
active(g(0())) -> mark(s(0()))
active(g(s(X))) -> mark(s(s(g(X))))
active(s(X)) -> s(active(X))
active(sel(X1,X2)) -> sel(X1,active(X2))
active(sel(X1,X2)) -> sel(active(X1),X2)
active(sel(0(),cons(X,Y))) -> mark(X)
active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
f(mark(X)) -> mark(f(X))
f(ok(X)) -> ok(f(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
proper(s(X)) -> s(proper(X))
proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
sel(X1,mark(X2)) -> mark(sel(X1,X2))
sel(mark(X1),X2) -> mark(sel(X1,X2))
sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
- Signature:
{active/1,cons/2,f/1,g/1,proper/1,s/1,sel/2,top/1,active#/1,cons#/2,f#/1,g#/1,proper#/1,s#/1,sel#/2
,top#/1} / {0/0,mark/1,ok/1,c_1/2,c_2/2,c_3/3,c_4/2,c_5/1,c_6/3,c_7/2,c_8/2,c_9/2,c_10/0,c_11/1,c_12/1
,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/0,c_19/3,c_20/2,c_21/2,c_22/2,c_23/3,c_24/1,c_25/1,c_26/1,c_27/1
,c_28/1,c_29/2,c_30/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {active#,cons#,f#,g#,proper#,s#,sel#
,top#} and constructors {0,mark,ok}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{5,10,18}
by application of
Pre({5,10,18}) = {1,2,4,7,8,9,19,20,21,22,23,29,30}.
Here rules are labelled as follows:
1: active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1))
2: active#(f(X)) -> c_2(f#(active(X)),active#(X))
3: active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X))
4: active#(g(X)) -> c_4(g#(active(X)),active#(X))
5: active#(g(0())) -> c_5(s#(0()))
6: active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X))
7: active#(s(X)) -> c_7(s#(active(X)),active#(X))
8: active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2))
9: active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1))
10: active#(sel(0(),cons(X,Y))) -> c_10()
11: active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z))
12: cons#(mark(X1),X2) -> c_12(cons#(X1,X2))
13: cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2))
14: f#(mark(X)) -> c_14(f#(X))
15: f#(ok(X)) -> c_15(f#(X))
16: g#(mark(X)) -> c_16(g#(X))
17: g#(ok(X)) -> c_17(g#(X))
18: proper#(0()) -> c_18()
19: proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
20: proper#(f(X)) -> c_20(f#(proper(X)),proper#(X))
21: proper#(g(X)) -> c_21(g#(proper(X)),proper#(X))
22: proper#(s(X)) -> c_22(s#(proper(X)),proper#(X))
23: proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
24: s#(mark(X)) -> c_24(s#(X))
25: s#(ok(X)) -> c_25(s#(X))
26: sel#(X1,mark(X2)) -> c_26(sel#(X1,X2))
27: sel#(mark(X1),X2) -> c_27(sel#(X1,X2))
28: sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2))
29: top#(mark(X)) -> c_29(top#(proper(X)),proper#(X))
30: top#(ok(X)) -> c_30(top#(active(X)),active#(X))
* Step 4: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1))
active#(f(X)) -> c_2(f#(active(X)),active#(X))
active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X))
active#(g(X)) -> c_4(g#(active(X)),active#(X))
active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X))
active#(s(X)) -> c_7(s#(active(X)),active#(X))
active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2))
active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1))
active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z))
cons#(mark(X1),X2) -> c_12(cons#(X1,X2))
cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2))
f#(mark(X)) -> c_14(f#(X))
f#(ok(X)) -> c_15(f#(X))
g#(mark(X)) -> c_16(g#(X))
g#(ok(X)) -> c_17(g#(X))
proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
proper#(f(X)) -> c_20(f#(proper(X)),proper#(X))
proper#(g(X)) -> c_21(g#(proper(X)),proper#(X))
proper#(s(X)) -> c_22(s#(proper(X)),proper#(X))
proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
s#(mark(X)) -> c_24(s#(X))
s#(ok(X)) -> c_25(s#(X))
sel#(X1,mark(X2)) -> c_26(sel#(X1,X2))
sel#(mark(X1),X2) -> c_27(sel#(X1,X2))
sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2))
top#(mark(X)) -> c_29(top#(proper(X)),proper#(X))
top#(ok(X)) -> c_30(top#(active(X)),active#(X))
- Weak DPs:
active#(g(0())) -> c_5(s#(0()))
active#(sel(0(),cons(X,Y))) -> c_10()
proper#(0()) -> c_18()
- Weak TRS:
active(cons(X1,X2)) -> cons(active(X1),X2)
active(f(X)) -> f(active(X))
active(f(X)) -> mark(cons(X,f(g(X))))
active(g(X)) -> g(active(X))
active(g(0())) -> mark(s(0()))
active(g(s(X))) -> mark(s(s(g(X))))
active(s(X)) -> s(active(X))
active(sel(X1,X2)) -> sel(X1,active(X2))
active(sel(X1,X2)) -> sel(active(X1),X2)
active(sel(0(),cons(X,Y))) -> mark(X)
active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
f(mark(X)) -> mark(f(X))
f(ok(X)) -> ok(f(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
proper(s(X)) -> s(proper(X))
proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
sel(X1,mark(X2)) -> mark(sel(X1,X2))
sel(mark(X1),X2) -> mark(sel(X1,X2))
sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
- Signature:
{active/1,cons/2,f/1,g/1,proper/1,s/1,sel/2,top/1,active#/1,cons#/2,f#/1,g#/1,proper#/1,s#/1,sel#/2
,top#/1} / {0/0,mark/1,ok/1,c_1/2,c_2/2,c_3/3,c_4/2,c_5/1,c_6/3,c_7/2,c_8/2,c_9/2,c_10/0,c_11/1,c_12/1
,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/0,c_19/3,c_20/2,c_21/2,c_22/2,c_23/3,c_24/1,c_25/1,c_26/1,c_27/1
,c_28/1,c_29/2,c_30/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {active#,cons#,f#,g#,proper#,s#,sel#
,top#} and constructors {0,mark,ok}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1))
-->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):11
-->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):10
-->_2 active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z)):9
-->_2 active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1)):8
-->_2 active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2)):7
-->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):6
-->_2 active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X)):5
-->_2 active#(g(X)) -> c_4(g#(active(X)),active#(X)):4
-->_2 active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X)):3
-->_2 active#(f(X)) -> c_2(f#(active(X)),active#(X)):2
-->_2 active#(sel(0(),cons(X,Y))) -> c_10():29
-->_2 active#(g(0())) -> c_5(s#(0())):28
-->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1
2:S:active#(f(X)) -> c_2(f#(active(X)),active#(X))
-->_1 f#(ok(X)) -> c_15(f#(X)):13
-->_1 f#(mark(X)) -> c_14(f#(X)):12
-->_2 active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z)):9
-->_2 active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1)):8
-->_2 active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2)):7
-->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):6
-->_2 active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X)):5
-->_2 active#(g(X)) -> c_4(g#(active(X)),active#(X)):4
-->_2 active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X)):3
-->_2 active#(sel(0(),cons(X,Y))) -> c_10():29
-->_2 active#(g(0())) -> c_5(s#(0())):28
-->_2 active#(f(X)) -> c_2(f#(active(X)),active#(X)):2
-->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1
3:S:active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X))
-->_3 g#(ok(X)) -> c_17(g#(X)):15
-->_3 g#(mark(X)) -> c_16(g#(X)):14
-->_2 f#(ok(X)) -> c_15(f#(X)):13
-->_2 f#(mark(X)) -> c_14(f#(X)):12
-->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):11
-->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):10
4:S:active#(g(X)) -> c_4(g#(active(X)),active#(X))
-->_1 g#(ok(X)) -> c_17(g#(X)):15
-->_1 g#(mark(X)) -> c_16(g#(X)):14
-->_2 active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z)):9
-->_2 active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1)):8
-->_2 active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2)):7
-->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):6
-->_2 active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X)):5
-->_2 active#(sel(0(),cons(X,Y))) -> c_10():29
-->_2 active#(g(0())) -> c_5(s#(0())):28
-->_2 active#(g(X)) -> c_4(g#(active(X)),active#(X)):4
-->_2 active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X)):3
-->_2 active#(f(X)) -> c_2(f#(active(X)),active#(X)):2
-->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1
5:S:active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X))
-->_2 s#(ok(X)) -> c_25(s#(X)):22
-->_1 s#(ok(X)) -> c_25(s#(X)):22
-->_2 s#(mark(X)) -> c_24(s#(X)):21
-->_1 s#(mark(X)) -> c_24(s#(X)):21
-->_3 g#(ok(X)) -> c_17(g#(X)):15
-->_3 g#(mark(X)) -> c_16(g#(X)):14
6:S:active#(s(X)) -> c_7(s#(active(X)),active#(X))
-->_1 s#(ok(X)) -> c_25(s#(X)):22
-->_1 s#(mark(X)) -> c_24(s#(X)):21
-->_2 active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z)):9
-->_2 active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1)):8
-->_2 active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2)):7
-->_2 active#(sel(0(),cons(X,Y))) -> c_10():29
-->_2 active#(g(0())) -> c_5(s#(0())):28
-->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):6
-->_2 active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X)):5
-->_2 active#(g(X)) -> c_4(g#(active(X)),active#(X)):4
-->_2 active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X)):3
-->_2 active#(f(X)) -> c_2(f#(active(X)),active#(X)):2
-->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1
7:S:active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2))
-->_1 sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2)):25
-->_1 sel#(mark(X1),X2) -> c_27(sel#(X1,X2)):24
-->_1 sel#(X1,mark(X2)) -> c_26(sel#(X1,X2)):23
-->_2 active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z)):9
-->_2 active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1)):8
-->_2 active#(sel(0(),cons(X,Y))) -> c_10():29
-->_2 active#(g(0())) -> c_5(s#(0())):28
-->_2 active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2)):7
-->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):6
-->_2 active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X)):5
-->_2 active#(g(X)) -> c_4(g#(active(X)),active#(X)):4
-->_2 active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X)):3
-->_2 active#(f(X)) -> c_2(f#(active(X)),active#(X)):2
-->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1
8:S:active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1))
-->_1 sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2)):25
-->_1 sel#(mark(X1),X2) -> c_27(sel#(X1,X2)):24
-->_1 sel#(X1,mark(X2)) -> c_26(sel#(X1,X2)):23
-->_2 active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z)):9
-->_2 active#(sel(0(),cons(X,Y))) -> c_10():29
-->_2 active#(g(0())) -> c_5(s#(0())):28
-->_2 active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1)):8
-->_2 active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2)):7
-->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):6
-->_2 active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X)):5
-->_2 active#(g(X)) -> c_4(g#(active(X)),active#(X)):4
-->_2 active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X)):3
-->_2 active#(f(X)) -> c_2(f#(active(X)),active#(X)):2
-->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1
9:S:active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z))
-->_1 sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2)):25
-->_1 sel#(mark(X1),X2) -> c_27(sel#(X1,X2)):24
-->_1 sel#(X1,mark(X2)) -> c_26(sel#(X1,X2)):23
10:S:cons#(mark(X1),X2) -> c_12(cons#(X1,X2))
-->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):11
-->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):10
11:S:cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2))
-->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):11
-->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):10
12:S:f#(mark(X)) -> c_14(f#(X))
-->_1 f#(ok(X)) -> c_15(f#(X)):13
-->_1 f#(mark(X)) -> c_14(f#(X)):12
13:S:f#(ok(X)) -> c_15(f#(X))
-->_1 f#(ok(X)) -> c_15(f#(X)):13
-->_1 f#(mark(X)) -> c_14(f#(X)):12
14:S:g#(mark(X)) -> c_16(g#(X))
-->_1 g#(ok(X)) -> c_17(g#(X)):15
-->_1 g#(mark(X)) -> c_16(g#(X)):14
15:S:g#(ok(X)) -> c_17(g#(X))
-->_1 g#(ok(X)) -> c_17(g#(X)):15
-->_1 g#(mark(X)) -> c_16(g#(X)):14
16:S:proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
-->_3 proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20
-->_2 proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20
-->_3 proper#(s(X)) -> c_22(s#(proper(X)),proper#(X)):19
-->_2 proper#(s(X)) -> c_22(s#(proper(X)),proper#(X)):19
-->_3 proper#(g(X)) -> c_21(g#(proper(X)),proper#(X)):18
-->_2 proper#(g(X)) -> c_21(g#(proper(X)),proper#(X)):18
-->_3 proper#(f(X)) -> c_20(f#(proper(X)),proper#(X)):17
-->_2 proper#(f(X)) -> c_20(f#(proper(X)),proper#(X)):17
-->_3 proper#(0()) -> c_18():30
-->_2 proper#(0()) -> c_18():30
-->_3 proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16
-->_2 proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16
-->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):11
-->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):10
17:S:proper#(f(X)) -> c_20(f#(proper(X)),proper#(X))
-->_2 proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20
-->_2 proper#(s(X)) -> c_22(s#(proper(X)),proper#(X)):19
-->_2 proper#(g(X)) -> c_21(g#(proper(X)),proper#(X)):18
-->_2 proper#(0()) -> c_18():30
-->_2 proper#(f(X)) -> c_20(f#(proper(X)),proper#(X)):17
-->_2 proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16
-->_1 f#(ok(X)) -> c_15(f#(X)):13
-->_1 f#(mark(X)) -> c_14(f#(X)):12
18:S:proper#(g(X)) -> c_21(g#(proper(X)),proper#(X))
-->_2 proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20
-->_2 proper#(s(X)) -> c_22(s#(proper(X)),proper#(X)):19
-->_2 proper#(0()) -> c_18():30
-->_2 proper#(g(X)) -> c_21(g#(proper(X)),proper#(X)):18
-->_2 proper#(f(X)) -> c_20(f#(proper(X)),proper#(X)):17
-->_2 proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16
-->_1 g#(ok(X)) -> c_17(g#(X)):15
-->_1 g#(mark(X)) -> c_16(g#(X)):14
19:S:proper#(s(X)) -> c_22(s#(proper(X)),proper#(X))
-->_1 s#(ok(X)) -> c_25(s#(X)):22
-->_1 s#(mark(X)) -> c_24(s#(X)):21
-->_2 proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20
-->_2 proper#(0()) -> c_18():30
-->_2 proper#(s(X)) -> c_22(s#(proper(X)),proper#(X)):19
-->_2 proper#(g(X)) -> c_21(g#(proper(X)),proper#(X)):18
-->_2 proper#(f(X)) -> c_20(f#(proper(X)),proper#(X)):17
-->_2 proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16
20:S:proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
-->_1 sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2)):25
-->_1 sel#(mark(X1),X2) -> c_27(sel#(X1,X2)):24
-->_1 sel#(X1,mark(X2)) -> c_26(sel#(X1,X2)):23
-->_3 proper#(0()) -> c_18():30
-->_2 proper#(0()) -> c_18():30
-->_3 proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20
-->_2 proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20
-->_3 proper#(s(X)) -> c_22(s#(proper(X)),proper#(X)):19
-->_2 proper#(s(X)) -> c_22(s#(proper(X)),proper#(X)):19
-->_3 proper#(g(X)) -> c_21(g#(proper(X)),proper#(X)):18
-->_2 proper#(g(X)) -> c_21(g#(proper(X)),proper#(X)):18
-->_3 proper#(f(X)) -> c_20(f#(proper(X)),proper#(X)):17
-->_2 proper#(f(X)) -> c_20(f#(proper(X)),proper#(X)):17
-->_3 proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16
-->_2 proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16
21:S:s#(mark(X)) -> c_24(s#(X))
-->_1 s#(ok(X)) -> c_25(s#(X)):22
-->_1 s#(mark(X)) -> c_24(s#(X)):21
22:S:s#(ok(X)) -> c_25(s#(X))
-->_1 s#(ok(X)) -> c_25(s#(X)):22
-->_1 s#(mark(X)) -> c_24(s#(X)):21
23:S:sel#(X1,mark(X2)) -> c_26(sel#(X1,X2))
-->_1 sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2)):25
-->_1 sel#(mark(X1),X2) -> c_27(sel#(X1,X2)):24
-->_1 sel#(X1,mark(X2)) -> c_26(sel#(X1,X2)):23
24:S:sel#(mark(X1),X2) -> c_27(sel#(X1,X2))
-->_1 sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2)):25
-->_1 sel#(mark(X1),X2) -> c_27(sel#(X1,X2)):24
-->_1 sel#(X1,mark(X2)) -> c_26(sel#(X1,X2)):23
25:S:sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2))
-->_1 sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2)):25
-->_1 sel#(mark(X1),X2) -> c_27(sel#(X1,X2)):24
-->_1 sel#(X1,mark(X2)) -> c_26(sel#(X1,X2)):23
26:S:top#(mark(X)) -> c_29(top#(proper(X)),proper#(X))
-->_1 top#(ok(X)) -> c_30(top#(active(X)),active#(X)):27
-->_2 proper#(0()) -> c_18():30
-->_1 top#(mark(X)) -> c_29(top#(proper(X)),proper#(X)):26
-->_2 proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20
-->_2 proper#(s(X)) -> c_22(s#(proper(X)),proper#(X)):19
-->_2 proper#(g(X)) -> c_21(g#(proper(X)),proper#(X)):18
-->_2 proper#(f(X)) -> c_20(f#(proper(X)),proper#(X)):17
-->_2 proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16
27:S:top#(ok(X)) -> c_30(top#(active(X)),active#(X))
-->_2 active#(sel(0(),cons(X,Y))) -> c_10():29
-->_2 active#(g(0())) -> c_5(s#(0())):28
-->_1 top#(ok(X)) -> c_30(top#(active(X)),active#(X)):27
-->_1 top#(mark(X)) -> c_29(top#(proper(X)),proper#(X)):26
-->_2 active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z)):9
-->_2 active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1)):8
-->_2 active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2)):7
-->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):6
-->_2 active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X)):5
-->_2 active#(g(X)) -> c_4(g#(active(X)),active#(X)):4
-->_2 active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X)):3
-->_2 active#(f(X)) -> c_2(f#(active(X)),active#(X)):2
-->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1
28:W:active#(g(0())) -> c_5(s#(0()))
29:W:active#(sel(0(),cons(X,Y))) -> c_10()
30:W:proper#(0()) -> c_18()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
30: proper#(0()) -> c_18()
28: active#(g(0())) -> c_5(s#(0()))
29: active#(sel(0(),cons(X,Y))) -> c_10()
* Step 5: Failure MAYBE
+ Considered Problem:
- Strict DPs:
active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1))
active#(f(X)) -> c_2(f#(active(X)),active#(X))
active#(f(X)) -> c_3(cons#(X,f(g(X))),f#(g(X)),g#(X))
active#(g(X)) -> c_4(g#(active(X)),active#(X))
active#(g(s(X))) -> c_6(s#(s(g(X))),s#(g(X)),g#(X))
active#(s(X)) -> c_7(s#(active(X)),active#(X))
active#(sel(X1,X2)) -> c_8(sel#(X1,active(X2)),active#(X2))
active#(sel(X1,X2)) -> c_9(sel#(active(X1),X2),active#(X1))
active#(sel(s(X),cons(Y,Z))) -> c_11(sel#(X,Z))
cons#(mark(X1),X2) -> c_12(cons#(X1,X2))
cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2))
f#(mark(X)) -> c_14(f#(X))
f#(ok(X)) -> c_15(f#(X))
g#(mark(X)) -> c_16(g#(X))
g#(ok(X)) -> c_17(g#(X))
proper#(cons(X1,X2)) -> c_19(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
proper#(f(X)) -> c_20(f#(proper(X)),proper#(X))
proper#(g(X)) -> c_21(g#(proper(X)),proper#(X))
proper#(s(X)) -> c_22(s#(proper(X)),proper#(X))
proper#(sel(X1,X2)) -> c_23(sel#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
s#(mark(X)) -> c_24(s#(X))
s#(ok(X)) -> c_25(s#(X))
sel#(X1,mark(X2)) -> c_26(sel#(X1,X2))
sel#(mark(X1),X2) -> c_27(sel#(X1,X2))
sel#(ok(X1),ok(X2)) -> c_28(sel#(X1,X2))
top#(mark(X)) -> c_29(top#(proper(X)),proper#(X))
top#(ok(X)) -> c_30(top#(active(X)),active#(X))
- Weak TRS:
active(cons(X1,X2)) -> cons(active(X1),X2)
active(f(X)) -> f(active(X))
active(f(X)) -> mark(cons(X,f(g(X))))
active(g(X)) -> g(active(X))
active(g(0())) -> mark(s(0()))
active(g(s(X))) -> mark(s(s(g(X))))
active(s(X)) -> s(active(X))
active(sel(X1,X2)) -> sel(X1,active(X2))
active(sel(X1,X2)) -> sel(active(X1),X2)
active(sel(0(),cons(X,Y))) -> mark(X)
active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
f(mark(X)) -> mark(f(X))
f(ok(X)) -> ok(f(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
proper(s(X)) -> s(proper(X))
proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
sel(X1,mark(X2)) -> mark(sel(X1,X2))
sel(mark(X1),X2) -> mark(sel(X1,X2))
sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
- Signature:
{active/1,cons/2,f/1,g/1,proper/1,s/1,sel/2,top/1,active#/1,cons#/2,f#/1,g#/1,proper#/1,s#/1,sel#/2
,top#/1} / {0/0,mark/1,ok/1,c_1/2,c_2/2,c_3/3,c_4/2,c_5/1,c_6/3,c_7/2,c_8/2,c_9/2,c_10/0,c_11/1,c_12/1
,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/0,c_19/3,c_20/2,c_21/2,c_22/2,c_23/3,c_24/1,c_25/1,c_26/1,c_27/1
,c_28/1,c_29/2,c_30/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {active#,cons#,f#,g#,proper#,s#,sel#
,top#} and constructors {0,mark,ok}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE