*** 1 Progress [(?,O(n^4))] ***
Considered Problem:
Strict DP Rules:
Strict TRS 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)
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()
Weak DP Rules:
Weak TRS Rules:
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
basic terms: {app,eq,if,ifinter,ifmem,inter,mem}/{0,cons,false,nil,s,true}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
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.
*** 1.1 Progress [(?,O(n^4))] ***
Considered Problem:
Strict DP Rules:
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()
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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)
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
UsableRules
Proof:
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()
*** 1.1.1 Progress [(?,O(n^4))] ***
Considered Problem:
Strict DP Rules:
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()
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
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()
*** 1.1.1.1 Progress [(?,O(n^4))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
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()
*** 1.1.1.1.1 Progress [(?,O(n^4))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
Proof:
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 DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Problem (S)
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
*** 1.1.1.1.1.1 Progress [(?,O(n^4))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
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#(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: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))
-->_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#(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#(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: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)):5
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
-->_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))
-->_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
-->_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#(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)):5
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
-->_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))
*** 1.1.1.1.1.1.1 Progress [(?,O(n^4))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
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#(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
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))
-->_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#(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#(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: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)):5
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
9: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),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
-->_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#(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)):5
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):4
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))
*** 1.1.1.1.1.1.1.1 Progress [(?,O(n^4))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing}
Proof:
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)
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} 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.
*** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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) = 0
p(mem) = 0
p(nil) = 0
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))
*** 1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))
*** 1.1.1.1.1.1.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} 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.
*** 1.1.1.1.1.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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 + 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#(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 + 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)) = l1 + l1*l2 + l1*l3 + l2 + l3
>= l1*l2
= app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) = l1 + l1*l2 + l1*l3 + l2 + l3
>= l1 + l1*l2 + l2
= inter#(l1,l2)
inter#(l1,app(l2,l3)) = l1 + l1*l2 + l1*l3 + l2 + l3
>= l1 + l1*l3 + l3
= inter#(l1,l3)
inter#(l1,cons(x,l2)) = 1 + 2*l1 + l1*l2 + l2
>= l1 + l1*l2 + l2
= ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) = l1 + l1*l3 + l2 + l2*l3 + l3
>= l1*l3
= app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) = l1 + l1*l3 + l2 + l2*l3 + l3
>= l1 + l1*l3 + l3
= inter#(l1,l3)
inter#(app(l1,l2),l3) = l1 + l1*l3 + l2 + l2*l3 + l3
>= l2 + l2*l3 + l3
= inter#(l2,l3)
inter#(cons(x,l1),l2) = 1 + l1 + l1*l2 + 2*l2
>= l1 + l1*l2 + 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()
*** 1.1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.2.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} 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.
*** 1.1.1.1.1.1.1.1.2.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
app#(app(l1,l2),l3) -> c_1(app#(l1,app(l2,l3)),app#(l2,l3))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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) = 0
p(app) = 1 + x1 + x2
p(cons) = x2
p(eq) = x1 + x1*x2 + x2
p(false) = 0
p(if) = 0
p(ifinter) = x3 + x3*x4 + x4
p(ifmem) = x1*x2
p(inter) = x1 + x1*x2 + x2
p(mem) = 1
p(nil) = 1
p(s) = 1
p(true) = 0
p(app#) = x1
p(eq#) = 0
p(if#) = 0
p(ifinter#) = x3*x4 + x3^2 + x4^2
p(ifmem#) = 0
p(inter#) = x1*x2 + x1^2 + x2^2
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*l2 + l1^2 + l2^2
>= l1*l2 + l1^2 + l2^2
= inter#(l1,l2)
ifinter#(true(),x,l1,l2) = l1*l2 + l1^2 + l2^2
>= l1*l2 + l1^2 + l2^2
= inter#(l1,l2)
inter#(l1,app(l2,l3)) = 1 + l1 + l1*l2 + l1*l3 + l1^2 + 2*l2 + 2*l2*l3 + l2^2 + 2*l3 + l3^2
>= l1 + l1*l2 + l2
= app#(inter(l1,l2),inter(l1,l3))
inter#(l1,app(l2,l3)) = 1 + l1 + l1*l2 + l1*l3 + l1^2 + 2*l2 + 2*l2*l3 + l2^2 + 2*l3 + l3^2
>= l1*l2 + l1^2 + l2^2
= inter#(l1,l2)
inter#(l1,app(l2,l3)) = 1 + l1 + l1*l2 + l1*l3 + l1^2 + 2*l2 + 2*l2*l3 + l2^2 + 2*l3 + l3^2
>= l1*l3 + l1^2 + l3^2
= inter#(l1,l3)
inter#(l1,cons(x,l2)) = l1*l2 + l1^2 + l2^2
>= l1*l2 + l1^2 + l2^2
= ifinter#(mem(x,l1),x,l2,l1)
inter#(app(l1,l2),l3) = 1 + 2*l1 + 2*l1*l2 + l1*l3 + l1^2 + 2*l2 + l2*l3 + l2^2 + l3 + l3^2
>= l1 + l1*l3 + l3
= app#(inter(l1,l3),inter(l2,l3))
inter#(app(l1,l2),l3) = 1 + 2*l1 + 2*l1*l2 + l1*l3 + l1^2 + 2*l2 + l2*l3 + l2^2 + l3 + l3^2
>= l1*l3 + l1^2 + l3^2
= inter#(l1,l3)
inter#(app(l1,l2),l3) = 1 + 2*l1 + 2*l1*l2 + l1*l3 + l1^2 + 2*l2 + l2*l3 + l2^2 + l3 + l3^2
>= l2*l3 + l2^2 + l3^2
= inter#(l2,l3)
inter#(cons(x,l1),l2) = l1*l2 + l1^2 + l2^2
>= l1*l2 + l1^2 + l2^2
= 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) = 2 + 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()) = 1 + 2*x
>= 1
= 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) = 1 + 2*x
>= 1
= nil()
*** 1.1.1.1.1.1.1.1.2.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.2.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))
*** 1.1.1.1.1.1.1.1.2.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))
*** 1.1.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
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))
*** 1.1.1.1.1.2.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
UsableRules
Proof:
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))
*** 1.1.1.1.1.2.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
Proof:
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 DP Rules:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Problem (S)
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
*** 1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} 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.
*** 1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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) = x1 + x1*x2 + 2*x2
p(cons) = x1 + x2
p(eq) = 2*x1
p(false) = 0
p(if) = 2*x1*x3 + x1^2 + 2*x2*x3 + x2^2 + x3
p(ifinter) = 2*x2
p(ifmem) = 1 + 2*x1*x2 + x1*x3 + x3^2
p(inter) = 2
p(mem) = x1*x2
p(nil) = 0
p(s) = 1 + x1
p(true) = 0
p(app#) = x2
p(eq#) = x1*x2
p(if#) = 2 + x1*x2 + x1*x3 + 2*x2^2 + x3^2
p(ifinter#) = x3*x4
p(ifmem#) = x2*x3
p(inter#) = x1*x2
p(mem#) = x1*x2
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) = 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) = 0
Following rules are strictly oriented:
eq#(s(x),s(y)) = 1 + x + x*y + y
> x*y
= c_7(eq#(x,y))
Following rules are (at-least) weakly oriented:
ifinter#(false(),x,l1,l2) = l1*l2
>= l1*l2
= c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) = l1*l2
>= l1*l2
= c_11(inter#(l1,l2))
ifmem#(false(),x,l) = l*x
>= l*x
= c_12(mem#(x,l))
inter#(l1,app(l2,l3)) = l1*l2 + l1*l2*l3 + 2*l1*l3
>= l1*l2 + l1*l3
= c_14(inter#(l1,l2)
,inter#(l1,l3))
inter#(l1,cons(x,l2)) = l1*l2 + l1*x
>= l1*l2 + l1*x
= c_15(ifinter#(mem(x,l1),x,l2,l1)
,mem#(x,l1))
inter#(app(l1,l2),l3) = l1*l2*l3 + l1*l3 + 2*l2*l3
>= l1*l3 + l2*l3
= c_17(inter#(l1,l3)
,inter#(l2,l3))
inter#(cons(x,l1),l2) = l1*l2 + l2*x
>= l1*l2 + l2*x
= c_18(ifinter#(mem(x,l2),x,l1,l2)
,mem#(x,l2))
mem#(x,cons(y,l)) = l*x + x*y
>= l*x + x*y
= c_20(ifmem#(eq(x,y),x,l)
,eq#(x,y))
*** 1.1.1.1.1.2.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))
*** 1.1.1.1.1.2.1.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.2.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
eq#(s(x),s(y)) -> c_7(eq#(x,y))
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))
*** 1.1.1.1.1.2.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
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))
*** 1.1.1.1.1.2.1.1.1.2.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
3: ifmem#(false(),x,l) ->
c_12(mem#(x,l))
8: mem#(x,cons(y,l)) ->
c_20(ifmem#(eq(x,y),x,l))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.2.1.1.1.2.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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) = 0
p(app) = x1 + 2*x2
p(cons) = 1 + x1 + x2
p(eq) = x1 + x2
p(false) = 1
p(if) = 2*x2^2 + x3 + 2*x3^2
p(ifinter) = x1 + 2*x1*x4 + x1^2 + x2 + x3 + x4 + 2*x4^2
p(ifmem) = x1*x2 + 2*x2 + 3*x3
p(inter) = 0
p(mem) = x1*x2
p(nil) = 0
p(s) = 1 + x1
p(true) = 0
p(app#) = 2 + 2*x1 + 2*x2^2
p(eq#) = 1 + 2*x1
p(if#) = 2 + 2*x1*x3 + 2*x2 + 2*x2*x3
p(ifinter#) = x3*x4
p(ifmem#) = x1 + x2*x3 + x3
p(inter#) = x1*x2
p(mem#) = x1*x2 + x2
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = 1
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) = x1
p(c_13) = 0
p(c_14) = x1 + x2
p(c_15) = x1 + x2
p(c_16) = 1
p(c_17) = 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) = 1 + l + l*x
> l + l*x
= c_12(mem#(x,l))
mem#(x,cons(y,l)) = 1 + l + l*x + x + x*y + y
> l + l*x + x + y
= c_20(ifmem#(eq(x,y),x,l))
Following rules are (at-least) weakly oriented:
ifinter#(false(),x,l1,l2) = l1*l2
>= l1*l2
= c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) = l1*l2
>= l1*l2
= c_11(inter#(l1,l2))
inter#(l1,app(l2,l3)) = l1*l2 + 2*l1*l3
>= l1*l2 + l1*l3
= c_14(inter#(l1,l2)
,inter#(l1,l3))
inter#(l1,cons(x,l2)) = l1 + l1*l2 + l1*x
>= l1 + l1*l2 + l1*x
= c_15(ifinter#(mem(x,l1),x,l2,l1)
,mem#(x,l1))
inter#(app(l1,l2),l3) = l1*l3 + 2*l2*l3
>= l1*l3 + l2*l3
= c_17(inter#(l1,l3)
,inter#(l2,l3))
inter#(cons(x,l1),l2) = l1*l2 + l2 + l2*x
>= l1*l2 + l2 + l2*x
= c_18(ifinter#(mem(x,l2),x,l1,l2)
,mem#(x,l2))
eq(0(),0()) = 0
>= 0
= true()
eq(0(),s(x)) = 1 + x
>= 1
= false()
eq(s(x),0()) = 1 + x
>= 1
= false()
eq(s(x),s(y)) = 2 + x + y
>= x + y
= eq(x,y)
*** 1.1.1.1.1.2.1.1.1.2.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
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#(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))
Strict TRS Rules:
Weak DP Rules:
ifmem#(false(),x,l) -> c_12(mem#(x,l))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.1.2.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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#(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))
Strict TRS Rules:
Weak DP Rules:
ifmem#(false(),x,l) -> c_12(mem#(x,l))
mem#(x,cons(y,l)) -> c_20(ifmem#(eq(x,y),x,l))
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
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)):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),mem#(x,l1)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
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)):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),mem#(x,l1)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
3: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)):6
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,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),mem#(x,l1)):4
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,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: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)):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
5: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)):6
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,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),mem#(x,l1)):4
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,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: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)):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
7: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
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)):7
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))
7: ifmem#(false(),x,l) ->
c_12(mem#(x,l))
*** 1.1.1.1.1.2.1.1.1.2.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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#(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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
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)):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),mem#(x,l1)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
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)):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),mem#(x,l1)):4
-->_1 inter#(l1,app(l2,l3)) -> c_14(inter#(l1,l2),inter#(l1,l3)):3
3: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)):6
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,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),mem#(x,l1)):4
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,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:S: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)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
5: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)):6
-->_1 inter#(cons(x,l1),l2) -> c_18(ifinter#(mem(x,l2),x,l1,l2),mem#(x,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),mem#(x,l1)):4
-->_1 inter#(l1,cons(x,l2)) -> c_15(ifinter#(mem(x,l1),x,l2,l1),mem#(x,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:S: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)):2
-->_1 ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2)):1
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))
*** 1.1.1.1.1.2.1.1.1.2.1.1.2.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
3: inter#(l1,app(l2,l3)) ->
c_14(inter#(l1,l2)
,inter#(l1,l3))
4: inter#(l1,cons(x,l2)) ->
c_15(ifinter#(mem(x,l1)
,x
,l2
,l1))
5: inter#(app(l1,l2),l3) ->
c_17(inter#(l1,l3)
,inter#(l2,l3))
6: inter#(cons(x,l1),l2) ->
c_18(ifinter#(mem(x,l2)
,x
,l1
,l2))
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: inter#(l1,app(l2,l3)) ->
c_14(inter#(l1,l2)
,inter#(l1,l3))
4: inter#(l1,cons(x,l2)) ->
c_15(ifinter#(mem(x,l1)
,x
,l2
,l1))
5: inter#(app(l1,l2),l3) ->
c_17(inter#(l1,l3)
,inter#(l2,l3))
6: inter#(cons(x,l1),l2) ->
c_18(ifinter#(mem(x,l2)
,x
,l1
,l2))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{3,4,5,6}
These cover all (indirect) predecessors of dependency pairs
{1,2,3,4,5,6}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.2.1.1.1.2.1.1.2.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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) = 1
p(app) = 2 + x1 + x2
p(cons) = 1 + x2
p(eq) = x1 + x2
p(false) = 1
p(if) = x1*x3 + x2 + x2^2 + x3 + 2*x3^2
p(ifinter) = x1*x2 + x1*x3 + x1^2 + x2 + 2*x2*x3 + x2*x4 + x2^2 + x3 + 2*x4
p(ifmem) = 1 + x1 + x1*x2 + 3*x2^2 + 2*x3
p(inter) = 2*x1*x2 + 2*x1^2
p(mem) = x1^2
p(nil) = 0
p(s) = x1
p(true) = 0
p(app#) = 1 + 2*x2 + 2*x2^2
p(eq#) = 1
p(if#) = 2 + 2*x1 + x3
p(ifinter#) = 2*x3 + x3*x4 + 2*x4
p(ifmem#) = 2*x2 + x2*x3 + x2^2 + x3^2
p(inter#) = 2*x1 + x1*x2 + 2*x2
p(mem#) = x1^2 + x2 + x2^2
p(c_1) = 0
p(c_2) = 1 + x1
p(c_3) = 1
p(c_4) = 1
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) = 1
p(c_13) = 0
p(c_14) = x1 + x2
p(c_15) = x1
p(c_16) = 1
p(c_17) = 1 + x1 + x2
p(c_18) = x1
p(c_19) = 1
p(c_20) = 0
p(c_21) = 1
Following rules are strictly oriented:
inter#(l1,app(l2,l3)) = 4 + 4*l1 + l1*l2 + l1*l3 + 2*l2 + 2*l3
> 4*l1 + l1*l2 + l1*l3 + 2*l2 + 2*l3
= c_14(inter#(l1,l2)
,inter#(l1,l3))
inter#(l1,cons(x,l2)) = 2 + 3*l1 + l1*l2 + 2*l2
> 2*l1 + l1*l2 + 2*l2
= c_15(ifinter#(mem(x,l1)
,x
,l2
,l1))
inter#(app(l1,l2),l3) = 4 + 2*l1 + l1*l3 + 2*l2 + l2*l3 + 4*l3
> 1 + 2*l1 + l1*l3 + 2*l2 + l2*l3 + 4*l3
= c_17(inter#(l1,l3)
,inter#(l2,l3))
inter#(cons(x,l1),l2) = 2 + 2*l1 + l1*l2 + 3*l2
> 2*l1 + l1*l2 + 2*l2
= c_18(ifinter#(mem(x,l2)
,x
,l1
,l2))
Following rules are (at-least) weakly oriented:
ifinter#(false(),x,l1,l2) = 2*l1 + l1*l2 + 2*l2
>= 2*l1 + l1*l2 + 2*l2
= c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) = 2*l1 + l1*l2 + 2*l2
>= 2*l1 + l1*l2 + 2*l2
= c_11(inter#(l1,l2))
*** 1.1.1.1.1.2.1.1.1.2.1.1.2.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
ifinter#(false(),x,l1,l2) -> c_10(inter#(l1,l2))
ifinter#(true(),x,l1,l2) -> c_11(inter#(l1,l2))
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.1.2.1.1.2.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))
*** 1.1.1.1.1.2.1.1.1.2.1.1.2.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()
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
basic terms: {app#,eq#,if#,ifinter#,ifmem#,inter#,mem#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).