(0) Obligation:
Runtime Complexity TRS:
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: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
Tuples:
IF(true, z0, z1) → c
IF(false, z0, z1) → c1
EQ(0, 0) → c2
EQ(0, s(z0)) → c3
EQ(s(z0), 0) → c4
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(nil, z0) → c6
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, nil) → c9
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(true, z0, z1) → c11
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, nil) → c13
INTER(nil, z0) → c14
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:
IF(true, z0, z1) → c
IF(false, z0, z1) → c1
EQ(0, 0) → c2
EQ(0, s(z0)) → c3
EQ(s(z0), 0) → c4
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(nil, z0) → c6
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, nil) → c9
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(true, z0, z1) → c11
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(z0, nil) → c13
INTER(nil, z0) → c14
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:none
Defined Rule Symbols:
if, eq, app, mem, ifmem, inter, ifinter
Defined Pair Symbols:
IF, EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 10 trailing nodes:
IFMEM(true, z0, z1) → c11
IF(true, z0, z1) → c
INTER(nil, z0) → c14
IF(false, z0, z1) → c1
EQ(0, 0) → c2
EQ(0, s(z0)) → c3
EQ(s(z0), 0) → c4
MEM(z0, nil) → c9
APP(nil, z0) → c6
INTER(z0, nil) → c13
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, nil) → nil
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:none
Defined Rule Symbols:
if, eq, app, mem, ifmem, inter, ifinter
Defined Pair Symbols:
EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
(5) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
if(true, z0, z1) → z0
if(false, z0, z1) → z1
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:none
Defined Rule Symbols:
app, eq, inter, ifinter, mem, ifmem
Defined Pair Symbols:
EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
(7) CdtRuleRemovalProof (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(s(z0), s(z1)) → c5(EQ(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(APP(x1, x2)) = 0
POL(EQ(x1, x2)) = x1·x2
POL(IFINTER(x1, x2, x3, x4)) = x3·x4
POL(IFMEM(x1, x2, x3)) = x2·x3
POL(INTER(x1, x2)) = x1·x2
POL(MEM(x1, x2)) = x1·x2
POL(app(x1, x2)) = [2] + [2]x1 + [2]x2
POL(c10(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c15(x1, x2, x3)) = x1 + x2 + x3
POL(c16(x1, x2, x3)) = x1 + x2 + x3
POL(c17(x1, x2)) = x1 + x2
POL(c18(x1, x2)) = x1 + x2
POL(c19(x1)) = x1
POL(c20(x1)) = x1
POL(c5(x1)) = x1
POL(c7(x1)) = x1
POL(c8(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = x1 + x2
POL(eq(x1, x2)) = 0
POL(false) = 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(nil) = 0
POL(s(x1)) = [2] + x1
POL(true) = 0
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
Defined Rule Symbols:
app, eq, inter, ifinter, mem, ifmem
Defined Pair Symbols:
EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
(9) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
We considered the (Usable) Rules:none
And the Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(APP(x1, x2)) = 0
POL(EQ(x1, x2)) = 0
POL(IFINTER(x1, x2, x3, x4)) = [2]x3 + [2]x4 + [2]x3·x4
POL(IFMEM(x1, x2, x3)) = [3] + x2 + [2]x2·x3
POL(INTER(x1, x2)) = [2]x1 + [2]x2 + [2]x1·x2
POL(MEM(x1, x2)) = [3] + [2]x1·x2
POL(app(x1, x2)) = [1] + [2]x1 + x2
POL(c10(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c15(x1, x2, x3)) = x1 + x2 + x3
POL(c16(x1, x2, x3)) = x1 + x2 + x3
POL(c17(x1, x2)) = x1 + x2
POL(c18(x1, x2)) = x1 + x2
POL(c19(x1)) = x1
POL(c20(x1)) = x1
POL(c5(x1)) = x1
POL(c7(x1)) = x1
POL(c8(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = [2] + x1 + x2
POL(eq(x1, x2)) = 0
POL(false) = 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(nil) = 0
POL(s(x1)) = 0
POL(true) = 0
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
Defined Rule Symbols:
app, eq, inter, ifinter, mem, ifmem
Defined Pair Symbols:
EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
(11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)
The following tuples could be moved from S to K by knowledge propagation:
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
K tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
Defined Rule Symbols:
app, eq, inter, ifinter, mem, ifmem
Defined Pair Symbols:
EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
(13) CdtRuleRemovalProof (UPPER BOUND (ADD(O(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)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(APP(x1, x2)) = 0
POL(EQ(x1, x2)) = [3]
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(app(x1, x2)) = [2]x1 + [2]x2
POL(c10(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c15(x1, x2, x3)) = x1 + x2 + x3
POL(c16(x1, x2, x3)) = x1 + x2 + x3
POL(c17(x1, x2)) = x1 + x2
POL(c18(x1, x2)) = x1 + x2
POL(c19(x1)) = x1
POL(c20(x1)) = x1
POL(c5(x1)) = x1
POL(c7(x1)) = x1
POL(c8(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = [2] + x2
POL(eq(x1, x2)) = 0
POL(false) = [2]
POL(ifinter(x1, x2, x3, x4)) = 0
POL(ifmem(x1, x2, x3)) = x3 + [3]x32 + x1·x3
POL(inter(x1, x2)) = 0
POL(mem(x1, x2)) = [3]x22
POL(nil) = [1]
POL(s(x1)) = 0
POL(true) = 0
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
K tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
Defined Rule Symbols:
app, eq, inter, ifinter, mem, ifmem
Defined Pair Symbols:
EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
(15) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)
The following tuples could be moved from S to K by knowledge propagation:
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
K tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
Defined Rule Symbols:
app, eq, inter, ifinter, mem, ifmem
Defined Pair Symbols:
EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
(17) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
We considered the (Usable) Rules:
inter(z0, nil) → nil
inter(nil, z0) → nil
eq(0, 0) → true
ifmem(true, z0, z1) → true
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
eq(s(z0), s(z1)) → eq(z0, z1)
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
mem(z0, nil) → false
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
app(nil, z0) → z0
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(false, z0, z1) → mem(z0, z1)
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
eq(0, s(z0)) → false
eq(s(z0), 0) → false
ifinter(false, z0, z1, z2) → inter(z1, z2)
And the Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(APP(x1, x2)) = [2]x1
POL(EQ(x1, x2)) = 0
POL(IFINTER(x1, x2, x3, x4)) = [2]x1 + [3]x3·x4
POL(IFMEM(x1, x2, x3)) = 0
POL(INTER(x1, x2)) = [3]x1·x2
POL(MEM(x1, x2)) = 0
POL(app(x1, x2)) = [3]x1 + x2
POL(c10(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c15(x1, x2, x3)) = x1 + x2 + x3
POL(c16(x1, x2, x3)) = x1 + x2 + x3
POL(c17(x1, x2)) = x1 + x2
POL(c18(x1, x2)) = x1 + x2
POL(c19(x1)) = x1
POL(c20(x1)) = x1
POL(c5(x1)) = x1
POL(c7(x1)) = x1
POL(c8(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = [2] + x2
POL(eq(x1, x2)) = [1]
POL(false) = 0
POL(ifinter(x1, x2, x3, x4)) = [2]x1 + [3]x3·x4
POL(ifmem(x1, x2, x3)) = [3] + [2]x3 + x12
POL(inter(x1, x2)) = [3]x1·x2
POL(mem(x1, x2)) = [2]x2
POL(nil) = 0
POL(s(x1)) = 0
POL(true) = [1]
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
K tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
Defined Rule Symbols:
app, eq, inter, ifinter, mem, ifmem
Defined Pair Symbols:
EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
(19) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
We considered the (Usable) Rules:
inter(nil, z0) → nil
inter(z0, nil) → nil
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
app(nil, z0) → z0
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
And the Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(APP(x1, x2)) = x1
POL(EQ(x1, x2)) = 0
POL(IFINTER(x1, x2, x3, x4)) = [2]x3 + [2]x4 + [3]x3·x4
POL(IFMEM(x1, x2, x3)) = 0
POL(INTER(x1, x2)) = [2]x1 + [2]x2 + [3]x1·x2
POL(MEM(x1, x2)) = 0
POL(app(x1, x2)) = [1] + [2]x1 + x2
POL(c10(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c15(x1, x2, x3)) = x1 + x2 + x3
POL(c16(x1, x2, x3)) = x1 + x2 + x3
POL(c17(x1, x2)) = x1 + x2
POL(c18(x1, x2)) = x1 + x2
POL(c19(x1)) = x1
POL(c20(x1)) = x1
POL(c5(x1)) = x1
POL(c7(x1)) = x1
POL(c8(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = x2
POL(eq(x1, x2)) = 0
POL(false) = 0
POL(ifinter(x1, x2, x3, x4)) = x3 + x4 + [2]x3·x4
POL(ifmem(x1, x2, x3)) = 0
POL(inter(x1, x2)) = x1 + x2 + [2]x1·x2
POL(mem(x1, x2)) = 0
POL(nil) = 0
POL(s(x1)) = 0
POL(true) = 0
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(nil, z0) → z0
app(cons(z0, z1), z2) → cons(z0, app(z1, z2))
app(app(z0, z1), z2) → app(z0, app(z1, z2))
eq(0, 0) → true
eq(0, s(z0)) → false
eq(s(z0), 0) → false
eq(s(z0), s(z1)) → eq(z0, z1)
inter(z0, nil) → nil
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2))
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0)
inter(nil, z0) → nil
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2))
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2)
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2))
ifinter(false, z0, z1, z2) → inter(z1, z2)
mem(z0, nil) → false
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2)
ifmem(true, z0, z1) → true
ifmem(false, z0, z1) → mem(z0, z1)
Tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
S tuples:none
K tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1))
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2))
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2))
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2))
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
Defined Rule Symbols:
app, eq, inter, ifinter, mem, ifmem
Defined Pair Symbols:
EQ, APP, MEM, IFMEM, INTER, IFINTER
Compound Symbols:
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
(21) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(22) BOUNDS(O(1), O(1))