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
         ↳Usable Rules (Innermost)
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules


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




As we are in the innermost case, we can delete all 21 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 5
             ↳Size-Change Principle
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. EQ(s(x), s(y)) -> EQ(x, y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳Usable Rules (Innermost)
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules


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




As we are in the innermost case, we can delete all 21 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 6
             ↳Size-Change Principle
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules


Dependency Pairs:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. APP(app(l1, l2), l3) -> APP(l2, l3)
  2. APP(cons(x, l1), l2) -> APP(l1, l2)
and get the following Size-Change Graph(s):
{1, 2} , {1, 2}
1>1
2=2

which lead(s) to this/these maximal multigraph(s):
{1, 2} , {1, 2}
1>1
2=2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)
app(x1, x2) -> app(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳Usable Rules (Innermost)
       →DP Problem 4
         ↳UsableRules


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




As we are in the innermost case, we can delete all 17 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 7
             ↳Size-Change Principle
       →DP Problem 4
         ↳UsableRules


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




We number the DPs as follows:
  1. IFMEM(false, x, l) -> MEM(x, l)
  2. MEM(x, cons(y, l)) -> IFMEM(eq(x, y), x, l)
and get the following Size-Change Graph(s):
{1} , {1}
2=1
3=2
{2} , {2}
1=2
2>3

which lead(s) to this/these maximal multigraph(s):
{1} , {2}
2=2
3>3
{2} , {1}
1=1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳Usable Rules (Innermost)


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




As we are in the innermost case, we can delete all 13 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
           →DP Problem 8
             ↳Size-Change Principle


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:


eq(0, 0) -> true
eq(s(x), s(y)) -> eq(x, y)
eq(s(x), 0) -> false
eq(0, s(x)) -> false
ifmem(true, x, l) -> true
ifmem(false, x, l) -> mem(x, l)
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)


Strategy:

innermost




We number the DPs as follows:
  1. IFINTER(false, x, l1, l2) -> INTER(l1, l2)
  2. INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
  3. IFINTER(true, x, l1, l2) -> INTER(l1, l2)
  4. INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
  5. INTER(l1, app(l2, l3)) -> INTER(l1, l3)
  6. INTER(app(l1, l2), l3) -> INTER(l2, l3)
  7. INTER(l1, app(l2, l3)) -> INTER(l1, l2)
  8. INTER(app(l1, l2), l3) -> INTER(l1, l3)
and get the following Size-Change Graph(s):
{1, 3} , {1, 3}
3=1
4=2
{2} , {2}
1=4
2>2
2>3
{4} , {4}
1>2
1>3
2=4
{5} , {5}
1=1
2>2
{6} , {6}
1>1
2=2
{7} , {7}
1=1
2>2
{8} , {8}
1>1
2=2

which lead(s) to this/these maximal multigraph(s):
{5} , {5}
1=1
2>2
{6} , {6}
1>1
2=2
{1, 3} , {4}
3>2
3>3
4=4
{8} , {7}
1>1
2>2
{6} , {7}
1>1
2>2
{8} , {5}
1>1
2>2
{7} , {8}
1>1
2>2
{5} , {8}
1>1
2>2
{7} , {6}
1>1
2>2
{5} , {6}
1>1
2>2
{4} , {1, 3}
1>1
2=2
{6} , {5}
1>1
2>2
{7} , {5}
1>1
2>2
{4} , {7}
1>1
2>2
{6} , {1, 3}
1>1
2=2
{5} , {5}
1>1
2>2
{1, 3} , {4}
3>2
3>3
4>4
{7} , {1, 3}
1>1
2>2
{8} , {6}
1>1
2>2
{4} , {5}
1>1
2>2
{6} , {6}
1>1
2>2
{5} , {1, 3}
1>1
2>2
{4} , {6}
1>1
2=2
{8} , {1, 3}
1>1
2>2
{1, 3} , {2}
3>2
3>3
4>4
{6} , {1, 3}
1>1
2>2
{4} , {6}
1>1
2>2
{2} , {1, 3}
1>1
2>2
{2} , {8}
1>1
2>2
{4} , {1, 3}
1>1
2>2
{2} , {5}
1>1
2>2
{2} , {6}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)
app(x1, x2) -> app(x1, x2)

We obtain no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:00 minutes