Runtime Complexity (innermost) proof of /tmp/tmpk5WzHp/duplicates.raml.xml

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

0 CpxRelTRS

↳1 CpxTrsToCdtProof (UPPER BOUND(ID), 0 ms)

↳2 CdtProblem

↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CdtProblem

↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtUsableRulesProof (⇔, 0 ms)

↳8 CdtProblem

↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 428 ms)

↳10 CdtProblem

↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳12 CdtProblem

↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 831 ms)

↳14 CdtProblem

↳15 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 746 ms)

↳18 CdtProblem

↳19 CdtKnowledgeProof (⇔, 0 ms)

↳20 BOUNDS(1, 1)

(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) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#eq(#0, #0) → #true
#eq(#0, #neg(z0)) → #false
#eq(#0, #pos(z0)) → #false
#eq(#0, #s(z0)) → #false
#eq(#neg(z0), #0) → #false
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1)
#eq(#neg(z0), #pos(z1)) → #false
#eq(#pos(z0), #0) → #false
#eq(#pos(z0), #neg(z1)) → #false
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1)
#eq(#s(z0), #0) → #false
#eq(#s(z0), #s(z1)) → #eq(z0, z1)
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3))
#eq(::(z0, z1), nil) → #false
#eq(nil, ::(z0, z1)) → #false
#eq(nil, nil) → #true
#equal(z0, z1) → #eq(z0, z1)
and(z0, z1) → #and(z0, z1)
eq(z0, z1) → eq#1(z0, z1)
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1)
eq#1(nil, z0) → eq#2(z0)
eq#2(::(z0, z1)) → #false
eq#2(nil) → #true
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1))
eq#3(nil, z0, z1) → #false
nub(z0) → nub#1(z0)
nub#1(::(z0, z1)) → ::(z0, nub(remove(z0, z1)))
nub#1(nil) → nil
remove(z0, z1) → remove#1(z1, z0)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove#1(nil, z0) → nil
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)

Tuples:

#AND(#false, #false) → c
#AND(#false, #true) → c1
#AND(#true, #false) → c2
#AND(#true, #true) → c3
#EQ(#0, #0) → c4
#EQ(#0, #neg(z0)) → c5
#EQ(#0, #pos(z0)) → c6
#EQ(#0, #s(z0)) → c7
#EQ(#neg(z0), #0) → c8
#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#neg(z0), #pos(z1)) → c10
#EQ(#pos(z0), #0) → c11
#EQ(#pos(z0), #neg(z1)) → c12
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #0) → c14
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2), #EQ(z1, z3))
#EQ(::(z0, z1), nil) → c17
#EQ(nil, ::(z0, z1)) → c18
#EQ(nil, nil) → c19
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
AND(z0, z1) → c21(#AND(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
EQ#1(nil, z0) → c24(EQ#2(z0))
EQ#2(::(z0, z1)) → c25
EQ#2(nil) → c26
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1))
EQ#3(nil, z0, z1) → c28
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
NUB#1(nil) → c31
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#1(nil, z0) → c34
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))

S tuples:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
AND(z0, z1) → c21(#AND(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
EQ#1(nil, z0) → c24(EQ#2(z0))
EQ#2(::(z0, z1)) → c25
EQ#2(nil) → c26
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1))
EQ#3(nil, z0, z1) → c28
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
NUB#1(nil) → c31
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#1(nil, z0) → c34
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))

K tuples:none
Defined Rule Symbols:

#equal, and, eq, eq#1, eq#2, eq#3, nub, nub#1, remove, remove#1, remove#2, #and, #eq

Defined Pair Symbols:

#AND, #EQ, #EQUAL, AND, EQ, EQ#1, EQ#2, EQ#3, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36

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

Removed 23 trailing nodes:

