The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)

The (relative) TRS S consists of the following rules:

#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)

The (relative) TRS S consists of the following rules:

#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#eq, eq, eq#1, nub, nub#1, remove, remove#1

They will be analysed ascendingly in the following order:
eq = eq#1
eq < remove#1
nub = nub#1
remove < nub#1
remove = remove#1

(6) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

The following defined symbols remain to be analysed:
#eq, eq, eq#1, nub, nub#1, remove, remove#1

They will be analysed ascendingly in the following order:
eq = eq#1
eq < remove#1
nub = nub#1
remove < nub#1
remove = remove#1

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)

Induction Base:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, 0)), gen_:::nil:#0:#neg:#pos:#s3_4(0)) →_R^Ω(0)
#false

Induction Step:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, +(n5_4, 1))), gen_:::nil:#0:#neg:#pos:#s3_4(+(n5_4, 1))) →_R^Ω(0)
#and(#eq(nil, nil), #eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4))) →_R^Ω(0)
#and(#true, #eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4))) →_IH
#and(#true, #false) →_R^Ω(0)
#false

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n⁰).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

The following defined symbols remain to be analysed:
eq#1, eq, nub, nub#1, remove, remove#1

They will be analysed ascendingly in the following order:
eq = eq#1
eq < remove#1
nub = nub#1
remove < nub#1
remove = remove#1

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)

Induction Base:
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, 0)), gen_:::nil:#0:#neg:#pos:#s3_4(0)) →_R^Ω(1)
eq#3(gen_:::nil:#0:#neg:#pos:#s3_4(0), nil, gen_:::nil:#0:#neg:#pos:#s3_4(0)) →_R^Ω(1)
#false

Induction Step:
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, +(n6574398_4, 1))), gen_:::nil:#0:#neg:#pos:#s3_4(+(n6574398_4, 1))) →_R^Ω(1)
eq#3(gen_:::nil:#0:#neg:#pos:#s3_4(+(n6574398_4, 1)), nil, gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4))) →_R^Ω(1)
and(#equal(nil, nil), eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4))) →_R^Ω(1)
and(#eq(nil, nil), eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4))) →_R^Ω(0)
and(#true, eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4))) →_R^Ω(1)
and(#true, eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4))) →_IH
and(#true, #false) →_R^Ω(1)
#and(#true, #false) →_R^Ω(0)
#false

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

The following defined symbols remain to be analysed:
eq, nub, nub#1, remove, remove#1

They will be analysed ascendingly in the following order:
eq = eq#1
eq < remove#1
nub = nub#1
remove < nub#1
remove = remove#1

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol eq.

(14) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

The following defined symbols remain to be analysed:
remove#1, nub, nub#1, remove

They will be analysed ascendingly in the following order:
nub = nub#1
remove < nub#1
remove = remove#1

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
remove#1(gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), gen_:::nil:#0:#neg:#pos:#s3_4(1)) → gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), rt ∈ Ω(1 + n6575392₄)

Induction Base:
remove#1(gen_:::nil:#0:#neg:#pos:#s3_4(0), gen_:::nil:#0:#neg:#pos:#s3_4(1)) →_R^Ω(1)
nil

Induction Step:
remove#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(n6575392_4, 1)), gen_:::nil:#0:#neg:#pos:#s3_4(1)) →_R^Ω(1)
remove#2(eq(gen_:::nil:#0:#neg:#pos:#s3_4(1), nil), gen_:::nil:#0:#neg:#pos:#s3_4(1), nil, gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4)) →_R^Ω(1)
remove#2(eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(1), nil), gen_:::nil:#0:#neg:#pos:#s3_4(1), nil, gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4)) →_L^Ω(1)
remove#2(#false, gen_:::nil:#0:#neg:#pos:#s3_4(1), nil, gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4)) →_R^Ω(1)
::(nil, remove(gen_:::nil:#0:#neg:#pos:#s3_4(1), gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4))) →_R^Ω(1)
::(nil, remove#1(gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), gen_:::nil:#0:#neg:#pos:#s3_4(1))) →_IH
::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(c6575393_4))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(16) Complex Obligation (BEST)

(17) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)
remove#1(gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), gen_:::nil:#0:#neg:#pos:#s3_4(1)) → gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), rt ∈ Ω(1 + n6575392₄)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

The following defined symbols remain to be analysed:
remove, nub, nub#1

They will be analysed ascendingly in the following order:
nub = nub#1
remove < nub#1
remove = remove#1

(18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol remove.

(19) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)
remove#1(gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), gen_:::nil:#0:#neg:#pos:#s3_4(1)) → gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), rt ∈ Ω(1 + n6575392₄)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

The following defined symbols remain to be analysed:
nub#1, nub

They will be analysed ascendingly in the following order:
nub = nub#1

(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol nub#1.

(21) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)
remove#1(gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), gen_:::nil:#0:#neg:#pos:#s3_4(1)) → gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), rt ∈ Ω(1 + n6575392₄)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

The following defined symbols remain to be analysed:
nub

They will be analysed ascendingly in the following order:
nub = nub#1

(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol nub.

(23) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)
remove#1(gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), gen_:::nil:#0:#neg:#pos:#s3_4(1)) → gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), rt ∈ Ω(1 + n6575392₄)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

No more defined symbols left to analyse.

(24) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)

(25) BOUNDS(n^1, INF)

(26) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)
remove#1(gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), gen_:::nil:#0:#neg:#pos:#s3_4(1)) → gen_:::nil:#0:#neg:#pos:#s3_4(n6575392_4), rt ∈ Ω(1 + n6575392₄)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)

(28) BOUNDS(n^1, INF)

(29) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eq#1(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n6574398_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n6574398_4)) → #false, rt ∈ Ω(1 + n6574398₄)

(31) BOUNDS(n^1, INF)

(32) Obligation:

Innermost TRS:
Rules:
#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#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
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)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #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)
#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

Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true
#false :: #false:#true
#true :: #false:#true
nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_4 :: :::nil:#0:#neg:#pos:#s
gen_:::nil:#0:#neg:#pos:#s3_4 :: Nat → :::nil:#0:#neg:#pos:#s

Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)

Generator Equations:
gen_:::nil:#0:#neg:#pos:#s3_4(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s3_4(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s3_4(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#eq(gen_:::nil:#0:#neg:#pos:#s3_4(+(1, n5_4)), gen_:::nil:#0:#neg:#pos:#s3_4(n5_4)) → #false, rt ∈ Ω(0)

(34) BOUNDS(1, INF)