* Step 1: Sum WORST_CASE(Omega(n^1),O(n^4))
+ Considered Problem:
- Strict TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
app(y,z){y -> cons(x,y)} =
app(cons(x,y),z) ->^+ cons(x,app(y,z))
= C[app(y,z) = app(y,z){}]
** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^4))
+ Considered Problem:
- Strict TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
app#(nil(),l) -> c_3()
eq#(0(),0()) -> c_4()
eq#(0(),s(x)) -> c_5()
eq#(s(x),0()) -> c_6()
eq#(s(x),s(y)) -> c_7(eq#(x,y))
if#(false(),x,y) -> c_8()
if#(true(),x,y) -> c_9()
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
ifmem#(true(),x,l) -> c_13()
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(x,nil()) -> c_16()
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
inter#(nil(),x) -> c_19()
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
mem#(x,nil()) -> c_21()
Weak DPs
and mark the set of starting terms.
** Step 1.b:2: UsableRules WORST_CASE(?,O(n^4))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
app#(nil(),l) -> c_3()
eq#(0(),0()) -> c_4()
eq#(0(),s(x)) -> c_5()
eq#(s(x),0()) -> c_6()
eq#(s(x),s(y)) -> c_7(eq#(x,y))
if#(false(),x,y) -> c_8()
if#(true(),x,y) -> c_9()
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
ifmem#(true(),x,l) -> c_13()
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(x,nil()) -> c_16()
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
inter#(nil(),x) -> c_19()
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
mem#(x,nil()) -> c_21()
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
app#(nil(),l) -> c_3()
eq#(0(),0()) -> c_4()
eq#(0(),s(x)) -> c_5()
eq#(s(x),0()) -> c_6()
eq#(s(x),s(y)) -> c_7(eq#(x,y))
if#(false(),x,y) -> c_8()
if#(true(),x,y) -> c_9()
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
ifmem#(true(),x,l) -> c_13()
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(x,nil()) -> c_16()
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
inter#(nil(),x) -> c_19()
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
mem#(x,nil()) -> c_21()
** Step 1.b:3: PredecessorEstimation WORST_CASE(?,O(n^4))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
app#(nil(),l) -> c_3()
eq#(0(),0()) -> c_4()
eq#(0(),s(x)) -> c_5()
eq#(s(x),0()) -> c_6()
eq#(s(x),s(y)) -> c_7(eq#(x,y))
if#(false(),x,y) -> c_8()
if#(true(),x,y) -> c_9()
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
ifmem#(true(),x,l) -> c_13()
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(x,nil()) -> c_16()
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
inter#(nil(),x) -> c_19()
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
mem#(x,nil()) -> c_21()
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{3,4,5,6,8,9,13,16,19,21}
by application of
Pre({3,4,5,6,8,9,13,16,19,21}) = {1,2,7,10,11,12,14,15,17,18,20}.
Here rules are labelled as follows:
1: app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
2: app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
3: app#(nil(),l) -> c_3()
4: eq#(0(),0()) -> c_4()
5: eq#(0(),s(x)) -> c_5()
6: eq#(s(x),0()) -> c_6()
7: eq#(s(x),s(y)) -> c_7(eq#(x,y))
8: if#(false(),x,y) -> c_8()
9: if#(true(),x,y) -> c_9()
10: ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
11: ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
12: ifmem#(false(),x,l) -> c_12(mem#(x,l))
13: ifmem#(true(),x,l) -> c_13()
14: inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
15: inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
16: inter#(x,nil()) -> c_16()
17: inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
18: inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
19: inter#(nil(),x) -> c_19()
20: mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
21: mem#(x,nil()) -> c_21()
** Step 1.b:4: RemoveWeakSuffixes WORST_CASE(?,O(n^4))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak DPs:
app#(nil(),l) -> c_3()
eq#(0(),0()) -> c_4()
eq#(0(),s(x)) -> c_5()
eq#(s(x),0()) -> c_6()
if#(false(),x,y) -> c_8()
if#(true(),x,y) -> c_9()
ifmem#(true(),x,l) -> c_13()
inter#(x,nil()) -> c_16()
inter#(nil(),x) -> c_19()
mem#(x,nil()) -> c_21()
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
-->_2 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_2 app#(nil(),l) -> c_3():12
-->_1 app#(nil(),l) -> c_3():12
-->_2 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
2:S:app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
-->_1 app#(nil(),l) -> c_3():12
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
3:S:eq#(s(x),s(y)) -> c_7(eq#(x,y))
-->_1 eq#(s(x),0()) -> c_6():15
-->_1 eq#(0(),s(x)) -> c_5():14
-->_1 eq#(0(),0()) -> c_4():13
-->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3
4:S:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_1 inter#(nil(),x) -> c_19():20
-->_1 inter#(x,nil()) -> c_16():19
5:S:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_1 inter#(nil(),x) -> c_19():20
-->_1 inter#(x,nil()) -> c_16():19
6:S:ifmem#(false(),x,l) -> c_12(mem#(x,l))
-->_1 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):11
-->_1 mem#(x,nil()) -> c_21():21
7:S:inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_3 inter#(nil(),x) -> c_19():20
-->_2 inter#(nil(),x) -> c_19():20
-->_3 inter#(x,nil()) -> c_16():19
-->_2 inter#(x,nil()) -> c_16():19
-->_1 app#(nil(),l) -> c_3():12
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
8:S:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):11
-->_2 mem#(x,nil()) -> c_21():21
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):5
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
9:S:inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_3 inter#(nil(),x) -> c_19():20
-->_2 inter#(nil(),x) -> c_19():20
-->_3 inter#(x,nil()) -> c_16():19
-->_2 inter#(x,nil()) -> c_16():19
-->_1 app#(nil(),l) -> c_3():12
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
10:S:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):11
-->_2 mem#(x,nil()) -> c_21():21
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):5
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
11:S:mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
-->_1 ifmem#(true(),x,l) -> c_13():18
-->_2 eq#(s(x),0()) -> c_6():15
-->_2 eq#(0(),s(x)) -> c_5():14
-->_2 eq#(0(),0()) -> c_4():13
-->_1 ifmem#(false(),x,l) -> c_12(mem#(x,l)):6
-->_2 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3
12:W:app#(nil(),l) -> c_3()
13:W:eq#(0(),0()) -> c_4()
14:W:eq#(0(),s(x)) -> c_5()
15:W:eq#(s(x),0()) -> c_6()
16:W:if#(false(),x,y) -> c_8()
17:W:if#(true(),x,y) -> c_9()
18:W:ifmem#(true(),x,l) -> c_13()
19:W:inter#(x,nil()) -> c_16()
20:W:inter#(nil(),x) -> c_19()
21:W:mem#(x,nil()) -> c_21()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
17: if#(true(),x,y) -> c_9()
16: if#(false(),x,y) -> c_8()
19: inter#(x,nil()) -> c_16()
20: inter#(nil(),x) -> c_19()
21: mem#(x,nil()) -> c_21()
18: ifmem#(true(),x,l) -> c_13()
13: eq#(0(),0()) -> c_4()
14: eq#(0(),s(x)) -> c_5()
15: eq#(s(x),0()) -> c_6()
12: app#(nil(),l) -> c_3()
** Step 1.b:5: Decompose WORST_CASE(?,O(n^4))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
- Weak DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0
,c_10/1,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
Problem (S)
- Strict DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0
,c_10/1,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
*** Step 1.b:5.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^4))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
- Weak DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
-->_2 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_2 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
2:S:app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
3:W:eq#(s(x),s(y)) -> c_7(eq#(x,y))
-->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3
4:W:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
5:W:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
6:W:ifmem#(false(),x,l) -> c_12(mem#(x,l))
-->_1 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):11
7:W:inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
8:W:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):5
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):11
9:W:inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
10:W:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):5
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):11
11:W:mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
-->_2 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3
-->_1 ifmem#(false(),x,l) -> c_12(mem#(x,l)):6
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
11: mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
6: ifmem#(false(),x,l) -> c_12(mem#(x,l))
3: eq#(s(x),s(y)) -> c_7(eq#(x,y))
*** Step 1.b:5.a:2: SimplifyRHS WORST_CASE(?,O(n^4))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
-->_2 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_2 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
2:S:app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
4:W:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
5:W:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
7:W:inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
8:W:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):5
9:W:inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):7
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):8
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):10
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):9
10:W:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):5
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
*** Step 1.b:5.a:3: DecomposeDG WORST_CASE(?,O(n^4))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
and a lower component
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
Further, following extension rules are added to the lower component.
ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> inter#(l1,l3)
inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) -> inter#(l1,l3)
inter#(app(l1,l2),l3) -> inter#(l2,l3)
inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
**** Step 1.b:5.a:3.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
2: inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
The strictly oriented rules are moved into the weak component.
***** Step 1.b:5.a:3.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_10) = {1},
uargs(c_11) = {1},
uargs(c_14) = {1,2,3},
uargs(c_15) = {1},
uargs(c_17) = {1,2,3},
uargs(c_18) = {1}
Following symbols are considered usable:
{app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}
TcT has computed the following interpretation:
p(0) = 0
p(app) = 1 + x1 + x2
p(cons) = x2
p(eq) = 0
p(false) = 1
p(if) = 0
p(ifinter) = 0
p(ifmem) = x1 + x1^2
p(inter) = 1
p(mem) = 0
p(nil) = 1
p(s) = 0
p(true) = 0
p(app#) = 0
p(eq#) = 0
p(if#) = 0
p(ifinter#) = x3 + x3*x4 + x4
p(ifmem#) = 0
p(inter#) = x1 + x1*x2 + x2
p(mem#) = 0
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 0
p(c_7) = 0
p(c_8) = 0
p(c_9) = 0
p(c_10) = x1
p(c_11) = x1
p(c_12) = 0
p(c_13) = 0
p(c_14) = x1 + x2 + x3
p(c_15) = x1
p(c_16) = 0
p(c_17) = x1 + x2 + x3
p(c_18) = x1
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
Following rules are strictly oriented:
inter#(l1,app(l2,l3)) = 1 + 2*l1 + l1*l2 + l1*l3 + l2 + l3
> 2*l1 + l1*l2 + l1*l3 + l2 + l3
= c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(app(l1,l2),l3) = 1 + l1 + l1*l3 + l2 + l2*l3 + 2*l3
> l1 + l1*l3 + l2 + l2*l3 + 2*l3
= c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
Following rules are (at-least) weakly oriented:
ifinter#(false(),x,l1,l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= c_11(inter#(l1,l2))
inter#(l1,cons(x,l2)) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(cons(x,l1),l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= c_18(ifinter#(mem(x,l2),x,l1,l2))
***** Step 1.b:5.a:3.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 1.b:5.a:3.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):5
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):3
2:W:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):5
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):3
3:W:inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):5
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):5
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):3
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):3
4:W:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
5:W:inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):5
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):5
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):3
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):3
6:W:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
6: inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
5: inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
3: inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
2: ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
4: inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
***** Step 1.b:5.a:3.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
**** Step 1.b:5.a:3.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> inter#(l1,l3)
inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) -> inter#(l1,l3)
inter#(app(l1,l2),l3) -> inter#(l2,l3)
inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
2: app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
The strictly oriented rules are moved into the weak component.
***** Step 1.b:5.a:3.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> inter#(l1,l3)
inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) -> inter#(l1,l3)
inter#(app(l1,l2),l3) -> inter#(l2,l3)
inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_1) = {1,2},
uargs(c_2) = {1}
Following symbols are considered usable:
{app,ifinter,ifmem,inter,mem,app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}
TcT has computed the following interpretation:
p(0) = 0
p(app) = x1 + x2
p(cons) = 1 + x2
p(eq) = 0
p(false) = 0
p(if) = 0
p(ifinter) = x1 + x3*x4
p(ifmem) = 1 + x3
p(inter) = x1*x2
p(mem) = x2
p(nil) = 0
p(s) = 0
p(true) = 1
p(app#) = x1
p(eq#) = 0
p(if#) = 0
p(ifinter#) = x3*x4
p(ifmem#) = 0
p(inter#) = x1*x2
p(mem#) = 0
p(c_1) = x1 + x2
p(c_2) = x1
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 0
p(c_7) = 0
p(c_8) = 0
p(c_9) = 0
p(c_10) = 0
p(c_11) = 0
p(c_12) = 0
p(c_13) = 0
p(c_14) = 0
p(c_15) = 0
p(c_16) = 0
p(c_17) = 0
p(c_18) = 0
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
Following rules are strictly oriented:
app#(cons(x,l1),l2) = 1 + l1
> l1
= c_2(app#(l1,l2))
Following rules are (at-least) weakly oriented:
app#(app(l1,l2),l3) = l1 + l2
>= l1 + l2
= c_1(app#(l1,app(l2,l3)),app#(l2,l3))
ifinter#(false(),x,l1,l2) = l1*l2
>= l1*l2
= inter#(l1,l2)
ifinter#(true(),x,l1,l2) = l1*l2
>= l1*l2
= inter#(l1,l2)
inter#(l1,app(l2,l3)) = l1*l2 + l1*l3
>= l1*l2
= app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) = l1*l2 + l1*l3
>= l1*l2
= inter#(l1,l2)
inter#(l1,app(l2,l3)) = l1*l2 + l1*l3
>= l1*l3
= inter#(l1,l3)
inter#(l1,cons(x,l2)) = l1 + l1*l2
>= l1*l2
= ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) = l1*l3 + l2*l3
>= l1*l3
= app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) = l1*l3 + l2*l3
>= l1*l3
= inter#(l1,l3)
inter#(app(l1,l2),l3) = l1*l3 + l2*l3
>= l2*l3
= inter#(l2,l3)
inter#(cons(x,l1),l2) = l1*l2 + l2
>= l1*l2
= ifinter#(mem(x,l2),x,l1,l2)
app(app(l1,l2),l3) = l1 + l2 + l3
>= l1 + l2 + l3
= app(l1,app(l2,l3))
app(cons(x,l1),l2) = 1 + l1 + l2
>= 1 + l1 + l2
= cons(x,app(l1,l2))
app(nil(),l) = l
>= l
= l
ifinter(false(),x,l1,l2) = l1*l2
>= l1*l2
= inter(l1,l2)
ifinter(true(),x,l1,l2) = 1 + l1*l2
>= 1 + l1*l2
= cons(x,inter(l1,l2))
ifmem(false(),x,l) = 1 + l
>= l
= mem(x,l)
ifmem(true(),x,l) = 1 + l
>= 1
= true()
inter(l1,app(l2,l3)) = l1*l2 + l1*l3
>= l1*l2 + l1*l3
= app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) = l1 + l1*l2
>= l1 + l1*l2
= ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) = 0
>= 0
= nil()
inter(app(l1,l2),l3) = l1*l3 + l2*l3
>= l1*l3 + l2*l3
= app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) = l1*l2 + l2
>= l1*l2 + l2
= ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) = 0
>= 0
= nil()
mem(x,cons(y,l)) = 1 + l
>= 1 + l
= ifmem(eq(x,y),x,l)
mem(x,nil()) = 0
>= 0
= false()
***** Step 1.b:5.a:3.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
- Weak DPs:
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> inter#(l1,l3)
inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) -> inter#(l1,l3)
inter#(app(l1,l2),l3) -> inter#(l2,l3)
inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 1.b:5.a:3.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
- Weak DPs:
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> inter#(l1,l3)
inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) -> inter#(l1,l3)
inter#(app(l1,l2),l3) -> inter#(l2,l3)
inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
The strictly oriented rules are moved into the weak component.
****** Step 1.b:5.a:3.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
- Weak DPs:
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> inter#(l1,l3)
inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) -> inter#(l1,l3)
inter#(app(l1,l2),l3) -> inter#(l2,l3)
inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_1) = {1,2},
uargs(c_2) = {1}
Following symbols are considered usable:
{app,ifinter,inter,app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}
TcT has computed the following interpretation:
p(0) = 1
p(app) = 1 + x1 + x2
p(cons) = x2
p(eq) = 1 + x1 + x1^2
p(false) = 0
p(if) = 0
p(ifinter) = x3 + x3*x4 + x4
p(ifmem) = 1 + x1*x2 + x2^2 + x3^2
p(inter) = x1 + x1*x2 + x2
p(mem) = 0
p(nil) = 0
p(s) = 0
p(true) = 0
p(app#) = x1
p(eq#) = 0
p(if#) = 0
p(ifinter#) = x3 + x3*x4 + x4
p(ifmem#) = 0
p(inter#) = x1 + x1*x2 + x2
p(mem#) = 0
p(c_1) = x1 + x2
p(c_2) = x1
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 0
p(c_7) = 0
p(c_8) = 0
p(c_9) = 0
p(c_10) = 0
p(c_11) = 0
p(c_12) = 0
p(c_13) = 0
p(c_14) = 0
p(c_15) = 0
p(c_16) = 0
p(c_17) = 0
p(c_18) = 0
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
Following rules are strictly oriented:
app#(app(l1,l2),l3) = 1 + l1 + l2
> l1 + l2
= c_1(app#(l1,app(l2,l3)),app#(l2,l3))
Following rules are (at-least) weakly oriented:
app#(cons(x,l1),l2) = l1
>= l1
= c_2(app#(l1,l2))
ifinter#(false(),x,l1,l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= inter#(l1,l2)
ifinter#(true(),x,l1,l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= inter#(l1,l2)
inter#(l1,app(l2,l3)) = 1 + 2*l1 + l1*l2 + l1*l3 + l2 + l3
>= l1 + l1*l2 + l2
= app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) = 1 + 2*l1 + l1*l2 + l1*l3 + l2 + l3
>= l1 + l1*l2 + l2
= inter#(l1,l2)
inter#(l1,app(l2,l3)) = 1 + 2*l1 + l1*l2 + l1*l3 + l2 + l3
>= l1 + l1*l3 + l3
= inter#(l1,l3)
inter#(l1,cons(x,l2)) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) = 1 + l1 + l1*l3 + l2 + l2*l3 + 2*l3
>= l1 + l1*l3 + l3
= app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) = 1 + l1 + l1*l3 + l2 + l2*l3 + 2*l3
>= l1 + l1*l3 + l3
= inter#(l1,l3)
inter#(app(l1,l2),l3) = 1 + l1 + l1*l3 + l2 + l2*l3 + 2*l3
>= l2 + l2*l3 + l3
= inter#(l2,l3)
inter#(cons(x,l1),l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= ifinter#(mem(x,l2),x,l1,l2)
app(app(l1,l2),l3) = 2 + l1 + l2 + l3
>= 2 + l1 + l2 + l3
= app(l1,app(l2,l3))
app(cons(x,l1),l2) = 1 + l1 + l2
>= 1 + l1 + l2
= cons(x,app(l1,l2))
app(nil(),l) = 1 + l
>= l
= l
ifinter(false(),x,l1,l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= inter(l1,l2)
ifinter(true(),x,l1,l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= cons(x,inter(l1,l2))
inter(l1,app(l2,l3)) = 1 + 2*l1 + l1*l2 + l1*l3 + l2 + l3
>= 1 + 2*l1 + l1*l2 + l1*l3 + l2 + l3
= app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) = x
>= 0
= nil()
inter(app(l1,l2),l3) = 1 + l1 + l1*l3 + l2 + l2*l3 + 2*l3
>= 1 + l1 + l1*l3 + l2 + l2*l3 + 2*l3
= app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) = x
>= 0
= nil()
****** Step 1.b:5.a:3.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> inter#(l1,l3)
inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) -> inter#(l1,l3)
inter#(app(l1,l2),l3) -> inter#(l2,l3)
inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
****** Step 1.b:5.a:3.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) -> inter#(l1,l2)
inter#(l1,app(l2,l3)) -> inter#(l1,l3)
inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) -> inter#(l1,l3)
inter#(app(l1,l2),l3) -> inter#(l2,l3)
inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
-->_2 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_2 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
2:W:app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
3:W:ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
-->_1 inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2):12
-->_1 inter#(app(l1,l2),l3) -> inter#(l2,l3):11
-->_1 inter#(app(l1,l2),l3) -> inter#(l1,l3):10
-->_1 inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1):8
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l3):7
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l2):6
-->_1 inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)):5
4:W:ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
-->_1 inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2):12
-->_1 inter#(app(l1,l2),l3) -> inter#(l2,l3):11
-->_1 inter#(app(l1,l2),l3) -> inter#(l1,l3):10
-->_1 inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1):8
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l3):7
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l2):6
-->_1 inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)):5
5:W:inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
6:W:inter#(l1,app(l2,l3)) -> inter#(l1,l2)
-->_1 inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2):12
-->_1 inter#(app(l1,l2),l3) -> inter#(l2,l3):11
-->_1 inter#(app(l1,l2),l3) -> inter#(l1,l3):10
-->_1 inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1):8
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l3):7
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l2):6
-->_1 inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)):5
7:W:inter#(l1,app(l2,l3)) -> inter#(l1,l3)
-->_1 inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2):12
-->_1 inter#(app(l1,l2),l3) -> inter#(l2,l3):11
-->_1 inter#(app(l1,l2),l3) -> inter#(l1,l3):10
-->_1 inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1):8
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l3):7
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l2):6
-->_1 inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)):5
8:W:inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
-->_1 ifinter#(true(),x,l1,l2) -> inter#(l1,l2):4
-->_1 ifinter#(false(),x,l1,l2) -> inter#(l1,l2):3
9:W:inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):2
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):1
10:W:inter#(app(l1,l2),l3) -> inter#(l1,l3)
-->_1 inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2):12
-->_1 inter#(app(l1,l2),l3) -> inter#(l2,l3):11
-->_1 inter#(app(l1,l2),l3) -> inter#(l1,l3):10
-->_1 inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1):8
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l3):7
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l2):6
-->_1 inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)):5
11:W:inter#(app(l1,l2),l3) -> inter#(l2,l3)
-->_1 inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2):12
-->_1 inter#(app(l1,l2),l3) -> inter#(l2,l3):11
-->_1 inter#(app(l1,l2),l3) -> inter#(l1,l3):10
-->_1 inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)):9
-->_1 inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1):8
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l3):7
-->_1 inter#(l1,app(l2,l3)) -> inter#(l1,l2):6
-->_1 inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)):5
12:W:inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
-->_1 ifinter#(true(),x,l1,l2) -> inter#(l1,l2):4
-->_1 ifinter#(false(),x,l1,l2) -> inter#(l1,l2):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
12: inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
11: inter#(app(l1,l2),l3) -> inter#(l2,l3)
10: inter#(app(l1,l2),l3) -> inter#(l1,l3)
7: inter#(l1,app(l2,l3)) -> inter#(l1,l3)
6: inter#(l1,app(l2,l3)) -> inter#(l1,l2)
4: ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
8: inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
5: inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
9: inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
1: app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
2: app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
****** Step 1.b:5.a:3.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/1,c_16/0,c_17/3,c_18/1,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
*** Step 1.b:5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak DPs:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:eq#(s(x),s(y)) -> c_7(eq#(x,y))
-->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):1
2:S:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
3:S:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
4:S:ifmem#(false(),x,l) -> c_12(mem#(x,l))
-->_1 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):9
5:S:inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):11
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):10
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
6:S:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):9
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
7:S:inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):11
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):10
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
8:S:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):9
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
9:S:mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
-->_1 ifmem#(false(),x,l) -> c_12(mem#(x,l)):4
-->_2 eq#(s(x),s(y)) -> c_7(eq#(x,y)):1
10:W:app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
-->_2 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):11
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):11
-->_2 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):10
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):10
11:W:app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
-->_1 app#(cons(x,l1),l2) -> c_2(app#(l1,l2)):11
-->_1 app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3)):10
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
11: app#(cons(x,l1),l2) -> c_2(app#(l1,l2))
10: app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
*** Step 1.b:5.b:2: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0,c_17/3,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:eq#(s(x),s(y)) -> c_7(eq#(x,y))
-->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):1
2:S:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
3:S:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_1 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
4:S:ifmem#(false(),x,l) -> c_12(mem#(x,l))
-->_1 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):9
5:S:inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3))
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
6:S:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):9
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
7:S:inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3))
-->_3 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_3 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_2 inter#(app(l1,l2),l3) -> c_17(app#(inter(l1,l3),inter(l2,l3)),inter#(l1,l3),inter#(l2,l3)):7
-->_3 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_3 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
-->_2 inter#(l1,app(l2,l3)) -> c_14(app#(inter(l1,l2),inter(l1,l3)),inter#(l1,l2),inter#(l1,l3)):5
8:S:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):9
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
9:S:mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
-->_1 ifmem#(false(),x,l) -> c_12(mem#(x,l)):4
-->_2 eq#(s(x),s(y)) -> c_7(eq#(x,y)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
*** Step 1.b:5.b:3: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
app(app(l1,l2),l3) -> app(l1,app(l2,l3))
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
*** Step 1.b:5.b:4: Decompose WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
- Strict DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0
,c_10/1,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
Problem (S)
- Strict DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0
,c_10/1,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
**** Step 1.b:5.b:4.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: eq#(s(x),s(y)) -> c_7(eq#(x,y))
The strictly oriented rules are moved into the weak component.
***** Step 1.b:5.b:4.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_7) = {1},
uargs(c_10) = {1},
uargs(c_11) = {1},
uargs(c_12) = {1},
uargs(c_14) = {1,2},
uargs(c_15) = {1,2},
uargs(c_17) = {1,2},
uargs(c_18) = {1,2},
uargs(c_20) = {1,2}
Following symbols are considered usable:
{app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}
TcT has computed the following interpretation:
p(0) = 0
p(app) = 1 + x1 + x1*x2 + 2*x2 + x2^2
p(cons) = x1 + x2
p(eq) = 2*x1*x2
p(false) = 0
p(if) = 2 + 2*x1 + 2*x1*x2 + 2*x1^2 + x2 + 2*x2*x3 + x3
p(ifinter) = 1 + 2*x1*x3 + 2*x1^2 + x2*x3 + 2*x3*x4
p(ifmem) = 2 + x1 + 3*x1*x2 + 2*x1*x3 + x2 + 2*x2*x3 + 2*x2^2 + 2*x3 + x3^2
p(inter) = x1 + x1^2 + 2*x2^2
p(mem) = 0
p(nil) = 0
p(s) = 1 + x1
p(true) = 1
p(app#) = x1 + x1*x2 + 2*x1^2 + 2*x2
p(eq#) = 2*x1*x2
p(if#) = 1 + x2 + x2^2 + x3 + x3^2
p(ifinter#) = 3*x3*x4
p(ifmem#) = 3*x2*x3
p(inter#) = 3*x1*x2
p(mem#) = 3*x1*x2
p(c_1) = x2
p(c_2) = x1
p(c_3) = 1
p(c_4) = 0
p(c_5) = 0
p(c_6) = 1
p(c_7) = x1
p(c_8) = 1
p(c_9) = 0
p(c_10) = x1
p(c_11) = x1
p(c_12) = x1
p(c_13) = 0
p(c_14) = x1 + x2
p(c_15) = x1 + x2
p(c_16) = 0
p(c_17) = x1 + x2
p(c_18) = x1 + x2
p(c_19) = 0
p(c_20) = x1 + x2
p(c_21) = 1
Following rules are strictly oriented:
eq#(s(x),s(y)) = 2 + 2*x + 2*x*y + 2*y
> 2*x*y
= c_7(eq#(x,y))
Following rules are (at-least) weakly oriented:
ifinter#(false(),x,l1,l2) = 3*l1*l2
>= 3*l1*l2
= c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) = 3*l1*l2
>= 3*l1*l2
= c_11(inter#(l1,l2))
ifmem#(false(),x,l) = 3*l*x
>= 3*l*x
= c_12(mem#(x,l))
inter#(l1,app(l2,l3)) = 3*l1 + 3*l1*l2 + 3*l1*l2*l3 + 6*l1*l3 + 3*l1*l3^2
>= 3*l1*l2 + 3*l1*l3
= c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) = 3*l1*l2 + 3*l1*x
>= 3*l1*l2 + 3*l1*x
= c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) = 3*l1*l2*l3 + 3*l1*l3 + 6*l2*l3 + 3*l2^2*l3 + 3*l3
>= 3*l1*l3 + 3*l2*l3
= c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) = 3*l1*l2 + 3*l2*x
>= 3*l1*l2 + 3*l2*x
= c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) = 3*l*x + 3*x*y
>= 3*l*x + 2*x*y
= c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
***** Step 1.b:5.b:4.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 1.b:5.b:4.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:eq#(s(x),s(y)) -> c_7(eq#(x,y))
-->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):1
2:W:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
3:W:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
4:W:ifmem#(false(),x,l) -> c_12(mem#(x,l))
-->_1 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):9
5:W:inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):7
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):7
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
6:W:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):9
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
7:W:inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):8
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):7
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):7
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
8:W:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):9
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
9:W:mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
-->_1 ifmem#(false(),x,l) -> c_12(mem#(x,l)):4
-->_2 eq#(s(x),s(y)) -> c_7(eq#(x,y)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
2: ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
8: inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
7: inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
5: inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
3: ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
6: inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
9: mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
4: ifmem#(false(),x,l) -> c_12(mem#(x,l))
1: eq#(s(x),s(y)) -> c_7(eq#(x,y))
***** Step 1.b:5.b:4.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
**** Step 1.b:5.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak DPs:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
2:S:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
3:S:ifmem#(false(),x,l) -> c_12(mem#(x,l))
-->_1 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):8
4:S:inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
5:S:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):8
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
6:S:inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
7:S:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):8
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
8:S:mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
-->_2 eq#(s(x),s(y)) -> c_7(eq#(x,y)):9
-->_1 ifmem#(false(),x,l) -> c_12(mem#(x,l)):3
9:W:eq#(s(x),s(y)) -> c_7(eq#(x,y))
-->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):9
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: eq#(s(x),s(y)) -> c_7(eq#(x,y))
**** Step 1.b:5.b:4.b:2: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/2,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
2:S:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
3:S:ifmem#(false(),x,l) -> c_12(mem#(x,l))
-->_1 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):8
4:S:inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
5:S:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):8
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
6:S:inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):6
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):5
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):4
7:S:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y)):8
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
8:S:mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l),eq#(x,y))
-->_1 ifmem#(false(),x,l) -> c_12(mem#(x,l)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
**** Step 1.b:5.b:4.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
3: ifmem#(false(),x,l) -> c_12(mem#(x,l))
4: inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
5: inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
7: inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
8: mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
Consider the set of all dependency pairs
1: ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
2: ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
3: ifmem#(false(),x,l) -> c_12(mem#(x,l))
4: inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
5: inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
6: inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
7: inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
8: mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{3,4,5,7,8}
These cover all (indirect) predecessors of dependency pairs
{1,2,3,4,5,7,8}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
***** Step 1.b:5.b:4.b:3.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_10) = {1},
uargs(c_11) = {1},
uargs(c_12) = {1},
uargs(c_14) = {1,2},
uargs(c_15) = {1,2},
uargs(c_17) = {1,2},
uargs(c_18) = {1,2},
uargs(c_20) = {1}
Following symbols are considered usable:
{eq,app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}
TcT has computed the following interpretation:
p(0) = 1
p(app) = 1 + x1 + 2*x1^2 + x2
p(cons) = 1 + x1 + x2
p(eq) = x1*x2
p(false) = 1
p(if) = 2*x1 + x2 + x2*x3 + 2*x3^2
p(ifinter) = 2 + x1 + x3*x4
p(ifmem) = 2 + 2*x1 + x1*x2 + 2*x1^2 + 3*x2 + 2*x2*x3
p(inter) = 1
p(mem) = x1
p(nil) = 1
p(s) = 1 + x1
p(true) = 0
p(app#) = x2^2
p(eq#) = 0
p(if#) = 2*x1*x3 + 2*x3
p(ifinter#) = x2 + x3 + 2*x3*x4 + 2*x4
p(ifmem#) = 2*x1 + 2*x2 + 2*x2*x3 + x3
p(inter#) = x1 + 2*x1*x2 + x2
p(mem#) = 2*x1*x2 + x2
p(c_1) = 1 + x1 + x2
p(c_2) = 0
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 1
p(c_7) = 1
p(c_8) = 1
p(c_9) = 0
p(c_10) = x1
p(c_11) = x1
p(c_12) = x1
p(c_13) = 0
p(c_14) = x1 + x2
p(c_15) = x1 + x2
p(c_16) = 0
p(c_17) = 1 + x1 + x2
p(c_18) = x1 + x2
p(c_19) = 0
p(c_20) = x1
p(c_21) = 1
Following rules are strictly oriented:
ifmem#(false(),x,l) = 2 + l + 2*l*x + 2*x
> l + 2*l*x
= c_12(mem#(x,l))
inter#(l1,app(l2,l3)) = 1 + 3*l1 + 2*l1*l2 + 4*l1*l2^2 + 2*l1*l3 + l2 + 2*l2^2 + l3
> 2*l1 + 2*l1*l2 + 2*l1*l3 + l2 + l3
= c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) = 1 + 3*l1 + 2*l1*l2 + 2*l1*x + l2 + x
> 3*l1 + 2*l1*l2 + 2*l1*x + l2 + x
= c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(cons(x,l1),l2) = 1 + l1 + 2*l1*l2 + 3*l2 + 2*l2*x + x
> l1 + 2*l1*l2 + 3*l2 + 2*l2*x + x
= c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) = 1 + l + 2*l*x + 2*x + 2*x*y + y
> l + 2*l*x + 2*x + 2*x*y
= c_20(ifmem#(eq(x,y),x,l))
Following rules are (at-least) weakly oriented:
ifinter#(false(),x,l1,l2) = l1 + 2*l1*l2 + 2*l2 + x
>= l1 + 2*l1*l2 + l2
= c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) = l1 + 2*l1*l2 + 2*l2 + x
>= l1 + 2*l1*l2 + l2
= c_11(inter#(l1,l2))
inter#(app(l1,l2),l3) = 1 + l1 + 2*l1*l3 + 2*l1^2 + 4*l1^2*l3 + l2 + 2*l2*l3 + 3*l3
>= 1 + l1 + 2*l1*l3 + l2 + 2*l2*l3 + 2*l3
= c_17(inter#(l1,l3),inter#(l2,l3))
eq(0(),0()) = 1
>= 0
= true()
eq(0(),s(x)) = 1 + x
>= 1
= false()
eq(s(x),0()) = 1 + x
>= 1
= false()
eq(s(x),s(y)) = 1 + x + x*y + y
>= x*y
= eq(x,y)
***** Step 1.b:5.b:4.b:3.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
- Weak DPs:
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 1.b:5.b:4.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
ifmem#(false(),x,l) -> c_12(mem#(x,l))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
2:W:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
3:W:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
4:W:ifmem#(false(),x,l) -> c_12(mem#(x,l))
-->_1 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l)):8
5:W:inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
6:W:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l)):8
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
7:W:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_2 mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l)):8
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
8:W:mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
-->_1 ifmem#(false(),x,l) -> c_12(mem#(x,l)):4
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
8: mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
4: ifmem#(false(),x,l) -> c_12(mem#(x,l))
***** Step 1.b:5.b:4.b:3.b:2: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
2:W:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
3:W:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
5:W:inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2)):7
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1)):6
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):5
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):1
6:W:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,l1))
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
7:W:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,l2))
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):3
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):2
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
***** Step 1.b:5.b:4.b:3.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
The strictly oriented rules are moved into the weak component.
****** Step 1.b:5.b:4.b:3.b:3.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_10) = {1},
uargs(c_11) = {1},
uargs(c_14) = {1,2},
uargs(c_15) = {1},
uargs(c_17) = {1,2},
uargs(c_18) = {1}
Following symbols are considered usable:
{app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}
TcT has computed the following interpretation:
p(0) = 0
p(app) = 1 + x1 + x2
p(cons) = 1 + x2
p(eq) = x1 + x1^2 + x2^2
p(false) = 1
p(if) = 2 + x1*x2 + 2*x1^2
p(ifinter) = 2 + x2 + x3^2
p(ifmem) = x1 + 2*x1*x2 + x1^2 + 2*x2 + 2*x2^2 + 2*x3 + 2*x3^2
p(inter) = 2 + 2*x1 + x2
p(mem) = 2 + x1*x2
p(nil) = 0
p(s) = 1
p(true) = 1
p(app#) = 0
p(eq#) = 2 + x1*x2 + x1^2 + 2*x2 + x2^2
p(if#) = x1 + 2*x1*x2 + x2 + 2*x2^2
p(ifinter#) = x3 + x3*x4 + x4
p(ifmem#) = 1 + x1 + 2*x1*x2 + 2*x1^2 + x2 + 2*x2^2 + x3
p(inter#) = x1 + x1*x2 + x2
p(mem#) = 2*x1 + x1*x2
p(c_1) = x1
p(c_2) = 1
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 1
p(c_7) = 0
p(c_8) = 0
p(c_9) = 0
p(c_10) = x1
p(c_11) = x1
p(c_12) = 0
p(c_13) = 1
p(c_14) = x1 + x2
p(c_15) = 1 + x1
p(c_16) = 1
p(c_17) = x1 + x2
p(c_18) = 1 + x1
p(c_19) = 1
p(c_20) = 0
p(c_21) = 0
Following rules are strictly oriented:
inter#(app(l1,l2),l3) = 1 + l1 + l1*l3 + l2 + l2*l3 + 2*l3
> l1 + l1*l3 + l2 + l2*l3 + 2*l3
= c_17(inter#(l1,l3),inter#(l2,l3))
Following rules are (at-least) weakly oriented:
ifinter#(false(),x,l1,l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) = l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) = 1 + 2*l1 + l1*l2 + l1*l3 + l2 + l3
>= 2*l1 + l1*l2 + l1*l3 + l2 + l3
= c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) = 1 + 2*l1 + l1*l2 + l2
>= 1 + l1 + l1*l2 + l2
= c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(cons(x,l1),l2) = 1 + l1 + l1*l2 + 2*l2
>= 1 + l1 + l1*l2 + l2
= c_18(ifinter#(mem(x,l2),x,l1,l2))
****** Step 1.b:5.b:4.b:3.b:3.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
****** Step 1.b:5.b:4.b:3.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):5
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
2:W:ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):5
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
3:W:inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):5
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):5
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
4:W:inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
5:W:inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
-->_2 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2)):6
-->_2 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):5
-->_1 inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3)):5
-->_2 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1)):4
-->_2 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
6:W:inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
-->_1 ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
6: inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2))
5: inter#(app(l1,l2),l3) -> c_17(inter#(l1,l3),inter#(l2,l3))
3: inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3))
2: ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
4: inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1))
****** Step 1.b:5.b:4.b:3.b:3.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2,app#/2,eq#/2,if#/3,ifinter#/4,ifmem#/3,inter#/2
,mem#/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,eq#,if#,ifinter#,ifmem#,inter#
,mem#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^4))