YES(O(1), O(n^2)) 25.01/6.97 YES(O(1), O(n^2)) 25.52/7.01 25.52/7.01 25.52/7.01 25.52/7.01 25.52/7.01 25.52/7.01 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 25.52/7.01 25.52/7.01 25.52/7.01
25.52/7.01
25.52/7.01
25.52/7.01
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxRelTRS
25.52/7.01 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
25.52/7.01 
↳2 CdtProblem
25.52/7.01 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
25.52/7.01 
↳4 CdtProblem
25.52/7.01 
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
25.52/7.01 
↳6 CdtProblem
25.52/7.01 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
25.52/7.01 
↳8 CdtProblem
25.52/7.01 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
25.52/7.01 
↳10 CdtProblem
25.52/7.01 
↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
25.52/7.01 
↳12 CdtProblem
25.52/7.01 
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
25.52/7.01 
↳14 CdtProblem
25.52/7.01 
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
25.52/7.01 
↳16 CdtProblem
25.52/7.01 
↳17 CdtKnowledgeProof (⇔)
25.52/7.01 
↳18 BOUNDS(O(1), O(1))
25.52/7.01
25.52/7.01 25.52/7.01
25.52/7.01
25.52/7.01

(0) Obligation:

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

#equal(@x, @y) → #eq(@x, @y) 25.52/7.01
and(@x, @y) → #and(@x, @y) 25.52/7.01
eq(@l1, @l2) → eq#1(@l1, @l2) 25.52/7.01
eq#1(::(@x, @xs), @l2) → eq#3(@l2, @x, @xs) 25.52/7.01
eq#1(nil, @l2) → eq#2(@l2) 25.52/7.01
eq#2(::(@y, @ys)) → #false 25.52/7.01
eq#2(nil) → #true 25.52/7.01
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys)) 25.52/7.01
eq#3(nil, @x, @xs) → #false 25.52/7.01
nub(@l) → nub#1(@l) 25.52/7.01
nub#1(::(@x, @xs)) → ::(@x, nub(remove(@x, @xs))) 25.52/7.01
nub#1(nil) → nil 25.52/7.01
remove(@x, @l) → remove#1(@l, @x) 25.52/7.01
remove#1(::(@y, @ys), @x) → remove#2(eq(@x, @y), @x, @y, @ys) 25.52/7.01
remove#1(nil, @x) → nil 25.52/7.01
remove#2(#false, @x, @y, @ys) → ::(@y, remove(@x, @ys)) 25.52/7.01
remove#2(#true, @x, @y, @ys) → remove(@x, @ys)

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

#and(#false, #false) → #false 25.52/7.01
#and(#false, #true) → #false 25.52/7.01
#and(#true, #false) → #false 25.52/7.01
#and(#true, #true) → #true 25.52/7.01
#eq(#0, #0) → #true 25.52/7.01
#eq(#0, #neg(@y)) → #false 25.52/7.01
#eq(#0, #pos(@y)) → #false 25.52/7.01
#eq(#0, #s(@y)) → #false 25.52/7.01
#eq(#neg(@x), #0) → #false 25.52/7.01
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y) 25.52/7.01
#eq(#neg(@x), #pos(@y)) → #false 25.52/7.01
#eq(#pos(@x), #0) → #false 25.52/7.01
#eq(#pos(@x), #neg(@y)) → #false 25.52/7.01
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y) 25.52/7.01
#eq(#s(@x), #0) → #false 25.52/7.01
#eq(#s(@x), #s(@y)) → #eq(@x, @y) 25.52/7.01
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 25.52/7.01
#eq(::(@x_1, @x_2), nil) → #false 25.52/7.01
#eq(nil, ::(@y_1, @y_2)) → #false 25.52/7.01
#eq(nil, nil) → #true

