Consider the TRS R consisting of the rewrite rules

1: if(true,x,y) -> x
2: if(false,x,y) -> y
3: eq(0,0) -> true
4: eq(0,s(x)) -> false
5: eq(s(x),0) -> false
6: eq(s(x),s(y)) -> eq(x,y)
7: app(nil,l) -> l
8: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
9: app(app(l1,l2),l3) -> app(l1,app(l2,l3))
10: mem(x,nil) -> false
11: mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
12: ifmem(true,x,l) -> true
13: ifmem(false,x,l) -> mem(x,l)
14: inter(x,nil) -> nil
15: inter(nil,x) -> nil
16: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
17: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
18: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
19: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
20: ifinter(true,x,l1,l2) -> cons(x,inter(l1,l2))
21: ifinter(false,x,l1,l2) -> inter(l1,l2)

There are 19 dependency pairs:

22: EQ(s(x),s(y)) -> EQ(x,y)
23: APP(cons(x,l1),l2) -> APP(l1,l2)
24: APP(app(l1,l2),l3) -> APP(l1,app(l2,l3))
25: APP(app(l1,l2),l3) -> APP(l2,l3)
26: MEM(x,cons(y,l)) -> IFMEM(eq(x,y),x,l)
27: MEM(x,cons(y,l)) -> EQ(x,y)
28: IFMEM(false,x,l) -> MEM(x,l)
29: INTER(app(l1,l2),l3) -> APP(inter(l1,l3),inter(l2,l3))
30: INTER(app(l1,l2),l3) -> INTER(l1,l3)
31: INTER(app(l1,l2),l3) -> INTER(l2,l3)
32: INTER(l1,app(l2,l3)) -> APP(inter(l1,l2),inter(l1,l3))
33: INTER(l1,app(l2,l3)) -> INTER(l1,l2)
34: INTER(l1,app(l2,l3)) -> INTER(l1,l3)
35: INTER(cons(x,l1),l2) -> IFINTER(mem(x,l2),x,l1,l2)
36: INTER(cons(x,l1),l2) -> MEM(x,l2)
37: INTER(l1,cons(x,l2)) -> IFINTER(mem(x,l1),x,l2,l1)
38: INTER(l1,cons(x,l2)) -> MEM(x,l1)
39: IFINTER(true,x,l1,l2) -> INTER(l1,l2)
40: IFINTER(false,x,l1,l2) -> INTER(l1,l2)

The approximated dependency graph contains 4 SCCs:
{23-25},
{22},
{26,28}
and {30,31,33-35,37,39,40}.

- Consider the SCC {23-25}.
The usable rules are {7-9}.
By taking the polynomial interpretation
[nil] = 1
and [app](x,y) = [APP](x,y) = [cons](x,y) = x + y + 1,
the rules in {8,9,24}
are weakly decreasing and
the rules in {7,23,25}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {24}.
By taking the polynomial interpretation
[nil] = 1,
[APP](x,y) = x + 1
and [app](x,y) = [cons](x,y) = x + y + 1,
the rules in {8,9}
are weakly decreasing and
the rules in {7,24}
are strictly decreasing.


- Consider the SCC {22}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [EQ](x,y) = x + y + 1,
rule 22
is strictly decreasing.

- Consider the SCC {26,28}.
The usable rules are {3-6}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[s](x) = x + 1,
[cons](x,y) = [eq](x,y) = [MEM](x,y) = x + y + 1
and [IFMEM](x,y,z) = y + z + 1,
rule 28
is weakly decreasing and
the rules in {3-6,26}
are strictly decreasing.

- Consider the SCC {30,31,33-35,37,39,40}.
The usable rules are {3-6,10-13}.
By taking the polynomial interpretation
[0] = [false] = [nil] = [true] = 1,
[s](x) = x + 1,
[app](x,y) = [cons](x,y) = [eq](x,y) = [INTER](x,y) = [mem](x,y) = x + y + 1,
[ifmem](x,y,z) = y + z + 1
and [IFINTER](x,y,z,w) = y + z + w + 1,
the rules in {12,13,39,40}
are weakly decreasing and
the rules in {3-6,10,11,30,31,33-35,37}
are strictly decreasing.

Hence the TRS is terminating.