YES(O(1), O(n^2)) 31.89/8.79 YES(O(1), O(n^2)) 32.19/8.83 32.19/8.83 32.19/8.83
32.19/8.83 32.19/8.830 CpxTRS32.19/8.83
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))32.19/8.83
↳2 CdtProblem32.19/8.83
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))32.19/8.83
↳4 CdtProblem32.19/8.83
↳5 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))32.19/8.83
↳6 CdtProblem32.19/8.83
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))32.19/8.83
↳8 CdtProblem32.19/8.83
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))32.19/8.83
↳10 CdtProblem32.19/8.83
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))32.19/8.83
↳12 CdtProblem32.19/8.83
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))32.19/8.83
↳14 CdtProblem32.19/8.83
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))32.19/8.83
↳16 CdtProblem32.19/8.83
↳17 SIsEmptyProof (BOTH BOUNDS(ID, ID))32.19/8.83
↳18 BOUNDS(O(1), O(1))32.19/8.83
if(true, x, y) → x 32.19/8.83
if(false, x, y) → y 32.19/8.83
eq(0, 0) → true 32.19/8.83
eq(0, s(x)) → false 32.19/8.83
eq(s(x), 0) → false 32.19/8.83
eq(s(x), s(y)) → eq(x, y) 32.19/8.83
app(nil, l) → l 32.19/8.83
app(cons(x, l1), l2) → cons(x, app(l1, l2)) 32.19/8.83
app(app(l1, l2), l3) → app(l1, app(l2, l3)) 32.19/8.83
mem(x, nil) → false 32.19/8.83
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l) 32.19/8.83
ifmem(true, x, l) → true 32.19/8.83
ifmem(false, x, l) → mem(x, l) 32.19/8.83
inter(x, nil) → nil 32.19/8.83
inter(nil, x) → nil 32.19/8.83
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3)) 32.19/8.83
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3)) 32.19/8.83
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2) 32.19/8.83
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1) 32.19/8.83
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2)) 32.19/8.83
ifinter(false, x, l1, l2) → inter(l1, l2)
Tuples:
if(true, z0, z1) → z0 32.19/8.83
if(false, z0, z1) → z1 32.19/8.83
eq(0, 0) → true 32.19/8.83
eq(0, s(z0)) → false 32.19/8.83
eq(s(z0), 0) → false 32.19/8.83
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.83
app(nil, z0) → z0 32.19/8.83
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.83
app(app(z0, z1), z2) → app(z0, app(z1, z2)) 32.19/8.83
mem(z0, nil) → false 32.19/8.83
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.83
ifmem(true, z0, z1) → true 32.19/8.83
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.83
inter(z0, nil) → nil 32.19/8.83
inter(nil, z0) → nil 32.19/8.83
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.83
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.83
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.83
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.83
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.83
ifinter(false, z0, z1, z2) → inter(z1, z2)
S tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.83
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.83
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.83
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.86
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.86
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.86
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.86
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.86
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.86
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.86
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:none
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.86
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.86
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.86
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.86
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.86
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.86
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.86
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.86
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.86
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.86
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
if, eq, app, mem, ifmem, inter, ifinter
EQ, APP, MEM, IFMEM, INTER, IFINTER
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
We considered the (Usable) Rules:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.86
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
And the Tuples:
mem(z0, nil) → false 32.19/8.86
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.86
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.86
ifmem(true, z0, z1) → true 32.19/8.86
eq(0, 0) → true 32.19/8.86
eq(0, s(z0)) → false 32.19/8.86
eq(s(z0), 0) → false 32.19/8.86
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.86
inter(nil, z0) → nil 32.19/8.86
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.86
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.86
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.86
inter(z0, nil) → nil 32.19/8.86
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.86
ifinter(false, z0, z1, z2) → inter(z1, z2) 32.19/8.86
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.86
app(nil, z0) → z0 32.19/8.86
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.86
app(app(z0, z1), z2) → app(z0, app(z1, z2))
The order we found is given by the following interpretation:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.86
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.86
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.86
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.86
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.86
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.86
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.86
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.86
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.86
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.86
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
POL(0) = [3] 32.19/8.86
POL(APP(x1, x2)) = 0 32.19/8.86
POL(EQ(x1, x2)) = [2]x1 32.19/8.86
POL(IFINTER(x1, x2, x3, x4)) = [2]x3·x4 32.19/8.86
POL(IFMEM(x1, x2, x3)) = x3 + [2]x2·x3 32.19/8.86
POL(INTER(x1, x2)) = [2]x1·x2 32.19/8.86
POL(MEM(x1, x2)) = x2 + [2]x1·x2 32.19/8.86
POL(app(x1, x2)) = x1 + x2 32.19/8.86
POL(c10(x1, x2)) = x1 + x2 32.19/8.86
POL(c12(x1)) = x1 32.19/8.86
POL(c15(x1, x2, x3)) = x1 + x2 + x3 32.19/8.86
POL(c16(x1, x2, x3)) = x1 + x2 + x3 32.19/8.86
POL(c17(x1, x2)) = x1 + x2 32.19/8.86
POL(c18(x1, x2)) = x1 + x2 32.19/8.86
POL(c19(x1)) = x1 32.19/8.86
POL(c20(x1)) = x1 32.19/8.86
POL(c5(x1)) = x1 32.19/8.86
POL(c7(x1)) = x1 32.19/8.86
POL(c8(x1, x2)) = x1 + x2 32.19/8.86
POL(cons(x1, x2)) = [2] + x1 + x2 32.19/8.86
POL(eq(x1, x2)) = 0 32.19/8.86
POL(false) = 0 32.19/8.86
POL(ifinter(x1, x2, x3, x4)) = [3] + [3]x2 + [3]x3 + [3]x4 + [3]x42 + [3]x3·x4 + [3]x2·x4 + [3]x32 + [3]x2·x3 + [3]x22 32.19/8.86
POL(ifmem(x1, x2, x3)) = [3] + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x22 32.19/8.86
POL(inter(x1, x2)) = 0 32.19/8.86
POL(mem(x1, x2)) = 0 32.19/8.86
POL(nil) = 0 32.19/8.86
POL(s(x1)) = [1] + x1 32.19/8.86
POL(true) = 0
Tuples:
if(true, z0, z1) → z0 32.19/8.86
if(false, z0, z1) → z1 32.19/8.86
eq(0, 0) → true 32.19/8.86
eq(0, s(z0)) → false 32.19/8.86
eq(s(z0), 0) → false 32.19/8.86
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.86
app(nil, z0) → z0 32.19/8.86
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.86
app(app(z0, z1), z2) → app(z0, app(z1, z2)) 32.19/8.86
mem(z0, nil) → false 32.19/8.86
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.86
ifmem(true, z0, z1) → true 32.19/8.86
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.86
inter(z0, nil) → nil 32.19/8.86
inter(nil, z0) → nil 32.19/8.86
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.86
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.86
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.86
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.86
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.86
ifinter(false, z0, z1, z2) → inter(z1, z2)
S tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.86
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.86
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.86
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.86
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.86
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.86
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.86
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.86
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.86
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.86
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.86
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.86
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.86
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.86
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.86
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.86
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.86
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.86
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
Defined Rule Symbols:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.86
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
if, eq, app, mem, ifmem, inter, ifinter
EQ, APP, MEM, IFMEM, INTER, IFINTER
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.86
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1))
Tuples:
if(true, z0, z1) → z0 32.19/8.86
if(false, z0, z1) → z1 32.19/8.86
eq(0, 0) → true 32.19/8.86
eq(0, s(z0)) → false 32.19/8.86
eq(s(z0), 0) → false 32.19/8.86
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.86
app(nil, z0) → z0 32.19/8.86
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.86
app(app(z0, z1), z2) → app(z0, app(z1, z2)) 32.19/8.86
mem(z0, nil) → false 32.19/8.86
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.86
ifmem(true, z0, z1) → true 32.19/8.86
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.86
inter(z0, nil) → nil 32.19/8.86
inter(nil, z0) → nil 32.19/8.86
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.86
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.86
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.86
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.86
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.86
ifinter(false, z0, z1, z2) → inter(z1, z2)
S tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.86
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.86
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.86
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.86
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.86
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.86
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.86
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.86
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.86
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.86
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.86
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.86
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.86
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.86
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.86
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.86
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.86
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
Defined Rule Symbols:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.86
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.86
IFMEM(false, z0, z1) → c12(MEM(z0, z1))
if, eq, app, mem, ifmem, inter, ifinter
EQ, APP, MEM, IFMEM, INTER, IFINTER
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
We considered the (Usable) Rules:
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.86
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
And the Tuples:
mem(z0, nil) → false 32.19/8.86
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.86
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.86
ifmem(true, z0, z1) → true 32.19/8.86
eq(0, 0) → true 32.19/8.86
eq(0, s(z0)) → false 32.19/8.86
eq(s(z0), 0) → false 32.19/8.86
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.86
inter(nil, z0) → nil 32.19/8.86
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.86
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.86
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.86
inter(z0, nil) → nil 32.19/8.86
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.86
ifinter(false, z0, z1, z2) → inter(z1, z2) 32.19/8.86
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.86
app(nil, z0) → z0 32.19/8.86
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.88
app(app(z0, z1), z2) → app(z0, app(z1, z2))
The order we found is given by the following interpretation:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
POL(0) = [3] 32.19/8.88
POL(APP(x1, x2)) = 0 32.19/8.88
POL(EQ(x1, x2)) = 0 32.19/8.88
POL(IFINTER(x1, x2, x3, x4)) = [2]x4 + [2]x3·x4 32.19/8.88
POL(IFMEM(x1, x2, x3)) = 0 32.19/8.88
POL(INTER(x1, x2)) = [2]x2 + [2]x1·x2 32.19/8.88
POL(MEM(x1, x2)) = 0 32.19/8.88
POL(app(x1, x2)) = [1] + [2]x1 + x2 32.19/8.88
POL(c10(x1, x2)) = x1 + x2 32.19/8.88
POL(c12(x1)) = x1 32.19/8.88
POL(c15(x1, x2, x3)) = x1 + x2 + x3 32.19/8.88
POL(c16(x1, x2, x3)) = x1 + x2 + x3 32.19/8.88
POL(c17(x1, x2)) = x1 + x2 32.19/8.88
POL(c18(x1, x2)) = x1 + x2 32.19/8.88
POL(c19(x1)) = x1 32.19/8.88
POL(c20(x1)) = x1 32.19/8.88
POL(c5(x1)) = x1 32.19/8.88
POL(c7(x1)) = x1 32.19/8.88
POL(c8(x1, x2)) = x1 + x2 32.19/8.88
POL(cons(x1, x2)) = [1] + x2 32.19/8.88
POL(eq(x1, x2)) = 0 32.19/8.88
POL(false) = 0 32.19/8.88
POL(ifinter(x1, x2, x3, x4)) = [3] + [3]x2 + [3]x3 + [3]x4 + [3]x42 + [3]x3·x4 + [3]x2·x4 + [3]x32 + [3]x2·x3 + [3]x22 32.19/8.88
POL(ifmem(x1, x2, x3)) = [3] + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x22 32.19/8.88
POL(inter(x1, x2)) = 0 32.19/8.88
POL(mem(x1, x2)) = 0 32.19/8.88
POL(nil) = 0 32.19/8.88
POL(s(x1)) = 0 32.19/8.88
POL(true) = 0
Tuples:
if(true, z0, z1) → z0 32.19/8.88
if(false, z0, z1) → z1 32.19/8.88
eq(0, 0) → true 32.19/8.88
eq(0, s(z0)) → false 32.19/8.88
eq(s(z0), 0) → false 32.19/8.88
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.88
app(nil, z0) → z0 32.19/8.88
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.88
app(app(z0, z1), z2) → app(z0, app(z1, z2)) 32.19/8.88
mem(z0, nil) → false 32.19/8.88
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.88
ifmem(true, z0, z1) → true 32.19/8.88
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.88
inter(z0, nil) → nil 32.19/8.88
inter(nil, z0) → nil 32.19/8.88
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.88
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.88
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.88
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.88
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.88
ifinter(false, z0, z1, z2) → inter(z1, z2)
S tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
Defined Rule Symbols:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0))
if, eq, app, mem, ifmem, inter, ifinter
EQ, APP, MEM, IFMEM, INTER, IFINTER
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
We considered the (Usable) Rules:
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
And the Tuples:
mem(z0, nil) → false 32.19/8.88
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.88
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.88
ifmem(true, z0, z1) → true 32.19/8.88
eq(0, 0) → true 32.19/8.88
eq(0, s(z0)) → false 32.19/8.88
eq(s(z0), 0) → false 32.19/8.88
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.88
inter(nil, z0) → nil 32.19/8.88
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.88
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.88
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.88
inter(z0, nil) → nil 32.19/8.88
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.88
ifinter(false, z0, z1, z2) → inter(z1, z2) 32.19/8.88
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.88
app(nil, z0) → z0 32.19/8.88
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.88
app(app(z0, z1), z2) → app(z0, app(z1, z2))
The order we found is given by the following interpretation:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
POL(0) = [3] 32.19/8.88
POL(APP(x1, x2)) = 0 32.19/8.88
POL(EQ(x1, x2)) = 0 32.19/8.88
POL(IFINTER(x1, x2, x3, x4)) = x1 + x3·x4 32.19/8.88
POL(IFMEM(x1, x2, x3)) = 0 32.19/8.88
POL(INTER(x1, x2)) = x1·x2 32.19/8.88
POL(MEM(x1, x2)) = 0 32.19/8.88
POL(app(x1, x2)) = [2]x1 + [2]x2 32.19/8.88
POL(c10(x1, x2)) = x1 + x2 32.19/8.88
POL(c12(x1)) = x1 32.19/8.88
POL(c15(x1, x2, x3)) = x1 + x2 + x3 32.19/8.88
POL(c16(x1, x2, x3)) = x1 + x2 + x3 32.19/8.88
POL(c17(x1, x2)) = x1 + x2 32.19/8.88
POL(c18(x1, x2)) = x1 + x2 32.19/8.88
POL(c19(x1)) = x1 32.19/8.88
POL(c20(x1)) = x1 32.19/8.88
POL(c5(x1)) = x1 32.19/8.88
POL(c7(x1)) = x1 32.19/8.88
POL(c8(x1, x2)) = x1 + x2 32.19/8.88
POL(cons(x1, x2)) = [2] + x2 32.19/8.88
POL(eq(x1, x2)) = 0 32.19/8.88
POL(false) = [1] 32.19/8.88
POL(ifinter(x1, x2, x3, x4)) = [3] + [3]x2 + [3]x3 + [3]x4 + [3]x42 + [3]x3·x4 + [3]x2·x4 + [3]x32 + [3]x2·x3 + [3]x22 32.19/8.88
POL(ifmem(x1, x2, x3)) = [2] + [2]x3 32.19/8.88
POL(inter(x1, x2)) = 0 32.19/8.88
POL(mem(x1, x2)) = [2]x2 32.19/8.88
POL(nil) = [1] 32.19/8.88
POL(s(x1)) = 0 32.19/8.88
POL(true) = 0
Tuples:
if(true, z0, z1) → z0 32.19/8.88
if(false, z0, z1) → z1 32.19/8.88
eq(0, 0) → true 32.19/8.88
eq(0, s(z0)) → false 32.19/8.88
eq(s(z0), 0) → false 32.19/8.88
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.88
app(nil, z0) → z0 32.19/8.88
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.88
app(app(z0, z1), z2) → app(z0, app(z1, z2)) 32.19/8.88
mem(z0, nil) → false 32.19/8.88
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.88
ifmem(true, z0, z1) → true 32.19/8.88
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.88
inter(z0, nil) → nil 32.19/8.88
inter(nil, z0) → nil 32.19/8.88
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.88
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.88
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.88
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.88
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.88
ifinter(false, z0, z1, z2) → inter(z1, z2)
S tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
Defined Rule Symbols:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
if, eq, app, mem, ifmem, inter, ifinter
EQ, APP, MEM, IFMEM, INTER, IFINTER
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
We considered the (Usable) Rules:
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
And the Tuples:
mem(z0, nil) → false 32.19/8.88
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.88
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.88
ifmem(true, z0, z1) → true 32.19/8.88
eq(0, 0) → true 32.19/8.88
eq(0, s(z0)) → false 32.19/8.88
eq(s(z0), 0) → false 32.19/8.88
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.88
inter(nil, z0) → nil 32.19/8.88
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.88
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.88
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.88
inter(z0, nil) → nil 32.19/8.88
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.88
ifinter(false, z0, z1, z2) → inter(z1, z2) 32.19/8.88
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.88
app(nil, z0) → z0 32.19/8.88
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.88
app(app(z0, z1), z2) → app(z0, app(z1, z2))
The order we found is given by the following interpretation:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
POL(0) = [3] 32.19/8.88
POL(APP(x1, x2)) = 0 32.19/8.88
POL(EQ(x1, x2)) = 0 32.19/8.88
POL(IFINTER(x1, x2, x3, x4)) = [1] + [2]x3 + [2]x4 + x3·x4 32.19/8.88
POL(IFMEM(x1, x2, x3)) = [1] + [2]x2 + x2·x3 32.19/8.88
POL(INTER(x1, x2)) = [2]x1 + [2]x2 + x1·x2 32.19/8.88
POL(MEM(x1, x2)) = [1] + [2]x1 + x1·x2 32.19/8.88
POL(app(x1, x2)) = [2] + x1 + x2 + x12 32.19/8.88
POL(c10(x1, x2)) = x1 + x2 32.19/8.88
POL(c12(x1)) = x1 32.19/8.88
POL(c15(x1, x2, x3)) = x1 + x2 + x3 32.19/8.88
POL(c16(x1, x2, x3)) = x1 + x2 + x3 32.19/8.88
POL(c17(x1, x2)) = x1 + x2 32.19/8.88
POL(c18(x1, x2)) = x1 + x2 32.19/8.88
POL(c19(x1)) = x1 32.19/8.88
POL(c20(x1)) = x1 32.19/8.88
POL(c5(x1)) = x1 32.19/8.88
POL(c7(x1)) = x1 32.19/8.88
POL(c8(x1, x2)) = x1 + x2 32.19/8.88
POL(cons(x1, x2)) = [2] + x1 + x2 32.19/8.88
POL(eq(x1, x2)) = 0 32.19/8.88
POL(false) = 0 32.19/8.88
POL(ifinter(x1, x2, x3, x4)) = [3] + [3]x2 + [3]x3 + [3]x4 + [3]x42 + [3]x3·x4 + [3]x2·x4 + [3]x32 + [3]x2·x3 + [3]x22 32.19/8.88
POL(ifmem(x1, x2, x3)) = [3] + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x22 32.19/8.88
POL(inter(x1, x2)) = 0 32.19/8.88
POL(mem(x1, x2)) = 0 32.19/8.88
POL(nil) = 0 32.19/8.88
POL(s(x1)) = 0 32.19/8.88
POL(true) = 0
Tuples:
if(true, z0, z1) → z0 32.19/8.88
if(false, z0, z1) → z1 32.19/8.88
eq(0, 0) → true 32.19/8.88
eq(0, s(z0)) → false 32.19/8.88
eq(s(z0), 0) → false 32.19/8.88
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.88
app(nil, z0) → z0 32.19/8.88
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.88
app(app(z0, z1), z2) → app(z0, app(z1, z2)) 32.19/8.88
mem(z0, nil) → false 32.19/8.88
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.88
ifmem(true, z0, z1) → true 32.19/8.88
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.88
inter(z0, nil) → nil 32.19/8.88
inter(nil, z0) → nil 32.19/8.88
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.88
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.88
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.88
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.88
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.88
ifinter(false, z0, z1, z2) → inter(z1, z2)
S tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
Defined Rule Symbols:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2))
if, eq, app, mem, ifmem, inter, ifinter
EQ, APP, MEM, IFMEM, INTER, IFINTER
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
We considered the (Usable) Rules:
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
And the Tuples:
mem(z0, nil) → false 32.19/8.88
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.88
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.88
ifmem(true, z0, z1) → true 32.19/8.88
eq(0, 0) → true 32.19/8.88
eq(0, s(z0)) → false 32.19/8.88
eq(s(z0), 0) → false 32.19/8.88
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.88
inter(nil, z0) → nil 32.19/8.88
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.88
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.88
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.88
inter(z0, nil) → nil 32.19/8.88
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.88
ifinter(false, z0, z1, z2) → inter(z1, z2) 32.19/8.88
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.88
app(nil, z0) → z0 32.19/8.88
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.88
app(app(z0, z1), z2) → app(z0, app(z1, z2))
The order we found is given by the following interpretation:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
POL(0) = [3] 32.19/8.88
POL(APP(x1, x2)) = [2]x1 32.19/8.88
POL(EQ(x1, x2)) = 0 32.19/8.88
POL(IFINTER(x1, x2, x3, x4)) = x3 + x4 + [3]x3·x4 32.19/8.88
POL(IFMEM(x1, x2, x3)) = 0 32.19/8.88
POL(INTER(x1, x2)) = x1 + x2 + [3]x1·x2 32.19/8.88
POL(MEM(x1, x2)) = 0 32.19/8.88
POL(app(x1, x2)) = [1] + [3]x1 + x2 32.19/8.88
POL(c10(x1, x2)) = x1 + x2 32.19/8.88
POL(c12(x1)) = x1 32.19/8.88
POL(c15(x1, x2, x3)) = x1 + x2 + x3 32.19/8.88
POL(c16(x1, x2, x3)) = x1 + x2 + x3 32.19/8.88
POL(c17(x1, x2)) = x1 + x2 32.19/8.88
POL(c18(x1, x2)) = x1 + x2 32.19/8.88
POL(c19(x1)) = x1 32.19/8.88
POL(c20(x1)) = x1 32.19/8.88
POL(c5(x1)) = x1 32.19/8.88
POL(c7(x1)) = x1 32.19/8.88
POL(c8(x1, x2)) = x1 + x2 32.19/8.88
POL(cons(x1, x2)) = x2 32.19/8.88
POL(eq(x1, x2)) = 0 32.19/8.88
POL(false) = 0 32.19/8.88
POL(ifinter(x1, x2, x3, x4)) = x3 + x4 + [3]x3·x4 32.19/8.88
POL(ifmem(x1, x2, x3)) = [3] + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x22 32.19/8.88
POL(inter(x1, x2)) = x1 + x2 + [3]x1·x2 32.19/8.88
POL(mem(x1, x2)) = 0 32.19/8.88
POL(nil) = 0 32.19/8.88
POL(s(x1)) = 0 32.19/8.88
POL(true) = 0
Tuples:
if(true, z0, z1) → z0 32.19/8.88
if(false, z0, z1) → z1 32.19/8.88
eq(0, 0) → true 32.19/8.88
eq(0, s(z0)) → false 32.19/8.88
eq(s(z0), 0) → false 32.19/8.88
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.88
app(nil, z0) → z0 32.19/8.88
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.88
app(app(z0, z1), z2) → app(z0, app(z1, z2)) 32.19/8.88
mem(z0, nil) → false 32.19/8.88
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.88
ifmem(true, z0, z1) → true 32.19/8.88
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.88
inter(z0, nil) → nil 32.19/8.88
inter(nil, z0) → nil 32.19/8.88
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.88
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.88
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.88
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.88
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.88
ifinter(false, z0, z1, z2) → inter(z1, z2)
S tuples:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
K tuples:
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
Defined Rule Symbols:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.88
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.88
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.88
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.88
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.88
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2)) 32.19/8.88
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.88
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.88
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.88
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2))
if, eq, app, mem, ifmem, inter, ifinter
EQ, APP, MEM, IFMEM, INTER, IFINTER
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20
We considered the (Usable) Rules:
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
And the Tuples:
mem(z0, nil) → false 32.19/8.89
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.89
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.89
ifmem(true, z0, z1) → true 32.19/8.89
eq(0, 0) → true 32.19/8.89
eq(0, s(z0)) → false 32.19/8.89
eq(s(z0), 0) → false 32.19/8.89
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.89
inter(nil, z0) → nil 32.19/8.89
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.89
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.89
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.89
inter(z0, nil) → nil 32.19/8.89
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.89
ifinter(false, z0, z1, z2) → inter(z1, z2) 32.19/8.89
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.89
app(nil, z0) → z0 32.19/8.89
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.89
app(app(z0, z1), z2) → app(z0, app(z1, z2))
The order we found is given by the following interpretation:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.89
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.89
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.89
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.89
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.89
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.89
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.89
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.89
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.89
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.89
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
POL(0) = [3] 32.19/8.89
POL(APP(x1, x2)) = x1 32.19/8.89
POL(EQ(x1, x2)) = 0 32.19/8.89
POL(IFINTER(x1, x2, x3, x4)) = [1] + x3 + x4 + x3·x4 32.19/8.89
POL(IFMEM(x1, x2, x3)) = x2 + x2·x3 32.19/8.89
POL(INTER(x1, x2)) = x1 + x2 + x1·x2 32.19/8.89
POL(MEM(x1, x2)) = x1 + x1·x2 32.19/8.89
POL(app(x1, x2)) = [2] + [2]x1 + x2 32.19/8.89
POL(c10(x1, x2)) = x1 + x2 32.19/8.89
POL(c12(x1)) = x1 32.19/8.89
POL(c15(x1, x2, x3)) = x1 + x2 + x3 32.19/8.89
POL(c16(x1, x2, x3)) = x1 + x2 + x3 32.19/8.89
POL(c17(x1, x2)) = x1 + x2 32.19/8.89
POL(c18(x1, x2)) = x1 + x2 32.19/8.89
POL(c19(x1)) = x1 32.19/8.89
POL(c20(x1)) = x1 32.19/8.89
POL(c5(x1)) = x1 32.19/8.89
POL(c7(x1)) = x1 32.19/8.89
POL(c8(x1, x2)) = x1 + x2 32.19/8.89
POL(cons(x1, x2)) = [1] + x1 + x2 32.19/8.89
POL(eq(x1, x2)) = 0 32.19/8.89
POL(false) = 0 32.19/8.89
POL(ifinter(x1, x2, x3, x4)) = [1] + x2 + x3 + x4 + x3·x4 32.19/8.89
POL(ifmem(x1, x2, x3)) = [3] + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x22 32.19/8.89
POL(inter(x1, x2)) = x1 + x2 + x1·x2 32.19/8.89
POL(mem(x1, x2)) = 0 32.19/8.89
POL(nil) = 0 32.19/8.89
POL(s(x1)) = 0 32.19/8.89
POL(true) = 0
Tuples:
if(true, z0, z1) → z0 32.19/8.89
if(false, z0, z1) → z1 32.19/8.89
eq(0, 0) → true 32.19/8.89
eq(0, s(z0)) → false 32.19/8.89
eq(s(z0), 0) → false 32.19/8.89
eq(s(z0), s(z1)) → eq(z0, z1) 32.19/8.89
app(nil, z0) → z0 32.19/8.89
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 32.19/8.89
app(app(z0, z1), z2) → app(z0, app(z1, z2)) 32.19/8.89
mem(z0, nil) → false 32.19/8.89
mem(z0, cons(z1, z2)) → ifmem(eq(z0, z1), z0, z2) 32.19/8.89
ifmem(true, z0, z1) → true 32.19/8.89
ifmem(false, z0, z1) → mem(z0, z1) 32.19/8.89
inter(z0, nil) → nil 32.19/8.89
inter(nil, z0) → nil 32.19/8.89
inter(app(z0, z1), z2) → app(inter(z0, z2), inter(z1, z2)) 32.19/8.89
inter(z0, app(z1, z2)) → app(inter(z0, z1), inter(z0, z2)) 32.19/8.89
inter(cons(z0, z1), z2) → ifinter(mem(z0, z2), z0, z1, z2) 32.19/8.89
inter(z0, cons(z1, z2)) → ifinter(mem(z1, z0), z1, z2, z0) 32.19/8.89
ifinter(true, z0, z1, z2) → cons(z0, inter(z1, z2)) 32.19/8.89
ifinter(false, z0, z1, z2) → inter(z1, z2)
S tuples:none
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.89
APP(cons(z0, z1), z2) → c7(APP(z1, z2)) 32.19/8.89
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.89
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.89
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.89
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.89
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.89
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.89
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.89
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.89
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2))
Defined Rule Symbols:
EQ(s(z0), s(z1)) → c5(EQ(z0, z1)) 32.19/8.89
MEM(z0, cons(z1, z2)) → c10(IFMEM(eq(z0, z1), z0, z2), EQ(z0, z1)) 32.19/8.89
IFMEM(false, z0, z1) → c12(MEM(z0, z1)) 32.19/8.89
INTER(z0, app(z1, z2)) → c16(APP(inter(z0, z1), inter(z0, z2)), INTER(z0, z1), INTER(z0, z2)) 32.19/8.89
INTER(z0, cons(z1, z2)) → c18(IFINTER(mem(z1, z0), z1, z2, z0), MEM(z1, z0)) 32.19/8.89
IFINTER(false, z0, z1, z2) → c20(INTER(z1, z2)) 32.19/8.89
INTER(app(z0, z1), z2) → c15(APP(inter(z0, z2), inter(z1, z2)), INTER(z0, z2), INTER(z1, z2)) 32.19/8.89
INTER(cons(z0, z1), z2) → c17(IFINTER(mem(z0, z2), z0, z1, z2), MEM(z0, z2)) 32.19/8.89
IFINTER(true, z0, z1, z2) → c19(INTER(z1, z2)) 32.19/8.89
APP(app(z0, z1), z2) → c8(APP(z0, app(z1, z2)), APP(z1, z2)) 32.19/8.89
APP(cons(z0, z1), z2) → c7(APP(z1, z2))
if, eq, app, mem, ifmem, inter, ifinter
EQ, APP, MEM, IFMEM, INTER, IFINTER
c5, c7, c8, c10, c12, c15, c16, c17, c18, c19, c20