#EQ(#neg(z0), #pos(z1)) → c10
#EQ(#0, #neg(z0)) → c5
NUB#1(nil) → c31
#EQ(::(z0, z1), nil) → c17
EQ#2(::(z0, z1)) → c25
#EQ(#s(z0), #0) → c14
EQ#3(nil, z0, z1) → c28
#EQ(#0, #0) → c4
REMOVE#1(nil, z0) → c34
#EQ(nil, nil) → c19
#EQ(#0, #pos(z0)) → c6
#AND(#false, #false) → c
EQ#1(nil, z0) → c24(EQ#2(z0))
#AND(#true, #false) → c2
#EQ(#pos(z0), #neg(z1)) → c12
#EQ(#pos(z0), #0) → c11
#EQ(#neg(z0), #0) → c8
#EQ(#0, #s(z0)) → c7
#EQ(nil, ::(z0, z1)) → c18
EQ#2(nil) → c26
#AND(#false, #true) → c1
#AND(#true, #true) → c3
AND(z0, z1) → c21(#AND(z0, z1))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#eq(#0, #0) → #true
#eq(#0, #neg(z0)) → #false
#eq(#0, #pos(z0)) → #false
#eq(#0, #s(z0)) → #false
#eq(#neg(z0), #0) → #false
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1)
#eq(#neg(z0), #pos(z1)) → #false
#eq(#pos(z0), #0) → #false
#eq(#pos(z0), #neg(z1)) → #false
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1)
#eq(#s(z0), #0) → #false
#eq(#s(z0), #s(z1)) → #eq(z0, z1)
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3))
#eq(::(z0, z1), nil) → #false
#eq(nil, ::(z0, z1)) → #false
#eq(nil, nil) → #true
#equal(z0, z1) → #eq(z0, z1)
and(z0, z1) → #and(z0, z1)
eq(z0, z1) → eq#1(z0, z1)
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1)
eq#1(nil, z0) → eq#2(z0)
eq#2(::(z0, z1)) → #false
eq#2(nil) → #true
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1))
eq#3(nil, z0, z1) → #false
nub(z0) → nub#1(z0)
nub#1(::(z0, z1)) → ::(z0, nub(remove(z0, z1)))
nub#1(nil) → nil
remove(z0, z1) → remove#1(z1, z0)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove#1(nil, z0) → nil
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)

Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2), #EQ(z1, z3))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))

S tuples:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))

K tuples:none
Defined Rule Symbols:

#equal, and, eq, eq#1, eq#2, eq#3, nub, nub#1, remove, remove#1, remove#2, #and, #eq

Defined Pair Symbols:

#EQ, #EQUAL, EQ, EQ#1, EQ#3, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2

Compound Symbols:

c9, c13, c15, c16, c20, c22, c23, c27, c29, c30, c32, c33, c35, c36

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#eq(#0, #0) → #true
#eq(#0, #neg(z0)) → #false
#eq(#0, #pos(z0)) → #false
#eq(#0, #s(z0)) → #false
#eq(#neg(z0), #0) → #false
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1)
#eq(#neg(z0), #pos(z1)) → #false
#eq(#pos(z0), #0) → #false
#eq(#pos(z0), #neg(z1)) → #false
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1)
#eq(#s(z0), #0) → #false
#eq(#s(z0), #s(z1)) → #eq(z0, z1)
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3))
#eq(::(z0, z1), nil) → #false
#eq(nil, ::(z0, z1)) → #false
#eq(nil, nil) → #true
#equal(z0, z1) → #eq(z0, z1)
and(z0, z1) → #and(z0, z1)
eq(z0, z1) → eq#1(z0, z1)
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1)
eq#1(nil, z0) → eq#2(z0)
eq#2(::(z0, z1)) → #false
eq#2(nil) → #true
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1))
eq#3(nil, z0, z1) → #false
nub(z0) → nub#1(z0)
nub#1(::(z0, z1)) → ::(z0, nub(remove(z0, z1)))
nub#1(nil) → nil
remove(z0, z1) → remove#1(z1, z0)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove#1(nil, z0) → nil
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)

Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

S tuples:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

K tuples:none
Defined Rule Symbols:

#equal, and, eq, eq#1, eq#2, eq#3, nub, nub#1, remove, remove#1, remove#2, #and, #eq

Defined Pair Symbols:

#EQ, #EQUAL, EQ, EQ#1, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2, EQ#3

