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

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

0 CpxRelTRS

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

↳2 CpxTRS

↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 4 ms)

↳4 CdtProblem

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

↳6 CdtProblem

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

↳8 CdtProblem

↳9 CdtUsableRulesProof (⇔, 0 ms)

↳10 CdtProblem

↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 281 ms)

↳12 CdtProblem

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

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 658 ms)

↳16 CdtProblem

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

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 490 ms)

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 329 ms)

↳22 CdtProblem

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

↳24 CdtProblem

↳25 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 485 ms)

↳26 CdtProblem

↳27 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳28 BOUNDS(1, 1)

(0) Obligation:

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

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

transformed relative TRS to TRS

(2) Obligation:

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

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)
#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) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

#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)
#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

Tuples:

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

S tuples:

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

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:

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

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

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

Removed 23 trailing nodes:

#AND(#false, #false) → c17
EQ#1(nil, z0) → c4(EQ#2(z0))
NUB#1(nil) → c11
#EQ(#pos(z0), #0) → c28
#AND(#true, #true) → c20
EQ#2(nil) → c6
#EQ(#0, #s(z0)) → c24
EQ#3(nil, z0, z1) → c8
#EQ(#neg(z0), #0) → c25
#EQ(nil, ::(z0, z1)) → c35
#EQ(#pos(z0), #neg(z1)) → c29
EQ#2(::(z0, z1)) → c5
#EQ(#s(z0), #0) → c31
#AND(#false, #true) → c18
#AND(#true, #false) → c19
#EQ(#0, #pos(z0)) → c23
#EQ(#0, #0) → c21
#EQ(#0, #neg(z0)) → c22
#EQ(::(z0, z1), nil) → c34
AND(z0, z1) → c1(#AND(z0, z1))
#EQ(nil, nil) → c36
#EQ(#neg(z0), #pos(z1)) → c27
REMOVE#1(nil, z0) → c14

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

#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)
#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

Tuples:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2), #EQ(z1, z3))

S tuples:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2), #EQ(z1, z3))

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:

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

Compound Symbols:

c, c2, c3, c7, c9, c10, c12, c13, c15, c16, c26, c30, c32, c33

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

Removed 2 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

#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)
#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

Tuples:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

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:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

(9) 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

(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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

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:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

(11) 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(z0) → c9(NUB#1(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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

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₂)) = x₁
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₁)) = [1] + 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₂)) = 0
POL(c(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁, x₂)) = x₁ + x₂
POL(c7(x₁, x₂)) = 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₄

