Term Rewriting System R:
[x, y, l, l1, l2, l3]
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)

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

EQ(s(x), s(y)) -> EQ(x, y)
APP(cons(x, l1), l2) -> APP(l1, l2)
APP(app(l1, l2), l3) -> APP(l1, app(l2, l3))
APP(app(l1, l2), l3) -> APP(l2, l3)
MEM(x, cons(y, l)) -> IFMEM(eq(x, y), x, l)
MEM(x, cons(y, l)) -> EQ(x, y)
IFMEM(false, x, l) -> MEM(x, l)
INTER(app(l1, l2), l3) -> APP(inter(l1, l3), inter(l2, l3))
INTER(app(l1, l2), l3) -> INTER(l1, l3)
INTER(app(l1, l2), l3) -> INTER(l2, l3)
INTER(l1, app(l2, l3)) -> APP(inter(l1, l2), inter(l1, l3))
INTER(l1, app(l2, l3)) -> INTER(l1, l2)
INTER(l1, app(l2, l3)) -> INTER(l1, l3)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
INTER(cons(x, l1), l2) -> MEM(x, l2)
INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
INTER(l1, cons(x, l2)) -> MEM(x, l1)
IFINTER(true, x, l1, l2) -> INTER(l1, l2)
IFINTER(false, x, l1, l2) -> INTER(l1, l2)

Furthermore, R contains four SCCs.


   R
DPs
       →DP Problem 1
Argument Filtering and Ordering
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
Remaining


Dependency Pair:

EQ(s(x), s(y)) -> EQ(x, y)


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)


Strategy:

innermost




The following dependency pair can be strictly oriented:

EQ(s(x), s(y)) -> EQ(x, y)


There are no usable rules for innermost that need to be oriented.
Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
trivial

resulting in one new DP problem.
Used Argument Filtering System:
EQ(x1, x2) -> EQ(x1, x2)
s(x1) -> s(x1)


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 5
Dependency Graph
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
Remaining


Dependency Pair:


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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
Argument Filtering and Ordering
       →DP Problem 3
AFS
       →DP Problem 4
Remaining


Dependency Pairs:

APP(app(l1, l2), l3) -> APP(l2, l3)
APP(cons(x, l1), l2) -> APP(l1, l2)


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)


Strategy:

innermost




The following dependency pairs can be strictly oriented:

APP(app(l1, l2), l3) -> APP(l2, l3)
APP(cons(x, l1), l2) -> APP(l1, l2)


There are no usable rules for innermost that need to be oriented.
Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
trivial

resulting in one new DP problem.
Used Argument Filtering System:
APP(x1, x2) -> APP(x1, x2)
app(x1, x2) -> app(x1, x2)
cons(x1, x2) -> cons(x1, x2)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
           →DP Problem 6
Dependency Graph
       →DP Problem 3
AFS
       →DP Problem 4
Remaining


Dependency Pair:


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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Argument Filtering and Ordering
       →DP Problem 4
Remaining


Dependency Pairs:

IFMEM(false, x, l) -> MEM(x, l)
MEM(x, cons(y, l)) -> IFMEM(eq(x, y), x, l)


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)


Strategy:

innermost




The following dependency pair can be strictly oriented:

MEM(x, cons(y, l)) -> IFMEM(eq(x, y), x, l)


The following usable rules for innermost can be oriented:

eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
eq > false
{true, 0}
{IFMEM, MEM}

resulting in one new DP problem.
Used Argument Filtering System:
MEM(x1, x2) -> MEM(x1, x2)
IFMEM(x1, x2, x3) -> IFMEM(x2, x3)
cons(x1, x2) -> cons(x1, x2)
eq(x1, x2) -> eq(x1, x2)
s(x1) -> s(x1)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 7
Dependency Graph
       →DP Problem 4
Remaining


Dependency Pair:

IFMEM(false, x, l) -> MEM(x, l)


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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

IFINTER(false, x, l1, l2) -> INTER(l1, l2)
INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
IFINTER(true, x, l1, l2) -> INTER(l1, l2)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
INTER(l1, app(l2, l3)) -> INTER(l1, l3)
INTER(app(l1, l2), l3) -> INTER(l2, l3)
INTER(l1, app(l2, l3)) -> INTER(l1, l2)
INTER(app(l1, l2), l3) -> INTER(l1, l3)


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)


Strategy:

innermost



Innermost Termination of R could not be shown.
Duration:
0:04 minutes