Compound Symbols:

c9, c13, c15, c20, c22, c23, c29, c30, c32, c33, c35, c36, c16, c27

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

nub(z0) → nub#1(z0)
nub#1(::(z0, z1)) → ::(z0, nub(remove(z0, z1)))
nub#1(nil) → nil

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

remove(z0, z1) → remove#1(z1, z0)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove#1(nil, z0) → nil
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)
eq(z0, z1) → eq#1(z0, z1)
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1)
eq#1(nil, z0) → eq#2(z0)
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1))
eq#3(nil, z0, z1) → #false
and(z0, z1) → #and(z0, z1)
#equal(z0, z1) → #eq(z0, z1)
#eq(#0, #0) → #true
#eq(#0, #neg(z0)) → #false
#eq(#0, #pos(z0)) → #false
#eq(#0, #s(z0)) → #false
#eq(#neg(z0), #0) → #false
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1)
#eq(#neg(z0), #pos(z1)) → #false
#eq(#pos(z0), #0) → #false
#eq(#pos(z0), #neg(z1)) → #false
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1)
#eq(#s(z0), #0) → #false
#eq(#s(z0), #s(z1)) → #eq(z0, z1)
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3))
#eq(::(z0, z1), nil) → #false
#eq(nil, ::(z0, z1)) → #false
#eq(nil, nil) → #true
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
eq#2(::(z0, z1)) → #false
eq#2(nil) → #true

Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

S tuples:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

K tuples:none
Defined Rule Symbols:

remove, remove#1, remove#2, eq, eq#1, eq#3, and, #equal, #eq, #and, eq#2

Defined Pair Symbols:

#EQ, #EQUAL, EQ, EQ#1, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2, EQ#3

Compound Symbols:

c9, c13, c15, c20, c22, c23, c29, c30, c32, c33, c35, c36, c16, c27

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))

We considered the (Usable) Rules:

remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove(z0, z1) → remove#1(z1, z0)
remove#1(nil, z0) → nil