(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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

K tuples:

NUB(z0) → c9(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:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

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

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

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

(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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

K tuples:

NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(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:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

(15) 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#1(::(z0, z1), z2) → c3(EQ#3(z2, 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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

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

POL(#0) = [1]
POL(#EQ(x₁, x₂)) = 0
POL(#EQUAL(x₁, x₂)) = 0
POL(#and(x₁, x₂)) = [2] + [2]x₁ + [2]x₂
POL(#eq(x₁, x₂)) = [1] + x₂ + x₁·x₂ + [2]x₁²
POL(#equal(x₁, x₂)) = [1] + [2]x₁ + x₂ + [2]x₂² + [2]x₁·x₂ + [2]x₁²
POL(#false) = 0
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = [2]
POL(#s(x₁)) = [2]
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₁)) = [2]x₁²
POL(NUB#1(x₁)) = [2]x₁²
POL(REMOVE(x₁, x₂)) = x₁·x₂
POL(REMOVE#1(x₁, x₂)) = x₁·x₂
POL(REMOVE#2(x₁, x₂, x₃, x₄)) = x₂·x₄
POL(and(x₁, x₂)) = [2] + x₂
POL(c(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁, x₂)) = x₁ + x₂
POL(c7(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(eq(x₁, x₂)) = x₁·x₂
POL(eq#1(x₁, x₂)) = x₂ + [2]x₂² + x₁·x₂
POL(eq#2(x₁)) = [2] + [2]x₁ + [2]x₁²
POL(eq#3(x₁, x₂, x₃)) = [2] + [2]x₂ + x₃ + [2]x₃² + [2]x₂·x₃ + x₁·x₃ + [2]x₁·x₂ + [2]x₂²
POL(nil) = 0
POL(remove(x₁, x₂)) = [1] + x₂
POL(remove#1(x₁, x₂)) = [1] + x₁
POL(remove#2(x₁, x₂, x₃, x₄)) = [2] + x₃ + x₄

(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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

K tuples:

NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

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

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

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

(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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:

EQ(z0, z1) → c2(EQ#1(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

K tuples:

NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQUAL(z0, z1) → c(#EQ(z0, z1))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

(19) 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(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

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

POL(#0) = [1]
POL(#EQ(x₁, x₂)) = x₂
POL(#EQUAL(x₁, x₂)) = [2]x₂
POL(#and(x₁, x₂)) = [2] + [2]x₁ + [2]x₂ + [2]x₂² + x₁²
POL(#eq(x₁, x₂)) = [2] + [2]x₁ + [2]x₂ + x₂² + [2]x₁·x₂ + [2]x₁²
POL(#equal(x₁, x₂)) = x₁ + [2]x₂ + [2]x₂² + [2]x₁·x₂ + x₁²
POL(#false) = [2]
POL(#neg(x₁)) = [1] + x₁
POL(#pos(x₁)) = [1] + x₁
POL(#s(x₁)) = x₁
POL(#true) = 0
POL(::(x₁, x₂)) = [2] + x₁ + x₂
POL(EQ(x₁, x₂)) = [2]x₁ + [2]x₁·x₂
POL(EQ#1(x₁, x₂)) = x₁ + [2]x₁·x₂
POL(EQ#3(x₁, x₂, x₃)) = [2] + [2]x₁ + [2]x₁·x₃
POL(NUB(x₁)) = [2] + x₁²
POL(NUB#1(x₁)) = [2] + x₁²
POL(REMOVE(x₁, x₂)) = [2]x₁ + [2]x₁·x₂
POL(REMOVE#1(x₁, x₂)) = x₂ + [2]x₁·x₂
POL(REMOVE#2(x₁, x₂, x₃, x₄)) = [2]x₂ + [2]x₂·x₄
POL(and(x₁, x₂)) = [1] + [2]x₂ + [2]x₂² + x₁·x₂ + [2]x₁²
POL(c(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁, x₂)) = x₁ + x₂
POL(c7(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(eq(x₁, x₂)) = [2] + [2]x₂ + x₂² + [2]x₁·x₂ + [2]x₁²
POL(eq#1(x₁, x₂)) = [2] + [2]x₂ + [2]x₂² + x₁²
POL(eq#2(x₁)) = [1] + x₁ + x₁²
POL(eq#3(x₁, x₂, x₃)) = [2] + x₁ + x₂ + x₃ + [2]x₃² + x₂·x₃ + [2]x₁·x₃ + [2]x₁² + [2]x₁·x₂ + [2]x₂²
POL(nil) = 0
POL(remove(x₁, x₂)) = x₂
POL(remove#1(x₁, x₂)) = x₁
POL(remove#2(x₁, x₂, x₃, x₄)) = [2] + x₃ + x₄

(20) 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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:

EQ(z0, z1) → c2(EQ#1(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))

K tuples:

NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQUAL(z0, z1) → c(#EQ(z0, z1))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

(21) 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) → c13(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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

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

POL(#0) = [1]
POL(#EQ(x₁, x₂)) = 0
POL(#EQUAL(x₁, x₂)) = 0
POL(#and(x₁, x₂)) = [2]
POL(#eq(x₁, x₂)) = [2]x₂ + x₁·x₂
POL(#equal(x₁, x₂)) = [1] + [2]x₂ + [2]x₁·x₂
POL(#false) = [1]
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = [1]
POL(#s(x₁)) = 0
POL(#true) = 0
POL(::(x₁, x₂)) = [2] + 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₁)) = [2]x₁²
POL(REMOVE(x₁, x₂)) = [2]x₂
POL(REMOVE#1(x₁, x₂)) = [2]x₁
POL(REMOVE#2(x₁, x₂, x₃, x₄)) = [2]x₄
POL(and(x₁, x₂)) = [1] + [2]x₂ + x₁²
POL(c(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁, x₂)) = x₁ + x₂
POL(c7(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(eq(x₁, x₂)) = [2] + [2]x₂
POL(eq#1(x₁, x₂)) = [2] + x₂ + [2]x₂²
POL(eq#2(x₁)) = [1]
POL(eq#3(x₁, x₂, x₃)) = x₂ + x₃ + [2]x₃² + x₂·x₃ + x₁² + [2]x₁·x₂ + x₂²
POL(nil) = 0
POL(remove(x₁, x₂)) = x₂
POL(remove#1(x₁, x₂)) = x₁
POL(remove#2(x₁, x₂, x₃, x₄)) = [2] + x₄

(22) 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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:

EQ(z0, z1) → c2(EQ#1(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))

K tuples:

NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQUAL(z0, z1) → c(#EQ(z0, z1))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))
REMOVE#1(::(z0, z1), z2) → c13(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:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

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

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

EQ(z0, z1) → c2(EQ#1(z0, z1))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))

(24) 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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:

#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))

K tuples:

NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQUAL(z0, z1) → c(#EQ(z0, z1))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
EQ(z0, z1) → c2(EQ#1(z0, z1))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
REMOVE(z0, z1) → c12(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:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

(25) 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(#s(z0), #s(z1)) → c32(#EQ(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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

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

POL(#0) = [1]
POL(#EQ(x₁, x₂)) = x₂
POL(#EQUAL(x₁, x₂)) = x₂
POL(#and(x₁, x₂)) = [2] + [2]x₁ + [2]x₂ + [2]x₂² + [2]x₁·x₂
POL(#eq(x₁, x₂)) = [1] + [2]x₁ + [2]x₂ + x₂² + x₁·x₂ + [2]x₁²
POL(#equal(x₁, x₂)) = [2] + [2]x₂² + x₁·x₂ + [2]x₁²
POL(#false) = 0
POL(#neg(x₁)) = x₁
POL(#pos(x₁)) = [1] + x₁
POL(#s(x₁)) = [1] + x₁
POL(#true) = 0
POL(::(x₁, x₂)) = [2] + x₁ + x₂
POL(EQ(x₁, x₂)) = [2] + x₂
POL(EQ#1(x₁, x₂)) = [2] + x₂
POL(EQ#3(x₁, x₂, x₃)) = [1] + x₁
POL(NUB(x₁)) = x₁²
POL(NUB#1(x₁)) = x₁²
POL(REMOVE(x₁, x₂)) = x₂
POL(REMOVE#1(x₁, x₂)) = x₁
POL(REMOVE#2(x₁, x₂, x₃, x₄)) = x₄
POL(and(x₁, x₂)) = [2] + [2]x₁ + x₂ + [2]x₂² + [2]x₁·x₂ + [2]x₁²
POL(c(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c26(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c32(x₁)) = x₁
POL(c33(x₁, x₂)) = x₁ + x₂
POL(c7(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(eq(x₁, x₂)) = 0
POL(eq#1(x₁, x₂)) = [1] + x₂ + [2]x₂²
POL(eq#2(x₁)) = [1] + [2]x₁ + [2]x₁²
POL(eq#3(x₁, x₂, x₃)) = [2] + x₂ + x₃ + [2]x₃² + [2]x₂·x₃ + [2]x₁·x₂ + x₂²
POL(nil) = 0
POL(remove(x₁, x₂)) = x₂
POL(remove#1(x₁, x₂)) = x₁
POL(remove#2(x₁, x₂, x₃, x₄)) = [2] + x₃ + x₄

(26) 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:

#EQUAL(z0, z1) → c(#EQ(z0, z1))
EQ(z0, z1) → c2(EQ#1(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))

S tuples:none
K tuples:

NUB(z0) → c9(NUB#1(z0))
NUB#1(::(z0, z1)) → c10(NUB(remove(z0, z1)), REMOVE(z0, z1))
EQ#1(::(z0, z1), z2) → c3(EQ#3(z2, z0, z1))
EQ#3(::(z0, z1), z2, z3) → c7(#EQUAL(z2, z0), EQ(z3, z1))
#EQUAL(z0, z1) → c(#EQ(z0, z1))
#EQ(#neg(z0), #neg(z1)) → c26(#EQ(z0, z1))
#EQ(#pos(z0), #pos(z1)) → c30(#EQ(z0, z1))
#EQ(::(z0, z1), ::(z2, z3)) → c33(#EQ(z0, z2), #EQ(z1, z3))
REMOVE#1(::(z0, z1), z2) → c13(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
EQ(z0, z1) → c2(EQ#1(z0, z1))
REMOVE#2(#false, z0, z1, z2) → c15(REMOVE(z0, z2))
REMOVE#2(#true, z0, z1, z2) → c16(REMOVE(z0, z2))
REMOVE(z0, z1) → c12(REMOVE#1(z1, z0))
#EQ(#s(z0), #s(z1)) → c32(#EQ(z0, z1))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c3, c9, c10, c12, c13, c15, c16, c26, c30, c32, c7, c33

(27) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(0) Obligation:

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) CdtUsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

(27) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

(28) BOUNDS(1, 1)