Rewrite Strategy: INNERMOST
25.52/7.01
25.52/7.01

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
25.52/7.01
25.52/7.01

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.02
AND(z0, z1) → c21(#AND(z0, z1)) 25.52/7.02
EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.02
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.02
EQ#1(nil, z0) → c24(EQ#2(z0)) 25.52/7.02
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.02
NUB(z0) → c29(NUB#1(z0)) 25.52/7.02
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.02
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.02
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.02
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.02
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, AND, EQ, EQ#1, EQ#3, NUB, NUB#1, REMOVE, REMOVE#1, REMOVE#2

Compound Symbols:

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

25.52/7.02
25.52/7.02

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

Removed 3 trailing tuple parts
25.52/7.02
25.52/7.02

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.02
EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.02
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.02
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.02
NUB(z0) → c29(NUB#1(z0)) 25.52/7.02
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.02
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.02
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.02
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.02
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.02
AND(z0, z1) → c21 25.52/7.02
EQ#1(nil, z0) → c24
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, AND

Compound Symbols:

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

25.52/7.02
25.52/7.02

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

Removed 2 trailing nodes:

AND(z0, z1) → c21 25.52/7.02
EQ#1(nil, z0) → c24
25.52/7.02
25.52/7.02

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.02
EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.02
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.02
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.02
NUB(z0) → c29(NUB#1(z0)) 25.52/7.02
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.02
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.02
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.02
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.02
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.02
AND(z0, z1) → c21 25.52/7.02
EQ#1(nil, z0) → c24
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, AND

Compound Symbols:

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

25.52/7.02
25.52/7.02

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

NUB(z0) → c29(NUB#1(z0)) 25.52/7.02
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
We considered the (Usable) Rules:

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

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1)) 25.52/7.02
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1)) 25.52/7.02
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1)) 25.52/7.02
#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.02
EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.02
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.02
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.04
NUB(z0) → c29(NUB#1(z0)) 25.52/7.04
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.04
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.04
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.04
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.04
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.04
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3)) 25.52/7.04
AND(z0, z1) → c21 25.52/7.04
EQ#1(nil, z0) → c24
The order we found is given by the following interpretation:
Polynomial interpretation : 25.52/7.04