And the Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = 0
POL(#EQ(x₁, x₂)) = 0
POL(#EQUAL(x₁, x₂)) = 0
POL(#and(x₁, x₂)) = [3] + x₁ + [2]x₂
POL(#eq(x₁, x₂)) = [2] + [3]x₁ + [5]x₂
POL(#equal(x₁, x₂)) = [2] + [5]x₁ + [2]x₂
POL(#false) = 0
POL(#neg(x₁)) = [2]
POL(#pos(x₁)) = [3]
POL(#s(x₁)) = [3]
POL(#true) = [2]
POL(::(x₁, x₂)) = [1] + x₂
POL(EQ(x₁, x₂)) = 0
POL(EQ#1(x₁, x₂)) = 0
POL(EQ#3(x₁, x₂, x₃)) = 0
POL(NUB(x₁)) = x₁
POL(NUB#1(x₁)) = x₁
POL(REMOVE(x₁, x₂)) = 0
POL(REMOVE#1(x₁, x₂)) = 0
POL(REMOVE#2(x₁, x₂, x₃, x₄)) = 0
POL(and(x₁, x₂)) = [3] + [5]x₁
POL(c13(x₁)) = x₁
POL(c15(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c20(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c23(x₁)) = x₁
POL(c27(x₁, x₂)) = x₁ + x₂
POL(c29(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c32(x₁)) = x₁
POL(c33(x₁, x₂)) = x₁ + x₂
POL(c35(x₁)) = x₁
POL(c36(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(eq(x₁, x₂)) = 0
POL(eq#1(x₁, x₂)) = [3] + [3]x₁ + [3]x₂
POL(eq#2(x₁)) = [3] + x₁
POL(eq#3(x₁, x₂, x₃)) = [4] + [3]x₂ + [3]x₃
POL(nil) = 0
POL(remove(x₁, x₂)) = x₂
POL(remove#1(x₁, x₂)) = x₁
POL(remove#2(x₁, x₂, x₃, x₄)) = [1] + x₄

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

remove(z0, z1) → remove#1(z1, z0)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove#1(nil, z0) → nil
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)
eq(z0, z1) → eq#1(z0, z1)
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1)
eq#1(nil, z0) → eq#2(z0)
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1))
eq#3(nil, z0, z1) → #false
and(z0, z1) → #and(z0, z1)
#equal(z0, z1) → #eq(z0, z1)
#eq(#0, #0) → #true
#eq(#0, #neg(z0)) → #false
#eq(#0, #pos(z0)) → #false
#eq(#0, #s(z0)) → #false
#eq(#neg(z0), #0) → #false
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1)
#eq(#neg(z0), #pos(z1)) → #false
#eq(#pos(z0), #0) → #false
#eq(#pos(z0), #neg(z1)) → #false
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1)
#eq(#s(z0), #0) → #false
#eq(#s(z0), #s(z1)) → #eq(z0, z1)
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3))
#eq(::(z0, z1), nil) → #false
#eq(nil, ::(z0, z1)) → #false
#eq(nil, nil) → #true
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
eq#2(::(z0, z1)) → #false
eq#2(nil) → #true

Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

S tuples:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

K tuples:

NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))

Defined Rule Symbols:

remove, remove#1, remove#2, eq, eq#1, eq#3, and, #equal, #eq, #and, eq#2

Defined Pair Symbols:

#EQ, #EQUAL, EQ, EQ#1, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2, EQ#3

Compound Symbols:

c9, c13, c15, c20, c22, c23, c29, c30, c32, c33, c35, c36, c16, c27

(11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

remove(z0, z1) → remove#1(z1, z0)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove#1(nil, z0) → nil
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)
eq(z0, z1) → eq#1(z0, z1)
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1)
eq#1(nil, z0) → eq#2(z0)
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1))
eq#3(nil, z0, z1) → #false
and(z0, z1) → #and(z0, z1)
#equal(z0, z1) → #eq(z0, z1)
#eq(#0, #0) → #true
#eq(#0, #neg(z0)) → #false
#eq(#0, #pos(z0)) → #false
#eq(#0, #s(z0)) → #false
#eq(#neg(z0), #0) → #false
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1)
#eq(#neg(z0), #pos(z1)) → #false
#eq(#pos(z0), #0) → #false
#eq(#pos(z0), #neg(z1)) → #false
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1)
#eq(#s(z0), #0) → #false
#eq(#s(z0), #s(z1)) → #eq(z0, z1)
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3))
#eq(::(z0, z1), nil) → #false
#eq(nil, ::(z0, z1)) → #false
#eq(nil, nil) → #true
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
eq#2(::(z0, z1)) → #false
eq#2(nil) → #true

Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

S tuples:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

K tuples:

NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
NUB(z0) → c29(NUB#1(z0))

Defined Rule Symbols:

remove, remove#1, remove#2, eq, eq#1, eq#3, and, #equal, #eq, #and, eq#2

Defined Pair Symbols:

#EQ, #EQUAL, EQ, EQ#1, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2, EQ#3

Compound Symbols:

c9, c13, c15, c20, c22, c23, c29, c30, c32, c33, c35, c36, c16, c27

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))

We considered the (Usable) Rules:

remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove(z0, z1) → remove#1(z1, z0)
remove#1(nil, z0) → nil

And the Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = 0
POL(#EQ(x₁, x₂)) = 0
POL(#EQUAL(x₁, x₂)) = 0
POL(#and(x₁, x₂)) = 0
POL(#eq(x₁, x₂)) = 0
POL(#equal(x₁, x₂)) = 0
POL(#false) = 0
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = 0
POL(#true) = 0
POL(::(x₁, x₂)) = [1] + x₂
POL(EQ(x₁, x₂)) = 0
POL(EQ#1(x₁, x₂)) = 0
POL(EQ#3(x₁, x₂, x₃)) = 0
POL(NUB(x₁)) = [2] + x₁²
POL(NUB#1(x₁)) = [1] + x₁²
POL(REMOVE(x₁, x₂)) = x₂
POL(REMOVE#1(x₁, x₂)) = x₁
POL(REMOVE#2(x₁, x₂, x₃, x₄)) = x₄
POL(and(x₁, x₂)) = 0
POL(c13(x₁)) = x₁
POL(c15(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c20(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c23(x₁)) = x₁
POL(c27(x₁, x₂)) = x₁ + x₂
POL(c29(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c32(x₁)) = x₁
POL(c33(x₁, x₂)) = x₁ + x₂
POL(c35(x₁)) = x₁
POL(c36(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(eq(x₁, x₂)) = 0
POL(eq#1(x₁, x₂)) = 0
POL(eq#2(x₁)) = 0
POL(eq#3(x₁, x₂, x₃)) = 0
POL(nil) = 0
POL(remove(x₁, x₂)) = x₂
POL(remove#1(x₁, x₂)) = x₁
POL(remove#2(x₁, x₂, x₃, x₄)) = [1] + x₄

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

remove(z0, z1) → remove#1(z1, z0)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove#1(nil, z0) → nil
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)
eq(z0, z1) → eq#1(z0, z1)
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1)
eq#1(nil, z0) → eq#2(z0)
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1))
eq#3(nil, z0, z1) → #false
and(z0, z1) → #and(z0, z1)
#equal(z0, z1) → #eq(z0, z1)
#eq(#0, #0) → #true
#eq(#0, #neg(z0)) → #false
#eq(#0, #pos(z0)) → #false
#eq(#0, #s(z0)) → #false
#eq(#neg(z0), #0) → #false
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1)
#eq(#neg(z0), #pos(z1)) → #false
#eq(#pos(z0), #0) → #false
#eq(#pos(z0), #neg(z1)) → #false
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1)
#eq(#s(z0), #0) → #false
#eq(#s(z0), #s(z1)) → #eq(z0, z1)
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3))
#eq(::(z0, z1), nil) → #false
#eq(nil, ::(z0, z1)) → #false
#eq(nil, nil) → #true
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
eq#2(::(z0, z1)) → #false
eq#2(nil) → #true

Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

S tuples:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

K tuples:

NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
NUB(z0) → c29(NUB#1(z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))

Defined Rule Symbols:

remove, remove#1, remove#2, eq, eq#1, eq#3, and, #equal, #eq, #and, eq#2

Defined Pair Symbols:

#EQ, #EQUAL, EQ, EQ#1, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2, EQ#3

Compound Symbols:

c9, c13, c15, c20, c22, c23, c29, c30, c32, c33, c35, c36, c16, c27

(15) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

remove(z0, z1) → remove#1(z1, z0)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove#1(nil, z0) → nil
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)
eq(z0, z1) → eq#1(z0, z1)
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1)
eq#1(nil, z0) → eq#2(z0)
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1))
eq#3(nil, z0, z1) → #false
and(z0, z1) → #and(z0, z1)
#equal(z0, z1) → #eq(z0, z1)
#eq(#0, #0) → #true
#eq(#0, #neg(z0)) → #false
#eq(#0, #pos(z0)) → #false
#eq(#0, #s(z0)) → #false
#eq(#neg(z0), #0) → #false
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1)
#eq(#neg(z0), #pos(z1)) → #false
#eq(#pos(z0), #0) → #false
#eq(#pos(z0), #neg(z1)) → #false
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1)
#eq(#s(z0), #0) → #false
#eq(#s(z0), #s(z1)) → #eq(z0, z1)
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3))
#eq(::(z0, z1), nil) → #false
#eq(nil, ::(z0, z1)) → #false
#eq(nil, nil) → #true
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
eq#2(::(z0, z1)) → #false
eq#2(nil) → #true

Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

S tuples:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

K tuples:

NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
NUB(z0) → c29(NUB#1(z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))

Defined Rule Symbols:

remove, remove#1, remove#2, eq, eq#1, eq#3, and, #equal, #eq, #and, eq#2

Defined Pair Symbols:

#EQ, #EQUAL, EQ, EQ#1, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2, EQ#3

Compound Symbols:

c9, c13, c15, c20, c22, c23, c29, c30, c32, c33, c35, c36, c16, c27

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

We considered the (Usable) Rules:

remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove(z0, z1) → remove#1(z1, z0)
remove#1(nil, z0) → nil

And the Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = 0
POL(#EQ(x₁, x₂)) = 0
POL(#EQUAL(x₁, x₂)) = x₂
POL(#and(x₁, x₂)) = 0
POL(#eq(x₁, x₂)) = 0
POL(#equal(x₁, x₂)) = 0
POL(#false) = 0
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = 0
POL(#true) = 0
POL(::(x₁, x₂)) = [1] + x₁ + x₂
POL(EQ(x₁, x₂)) = x₂
POL(EQ#1(x₁, x₂)) = x₂
POL(EQ#3(x₁, x₂, x₃)) = x₁
POL(NUB(x₁)) = [1] + x₁²
POL(NUB#1(x₁)) = x₁²
POL(REMOVE(x₁, x₂)) = x₂
POL(REMOVE#1(x₁, x₂)) = x₁
POL(REMOVE#2(x₁, x₂, x₃, x₄)) = [1] + x₄
POL(and(x₁, x₂)) = 0
POL(c13(x₁)) = x₁
POL(c15(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c20(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c23(x₁)) = x₁
POL(c27(x₁, x₂)) = x₁ + x₂
POL(c29(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c32(x₁)) = x₁
POL(c33(x₁, x₂)) = x₁ + x₂
POL(c35(x₁)) = x₁
POL(c36(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(eq(x₁, x₂)) = 0
POL(eq#1(x₁, x₂)) = 0
POL(eq#2(x₁)) = 0
POL(eq#3(x₁, x₂, x₃)) = 0
POL(nil) = 0
POL(remove(x₁, x₂)) = x₂
POL(remove#1(x₁, x₂)) = x₁
POL(remove#2(x₁, x₂, x₃, x₄)) = [1] + x₃ + x₄

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

remove(z0, z1) → remove#1(z1, z0)
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1)
remove#1(nil, z0) → nil
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2))
remove#2(#true, z0, z1, z2) → remove(z0, z2)
eq(z0, z1) → eq#1(z0, z1)
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1)
eq#1(nil, z0) → eq#2(z0)
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1))
eq#3(nil, z0, z1) → #false
and(z0, z1) → #and(z0, z1)
#equal(z0, z1) → #eq(z0, z1)
#eq(#0, #0) → #true
#eq(#0, #neg(z0)) → #false
#eq(#0, #pos(z0)) → #false
#eq(#0, #s(z0)) → #false
#eq(#neg(z0), #0) → #false
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1)
#eq(#neg(z0), #pos(z1)) → #false
#eq(#pos(z0), #0) → #false
#eq(#pos(z0), #neg(z1)) → #false
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1)
#eq(#s(z0), #0) → #false
#eq(#s(z0), #s(z1)) → #eq(z0, z1)
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3))
#eq(::(z0, z1), nil) → #false
#eq(nil, ::(z0, z1)) → #false
#eq(nil, nil) → #true
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
eq#2(::(z0, z1)) → #false
eq#2(nil) → #true

Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1))
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
NUB(z0) → c29(NUB#1(z0))
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

S tuples:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))

K tuples:

NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
NUB(z0) → c29(NUB#1(z0))
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

Defined Rule Symbols:

remove, remove#1, remove#2, eq, eq#1, eq#3, and, #equal, #eq, #and, eq#2

Defined Pair Symbols:

#EQ, #EQUAL, EQ, EQ#1, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2, EQ#3

Compound Symbols:

c9, c13, c15, c20, c22, c23, c29, c30, c32, c33, c35, c36, c16, c27

(19) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
EQ(z0, z1) → c22(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c27(#EQUAL(z2, z0), EQ(z3, z1))

Now S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

(2) Obligation:

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

(4) Obligation:

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtUsableRulesProof (EQUIVALENT transformation)

(8) Obligation:

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(10) Obligation:

(11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(14) Obligation:

(15) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(18) Obligation:

(19) CdtKnowledgeProof (EQUIVALENT transformation)

(20) BOUNDS(1, 1)