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

0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 16 ms)
↳2 CpxTRS
↳3 RcToIrcProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTRS
↳5 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CdtProblem
↳9 CdtUsableRulesProof (⇔, 0 ms)
↳10 CdtProblem
↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 184 ms)
↳12 CdtProblem
↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 72 ms)
↳14 CdtProblem
↳15 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CdtProblem
↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 190 ms)
↳18 CdtProblem
↳19 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
↳20 CdtProblem
↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 148 ms)
↳22 CdtProblem
↳23 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳24 BOUNDS(1, 1)

(0) Obligation:

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


The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Rewrite Strategy: FULL

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The following defined symbols can occur below the 0th argument of ifinter: ifmem, eq, mem
The following defined symbols can occur below the 0th argument of ifmem: eq

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
app(app(l1, l2), l3) → app(l1, app(l2, l3))
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))

(2) Obligation:

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


The TRS R consists of the following rules:

inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
ifmem(false, x, l) → mem(x, l)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
mem(x, nil) → false
app(cons(x, l1), l2) → cons(x, app(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)
ifmem(true, x, l) → true
eq(0, 0) → true
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
app(nil, l) → l
inter(x, nil) → nil
inter(nil, x) → nil
if(true, x, y) → x
if(false, x, y) → y

Rewrite Strategy: FULL

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

Converted rc-obligation to irc-obligation.

The duplicating contexts are:
inter(cons([], l1), l2)
inter(cons(x, l1), [])
mem([], cons(y, l))
inter(l1, cons([], l2))
inter([], cons(x, l2))

The defined contexts are:
ifinter([], x1, x2, x3)
ifmem([], x1, x2)

[] just represents basic- or constructor-terms in the following defined contexts:
ifmem([], x1, x2)

As the TRS is an overlay system and the defined contexts and the duplicating contexts don't overlap, we have rc = irc.

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

inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
ifmem(false, x, l) → mem(x, l)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
mem(x, nil) → false
app(cons(x, l1), l2) → cons(x, app(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)
ifmem(true, x, l) → true
eq(0, 0) → true
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
app(nil, l) → l
inter(x, nil) → nil
inter(nil, x) → nil
if(true, x, y) → x
if(false, x, y) → y

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(nil, z0) → nil
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
mem(z0, nil) → false
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
eq(0, 0) → true
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(nil, z0) → z0
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
INTER(z0, nil) → c2
INTER(nil, z0) → c3
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
MEM(z0, nil) → c5
EQ(0, s(z0)) → c6
EQ(s(z0), 0) → c7
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
EQ(0, 0) → c9
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFMEM(true, z0, z1) → c11
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
APP(nil, z0) → c15
IF(true, z0, z1) → c16
IF(false, z0, z1) → c17
S tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
INTER(z0, nil) → c2
INTER(nil, z0) → c3
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
MEM(z0, nil) → c5
EQ(0, s(z0)) → c6
EQ(s(z0), 0) → c7
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
EQ(0, 0) → c9
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFMEM(true, z0, z1) → c11
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
APP(nil, z0) → c15
IF(true, z0, z1) → c16
IF(false, z0, z1) → c17
K tuples:none
Defined Rule Symbols:

inter, mem, eq, ifmem, ifinter, app, if

Defined Pair Symbols:

INTER, MEM, EQ, IFMEM, IFINTER, APP, IF

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17

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

Removed 10 trailing nodes:

EQ(0, s(z0)) → c6
INTER(nil, z0) → c3
IF(false, z0, z1) → c17
EQ(s(z0), 0) → c7
INTER(z0, nil) → c2
IF(true, z0, z1) → c16
IFMEM(true, z0, z1) → c11
MEM(z0, nil) → c5
APP(nil, z0) → c15
EQ(0, 0) → c9

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(nil, z0) → nil
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
mem(z0, nil) → false
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
eq(0, 0) → true
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(nil, z0) → z0
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
K tuples:none
Defined Rule Symbols:

inter, mem, eq, ifmem, ifinter, app, if

Defined Pair Symbols:

INTER, MEM, EQ, IFMEM, IFINTER, APP

Compound Symbols:

c, c1, c4, c8, c10, c12, c13, c14

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(z0, nil) → nil
inter(nil, z0) → nil
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(nil, z0) → z0
if(true, z0, z1) → z0
if(false, z0, z1) → z1

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
mem(z0, nil) → false
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
eq(0, 0) → true
Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
K tuples:none
Defined Rule Symbols:

mem, ifmem, eq

Defined Pair Symbols:

INTER, MEM, EQ, IFMEM, IFINTER, APP

Compound Symbols:

c, c1, c4, c8, c10, c12, c13, c14

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

APP(cons(z0, z1), z2) → c14(APP(z1, z2))
We considered the (Usable) Rules:none
And the Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]   
POL(APP(x1, x2)) = x1   
POL(EQ(x1, x2)) = 0   
POL(IFINTER(x1, x2, x3, x4)) = 0   
POL(IFMEM(x1, x2, x3)) = 0   
POL(INTER(x1, x2)) = 0   
POL(MEM(x1, x2)) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c14(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(cons(x1, x2)) = [1] + x2   
POL(eq(x1, x2)) = x1 + x2   
POL(false) = [1]   
POL(ifmem(x1, x2, x3)) = 0   
POL(mem(x1, x2)) = 0   
POL(nil) = 0   
POL(s(x1)) = [1] + x1   
POL(true) = [1]   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
mem(z0, nil) → false
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
eq(0, 0) → true
Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
K tuples:

APP(cons(z0, z1), z2) → c14(APP(z1, z2))
Defined Rule Symbols:

mem, ifmem, eq

Defined Pair Symbols:

INTER, MEM, EQ, IFMEM, IFINTER, APP

Compound Symbols:

c, c1, c4, c8, c10, c12, c13, c14

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

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

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
We considered the (Usable) Rules:none
And the Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]   
POL(APP(x1, x2)) = 0   
POL(EQ(x1, x2)) = 0   
POL(IFINTER(x1, x2, x3, x4)) = [2]x3 + [2]x4   
POL(IFMEM(x1, x2, x3)) = [3]   
POL(INTER(x1, x2)) = [2]x1 + [2]x2   
POL(MEM(x1, x2)) = [3]   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c14(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(cons(x1, x2)) = [2] + x2   
POL(eq(x1, x2)) = [2]x1   
POL(false) = 0   
POL(ifmem(x1, x2, x3)) = 0   
POL(mem(x1, x2)) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(true) = [1]   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
mem(z0, nil) → false
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
eq(0, 0) → true
Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
K tuples:

APP(cons(z0, z1), z2) → c14(APP(z1, z2))
INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
Defined Rule Symbols:

mem, ifmem, eq

Defined Pair Symbols:

INTER, MEM, EQ, IFMEM, IFINTER, APP

Compound Symbols:

c, c1, c4, c8, c10, c12, c13, c14

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

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

IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
mem(z0, nil) → false
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
eq(0, 0) → true
Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
K tuples:

APP(cons(z0, z1), z2) → c14(APP(z1, z2))
INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
Defined Rule Symbols:

mem, ifmem, eq

Defined Pair Symbols:

INTER, MEM, EQ, IFMEM, IFINTER, APP

Compound Symbols:

c, c1, c4, c8, c10, c12, c13, c14

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

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

MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]   
POL(APP(x1, x2)) = [2]x1·x2 + x12   
POL(EQ(x1, x2)) = [1]   
POL(IFINTER(x1, x2, x3, x4)) = [2]x4 + [2]x3·x4   
POL(IFMEM(x1, x2, x3)) = [2]x3   
POL(INTER(x1, x2)) = [2]x1·x2   
POL(MEM(x1, x2)) = [2]x2   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c14(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(cons(x1, x2)) = [2] + x2   
POL(eq(x1, x2)) = [2]x1   
POL(false) = 0   
POL(ifmem(x1, x2, x3)) = [2]x2 + x3 + [2]x32 + x2·x3 + x1·x3 + [2]x12 + x22   
POL(mem(x1, x2)) = [1] + x1·x2 + [2]x12   
POL(nil) = 0   
POL(s(x1)) = [1]   
POL(true) = [1]   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
mem(z0, nil) → false
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
eq(0, 0) → true
Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
K tuples:

APP(cons(z0, z1), z2) → c14(APP(z1, z2))
INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
Defined Rule Symbols:

mem, ifmem, eq

Defined Pair Symbols:

INTER, MEM, EQ, IFMEM, IFINTER, APP

Compound Symbols:

c, c1, c4, c8, c10, c12, c13, c14

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

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

IFMEM(false, z0, z1) → c10(MEM(z0, z1))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
mem(z0, nil) → false
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
eq(0, 0) → true
Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
K tuples:

APP(cons(z0, z1), z2) → c14(APP(z1, z2))
INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
Defined Rule Symbols:

mem, ifmem, eq

Defined Pair Symbols:

INTER, MEM, EQ, IFMEM, IFINTER, APP

Compound Symbols:

c, c1, c4, c8, c10, c12, c13, c14

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

EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]   
POL(APP(x1, x2)) = [2]x1 + [2]x1·x2 + x12   
POL(EQ(x1, x2)) = x1   
POL(IFINTER(x1, x2, x3, x4)) = [2] + [2]x3 + [2]x4 + [2]x3·x4   
POL(IFMEM(x1, x2, x3)) = [1] + [2]x3 + x2·x3   
POL(INTER(x1, x2)) = [2] + [2]x1 + [2]x2 + [2]x1·x2   
POL(MEM(x1, x2)) = [2]x2 + x1·x2   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c14(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(cons(x1, x2)) = [1] + x1 + x2   
POL(eq(x1, x2)) = 0   
POL(false) = 0   
POL(ifmem(x1, x2, x3)) = [1] + x1 + [2]x2 + x3 + x32 + x2·x3 + x1·x3 + [2]x12 + [2]x22   
POL(mem(x1, x2)) = x1 + [2]x1·x2   
POL(nil) = 0   
POL(s(x1)) = [2] + x1   
POL(true) = [1]   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
mem(z0, nil) → false
ifmem(false, z0, z1) → mem(z0, z1)
ifmem(true, z0, z1) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
eq(0, 0) → true
Tuples:

INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
APP(cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:none
K tuples:

APP(cons(z0, z1), z2) → c14(APP(z1, z2))
INTER(cons(z0, z1), z2) → c(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c1(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c12(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c13(INTER(z1, z2))
MEM(z0, cons(z1, z2)) → c4(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c10(MEM(z0, z1))
EQ(s(z0), s(z1)) → c8(EQ(z0, z1))
Defined Rule Symbols:

mem, ifmem, eq

Defined Pair Symbols:

INTER, MEM, EQ, IFMEM, IFINTER, APP

Compound Symbols:

c, c1, c4, c8, c10, c12, c13, c14

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

The set S is empty

(24) BOUNDS(1, 1)