YES
(VAR x y l l1 l2 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)
)

Proving termination of rewriting for intersect:

-> Dependency pairs:
nF_eq(s(x),s(y)) -> nF_eq(x,y)
nF_app(cons(x,l1),l2) -> nF_app(l1,l2)
nF_app(app(l1,l2),l3) -> nF_app(l1,app(l2,l3))
nF_app(app(l1,l2),l3) -> nF_app(l2,l3)
nF_mem(x,cons(y,l)) -> nF_ifmem(eq(x,y),x,l)
nF_mem(x,cons(y,l)) -> nF_eq(x,y)
nF_ifmem(false,x,l) -> nF_mem(x,l)
nF_inter(app(l1,l2),l3) -> nF_app(inter(l1,l3),inter(l2,l3))
nF_inter(app(l1,l2),l3) -> nF_inter(l1,l3)
nF_inter(app(l1,l2),l3) -> nF_inter(l2,l3)
nF_inter(l1,app(l2,l3)) -> nF_app(inter(l1,l2),inter(l1,l3))
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2)
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3)
nF_inter(cons(x,l1),l2) -> nF_ifinter(mem(x,l2),x,l1,l2)
nF_inter(cons(x,l1),l2) -> nF_mem(x,l2)
nF_inter(l1,cons(x,l2)) -> nF_ifinter(mem(x,l1),x,l2,l1)
nF_inter(l1,cons(x,l2)) -> nF_mem(x,l1)
nF_ifinter(true,x,l1,l2) -> nF_inter(l1,l2)
nF_ifinter(false,x,l1,l2) -> nF_inter(l1,l2)

-> Proof of termination for intersect_1_1:
-> -> Dependency pairs in cycle:
nF_inter(app(l1,l2),l3) -> nF_inter(l1,l3)
nF_ifinter(false,x,l1,l2) -> nF_inter(l1,l2)
nF_inter(l1,cons(x,l2)) -> nF_ifinter(mem(x,l1),x,l2,l1)
nF_ifinter(true,x,l1,l2) -> nF_inter(l1,l2)
nF_inter(cons(x,l1),l2) -> nF_ifinter(mem(x,l2),x,l1,l2)
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3)
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2)
nF_inter(app(l1,l2),l3) -> nF_inter(l2,l3)

UsableRules:
eq(0,0) -> true
eq(0,s(x)) -> false
eq(s(x),0) -> false
eq(s(x),s(y)) -> eq(x,y)
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)

Polynomial Interpretation:

[if](X1,X2,X3) = 0
[true] = 0
[false] = 1
[eq](X1,X2) = X2
[0] = 1
[s](X) = X + 1
[app](X1,X2) = X1 + X2 + 1
[nil] = 0
[cons](X1,X2) = X1 + X2
[mem](X1,X2) = X2 + 1
[ifmem](X1,X2,X3) = X1 + X3
[inter](X1,X2) = 0
[ifinter](X1,X2,X3,X4) = 0
[nF_inter](X1,X2) = X1 + X2
[nF_ifinter](X1,X2,X3,X4) = X3 + X4

TIME: 4.7837e-2

-> -> Dependency pairs in cycle:
nF_inter(app(l1,l2),l3) -> nF_inter(l1,l3)
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2)
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3)
nF_ifinter(true,x,l1,l2) -> nF_inter(l1,l2)
nF_inter(cons(x,l1),l2) -> nF_ifinter(mem(x,l2),x,l1,l2)
nF_ifinter(false,x,l1,l2) -> nF_inter(l1,l2)
nF_inter(l1,cons(x,l2)) -> nF_ifinter(mem(x,l1),x,l2,l1)

UsableRules:
eq(0,0) -> true
eq(0,s(x)) -> false
eq(s(x),0) -> false
eq(s(x),s(y)) -> eq(x,y)
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)

Polynomial Interpretation:

[if](X1,X2,X3) = 0
[true] = 0
[false] = 0
[eq](X1,X2) = 0
[0] = 0
[s](X) = 0
[app](X1,X2) = X1 + X2
[nil] = 1
[cons](X1,X2) = X2 + 1
[mem](X1,X2) = X2
[ifmem](X1,X2,X3) = X3
[inter](X1,X2) = 0
[ifinter](X1,X2,X3,X4) = 0
[nF_inter](X1,X2) = X1 + X2
[nF_ifinter](X1,X2,X3,X4) = X3 + X4

TIME: 4.7455e-2

-> -> Dependency pairs in cycle:
nF_inter(app(l1,l2),l3) -> nF_inter(l1,l3)
nF_ifinter(false,x,l1,l2) -> nF_inter(l1,l2)
nF_inter(cons(x,l1),l2) -> nF_ifinter(mem(x,l2),x,l1,l2)
nF_ifinter(true,x,l1,l2) -> nF_inter(l1,l2)
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3)
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2)
nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for intersect_1_2:
-> -> Dependency pairs in cycle:
nF_mem(x,cons(y,l)) -> nF_ifmem(eq(x,y),x,l)
nF_ifmem(false,x,l) -> nF_mem(x,l)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for intersect_1_3:
-> -> Dependency pairs in cycle:
nF_app(cons(x,l1),l2) -> nF_app(l1,l2)
nF_app(app(l1,l2),l3) -> nF_app(l2,l3)
nF_app(app(l1,l2),l3) -> nF_app(l1,app(l2,l3))

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for intersect_1_4:
-> -> Dependency pairs in cycle:
nF_eq(s(x),s(y)) -> nF_eq(x,y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.