POL(#0) = 0    25.52/7.04
POL(#EQ(x1, x2)) = 0    25.52/7.04
POL(#EQUAL(x1, x2)) = 0    25.52/7.04
POL(#and(x1, x2)) = [2]    25.52/7.04
POL(#eq(x1, x2)) = 0    25.52/7.04
POL(#equal(x1, x2)) = 0    25.52/7.04
POL(#false) = 0    25.52/7.04
POL(#neg(x1)) = x1    25.52/7.04
POL(#pos(x1)) = x1    25.52/7.04
POL(#s(x1)) = x1    25.52/7.04
POL(#true) = 0    25.52/7.04
POL(::(x1, x2)) = [4] + x2    25.52/7.04
POL(AND(x1, x2)) = 0    25.52/7.04
POL(EQ(x1, x2)) = 0    25.52/7.04
POL(EQ#1(x1, x2)) = 0    25.52/7.04
POL(EQ#3(x1, x2, x3)) = 0    25.52/7.04
POL(NUB(x1)) = [5] + [2]x1    25.52/7.04
POL(NUB#1(x1)) = [1] + [2]x1    25.52/7.04
POL(REMOVE(x1, x2)) = 0    25.52/7.04
POL(REMOVE#1(x1, x2)) = 0    25.52/7.04
POL(REMOVE#2(x1, x2, x3, x4)) = 0    25.52/7.04
POL(and(x1, x2)) = [3] + [3]x2    25.52/7.04
POL(c13(x1)) = x1    25.52/7.04
POL(c15(x1)) = x1    25.52/7.04
POL(c16(x1, x2)) = x1 + x2    25.52/7.04
POL(c20(x1)) = x1    25.52/7.04
POL(c21) = 0    25.52/7.04
POL(c22(x1)) = x1    25.52/7.04
POL(c23(x1)) = x1    25.52/7.04
POL(c24) = 0    25.52/7.04
POL(c27(x1, x2, x3)) = x1 + x2 + x3    25.52/7.04
POL(c29(x1)) = x1    25.52/7.04
POL(c30(x1, x2)) = x1 + x2    25.52/7.04
POL(c32(x1)) = x1    25.52/7.04
POL(c33(x1, x2)) = x1 + x2    25.52/7.04
POL(c35(x1)) = x1    25.52/7.04
POL(c36(x1)) = x1    25.52/7.04
POL(c9(x1)) = x1    25.52/7.04
POL(eq(x1, x2)) = 0    25.52/7.04
POL(eq#1(x1, x2)) = [3] + [3]x1 + [3]x2    25.52/7.04
POL(eq#2(x1)) = [3] + [3]x1    25.52/7.04
POL(eq#3(x1, x2, x3)) = [3] + [3]x1 + [3]x2 + [3]x3    25.52/7.04
POL(nil) = [3]    25.52/7.04
POL(remove(x1, x2)) = [1] + x2    25.52/7.04
POL(remove#1(x1, x2)) = [1] + x1    25.52/7.04
POL(remove#2(x1, x2, x3, x4)) = [5] + x4   
25.52/7.04
25.52/7.04

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.04
EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.04
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.04
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.04
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.04
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.04
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.04
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.04
AND(z0, z1) → c21 25.52/7.04
EQ#1(nil, z0) → c24
K tuples:

NUB(z0) → c29(NUB#1(z0)) 25.52/7.04
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1))
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, AND

Compound Symbols:

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

25.52/7.04
25.52/7.04

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(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(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.04
AND(z0, z1) → c21
We considered the (Usable) Rules:

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

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1)) 25.52/7.04
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1)) 25.52/7.04
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1)) 25.52/7.04
#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.04
EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.04
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.04
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.04
NUB(z0) → c29(NUB#1(z0)) 25.52/7.04
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.04
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.04
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.04
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.04
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.04
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3)) 25.52/7.04
AND(z0, z1) → c21 25.52/7.04
EQ#1(nil, z0) → c24
The order we found is given by the following interpretation:
Polynomial interpretation : 25.52/7.04

POL(#0) = [3]    25.52/7.04
POL(#EQ(x1, x2)) = 0    25.52/7.04
POL(#EQUAL(x1, x2)) = 0    25.52/7.04
POL(#and(x1, x2)) = 0    25.52/7.04
POL(#eq(x1, x2)) = 0    25.52/7.04
POL(#equal(x1, x2)) = 0    25.52/7.04
POL(#false) = 0    25.52/7.04
POL(#neg(x1)) = 0    25.52/7.04
POL(#pos(x1)) = 0    25.52/7.04
POL(#s(x1)) = 0    25.52/7.04
POL(#true) = 0    25.52/7.04
POL(::(x1, x2)) = [3] + x1 + x2    25.52/7.04
POL(AND(x1, x2)) = [3] + [2]x2    25.52/7.04
POL(EQ(x1, x2)) = [2]x1·x2    25.52/7.04
POL(EQ#1(x1, x2)) = [2]x1·x2    25.52/7.04
POL(EQ#3(x1, x2, x3)) = [3]x1 + [2]x1·x3    25.52/7.04
POL(NUB(x1)) = [1] + x12    25.52/7.04
POL(NUB#1(x1)) = [1] + x12    25.52/7.04
POL(REMOVE(x1, x2)) = [2]x1·x2    25.52/7.04
POL(REMOVE#1(x1, x2)) = [2]x1·x2    25.52/7.04
POL(REMOVE#2(x1, x2, x3, x4)) = [2]x2·x4    25.52/7.04
POL(and(x1, x2)) = 0    25.52/7.04
POL(c13(x1)) = x1    25.52/7.04
POL(c15(x1)) = x1    25.52/7.04
POL(c16(x1, x2)) = x1 + x2    25.52/7.04
POL(c20(x1)) = x1    25.52/7.04
POL(c21) = 0    25.52/7.04
POL(c22(x1)) = x1    25.52/7.04
POL(c23(x1)) = x1    25.52/7.04
POL(c24) = 0    25.52/7.04
POL(c27(x1, x2, x3)) = x1 + x2 + x3    25.52/7.04
POL(c29(x1)) = x1    25.52/7.04
POL(c30(x1, x2)) = x1 + x2    25.52/7.04
POL(c32(x1)) = x1    25.52/7.04
POL(c33(x1, x2)) = x1 + x2    25.52/7.04
POL(c35(x1)) = x1    25.52/7.04
POL(c36(x1)) = x1    25.52/7.04
POL(c9(x1)) = x1    25.52/7.04
POL(eq(x1, x2)) = [2]    25.52/7.04
POL(eq#1(x1, x2)) = 0    25.52/7.04
POL(eq#2(x1)) = 0    25.52/7.04
POL(eq#3(x1, x2, x3)) = 0    25.52/7.04
POL(nil) = 0    25.52/7.04
POL(remove(x1, x2)) = x2    25.52/7.04
POL(remove#1(x1, x2)) = x1    25.52/7.04
POL(remove#2(x1, x2, x3, x4)) = [3] + x3 + x4   
25.52/7.04
25.52/7.04

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.05
EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.05
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.05
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.05
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.05
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.05
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.05
EQ#1(nil, z0) → c24
K tuples:

NUB(z0) → c29(NUB#1(z0)) 25.52/7.05
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.05
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.05
AND(z0, z1) → c21
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, AND

Compound Symbols:

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

25.52/7.06
25.52/7.06

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

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

#EQUAL(z0, z1) → c20(#EQ(z0, z1))
25.52/7.06
25.52/7.06

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.06
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.06
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.06
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.06
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.06
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.06
EQ#1(nil, z0) → c24
K tuples:

NUB(z0) → c29(NUB#1(z0)) 25.52/7.06
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.06
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.06
AND(z0, z1) → c21 25.52/7.06
#EQUAL(z0, z1) → c20(#EQ(z0, z1))
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, AND

Compound Symbols:

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

25.52/7.06
25.52/7.06

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
We considered the (Usable) Rules:

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

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1)) 25.52/7.06
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1)) 25.52/7.06
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1)) 25.52/7.06
#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.06
EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.06
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.06
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.06
NUB(z0) → c29(NUB#1(z0)) 25.52/7.06
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.06
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.06
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.06
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.06
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.06
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3)) 25.52/7.06
AND(z0, z1) → c21 25.52/7.06
EQ#1(nil, z0) → c24
The order we found is given by the following interpretation:
Polynomial interpretation : 25.52/7.06

POL(#0) = [3]    25.52/7.06
POL(#EQ(x1, x2)) = 0    25.52/7.06
POL(#EQUAL(x1, x2)) = 0    25.52/7.06
POL(#and(x1, x2)) = x2    25.52/7.06
POL(#eq(x1, x2)) = 0    25.52/7.06
POL(#equal(x1, x2)) = 0    25.52/7.06
POL(#false) = 0    25.52/7.06
POL(#neg(x1)) = 0    25.52/7.06
POL(#pos(x1)) = 0    25.52/7.06
POL(#s(x1)) = 0    25.52/7.06
POL(#true) = [1]    25.52/7.06
POL(::(x1, x2)) = x1 + x2    25.52/7.06
POL(AND(x1, x2)) = 0    25.52/7.06
POL(EQ(x1, x2)) = 0    25.52/7.06
POL(EQ#1(x1, x2)) = 0    25.52/7.06
POL(EQ#3(x1, x2, x3)) = 0    25.52/7.06
POL(NUB(x1)) = x12    25.52/7.06
POL(NUB#1(x1)) = x12    25.52/7.06
POL(REMOVE(x1, x2)) = x1·x2    25.52/7.06
POL(REMOVE#1(x1, x2)) = x1·x2    25.52/7.06
POL(REMOVE#2(x1, x2, x3, x4)) = x1 + x2·x4    25.52/7.06
POL(and(x1, x2)) = x2    25.52/7.06
POL(c13(x1)) = x1    25.52/7.06
POL(c15(x1)) = x1    25.52/7.06
POL(c16(x1, x2)) = x1 + x2    25.52/7.06
POL(c20(x1)) = x1    25.52/7.06
POL(c21) = 0    25.52/7.06
POL(c22(x1)) = x1    25.52/7.06
POL(c23(x1)) = x1    25.52/7.06
POL(c24) = 0    25.52/7.06
POL(c27(x1, x2, x3)) = x1 + x2 + x3    25.52/7.06
POL(c29(x1)) = x1    25.52/7.06
POL(c30(x1, x2)) = x1 + x2    25.52/7.06
POL(c32(x1)) = x1    25.52/7.06
POL(c33(x1, x2)) = x1 + x2    25.52/7.06
POL(c35(x1)) = x1    25.52/7.06
POL(c36(x1)) = x1    25.52/7.06
POL(c9(x1)) = x1    25.52/7.06
POL(eq(x1, x2)) = x1·x2    25.52/7.06
POL(eq#1(x1, x2)) = x1·x2    25.52/7.06
POL(eq#2(x1)) = x1    25.52/7.06
POL(eq#3(x1, x2, x3)) = x1·x3    25.52/7.06
POL(nil) = [1]    25.52/7.06
POL(remove(x1, x2)) = x2    25.52/7.06
POL(remove#1(x1, x2)) = x1    25.52/7.06
POL(remove#2(x1, x2, x3, x4)) = x3 + x4   
25.52/7.06
25.52/7.06

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.06
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.06
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.06
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.06
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.06
EQ#1(nil, z0) → c24
K tuples:

NUB(z0) → c29(NUB#1(z0)) 25.52/7.06
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.06
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.06
AND(z0, z1) → c21 25.52/7.06
#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.06
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2))
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, AND

Compound Symbols:

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

25.52/7.06
25.52/7.06

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(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)) 25.52/7.06
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
We considered the (Usable) Rules:

eq(z0, z1) → eq#1(z0, z1) 25.52/7.06
eq#1(::(z0, z1), z2) → eq#3(z2, z0, z1) 25.52/7.06
eq#1(nil, z0) → eq#2(z0) 25.52/7.06
eq#2(::(z0, z1)) → #false 25.52/7.06
eq#2(nil) → #true 25.52/7.06
eq#3(::(z0, z1), z2, z3) → and(#equal(z2, z0), eq(z3, z1)) 25.52/7.06
eq#3(nil, z0, z1) → #false 25.52/7.06
#equal(z0, z1) → #eq(z0, z1) 25.52/7.06
and(z0, z1) → #and(z0, z1) 25.52/7.06
#and(#false, #false) → #false 25.52/7.06
#and(#false, #true) → #false 25.52/7.06
#and(#true, #false) → #false 25.52/7.06
#and(#true, #true) → #true 25.52/7.06
#eq(#0, #0) → #true 25.52/7.06
#eq(#0, #neg(z0)) → #false 25.52/7.06
#eq(#0, #pos(z0)) → #false 25.52/7.06
#eq(#0, #s(z0)) → #false 25.52/7.06
#eq(#neg(z0), #0) → #false 25.52/7.06
#eq(#neg(z0), #pos(z1)) → #false 25.52/7.06
#eq(#pos(z0), #0) → #false 25.52/7.06
#eq(#pos(z0), #neg(z1)) → #false 25.52/7.06
#eq(#pos(z0), #pos(z1)) → #eq(z0, z1) 25.52/7.06
#eq(#neg(z0), #neg(z1)) → #eq(z0, z1) 25.52/7.07
#eq(#s(z0), #s(z1)) → #eq(z0, z1) 25.52/7.07
#eq(#s(z0), #0) → #false 25.52/7.07
#eq(::(z0, z1), ::(z2, z3)) → #and(#eq(z0, z2), #eq(z1, z3)) 25.52/7.07
#eq(::(z0, z1), nil) → #false 25.52/7.07
#eq(nil, ::(z0, z1)) → #false 25.52/7.07
#eq(nil, nil) → #true 25.52/7.07
remove#1(::(z0, z1), z2) → remove#2(eq(z2, z0), z2, z0, z1) 25.52/7.07
remove#1(nil, z0) → nil 25.52/7.07
remove#2(#true, z0, z1, z2) → remove(z0, z2) 25.52/7.07
remove#2(#false, z0, z1, z2) → ::(z1, remove(z0, z2)) 25.52/7.07
remove(z0, z1) → remove#1(z1, z0)
And the Tuples:

#EQ(#neg(z0), #neg(z1)) → c9(#EQ(z0, z1)) 25.52/7.07
#EQ(#pos(z0), #pos(z1)) → c13(#EQ(z0, z1)) 25.52/7.07
#EQ(#s(z0), #s(z1)) → c15(#EQ(z0, z1)) 25.52/7.07
#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.07
EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.07
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.07
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.07
NUB(z0) → c29(NUB#1(z0)) 25.52/7.07
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.07
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.07
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.07
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2)) 25.52/7.07
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.07
#EQ(::(z0, z1), ::(z2, z3)) → c16(#EQ(z0, z2), #EQ(z1, z3)) 25.52/7.07
AND(z0, z1) → c21 25.52/7.07
EQ#1(nil, z0) → c24
The order we found is given by the following interpretation:
Polynomial interpretation : 25.52/7.07

POL(#0) = [3]    25.52/7.07
POL(#EQ(x1, x2)) = 0    25.52/7.07
POL(#EQUAL(x1, x2)) = 0    25.52/7.07
POL(#and(x1, x2)) = [3]    25.52/7.07
POL(#eq(x1, x2)) = 0    25.52/7.07
POL(#equal(x1, x2)) = 0    25.52/7.07
POL(#false) = 0    25.52/7.07
POL(#neg(x1)) = 0    25.52/7.07
POL(#pos(x1)) = 0    25.52/7.07
POL(#s(x1)) = 0    25.52/7.07
POL(#true) = 0    25.52/7.07
POL(::(x1, x2)) = [1] + x2    25.52/7.07
POL(AND(x1, x2)) = 0    25.52/7.07
POL(EQ(x1, x2)) = 0    25.52/7.07
POL(EQ#1(x1, x2)) = 0    25.52/7.07
POL(EQ#3(x1, x2, x3)) = 0    25.52/7.07
POL(NUB(x1)) = [1] + x12    25.52/7.07
POL(NUB#1(x1)) = x12    25.52/7.07
POL(REMOVE(x1, x2)) = [2]x2    25.52/7.07
POL(REMOVE#1(x1, x2)) = [2]x1    25.52/7.07
POL(REMOVE#2(x1, x2, x3, x4)) = [1] + [2]x4    25.52/7.07
POL(and(x1, x2)) = [3] + [3]x22    25.52/7.07
POL(c13(x1)) = x1    25.52/7.07
POL(c15(x1)) = x1    25.52/7.07
POL(c16(x1, x2)) = x1 + x2    25.52/7.07
POL(c20(x1)) = x1    25.52/7.07
POL(c21) = 0    25.52/7.07
POL(c22(x1)) = x1    25.52/7.07
POL(c23(x1)) = x1    25.52/7.07
POL(c24) = 0    25.52/7.07
POL(c27(x1, x2, x3)) = x1 + x2 + x3    25.52/7.07
POL(c29(x1)) = x1    25.52/7.07
POL(c30(x1, x2)) = x1 + x2    25.52/7.07
POL(c32(x1)) = x1    25.52/7.07
POL(c33(x1, x2)) = x1 + x2    25.52/7.07
POL(c35(x1)) = x1    25.52/7.07
POL(c36(x1)) = x1    25.52/7.07
POL(c9(x1)) = x1    25.52/7.07
POL(eq(x1, x2)) = 0    25.52/7.07
POL(eq#1(x1, x2)) = [3] + [3]x2 + [3]x22    25.52/7.07
POL(eq#2(x1)) = [3]    25.52/7.07
POL(eq#3(x1, x2, x3)) = [3] + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x22    25.52/7.07
POL(nil) = 0    25.52/7.07
POL(remove(x1, x2)) = x2    25.52/7.07
POL(remove#1(x1, x2)) = x1    25.52/7.07
POL(remove#2(x1, x2, x3, x4)) = [1] + x4   
25.52/7.07
25.52/7.07

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.07
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.07
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.07
EQ#1(nil, z0) → c24
K tuples:

NUB(z0) → c29(NUB#1(z0)) 25.52/7.07
NUB#1(::(z0, z1)) → c30(NUB(remove(z0, z1)), REMOVE(z0, z1)) 25.52/7.07
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.07
AND(z0, z1) → c21 25.52/7.07
#EQUAL(z0, z1) → c20(#EQ(z0, z1)) 25.52/7.07
REMOVE#2(#true, z0, z1, z2) → c36(REMOVE(z0, z2)) 25.52/7.07
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) 25.52/7.07
REMOVE#2(#false, z0, z1, z2) → c35(REMOVE(z0, z2))
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, AND

Compound Symbols:

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

25.52/7.07
25.52/7.07

(17) CdtKnowledgeProof (EQUIVALENT transformation)

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

EQ(z0, z1) → c22(EQ#1(z0, z1)) 25.52/7.07
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.07
REMOVE(z0, z1) → c32(REMOVE#1(z1, z0)) 25.52/7.07
EQ#1(nil, z0) → c24 25.52/7.07
EQ#1(::(z0, z1), z2) → c23(EQ#3(z2, z0, z1)) 25.52/7.07
EQ#1(nil, z0) → c24 25.52/7.07
EQ#3(::(z0, z1), z2, z3) → c27(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0), EQ(z3, z1)) 25.52/7.07
REMOVE#1(::(z0, z1), z2) → c33(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0))
Now S is empty
25.52/7.07
25.52/7.07

(18) BOUNDS(O(1), O(1))

25.52/7.07
25.52/7.07
25.89/7.13 EOF