tct
YES(O(1),O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Weak Trs:
{ #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add following dependency tuples
Strict DPs:
{ #equal^#(@x, @y) -> #eq^#(@x, @y)
, and^#(@x, @y) -> #and^#(@x, @y)
, eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, eq#3^#(nil(), @x, @xs) -> c_7()
, eq#2^#(::(@y, @ys)) -> c_8()
, eq#2^#(nil()) -> c_9()
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, nub#1^#(nil()) -> c_12()
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#1^#(nil(), @x) -> c_15()
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, #eq^#(nil(), nil()) -> c_21()
, #eq^#(#0(), #0()) -> c_22()
, #eq^#(#0(), #neg(@y)) -> c_23()
, #eq^#(#0(), #pos(@y)) -> c_24()
, #eq^#(#0(), #s(@y)) -> c_25()
, #eq^#(#neg(@x), #0()) -> c_26()
, #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, #eq^#(#neg(@x), #pos(@y)) -> c_28()
, #eq^#(#pos(@x), #0()) -> c_29()
, #eq^#(#pos(@x), #neg(@y)) -> c_30()
, #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, #eq^#(#s(@x), #0()) -> c_32()
, #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, #and^#(#false(), #false()) -> c_34()
, #and^#(#false(), #true()) -> c_35()
, #and^#(#true(), #false()) -> c_36()
, #and^#(#true(), #true()) -> c_37() }
and replace the set of basic marked basic terms accordingly.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ #equal^#(@x, @y) -> #eq^#(@x, @y)
, and^#(@x, @y) -> #and^#(@x, @y)
, eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, eq#3^#(nil(), @x, @xs) -> c_7()
, eq#2^#(::(@y, @ys)) -> c_8()
, eq#2^#(nil()) -> c_9()
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, nub#1^#(nil()) -> c_12()
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#1^#(nil(), @x) -> c_15()
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, #eq^#(nil(), nil()) -> c_21()
, #eq^#(#0(), #0()) -> c_22()
, #eq^#(#0(), #neg(@y)) -> c_23()
, #eq^#(#0(), #pos(@y)) -> c_24()
, #eq^#(#0(), #s(@y)) -> c_25()
, #eq^#(#neg(@x), #0()) -> c_26()
, #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, #eq^#(#neg(@x), #pos(@y)) -> c_28()
, #eq^#(#pos(@x), #0()) -> c_29()
, #eq^#(#pos(@x), #neg(@y)) -> c_30()
, #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, #eq^#(#s(@x), #0()) -> c_32()
, #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, #and^#(#false(), #false()) -> c_34()
, #and^#(#false(), #true()) -> c_35()
, #and^#(#true(), #false()) -> c_36()
, #and^#(#true(), #true()) -> c_37() }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: #equal^#(@x, @y) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
-->_1 #eq^#(#s(@x), #0()) -> c_32() :32
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_1 #eq^#(#0(), #0()) -> c_22() :22
-->_1 #eq^#(nil(), nil()) -> c_21() :21
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
2: and^#(@x, @y) -> #and^#(@x, @y)
-->_1 #and^#(#true(), #true()) -> c_37() :37
-->_1 #and^#(#true(), #false()) -> c_36() :36
-->_1 #and^#(#false(), #true()) -> c_35() :35
-->_1 #and^#(#false(), #false()) -> c_34() :34
3: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(nil(), @l2) -> eq#2^#(@l2) :5
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :4
4: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys)) :6
-->_1 eq#3^#(nil(), @x, @xs) -> c_7() :7
5: eq#1^#(nil(), @l2) -> eq#2^#(@l2)
-->_1 eq#2^#(nil()) -> c_9() :9
-->_1 eq#2^#(::(@y, @ys)) -> c_8() :8
6: eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
-->_3 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :3
-->_1 and^#(@x, @y) -> #and^#(@x, @y) :2
-->_2 #equal^#(@x, @y) -> #eq^#(@x, @y) :1
7: eq#3^#(nil(), @x, @xs) -> c_7()
8: eq#2^#(::(@y, @ys)) -> c_8()
9: eq#2^#(nil()) -> c_9()
10: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :11
-->_1 nub#1^#(nil()) -> c_12() :12
11: nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :13
-->_1 nub^#(@l) -> nub#1^#(@l) :10
12: nub#1^#(nil()) -> c_12()
13: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :14
-->_1 remove#1^#(nil(), @x) -> c_15() :15
14: remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :17
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :16
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :3
15: remove#1^#(nil(), @x) -> c_15()
16: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :13
17: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :13
18: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
-->_3 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_2 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_3 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_2 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_3 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_2 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #and^#(#true(), #true()) -> c_37() :37
-->_1 #and^#(#true(), #false()) -> c_36() :36
-->_1 #and^#(#false(), #true()) -> c_35() :35
-->_1 #and^#(#false(), #false()) -> c_34() :34
-->_3 #eq^#(#s(@x), #0()) -> c_32() :32
-->_2 #eq^#(#s(@x), #0()) -> c_32() :32
-->_3 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_2 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_3 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_2 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_3 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_2 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_3 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_2 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_3 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_2 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_3 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_2 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_3 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_2 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_3 #eq^#(#0(), #0()) -> c_22() :22
-->_2 #eq^#(#0(), #0()) -> c_22() :22
-->_3 #eq^#(nil(), nil()) -> c_21() :21
-->_2 #eq^#(nil(), nil()) -> c_21() :21
-->_3 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_2 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_3 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_2 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_3 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
-->_2 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
19: #eq^#(::(@x_1, @x_2), nil()) -> c_19()
20: #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
21: #eq^#(nil(), nil()) -> c_21()
22: #eq^#(#0(), #0()) -> c_22()
23: #eq^#(#0(), #neg(@y)) -> c_23()
24: #eq^#(#0(), #pos(@y)) -> c_24()
25: #eq^#(#0(), #s(@y)) -> c_25()
26: #eq^#(#neg(@x), #0()) -> c_26()
27: #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_1 #eq^#(#s(@x), #0()) -> c_32() :32
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_1 #eq^#(#0(), #0()) -> c_22() :22
-->_1 #eq^#(nil(), nil()) -> c_21() :21
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
28: #eq^#(#neg(@x), #pos(@y)) -> c_28()
29: #eq^#(#pos(@x), #0()) -> c_29()
30: #eq^#(#pos(@x), #neg(@y)) -> c_30()
31: #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_1 #eq^#(#s(@x), #0()) -> c_32() :32
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_1 #eq^#(#0(), #0()) -> c_22() :22
-->_1 #eq^#(nil(), nil()) -> c_21() :21
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
32: #eq^#(#s(@x), #0()) -> c_32()
33: #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_1 #eq^#(#s(@x), #0()) -> c_32() :32
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_1 #eq^#(#0(), #0()) -> c_22() :22
-->_1 #eq^#(nil(), nil()) -> c_21() :21
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
34: #and^#(#false(), #false()) -> c_34()
35: #and^#(#false(), #true()) -> c_35()
36: #and^#(#true(), #false()) -> c_36()
37: #and^#(#true(), #true()) -> c_37()
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {12} and add Pre({12}) = {10} to the strict component.
- We remove {15} and add Pre({15}) = {13} to the strict component.
- We remove {7} and add Pre({7}) = {4} to the strict component.
- We remove {8} and add Pre({8}) = {5} to the strict component.
- We remove {9} and add Pre({9}) = {5} to the strict component.
- We remove {2} and add Pre({2}) = {6} to the strict component.
- We remove {1} and add Pre({1}) = {6} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ #equal^#(@x, @y) -> #eq^#(@x, @y)
, #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, #eq^#(nil(), nil()) -> c_21()
, #eq^#(#0(), #0()) -> c_22()
, #eq^#(#0(), #neg(@y)) -> c_23()
, #eq^#(#0(), #pos(@y)) -> c_24()
, #eq^#(#0(), #s(@y)) -> c_25()
, #eq^#(#neg(@x), #0()) -> c_26()
, #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, #eq^#(#neg(@x), #pos(@y)) -> c_28()
, #eq^#(#pos(@x), #0()) -> c_29()
, #eq^#(#pos(@x), #neg(@y)) -> c_30()
, #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, #eq^#(#s(@x), #0()) -> c_32()
, #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, and^#(@x, @y) -> #and^#(@x, @y)
, #and^#(#false(), #false()) -> c_34()
, #and^#(#false(), #true()) -> c_35()
, #and^#(#true(), #false()) -> c_36()
, #and^#(#true(), #true()) -> c_37()
, eq#3^#(nil(), @x, @xs) -> c_7()
, eq#2^#(::(@y, @ys)) -> c_8()
, eq#2^#(nil()) -> c_9()
, nub#1^#(nil()) -> c_12()
, remove#1^#(nil(), @x) -> c_15() }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(nil(), @l2) -> eq#2^#(@l2) :3
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :2
2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys)) :4
-->_1 eq#3^#(nil(), @x, @xs) -> c_7() :33
3: eq#1^#(nil(), @l2) -> eq#2^#(@l2)
-->_1 eq#2^#(nil()) -> c_9() :35
-->_1 eq#2^#(::(@y, @ys)) -> c_8() :34
4: eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
-->_1 and^#(@x, @y) -> #and^#(@x, @y) :28
-->_2 #equal^#(@x, @y) -> #eq^#(@x, @y) :11
-->_3 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
5: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :6
-->_1 nub#1^#(nil()) -> c_12() :36
6: nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :7
-->_1 nub^#(@l) -> nub#1^#(@l) :5
7: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :8
-->_1 remove#1^#(nil(), @x) -> c_15() :37
8: remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :10
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
9: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :7
10: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :7
11: #equal^#(@x, @y) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
-->_1 #eq^#(#s(@x), #0()) -> c_32() :26
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_1 #eq^#(#0(), #0()) -> c_22() :16
-->_1 #eq^#(nil(), nil()) -> c_21() :15
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
12: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
-->_3 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_2 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_3 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_2 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_3 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_2 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #and^#(#true(), #true()) -> c_37() :32
-->_1 #and^#(#true(), #false()) -> c_36() :31
-->_1 #and^#(#false(), #true()) -> c_35() :30
-->_1 #and^#(#false(), #false()) -> c_34() :29
-->_3 #eq^#(#s(@x), #0()) -> c_32() :26
-->_2 #eq^#(#s(@x), #0()) -> c_32() :26
-->_3 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_2 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_3 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_2 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_3 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_2 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_3 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_2 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_3 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_2 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_3 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_2 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_3 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_2 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_3 #eq^#(#0(), #0()) -> c_22() :16
-->_2 #eq^#(#0(), #0()) -> c_22() :16
-->_3 #eq^#(nil(), nil()) -> c_21() :15
-->_2 #eq^#(nil(), nil()) -> c_21() :15
-->_3 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_2 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_3 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_2 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_3 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
-->_2 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
13: #eq^#(::(@x_1, @x_2), nil()) -> c_19()
14: #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
15: #eq^#(nil(), nil()) -> c_21()
16: #eq^#(#0(), #0()) -> c_22()
17: #eq^#(#0(), #neg(@y)) -> c_23()
18: #eq^#(#0(), #pos(@y)) -> c_24()
19: #eq^#(#0(), #s(@y)) -> c_25()
20: #eq^#(#neg(@x), #0()) -> c_26()
21: #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_1 #eq^#(#s(@x), #0()) -> c_32() :26
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_1 #eq^#(#0(), #0()) -> c_22() :16
-->_1 #eq^#(nil(), nil()) -> c_21() :15
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
22: #eq^#(#neg(@x), #pos(@y)) -> c_28()
23: #eq^#(#pos(@x), #0()) -> c_29()
24: #eq^#(#pos(@x), #neg(@y)) -> c_30()
25: #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#s(@x), #0()) -> c_32() :26
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_1 #eq^#(#0(), #0()) -> c_22() :16
-->_1 #eq^#(nil(), nil()) -> c_21() :15
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
26: #eq^#(#s(@x), #0()) -> c_32()
27: #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#s(@x), #0()) -> c_32() :26
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_1 #eq^#(#0(), #0()) -> c_22() :16
-->_1 #eq^#(nil(), nil()) -> c_21() :15
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
28: and^#(@x, @y) -> #and^#(@x, @y)
-->_1 #and^#(#true(), #true()) -> c_37() :32
-->_1 #and^#(#true(), #false()) -> c_36() :31
-->_1 #and^#(#false(), #true()) -> c_35() :30
-->_1 #and^#(#false(), #false()) -> c_34() :29
29: #and^#(#false(), #false()) -> c_34()
30: #and^#(#false(), #true()) -> c_35()
31: #and^#(#true(), #false()) -> c_36()
32: #and^#(#true(), #true()) -> c_37()
33: eq#3^#(nil(), @x, @xs) -> c_7()
34: eq#2^#(::(@y, @ys)) -> c_8()
35: eq#2^#(nil()) -> c_9()
36: nub#1^#(nil()) -> c_12()
37: remove#1^#(nil(), @x) -> c_15()
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ #equal^#(@x, @y) -> #eq^#(@x, @y)
, #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, #eq^#(nil(), nil()) -> c_21()
, #eq^#(#0(), #0()) -> c_22()
, #eq^#(#0(), #neg(@y)) -> c_23()
, #eq^#(#0(), #pos(@y)) -> c_24()
, #eq^#(#0(), #s(@y)) -> c_25()
, #eq^#(#neg(@x), #0()) -> c_26()
, #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, #eq^#(#neg(@x), #pos(@y)) -> c_28()
, #eq^#(#pos(@x), #0()) -> c_29()
, #eq^#(#pos(@x), #neg(@y)) -> c_30()
, #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, #eq^#(#s(@x), #0()) -> c_32()
, #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, and^#(@x, @y) -> #and^#(@x, @y)
, #and^#(#false(), #false()) -> c_34()
, #and^#(#false(), #true()) -> c_35()
, #and^#(#true(), #false()) -> c_36()
, #and^#(#true(), #true()) -> c_37()
, eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, eq#3^#(nil(), @x, @xs) -> c_7()
, eq#2^#(::(@y, @ys)) -> c_8()
, eq#2^#(nil()) -> c_9()
, nub#1^#(nil()) -> c_12()
, remove#1^#(nil(), @x) -> c_15() }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the the dependency graph
->1:{4,5}
|
|->3:{6,9,7,8}
| |
| |->5:{1,3,2}
| | |
| | |->7:{10} Weak SCC
| | | |
| | | |->9:{12} Weak SCC
| | | |
| | | |->10:{13} Weak SCC
| | | |
| | | |->11:{14} Weak SCC
| | | |
| | | |->12:{15} Weak SCC
| | | |
| | | |->13:{16} Weak SCC
| | | |
| | | |->14:{17} Weak SCC
| | | |
| | | |->15:{18} Weak SCC
| | | |
| | | |->16:{19} Weak SCC
| | | |
| | | |->17:{21} Weak SCC
| | | |
| | | |->18:{22} Weak SCC
| | | |
| | | |->19:{23} Weak SCC
| | | |
| | | |->20:{25} Weak SCC
| | | |
| | | `->8:{26,24,20,11} Weak SCC
| | | |
| | | |->9:{12} Weak SCC
| | | |
| | | |->10:{13} Weak SCC
| | | |
| | | |->11:{14} Weak SCC
| | | |
| | | |->12:{15} Weak SCC
| | | |
| | | |->13:{16} Weak SCC
| | | |
| | | |->14:{17} Weak SCC
| | | |
| | | |->15:{18} Weak SCC
| | | |
| | | |->16:{19} Weak SCC
| | | |
| | | |->17:{21} Weak SCC
| | | |
| | | |->18:{22} Weak SCC
| | | |
| | | |->19:{23} Weak SCC
| | | |
| | | |->20:{25} Weak SCC
| | | |
| | | |->22:{28} Weak SCC
| | | |
| | | |->23:{29} Weak SCC
| | | |
| | | |->24:{30} Weak SCC
| | | |
| | | `->25:{31} Weak SCC
| | |
| | |->21:{27} Weak SCC
| | | |
| | | |->22:{28} Weak SCC
| | | |
| | | |->23:{29} Weak SCC
| | | |
| | | |->24:{30} Weak SCC
| | | |
| | | `->25:{31} Weak SCC
| | |
| | |->26:{32} Weak SCC
| | | |
| | | |->27:{34} Weak SCC
| | | |
| | | `->28:{35} Weak SCC
| | |
| | `->6:{33} Weak SCC
| |
| `->4:{37} Weak SCC
|
`->2:{36} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, 2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, 3: eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, 4: nub^#(@l) -> nub#1^#(@l)
, 5: nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, 6: remove^#(@x, @l) -> remove#1^#(@l, @x)
, 7: remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, 8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, 9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ 10: #equal^#(@x, @y) -> #eq^#(@x, @y)
, 11: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, 12: #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, 13: #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, 14: #eq^#(nil(), nil()) -> c_21()
, 15: #eq^#(#0(), #0()) -> c_22()
, 16: #eq^#(#0(), #neg(@y)) -> c_23()
, 17: #eq^#(#0(), #pos(@y)) -> c_24()
, 18: #eq^#(#0(), #s(@y)) -> c_25()
, 19: #eq^#(#neg(@x), #0()) -> c_26()
, 20: #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, 21: #eq^#(#neg(@x), #pos(@y)) -> c_28()
, 22: #eq^#(#pos(@x), #0()) -> c_29()
, 23: #eq^#(#pos(@x), #neg(@y)) -> c_30()
, 24: #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, 25: #eq^#(#s(@x), #0()) -> c_32()
, 26: #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, 27: and^#(@x, @y) -> #and^#(@x, @y)
, 28: #and^#(#false(), #false()) -> c_34()
, 29: #and^#(#false(), #true()) -> c_35()
, 30: #and^#(#true(), #false()) -> c_36()
, 31: #and^#(#true(), #true()) -> c_37()
, 32: eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, 33: eq#3^#(nil(), @x, @xs) -> c_7()
, 34: eq#2^#(::(@y, @ys)) -> c_8()
, 35: eq#2^#(nil()) -> c_9()
, 36: nub#1^#(nil()) -> c_12()
, 37: remove#1^#(nil(), @x) -> c_15() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 36: nub#1^#(nil()) -> c_12()
, 37: remove#1^#(nil(), @x) -> c_15()
, 33: eq#3^#(nil(), @x, @xs) -> c_7()
, 10: #equal^#(@x, @y) -> #eq^#(@x, @y)
, 26: #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, 24: #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, 20: #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, 11: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, 12: #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, 13: #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, 14: #eq^#(nil(), nil()) -> c_21()
, 15: #eq^#(#0(), #0()) -> c_22()
, 16: #eq^#(#0(), #neg(@y)) -> c_23()
, 17: #eq^#(#0(), #pos(@y)) -> c_24()
, 18: #eq^#(#0(), #s(@y)) -> c_25()
, 19: #eq^#(#neg(@x), #0()) -> c_26()
, 21: #eq^#(#neg(@x), #pos(@y)) -> c_28()
, 22: #eq^#(#pos(@x), #0()) -> c_29()
, 23: #eq^#(#pos(@x), #neg(@y)) -> c_30()
, 25: #eq^#(#s(@x), #0()) -> c_32()
, 27: and^#(@x, @y) -> #and^#(@x, @y)
, 28: #and^#(#false(), #false()) -> c_34()
, 29: #and^#(#false(), #true()) -> c_35()
, 30: #and^#(#true(), #false()) -> c_36()
, 31: #and^#(#true(), #true()) -> c_37()
, 32: eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, 34: eq#2^#(::(@y, @ys)) -> c_8()
, 35: eq#2^#(nil()) -> c_9() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the following dependency-graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :2
2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys)) :3
3: eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
-->_3 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
4: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :5
5: nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
-->_1 nub^#(@l) -> nub#1^#(@l) :4
6: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :7
7: remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :2
2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :3
3: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
4: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :5
5: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
-->_1 nub^#(@l) -> nub#1^#(@l) :4
6: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :7
7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs: { eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :2
2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :9
3: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :4
4: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :5
-->_1 nub^#(@l) -> nub#1^#(@l) :3
5: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :6
6: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :7
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
7: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :5
8: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :5
9: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :8
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :3
3: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
-->_1 nub^#(@l) -> nub#1^#(@l) :2
4: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :5
5: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :7
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :6
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
6: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
7: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
8: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :9
9: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {7} and add Pre({7}) = {5} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :7
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :3
3: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
-->_1 nub^#(@l) -> nub#1^#(@l) :2
4: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :5
5: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :6
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
6: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
7: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :8
8: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {6} and add Pre({6}) = {5} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :6
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :3
3: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
-->_1 nub^#(@l) -> nub#1^#(@l) :2
4: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :5
5: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
6: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :7
7: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {5} and add Pre({5}) = {4} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :5
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :3
3: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
-->_1 nub^#(@l) -> nub#1^#(@l) :2
4: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :7
5: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :6
6: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, remove^#(@x, @l) -> remove#1^#(@l, @x) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, remove^#(@x, @l) -> remove#1^#(@l, @x) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 2: nub^#(@l) -> nub#1^#(@l)
, 4: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, 5: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, 6: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, 7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) }
Trs:
{ #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #and(#true(), #true()) -> #true()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#equal) = {}, Uargs(#eq) = {}, Uargs(and) = {},
Uargs(#and) = {}, Uargs(eq) = {}, Uargs(eq#1) = {}, Uargs(::) = {},
Uargs(eq#3) = {}, Uargs(eq#2) = {}, Uargs(remove) = {},
Uargs(remove#1) = {}, Uargs(remove#2) = {}, Uargs(#neg) = {},
Uargs(#pos) = {}, Uargs(#s) = {}, Uargs(#equal^#) = {},
Uargs(#eq^#) = {}, Uargs(and^#) = {}, Uargs(#and^#) = {},
Uargs(eq^#) = {}, Uargs(eq#1^#) = {}, Uargs(eq#3^#) = {},
Uargs(eq#2^#) = {}, Uargs(nub^#) = {}, Uargs(nub#1^#) = {},
Uargs(remove^#) = {}, Uargs(remove#1^#) = {},
Uargs(remove#2^#) = {}, Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#equal](x1, x2) = [3 3] x1 + [3 3] x2 + [0]
[0 1] [2 3] [2]
[#eq](x1, x2) = [1 2] x1 + [2 0] x2 + [0]
[0 1] [1 1] [1]
[and](x1, x2) = [0 0] x2 + [3]
[0 1] [0]
[#and](x1, x2) = [0 0] x2 + [3]
[0 1] [0]
[eq](x1, x2) = [1 2] x1 + [1 1] x2 + [0]
[0 0] [0 1] [0]
[eq#1](x1, x2) = [0 1] x1 + [1 1] x2 + [0]
[0 0] [0 1] [0]
[::](x1, x2) = [0 2] x1 + [1 3] x2 + [1]
[0 1] [0 1] [2]
[eq#3](x1, x2, x3) = [1 0] x1 + [2]
[0 1] [0]
[nil] = [1]
[1]
[eq#2](x1) = [1 1] x1 + [1]
[0 1] [0]
[#false] = [3]
[1]
[#true] = [0]
[1]
[remove](x1, x2) = [1 0] x2 + [0]
[0 1] [0]
[remove#1](x1, x2) = [1 0] x1 + [0]
[0 1] [0]
[remove#2](x1, x2, x3, x4) = [0 2] x3 + [1 3] x4 + [1]
[0 1] [0 1] [2]
[#0] = [2]
[0]
[#neg](x1) = [1 0] x1 + [3]
[0 1] [1]
[#pos](x1) = [1 2] x1 + [1]
[0 1] [2]
[#s](x1) = [1 0] x1 + [2]
[0 1] [3]
[#equal^#](x1, x2) = [0]
[0]
[#eq^#](x1, x2) = [0]
[0]
[and^#](x1, x2) = [0]
[0]
[#and^#](x1, x2) = [0]
[0]
[eq^#](x1, x2) = [0 1] x2 + [2]
[3 0] [1]
[eq#1^#](x1, x2) = [0 1] x2 + [2]
[3 0] [0]
[eq#3^#](x1, x2, x3) = [0 1] x1 + [1]
[3 0] [0]
[eq#2^#](x1) = [0]
[0]
[nub^#](x1) = [3 3] x1 + [1]
[0 1] [0]
[nub#1^#](x1) = [3 3] x1 + [0]
[0 0] [0]
[remove^#](x1, x2) = [0 2] x1 + [0 3] x2 + [1]
[0 0] [0 0] [0]
[remove#1^#](x1, x2) = [0 3] x1 + [0 2] x2 + [1]
[0 0] [0 0] [0]
[remove#2^#](x1, x2, x3, x4) = [0 1] x1 + [0 2] x2 + [0 3] x4 + [0]
[0 1] [0 0] [0 0] [1]
[c_1](x1, x2) = [1 2] x1 + [2 2] x2 + [1]
[0 0] [0 0] [0]
[c_2](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
This order satisfies following ordering constraints
[#equal(@x, @y)] = [3 3] @x + [3 3] @y + [0]
[0 1] [2 3] [2]
>= [1 2] @x + [2 0] @y + [0]
[0 1] [1 1] [1]
= [#eq(@x, @y)]
[#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [0 4] @x_1 + [1 5] @x_2 + [0 4] @y_1 + [2 6] @y_2 + [7]
[0 1] [0 1] [0 3] [1 4] [6]
> [0 0] @x_2 + [0 0] @y_2 + [3]
[0 1] [1 1] [1]
= [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))]
[#eq(::(@x_1, @x_2), nil())] = [0 4] @x_1 + [1 5] @x_2 + [7]
[0 1] [0 1] [5]
> [3]
[1]
= [#false()]
[#eq(nil(), ::(@y_1, @y_2))] = [0 4] @y_1 + [2 6] @y_2 + [5]
[0 3] [1 4] [5]
> [3]
[1]
= [#false()]
[#eq(nil(), nil())] = [5]
[4]
> [0]
[1]
= [#true()]
[#eq(#0(), #0())] = [6]
[3]
> [0]
[1]
= [#true()]
[#eq(#0(), #neg(@y))] = [2 0] @y + [8]
[1 1] [5]
> [3]
[1]
= [#false()]
[#eq(#0(), #pos(@y))] = [2 4] @y + [4]
[1 3] [4]
> [3]
[1]
= [#false()]
[#eq(#0(), #s(@y))] = [2 0] @y + [6]
[1 1] [6]
> [3]
[1]
= [#false()]
[#eq(#neg(@x), #0())] = [1 2] @x + [9]
[0 1] [4]
> [3]
[1]
= [#false()]
[#eq(#neg(@x), #neg(@y))] = [1 2] @x + [2 0] @y + [11]
[0 1] [1 1] [6]
> [1 2] @x + [2 0] @y + [0]
[0 1] [1 1] [1]
= [#eq(@x, @y)]
[#eq(#neg(@x), #pos(@y))] = [1 2] @x + [2 4] @y + [7]
[0 1] [1 3] [5]
> [3]
[1]
= [#false()]
[#eq(#pos(@x), #0())] = [1 4] @x + [9]
[0 1] [5]
> [3]
[1]
= [#false()]
[#eq(#pos(@x), #neg(@y))] = [1 4] @x + [2 0] @y + [11]
[0 1] [1 1] [7]
> [3]
[1]
= [#false()]
[#eq(#pos(@x), #pos(@y))] = [1 4] @x + [2 4] @y + [7]
[0 1] [1 3] [6]
> [1 2] @x + [2 0] @y + [0]
[0 1] [1 1] [1]
= [#eq(@x, @y)]
[#eq(#s(@x), #0())] = [1 2] @x + [12]
[0 1] [6]
> [3]
[1]
= [#false()]
[#eq(#s(@x), #s(@y))] = [1 2] @x + [2 0] @y + [12]
[0 1] [1 1] [9]
> [1 2] @x + [2 0] @y + [0]
[0 1] [1 1] [1]
= [#eq(@x, @y)]
[and(@x, @y)] = [0 0] @y + [3]
[0 1] [0]
>= [0 0] @y + [3]
[0 1] [0]
= [#and(@x, @y)]
[#and(#false(), #false())] = [3]
[1]
>= [3]
[1]
= [#false()]
[#and(#false(), #true())] = [3]
[1]
>= [3]
[1]
= [#false()]
[#and(#true(), #false())] = [3]
[1]
>= [3]
[1]
= [#false()]
[#and(#true(), #true())] = [3]
[1]
> [0]
[1]
= [#true()]
[eq(@l1, @l2)] = [1 2] @l1 + [1 1] @l2 + [0]
[0 0] [0 1] [0]
>= [0 1] @l1 + [1 1] @l2 + [0]
[0 0] [0 1] [0]
= [eq#1(@l1, @l2)]
[eq#1(::(@x, @xs), @l2)] = [1 1] @l2 + [0 1] @x + [0 1] @xs + [2]
[0 1] [0 0] [0 0] [0]
>= [1 0] @l2 + [2]
[0 1] [0]
= [eq#3(@l2, @x, @xs)]
[eq#1(nil(), @l2)] = [1 1] @l2 + [1]
[0 1] [0]
>= [1 1] @l2 + [1]
[0 1] [0]
= [eq#2(@l2)]
[eq#3(::(@y, @ys), @x, @xs)] = [0 2] @y + [1 3] @ys + [3]
[0 1] [0 1] [2]
>= [0 0] @ys + [3]
[0 1] [0]
= [and(#equal(@x, @y), eq(@xs, @ys))]
[eq#3(nil(), @x, @xs)] = [3]
[1]
>= [3]
[1]
= [#false()]
[eq#2(::(@y, @ys))] = [0 3] @y + [1 4] @ys + [4]
[0 1] [0 1] [2]
> [3]
[1]
= [#false()]
[eq#2(nil())] = [3]
[1]
> [0]
[1]
= [#true()]
[remove(@x, @l)] = [1 0] @l + [0]
[0 1] [0]
>= [1 0] @l + [0]
[0 1] [0]
= [remove#1(@l, @x)]
[remove#1(::(@y, @ys), @x)] = [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
>= [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
= [remove#2(eq(@x, @y), @x, @y, @ys)]
[remove#1(nil(), @x)] = [1]
[1]
>= [1]
[1]
= [nil()]
[remove#2(#false(), @x, @y, @ys)] = [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
>= [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
= [::(@y, remove(@x, @ys))]
[remove#2(#true(), @x, @y, @ys)] = [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
> [1 0] @ys + [0]
[0 1] [0]
= [remove(@x, @ys)]
[eq^#(@l1, @l2)] = [0 1] @l2 + [2]
[3 0] [1]
>= [0 1] @l2 + [2]
[3 0] [0]
= [eq#1^#(@l1, @l2)]
[eq#1^#(::(@x, @xs), @l2)] = [0 1] @l2 + [2]
[3 0] [0]
> [0 1] @l2 + [1]
[3 0] [0]
= [eq#3^#(@l2, @x, @xs)]
[eq#3^#(::(@y, @ys), @x, @xs)] = [0 1] @y + [0 1] @ys + [3]
[0 6] [3 9] [3]
> [0 1] @ys + [2]
[3 0] [1]
= [eq^#(@xs, @ys)]
[nub^#(@l)] = [3 3] @l + [1]
[0 1] [0]
> [3 3] @l + [0]
[0 0] [0]
= [nub#1^#(@l)]
[nub#1^#(::(@x, @xs))] = [0 9] @x + [3 12] @xs + [9]
[0 0] [0 0] [0]
> [0 4] @x + [3 11] @xs + [4]
[0 0] [0 0] [0]
= [c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))]
[remove^#(@x, @l)] = [0 3] @l + [0 2] @x + [1]
[0 0] [0 0] [0]
>= [0 3] @l + [0 2] @x + [1]
[0 0] [0 0] [0]
= [remove#1^#(@l, @x)]
[remove#1^#(::(@y, @ys), @x)] = [0 2] @x + [0 3] @y + [0 3] @ys + [7]
[0 0] [0 0] [0 0] [0]
> [0 2] @x + [0 3] @y + [0 3] @ys + [3]
[0 0] [0 0] [0 0] [0]
= [c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))]
[remove#2^#(#false(), @x, @y, @ys)] = [0 2] @x + [0 3] @ys + [1]
[0 0] [0 0] [2]
>= [0 2] @x + [0 3] @ys + [1]
[0 0] [0 0] [0]
= [remove^#(@x, @ys)]
[remove#2^#(#true(), @x, @y, @ys)] = [0 2] @x + [0 3] @ys + [1]
[0 0] [0 0] [2]
>= [0 2] @x + [0 3] @ys + [1]
[0 0] [0 0] [0]
= [remove^#(@x, @ys)]
Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of rules
{2,4,5,6,7}. Here rules are labeled according to the (estimated)
dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :4
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :6
3: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :7
4: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :5
5: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
6: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :3
-->_1 nub^#(@l) -> nub#1^#(@l) :2
7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :3
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :3
- The rules {2,4,5,6,7} have known complexity. These cover all
predecessors of {1,8,9}, their complexity is equally bounded.
- The rules {1,2,4,5,6,7,8,9} have known complexity. These cover
all predecessors of {3}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4,5,6,7,8,9} is given by YES(?,O(n^2)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{4,5} Weak SCC
|
`->2:{6,9,7,8} Weak SCC
|
`->3:{1,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, 2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, 3: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, 4: nub^#(@l) -> nub#1^#(@l)
, 5: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, 6: remove^#(@x, @l) -> remove#1^#(@l, @x)
, 7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, 8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, 9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 4: nub^#(@l) -> nub#1^#(@l)
, 5: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, 6: remove^#(@x, @l) -> remove#1^#(@l, @x)
, 9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
, 7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, 8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, 1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, 3: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, 2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))
tct-popstar
YES(O(1),O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Weak Trs:
{ #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add following dependency tuples
Strict DPs:
{ #equal^#(@x, @y) -> #eq^#(@x, @y)
, and^#(@x, @y) -> #and^#(@x, @y)
, eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, eq#3^#(nil(), @x, @xs) -> c_7()
, eq#2^#(::(@y, @ys)) -> c_8()
, eq#2^#(nil()) -> c_9()
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, nub#1^#(nil()) -> c_12()
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#1^#(nil(), @x) -> c_15()
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, #eq^#(nil(), nil()) -> c_21()
, #eq^#(#0(), #0()) -> c_22()
, #eq^#(#0(), #neg(@y)) -> c_23()
, #eq^#(#0(), #pos(@y)) -> c_24()
, #eq^#(#0(), #s(@y)) -> c_25()
, #eq^#(#neg(@x), #0()) -> c_26()
, #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, #eq^#(#neg(@x), #pos(@y)) -> c_28()
, #eq^#(#pos(@x), #0()) -> c_29()
, #eq^#(#pos(@x), #neg(@y)) -> c_30()
, #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, #eq^#(#s(@x), #0()) -> c_32()
, #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, #and^#(#false(), #false()) -> c_34()
, #and^#(#false(), #true()) -> c_35()
, #and^#(#true(), #false()) -> c_36()
, #and^#(#true(), #true()) -> c_37() }
and replace the set of basic marked basic terms accordingly.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ #equal^#(@x, @y) -> #eq^#(@x, @y)
, and^#(@x, @y) -> #and^#(@x, @y)
, eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, eq#3^#(nil(), @x, @xs) -> c_7()
, eq#2^#(::(@y, @ys)) -> c_8()
, eq#2^#(nil()) -> c_9()
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, nub#1^#(nil()) -> c_12()
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#1^#(nil(), @x) -> c_15()
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, #eq^#(nil(), nil()) -> c_21()
, #eq^#(#0(), #0()) -> c_22()
, #eq^#(#0(), #neg(@y)) -> c_23()
, #eq^#(#0(), #pos(@y)) -> c_24()
, #eq^#(#0(), #s(@y)) -> c_25()
, #eq^#(#neg(@x), #0()) -> c_26()
, #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, #eq^#(#neg(@x), #pos(@y)) -> c_28()
, #eq^#(#pos(@x), #0()) -> c_29()
, #eq^#(#pos(@x), #neg(@y)) -> c_30()
, #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, #eq^#(#s(@x), #0()) -> c_32()
, #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, #and^#(#false(), #false()) -> c_34()
, #and^#(#false(), #true()) -> c_35()
, #and^#(#true(), #false()) -> c_36()
, #and^#(#true(), #true()) -> c_37() }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: #equal^#(@x, @y) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
-->_1 #eq^#(#s(@x), #0()) -> c_32() :32
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_1 #eq^#(#0(), #0()) -> c_22() :22
-->_1 #eq^#(nil(), nil()) -> c_21() :21
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
2: and^#(@x, @y) -> #and^#(@x, @y)
-->_1 #and^#(#true(), #true()) -> c_37() :37
-->_1 #and^#(#true(), #false()) -> c_36() :36
-->_1 #and^#(#false(), #true()) -> c_35() :35
-->_1 #and^#(#false(), #false()) -> c_34() :34
3: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(nil(), @l2) -> eq#2^#(@l2) :5
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :4
4: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys)) :6
-->_1 eq#3^#(nil(), @x, @xs) -> c_7() :7
5: eq#1^#(nil(), @l2) -> eq#2^#(@l2)
-->_1 eq#2^#(nil()) -> c_9() :9
-->_1 eq#2^#(::(@y, @ys)) -> c_8() :8
6: eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
-->_3 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :3
-->_1 and^#(@x, @y) -> #and^#(@x, @y) :2
-->_2 #equal^#(@x, @y) -> #eq^#(@x, @y) :1
7: eq#3^#(nil(), @x, @xs) -> c_7()
8: eq#2^#(::(@y, @ys)) -> c_8()
9: eq#2^#(nil()) -> c_9()
10: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :11
-->_1 nub#1^#(nil()) -> c_12() :12
11: nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :13
-->_1 nub^#(@l) -> nub#1^#(@l) :10
12: nub#1^#(nil()) -> c_12()
13: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :14
-->_1 remove#1^#(nil(), @x) -> c_15() :15
14: remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :17
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :16
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :3
15: remove#1^#(nil(), @x) -> c_15()
16: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :13
17: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :13
18: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
-->_3 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_2 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_3 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_2 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_3 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_2 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #and^#(#true(), #true()) -> c_37() :37
-->_1 #and^#(#true(), #false()) -> c_36() :36
-->_1 #and^#(#false(), #true()) -> c_35() :35
-->_1 #and^#(#false(), #false()) -> c_34() :34
-->_3 #eq^#(#s(@x), #0()) -> c_32() :32
-->_2 #eq^#(#s(@x), #0()) -> c_32() :32
-->_3 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_2 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_3 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_2 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_3 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_2 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_3 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_2 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_3 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_2 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_3 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_2 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_3 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_2 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_3 #eq^#(#0(), #0()) -> c_22() :22
-->_2 #eq^#(#0(), #0()) -> c_22() :22
-->_3 #eq^#(nil(), nil()) -> c_21() :21
-->_2 #eq^#(nil(), nil()) -> c_21() :21
-->_3 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_2 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_3 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_2 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_3 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
-->_2 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
19: #eq^#(::(@x_1, @x_2), nil()) -> c_19()
20: #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
21: #eq^#(nil(), nil()) -> c_21()
22: #eq^#(#0(), #0()) -> c_22()
23: #eq^#(#0(), #neg(@y)) -> c_23()
24: #eq^#(#0(), #pos(@y)) -> c_24()
25: #eq^#(#0(), #s(@y)) -> c_25()
26: #eq^#(#neg(@x), #0()) -> c_26()
27: #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_1 #eq^#(#s(@x), #0()) -> c_32() :32
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_1 #eq^#(#0(), #0()) -> c_22() :22
-->_1 #eq^#(nil(), nil()) -> c_21() :21
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
28: #eq^#(#neg(@x), #pos(@y)) -> c_28()
29: #eq^#(#pos(@x), #0()) -> c_29()
30: #eq^#(#pos(@x), #neg(@y)) -> c_30()
31: #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_1 #eq^#(#s(@x), #0()) -> c_32() :32
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_1 #eq^#(#0(), #0()) -> c_22() :22
-->_1 #eq^#(nil(), nil()) -> c_21() :21
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
32: #eq^#(#s(@x), #0()) -> c_32()
33: #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :33
-->_1 #eq^#(#s(@x), #0()) -> c_32() :32
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :31
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :30
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :29
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :28
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :26
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :25
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :24
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :23
-->_1 #eq^#(#0(), #0()) -> c_22() :22
-->_1 #eq^#(nil(), nil()) -> c_21() :21
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :20
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :19
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :18
34: #and^#(#false(), #false()) -> c_34()
35: #and^#(#false(), #true()) -> c_35()
36: #and^#(#true(), #false()) -> c_36()
37: #and^#(#true(), #true()) -> c_37()
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {12} and add Pre({12}) = {10} to the strict component.
- We remove {15} and add Pre({15}) = {13} to the strict component.
- We remove {7} and add Pre({7}) = {4} to the strict component.
- We remove {8} and add Pre({8}) = {5} to the strict component.
- We remove {9} and add Pre({9}) = {5} to the strict component.
- We remove {2} and add Pre({2}) = {6} to the strict component.
- We remove {1} and add Pre({1}) = {6} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ #equal^#(@x, @y) -> #eq^#(@x, @y)
, #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, #eq^#(nil(), nil()) -> c_21()
, #eq^#(#0(), #0()) -> c_22()
, #eq^#(#0(), #neg(@y)) -> c_23()
, #eq^#(#0(), #pos(@y)) -> c_24()
, #eq^#(#0(), #s(@y)) -> c_25()
, #eq^#(#neg(@x), #0()) -> c_26()
, #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, #eq^#(#neg(@x), #pos(@y)) -> c_28()
, #eq^#(#pos(@x), #0()) -> c_29()
, #eq^#(#pos(@x), #neg(@y)) -> c_30()
, #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, #eq^#(#s(@x), #0()) -> c_32()
, #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, and^#(@x, @y) -> #and^#(@x, @y)
, #and^#(#false(), #false()) -> c_34()
, #and^#(#false(), #true()) -> c_35()
, #and^#(#true(), #false()) -> c_36()
, #and^#(#true(), #true()) -> c_37()
, eq#3^#(nil(), @x, @xs) -> c_7()
, eq#2^#(::(@y, @ys)) -> c_8()
, eq#2^#(nil()) -> c_9()
, nub#1^#(nil()) -> c_12()
, remove#1^#(nil(), @x) -> c_15() }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(nil(), @l2) -> eq#2^#(@l2) :3
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :2
2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys)) :4
-->_1 eq#3^#(nil(), @x, @xs) -> c_7() :33
3: eq#1^#(nil(), @l2) -> eq#2^#(@l2)
-->_1 eq#2^#(nil()) -> c_9() :35
-->_1 eq#2^#(::(@y, @ys)) -> c_8() :34
4: eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
-->_1 and^#(@x, @y) -> #and^#(@x, @y) :28
-->_2 #equal^#(@x, @y) -> #eq^#(@x, @y) :11
-->_3 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
5: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :6
-->_1 nub#1^#(nil()) -> c_12() :36
6: nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :7
-->_1 nub^#(@l) -> nub#1^#(@l) :5
7: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :8
-->_1 remove#1^#(nil(), @x) -> c_15() :37
8: remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :10
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
9: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :7
10: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :7
11: #equal^#(@x, @y) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
-->_1 #eq^#(#s(@x), #0()) -> c_32() :26
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_1 #eq^#(#0(), #0()) -> c_22() :16
-->_1 #eq^#(nil(), nil()) -> c_21() :15
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
12: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
-->_3 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_2 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_3 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_2 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_3 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_2 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #and^#(#true(), #true()) -> c_37() :32
-->_1 #and^#(#true(), #false()) -> c_36() :31
-->_1 #and^#(#false(), #true()) -> c_35() :30
-->_1 #and^#(#false(), #false()) -> c_34() :29
-->_3 #eq^#(#s(@x), #0()) -> c_32() :26
-->_2 #eq^#(#s(@x), #0()) -> c_32() :26
-->_3 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_2 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_3 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_2 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_3 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_2 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_3 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_2 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_3 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_2 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_3 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_2 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_3 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_2 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_3 #eq^#(#0(), #0()) -> c_22() :16
-->_2 #eq^#(#0(), #0()) -> c_22() :16
-->_3 #eq^#(nil(), nil()) -> c_21() :15
-->_2 #eq^#(nil(), nil()) -> c_21() :15
-->_3 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_2 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_3 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_2 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_3 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
-->_2 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
13: #eq^#(::(@x_1, @x_2), nil()) -> c_19()
14: #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
15: #eq^#(nil(), nil()) -> c_21()
16: #eq^#(#0(), #0()) -> c_22()
17: #eq^#(#0(), #neg(@y)) -> c_23()
18: #eq^#(#0(), #pos(@y)) -> c_24()
19: #eq^#(#0(), #s(@y)) -> c_25()
20: #eq^#(#neg(@x), #0()) -> c_26()
21: #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_1 #eq^#(#s(@x), #0()) -> c_32() :26
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_1 #eq^#(#0(), #0()) -> c_22() :16
-->_1 #eq^#(nil(), nil()) -> c_21() :15
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
22: #eq^#(#neg(@x), #pos(@y)) -> c_28()
23: #eq^#(#pos(@x), #0()) -> c_29()
24: #eq^#(#pos(@x), #neg(@y)) -> c_30()
25: #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#s(@x), #0()) -> c_32() :26
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_1 #eq^#(#0(), #0()) -> c_22() :16
-->_1 #eq^#(nil(), nil()) -> c_21() :15
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
26: #eq^#(#s(@x), #0()) -> c_32()
27: #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
-->_1 #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y) :27
-->_1 #eq^#(#s(@x), #0()) -> c_32() :26
-->_1 #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y) :25
-->_1 #eq^#(#pos(@x), #neg(@y)) -> c_30() :24
-->_1 #eq^#(#pos(@x), #0()) -> c_29() :23
-->_1 #eq^#(#neg(@x), #pos(@y)) -> c_28() :22
-->_1 #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y) :21
-->_1 #eq^#(#neg(@x), #0()) -> c_26() :20
-->_1 #eq^#(#0(), #s(@y)) -> c_25() :19
-->_1 #eq^#(#0(), #pos(@y)) -> c_24() :18
-->_1 #eq^#(#0(), #neg(@y)) -> c_23() :17
-->_1 #eq^#(#0(), #0()) -> c_22() :16
-->_1 #eq^#(nil(), nil()) -> c_21() :15
-->_1 #eq^#(nil(), ::(@y_1, @y_2)) -> c_20() :14
-->_1 #eq^#(::(@x_1, @x_2), nil()) -> c_19() :13
-->_1 #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2)) :12
28: and^#(@x, @y) -> #and^#(@x, @y)
-->_1 #and^#(#true(), #true()) -> c_37() :32
-->_1 #and^#(#true(), #false()) -> c_36() :31
-->_1 #and^#(#false(), #true()) -> c_35() :30
-->_1 #and^#(#false(), #false()) -> c_34() :29
29: #and^#(#false(), #false()) -> c_34()
30: #and^#(#false(), #true()) -> c_35()
31: #and^#(#true(), #false()) -> c_36()
32: #and^#(#true(), #true()) -> c_37()
33: eq#3^#(nil(), @x, @xs) -> c_7()
34: eq#2^#(::(@y, @ys)) -> c_8()
35: eq#2^#(nil()) -> c_9()
36: nub#1^#(nil()) -> c_12()
37: remove#1^#(nil(), @x) -> c_15()
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ #equal^#(@x, @y) -> #eq^#(@x, @y)
, #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, #eq^#(nil(), nil()) -> c_21()
, #eq^#(#0(), #0()) -> c_22()
, #eq^#(#0(), #neg(@y)) -> c_23()
, #eq^#(#0(), #pos(@y)) -> c_24()
, #eq^#(#0(), #s(@y)) -> c_25()
, #eq^#(#neg(@x), #0()) -> c_26()
, #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, #eq^#(#neg(@x), #pos(@y)) -> c_28()
, #eq^#(#pos(@x), #0()) -> c_29()
, #eq^#(#pos(@x), #neg(@y)) -> c_30()
, #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, #eq^#(#s(@x), #0()) -> c_32()
, #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, and^#(@x, @y) -> #and^#(@x, @y)
, #and^#(#false(), #false()) -> c_34()
, #and^#(#false(), #true()) -> c_35()
, #and^#(#true(), #false()) -> c_36()
, #and^#(#true(), #true()) -> c_37()
, eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, eq#3^#(nil(), @x, @xs) -> c_7()
, eq#2^#(::(@y, @ys)) -> c_8()
, eq#2^#(nil()) -> c_9()
, nub#1^#(nil()) -> c_12()
, remove#1^#(nil(), @x) -> c_15() }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the the dependency graph
->1:{4,5}
|
|->3:{6,9,7,8}
| |
| |->5:{1,3,2}
| | |
| | |->7:{10} Weak SCC
| | | |
| | | |->9:{12} Weak SCC
| | | |
| | | |->10:{13} Weak SCC
| | | |
| | | |->11:{14} Weak SCC
| | | |
| | | |->12:{15} Weak SCC
| | | |
| | | |->13:{16} Weak SCC
| | | |
| | | |->14:{17} Weak SCC
| | | |
| | | |->15:{18} Weak SCC
| | | |
| | | |->16:{19} Weak SCC
| | | |
| | | |->17:{21} Weak SCC
| | | |
| | | |->18:{22} Weak SCC
| | | |
| | | |->19:{23} Weak SCC
| | | |
| | | |->20:{25} Weak SCC
| | | |
| | | `->8:{26,24,20,11} Weak SCC
| | | |
| | | |->9:{12} Weak SCC
| | | |
| | | |->10:{13} Weak SCC
| | | |
| | | |->11:{14} Weak SCC
| | | |
| | | |->12:{15} Weak SCC
| | | |
| | | |->13:{16} Weak SCC
| | | |
| | | |->14:{17} Weak SCC
| | | |
| | | |->15:{18} Weak SCC
| | | |
| | | |->16:{19} Weak SCC
| | | |
| | | |->17:{21} Weak SCC
| | | |
| | | |->18:{22} Weak SCC
| | | |
| | | |->19:{23} Weak SCC
| | | |
| | | |->20:{25} Weak SCC
| | | |
| | | |->22:{28} Weak SCC
| | | |
| | | |->23:{29} Weak SCC
| | | |
| | | |->24:{30} Weak SCC
| | | |
| | | `->25:{31} Weak SCC
| | |
| | |->21:{27} Weak SCC
| | | |
| | | |->22:{28} Weak SCC
| | | |
| | | |->23:{29} Weak SCC
| | | |
| | | |->24:{30} Weak SCC
| | | |
| | | `->25:{31} Weak SCC
| | |
| | |->26:{32} Weak SCC
| | | |
| | | |->27:{34} Weak SCC
| | | |
| | | `->28:{35} Weak SCC
| | |
| | `->6:{33} Weak SCC
| |
| `->4:{37} Weak SCC
|
`->2:{36} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, 2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, 3: eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, 4: nub^#(@l) -> nub#1^#(@l)
, 5: nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, 6: remove^#(@x, @l) -> remove#1^#(@l, @x)
, 7: remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, 8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, 9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ 10: #equal^#(@x, @y) -> #eq^#(@x, @y)
, 11: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, 12: #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, 13: #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, 14: #eq^#(nil(), nil()) -> c_21()
, 15: #eq^#(#0(), #0()) -> c_22()
, 16: #eq^#(#0(), #neg(@y)) -> c_23()
, 17: #eq^#(#0(), #pos(@y)) -> c_24()
, 18: #eq^#(#0(), #s(@y)) -> c_25()
, 19: #eq^#(#neg(@x), #0()) -> c_26()
, 20: #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, 21: #eq^#(#neg(@x), #pos(@y)) -> c_28()
, 22: #eq^#(#pos(@x), #0()) -> c_29()
, 23: #eq^#(#pos(@x), #neg(@y)) -> c_30()
, 24: #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, 25: #eq^#(#s(@x), #0()) -> c_32()
, 26: #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, 27: and^#(@x, @y) -> #and^#(@x, @y)
, 28: #and^#(#false(), #false()) -> c_34()
, 29: #and^#(#false(), #true()) -> c_35()
, 30: #and^#(#true(), #false()) -> c_36()
, 31: #and^#(#true(), #true()) -> c_37()
, 32: eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, 33: eq#3^#(nil(), @x, @xs) -> c_7()
, 34: eq#2^#(::(@y, @ys)) -> c_8()
, 35: eq#2^#(nil()) -> c_9()
, 36: nub#1^#(nil()) -> c_12()
, 37: remove#1^#(nil(), @x) -> c_15() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 36: nub#1^#(nil()) -> c_12()
, 37: remove#1^#(nil(), @x) -> c_15()
, 33: eq#3^#(nil(), @x, @xs) -> c_7()
, 10: #equal^#(@x, @y) -> #eq^#(@x, @y)
, 26: #eq^#(#s(@x), #s(@y)) -> #eq^#(@x, @y)
, 24: #eq^#(#pos(@x), #pos(@y)) -> #eq^#(@x, @y)
, 20: #eq^#(#neg(@x), #neg(@y)) -> #eq^#(@x, @y)
, 11: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_18(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, 12: #eq^#(::(@x_1, @x_2), nil()) -> c_19()
, 13: #eq^#(nil(), ::(@y_1, @y_2)) -> c_20()
, 14: #eq^#(nil(), nil()) -> c_21()
, 15: #eq^#(#0(), #0()) -> c_22()
, 16: #eq^#(#0(), #neg(@y)) -> c_23()
, 17: #eq^#(#0(), #pos(@y)) -> c_24()
, 18: #eq^#(#0(), #s(@y)) -> c_25()
, 19: #eq^#(#neg(@x), #0()) -> c_26()
, 21: #eq^#(#neg(@x), #pos(@y)) -> c_28()
, 22: #eq^#(#pos(@x), #0()) -> c_29()
, 23: #eq^#(#pos(@x), #neg(@y)) -> c_30()
, 25: #eq^#(#s(@x), #0()) -> c_32()
, 27: and^#(@x, @y) -> #and^#(@x, @y)
, 28: #and^#(#false(), #false()) -> c_34()
, 29: #and^#(#false(), #true()) -> c_35()
, 30: #and^#(#true(), #false()) -> c_36()
, 31: #and^#(#true(), #true()) -> c_37()
, 32: eq#1^#(nil(), @l2) -> eq#2^#(@l2)
, 34: eq#2^#(::(@y, @ys)) -> c_8()
, 35: eq#2^#(nil()) -> c_9() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the following dependency-graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :2
2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys)) :3
3: eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys))
-->_3 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
4: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :5
5: nub#1^#(::(@x, @xs)) ->
c_11(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
-->_1 nub^#(@l) -> nub#1^#(@l) :4
6: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :7
7: remove#1^#(::(@y, @ys), @x) ->
c_14(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ eq#3^#(::(@y, @ys), @x, @xs) ->
c_6(and^#(#equal(@x, @y), eq(@xs, @ys)),
#equal^#(@x, @y),
eq^#(@xs, @ys)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :2
2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :3
3: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
4: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :5
5: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
-->_1 nub^#(@l) -> nub#1^#(@l) :4
6: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :7
7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :6
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs: { eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :2
2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :9
3: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :4
4: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :5
-->_1 nub^#(@l) -> nub#1^#(@l) :3
5: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :6
6: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :7
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
7: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :5
8: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :5
9: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :8
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :3
3: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
-->_1 nub^#(@l) -> nub#1^#(@l) :2
4: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :5
5: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :7
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :6
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
6: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
7: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
8: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :9
9: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {7} and add Pre({7}) = {5} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :7
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :3
3: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
-->_1 nub^#(@l) -> nub#1^#(@l) :2
4: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :5
5: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :6
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
6: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
7: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :8
8: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {6} and add Pre({6}) = {5} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :6
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :3
3: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
-->_1 nub^#(@l) -> nub#1^#(@l) :2
4: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :5
5: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
6: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :7
7: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {5} and add Pre({5}) = {4} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :5
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :3
3: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
-->_1 nub^#(@l) -> nub#1^#(@l) :2
4: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :7
5: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :6
6: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, remove^#(@x, @l) -> remove#1^#(@l, @x) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, nub#1(nil()) -> nil()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, nub^#(@l) -> nub#1^#(@l)
, remove^#(@x, @l) -> remove#1^#(@l, @x) }
Weak DPs:
{ eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 2: nub^#(@l) -> nub#1^#(@l)
, 4: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, 5: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, 6: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, 7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) }
Trs:
{ #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #and(#true(), #true()) -> #true()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#equal) = {}, Uargs(#eq) = {}, Uargs(and) = {},
Uargs(#and) = {}, Uargs(eq) = {}, Uargs(eq#1) = {}, Uargs(::) = {},
Uargs(eq#3) = {}, Uargs(eq#2) = {}, Uargs(remove) = {},
Uargs(remove#1) = {}, Uargs(remove#2) = {}, Uargs(#neg) = {},
Uargs(#pos) = {}, Uargs(#s) = {}, Uargs(#equal^#) = {},
Uargs(#eq^#) = {}, Uargs(and^#) = {}, Uargs(#and^#) = {},
Uargs(eq^#) = {}, Uargs(eq#1^#) = {}, Uargs(eq#3^#) = {},
Uargs(eq#2^#) = {}, Uargs(nub^#) = {}, Uargs(nub#1^#) = {},
Uargs(remove^#) = {}, Uargs(remove#1^#) = {},
Uargs(remove#2^#) = {}, Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#equal](x1, x2) = [3 3] x1 + [3 3] x2 + [0]
[0 1] [2 3] [2]
[#eq](x1, x2) = [1 2] x1 + [2 0] x2 + [0]
[0 1] [1 1] [1]
[and](x1, x2) = [0 0] x2 + [3]
[0 1] [0]
[#and](x1, x2) = [0 0] x2 + [3]
[0 1] [0]
[eq](x1, x2) = [1 2] x1 + [1 1] x2 + [0]
[0 0] [0 1] [0]
[eq#1](x1, x2) = [0 1] x1 + [1 1] x2 + [0]
[0 0] [0 1] [0]
[::](x1, x2) = [0 2] x1 + [1 3] x2 + [1]
[0 1] [0 1] [2]
[eq#3](x1, x2, x3) = [1 0] x1 + [2]
[0 1] [0]
[nil] = [1]
[1]
[eq#2](x1) = [1 1] x1 + [1]
[0 1] [0]
[#false] = [3]
[1]
[#true] = [0]
[1]
[remove](x1, x2) = [1 0] x2 + [0]
[0 1] [0]
[remove#1](x1, x2) = [1 0] x1 + [0]
[0 1] [0]
[remove#2](x1, x2, x3, x4) = [0 2] x3 + [1 3] x4 + [1]
[0 1] [0 1] [2]
[#0] = [2]
[0]
[#neg](x1) = [1 0] x1 + [3]
[0 1] [1]
[#pos](x1) = [1 2] x1 + [1]
[0 1] [2]
[#s](x1) = [1 0] x1 + [2]
[0 1] [3]
[#equal^#](x1, x2) = [0]
[0]
[#eq^#](x1, x2) = [0]
[0]
[and^#](x1, x2) = [0]
[0]
[#and^#](x1, x2) = [0]
[0]
[eq^#](x1, x2) = [0 1] x2 + [2]
[3 0] [1]
[eq#1^#](x1, x2) = [0 1] x2 + [2]
[3 0] [0]
[eq#3^#](x1, x2, x3) = [0 1] x1 + [1]
[3 0] [0]
[eq#2^#](x1) = [0]
[0]
[nub^#](x1) = [3 3] x1 + [1]
[0 1] [0]
[nub#1^#](x1) = [3 3] x1 + [0]
[0 0] [0]
[remove^#](x1, x2) = [0 2] x1 + [0 3] x2 + [1]
[0 0] [0 0] [0]
[remove#1^#](x1, x2) = [0 3] x1 + [0 2] x2 + [1]
[0 0] [0 0] [0]
[remove#2^#](x1, x2, x3, x4) = [0 1] x1 + [0 2] x2 + [0 3] x4 + [0]
[0 1] [0 0] [0 0] [1]
[c_1](x1, x2) = [1 2] x1 + [2 2] x2 + [1]
[0 0] [0 0] [0]
[c_2](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
This order satisfies following ordering constraints
[#equal(@x, @y)] = [3 3] @x + [3 3] @y + [0]
[0 1] [2 3] [2]
>= [1 2] @x + [2 0] @y + [0]
[0 1] [1 1] [1]
= [#eq(@x, @y)]
[#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [0 4] @x_1 + [1 5] @x_2 + [0 4] @y_1 + [2 6] @y_2 + [7]
[0 1] [0 1] [0 3] [1 4] [6]
> [0 0] @x_2 + [0 0] @y_2 + [3]
[0 1] [1 1] [1]
= [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))]
[#eq(::(@x_1, @x_2), nil())] = [0 4] @x_1 + [1 5] @x_2 + [7]
[0 1] [0 1] [5]
> [3]
[1]
= [#false()]
[#eq(nil(), ::(@y_1, @y_2))] = [0 4] @y_1 + [2 6] @y_2 + [5]
[0 3] [1 4] [5]
> [3]
[1]
= [#false()]
[#eq(nil(), nil())] = [5]
[4]
> [0]
[1]
= [#true()]
[#eq(#0(), #0())] = [6]
[3]
> [0]
[1]
= [#true()]
[#eq(#0(), #neg(@y))] = [2 0] @y + [8]
[1 1] [5]
> [3]
[1]
= [#false()]
[#eq(#0(), #pos(@y))] = [2 4] @y + [4]
[1 3] [4]
> [3]
[1]
= [#false()]
[#eq(#0(), #s(@y))] = [2 0] @y + [6]
[1 1] [6]
> [3]
[1]
= [#false()]
[#eq(#neg(@x), #0())] = [1 2] @x + [9]
[0 1] [4]
> [3]
[1]
= [#false()]
[#eq(#neg(@x), #neg(@y))] = [1 2] @x + [2 0] @y + [11]
[0 1] [1 1] [6]
> [1 2] @x + [2 0] @y + [0]
[0 1] [1 1] [1]
= [#eq(@x, @y)]
[#eq(#neg(@x), #pos(@y))] = [1 2] @x + [2 4] @y + [7]
[0 1] [1 3] [5]
> [3]
[1]
= [#false()]
[#eq(#pos(@x), #0())] = [1 4] @x + [9]
[0 1] [5]
> [3]
[1]
= [#false()]
[#eq(#pos(@x), #neg(@y))] = [1 4] @x + [2 0] @y + [11]
[0 1] [1 1] [7]
> [3]
[1]
= [#false()]
[#eq(#pos(@x), #pos(@y))] = [1 4] @x + [2 4] @y + [7]
[0 1] [1 3] [6]
> [1 2] @x + [2 0] @y + [0]
[0 1] [1 1] [1]
= [#eq(@x, @y)]
[#eq(#s(@x), #0())] = [1 2] @x + [12]
[0 1] [6]
> [3]
[1]
= [#false()]
[#eq(#s(@x), #s(@y))] = [1 2] @x + [2 0] @y + [12]
[0 1] [1 1] [9]
> [1 2] @x + [2 0] @y + [0]
[0 1] [1 1] [1]
= [#eq(@x, @y)]
[and(@x, @y)] = [0 0] @y + [3]
[0 1] [0]
>= [0 0] @y + [3]
[0 1] [0]
= [#and(@x, @y)]
[#and(#false(), #false())] = [3]
[1]
>= [3]
[1]
= [#false()]
[#and(#false(), #true())] = [3]
[1]
>= [3]
[1]
= [#false()]
[#and(#true(), #false())] = [3]
[1]
>= [3]
[1]
= [#false()]
[#and(#true(), #true())] = [3]
[1]
> [0]
[1]
= [#true()]
[eq(@l1, @l2)] = [1 2] @l1 + [1 1] @l2 + [0]
[0 0] [0 1] [0]
>= [0 1] @l1 + [1 1] @l2 + [0]
[0 0] [0 1] [0]
= [eq#1(@l1, @l2)]
[eq#1(::(@x, @xs), @l2)] = [1 1] @l2 + [0 1] @x + [0 1] @xs + [2]
[0 1] [0 0] [0 0] [0]
>= [1 0] @l2 + [2]
[0 1] [0]
= [eq#3(@l2, @x, @xs)]
[eq#1(nil(), @l2)] = [1 1] @l2 + [1]
[0 1] [0]
>= [1 1] @l2 + [1]
[0 1] [0]
= [eq#2(@l2)]
[eq#3(::(@y, @ys), @x, @xs)] = [0 2] @y + [1 3] @ys + [3]
[0 1] [0 1] [2]
>= [0 0] @ys + [3]
[0 1] [0]
= [and(#equal(@x, @y), eq(@xs, @ys))]
[eq#3(nil(), @x, @xs)] = [3]
[1]
>= [3]
[1]
= [#false()]
[eq#2(::(@y, @ys))] = [0 3] @y + [1 4] @ys + [4]
[0 1] [0 1] [2]
> [3]
[1]
= [#false()]
[eq#2(nil())] = [3]
[1]
> [0]
[1]
= [#true()]
[remove(@x, @l)] = [1 0] @l + [0]
[0 1] [0]
>= [1 0] @l + [0]
[0 1] [0]
= [remove#1(@l, @x)]
[remove#1(::(@y, @ys), @x)] = [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
>= [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
= [remove#2(eq(@x, @y), @x, @y, @ys)]
[remove#1(nil(), @x)] = [1]
[1]
>= [1]
[1]
= [nil()]
[remove#2(#false(), @x, @y, @ys)] = [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
>= [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
= [::(@y, remove(@x, @ys))]
[remove#2(#true(), @x, @y, @ys)] = [0 2] @y + [1 3] @ys + [1]
[0 1] [0 1] [2]
> [1 0] @ys + [0]
[0 1] [0]
= [remove(@x, @ys)]
[eq^#(@l1, @l2)] = [0 1] @l2 + [2]
[3 0] [1]
>= [0 1] @l2 + [2]
[3 0] [0]
= [eq#1^#(@l1, @l2)]
[eq#1^#(::(@x, @xs), @l2)] = [0 1] @l2 + [2]
[3 0] [0]
> [0 1] @l2 + [1]
[3 0] [0]
= [eq#3^#(@l2, @x, @xs)]
[eq#3^#(::(@y, @ys), @x, @xs)] = [0 1] @y + [0 1] @ys + [3]
[0 6] [3 9] [3]
> [0 1] @ys + [2]
[3 0] [1]
= [eq^#(@xs, @ys)]
[nub^#(@l)] = [3 3] @l + [1]
[0 1] [0]
> [3 3] @l + [0]
[0 0] [0]
= [nub#1^#(@l)]
[nub#1^#(::(@x, @xs))] = [0 9] @x + [3 12] @xs + [9]
[0 0] [0 0] [0]
> [0 4] @x + [3 11] @xs + [4]
[0 0] [0 0] [0]
= [c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))]
[remove^#(@x, @l)] = [0 3] @l + [0 2] @x + [1]
[0 0] [0 0] [0]
>= [0 3] @l + [0 2] @x + [1]
[0 0] [0 0] [0]
= [remove#1^#(@l, @x)]
[remove#1^#(::(@y, @ys), @x)] = [0 2] @x + [0 3] @y + [0 3] @ys + [7]
[0 0] [0 0] [0 0] [0]
> [0 2] @x + [0 3] @y + [0 3] @ys + [3]
[0 0] [0 0] [0 0] [0]
= [c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))]
[remove#2^#(#false(), @x, @y, @ys)] = [0 2] @x + [0 3] @ys + [1]
[0 0] [0 0] [2]
>= [0 2] @x + [0 3] @ys + [1]
[0 0] [0 0] [0]
= [remove^#(@x, @ys)]
[remove#2^#(#true(), @x, @y, @ys)] = [0 2] @x + [0 3] @ys + [1]
[0 0] [0 0] [2]
>= [0 2] @x + [0 3] @ys + [1]
[0 0] [0 0] [0]
= [remove^#(@x, @ys)]
Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of rules
{2,4,5,6,7}. Here rules are labeled according to the (estimated)
dependency graph
1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
-->_1 eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) :4
2: nub^#(@l) -> nub#1^#(@l)
-->_1 nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs)) :6
3: remove^#(@x, @l) -> remove#1^#(@l, @x)
-->_1 remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y)) :7
4: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
-->_1 eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys) :5
5: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
-->_1 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
6: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
-->_2 remove^#(@x, @l) -> remove#1^#(@l, @x) :3
-->_1 nub^#(@l) -> nub#1^#(@l) :2
7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
-->_1 remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) :9
-->_1 remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys) :8
-->_2 eq^#(@l1, @l2) -> eq#1^#(@l1, @l2) :1
8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :3
9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
-->_1 remove^#(@x, @l) -> remove#1^#(@l, @x) :3
- The rules {2,4,5,6,7} have known complexity. These cover all
predecessors of {1,8,9}, their complexity is equally bounded.
- The rules {1,2,4,5,6,7,8,9} have known complexity. These cover
all predecessors of {3}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4,5,6,7,8,9} is given by YES(?,O(n^2)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, nub^#(@l) -> nub#1^#(@l)
, nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, remove^#(@x, @l) -> remove#1^#(@l, @x)
, remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{4,5} Weak SCC
|
`->2:{6,9,7,8} Weak SCC
|
`->3:{1,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, 2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs)
, 3: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, 4: nub^#(@l) -> nub#1^#(@l)
, 5: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, 6: remove^#(@x, @l) -> remove#1^#(@l, @x)
, 7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, 8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, 9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 4: nub^#(@l) -> nub#1^#(@l)
, 5: nub#1^#(::(@x, @xs)) ->
c_1(nub^#(remove(@x, @xs)), remove^#(@x, @xs))
, 6: remove^#(@x, @l) -> remove#1^#(@l, @x)
, 9: remove#2^#(#true(), @x, @y, @ys) -> remove^#(@x, @ys)
, 7: remove#1^#(::(@y, @ys), @x) ->
c_2(remove#2^#(eq(@x, @y), @x, @y, @ys), eq^#(@x, @y))
, 8: remove#2^#(#false(), @x, @y, @ys) -> remove^#(@x, @ys)
, 1: eq^#(@l1, @l2) -> eq#1^#(@l1, @l2)
, 3: eq#3^#(::(@y, @ys), @x, @xs) -> eq^#(@xs, @ys)
, 2: eq#1^#(::(@x, @xs), @l2) -> eq#3^#(@l2, @x, @xs) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, and(@x, @y) -> #and(@x, @y)
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#1(nil(), @l2) -> eq#2(@l2)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, eq#3(nil(), @x, @xs) -> #false()
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#1(nil(), @x) -> nil()
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys) }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))