Termination w.r.t. Q proof of /tmp/tmpr2gaDX/intersect.trs

Termination w.r.t. Q of the given QTRS could not be shown:

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

  ↳5 QDP

  ↳6 QDP

  ↳7 QDP

  ↳8 QDP

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following 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)

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 4 SCCs with 5 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP(app(l1, l2), l3) → APP(l1, app(l2, l3))
APP(cons(x, l1), l2) → APP(l1, l2)
APP(app(l1, l2), l3) → APP(l2, l3)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MEM(x, cons(y, l)) → IFMEM(eq(x, y), x, l)
IFMEM(false, x, l) → MEM(x, l)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INTER(app(l1, l2), l3) → INTER(l2, l3)
INTER(app(l1, l2), l3) → 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)
IFINTER(true, x, l1, l2) → INTER(l1, l2)
INTER(l1, cons(x, l2)) → IFINTER(mem(x, l1), x, l2, l1)
IFINTER(false, x, l1, l2) → INTER(l1, l2)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.