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
         ↳Forward Instantiation Transformation
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Remaining
       →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




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

EQ(s(x), s(y)) -> EQ(x, y)
one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 5
             ↳Forward Instantiation Transformation
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pair:

EQ(s(s(x'')), s(s(y''))) -> EQ(s(x''), s(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




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

EQ(s(s(x'')), s(s(y''))) -> EQ(s(x''), s(y''))
one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 5
             ↳FwdInst
             ...
               →DP Problem 6
                 ↳Argument Filtering and Ordering
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pair:

EQ(s(s(s(x''''))), s(s(s(y'''')))) -> EQ(s(s(x'''')), s(s(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(s(s(x''''))), s(s(s(y'''')))) -> EQ(s(s(x'''')), s(s(y'''')))


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
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
         ↳FwdInst
           →DP Problem 5
             ↳FwdInst
             ...
               →DP Problem 7
                 ↳Dependency Graph
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Remaining
       →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
         ↳FwdInst
       →DP Problem 2
         ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →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




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(cons(x, l1), l2) -> APP(l1, l2)
two new Dependency Pairs are created:

APP(cons(x, cons(x'', l1'')), l2'') -> APP(cons(x'', l1''), l2'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 8
             ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pairs:

APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x'', l1'')), l2'') -> APP(cons(x'', l1''), l2'')
APP(app(l1, l2), l3) -> APP(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)


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(app(l1, l2), l3) -> APP(l2, l3)
three new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 8
             ↳FwdInst
             ...
               →DP Problem 9
                 ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pairs:

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


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




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(cons(x, cons(x'', l1'')), l2'') -> APP(cons(x'', l1''), l2'')
two new Dependency Pairs are created:

APP(cons(x, cons(x'''', cons(x''''', l1''''))), l2'''') -> APP(cons(x'''', cons(x''''', l1'''')), l2'''')
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 8
             ↳FwdInst
             ...
               →DP Problem 10
                 ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pairs:

APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x'''', cons(x''''', l1''''))), l2'''') -> APP(cons(x'''', cons(x''''', l1'''')), l2'''')
APP(app(l1, cons(x'', cons(x'''', l1''''))), l3') -> APP(cons(x'', cons(x'''', l1'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(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)


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(app(l1, cons(x'', cons(x'''', l1''''))), l3') -> APP(cons(x'', cons(x'''', l1'''')), l3')
two new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 8
             ↳FwdInst
             ...
               →DP Problem 11
                 ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pairs:

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


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




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(cons(x, cons(x'''', cons(x''''', l1''''))), l2'''') -> APP(cons(x'''', cons(x''''', l1'''')), l2'''')
two new Dependency Pairs are created:

APP(cons(x, cons(x''''0, cons(x'''''0, cons(x'''''''', l1'''''')))), l2'''''') -> APP(cons(x''''0, cons(x'''''0, cons(x'''''''', l1''''''))), l2'''''')
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 8
             ↳FwdInst
             ...
               →DP Problem 12
                 ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pairs:

APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(cons(x, cons(x''''0, cons(x'''''0, cons(x'''''''', l1'''''')))), l2'''''') -> APP(cons(x''''0, cons(x'''''0, cons(x'''''''', l1''''''))), l2'''''')
APP(app(l1, cons(x''', cons(x''''', cons(x'''''''', l1'''''')))), l3'') -> APP(cons(x''', cons(x''''', cons(x'''''''', l1''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(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)


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(app(l1, cons(x''', cons(x''''', cons(x'''''''', l1'''''')))), l3'') -> APP(cons(x''', cons(x''''', cons(x'''''''', l1''''''))), l3'')
two new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 8
             ↳FwdInst
             ...
               →DP Problem 13
                 ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pairs:

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


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




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(cons(x, cons(x''''0, cons(x'''''0, cons(x'''''''', l1'''''')))), l2'''''') -> APP(cons(x''''0, cons(x'''''0, cons(x'''''''', l1''''''))), l2'''''')
two new Dependency Pairs are created:

APP(cons(x, cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l2'''''''') -> APP(cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l2'''''''')
APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 8
             ↳FwdInst
             ...
               →DP Problem 14
                 ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pairs:

APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)
APP(cons(x, cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l2'''''''') -> APP(cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l2'''''''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l3''')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(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)


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(app(l1, cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l3''')
two new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 8
             ↳FwdInst
             ...
               →DP Problem 15
                 ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pairs:

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


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




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(cons(x, cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l2'''''''') -> APP(cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l2'''''''')
two new Dependency Pairs are created:

APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l2'''''''''')
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''''))))), l2'''''''''')

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 8
             ↳FwdInst
             ...
               →DP Problem 16
                 ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Remaining


Dependency Pairs:

APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''''))))), l2'''''''''')
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l2'''''''''')
APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l3'''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2'''''''')))), l3''')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)
APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(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)


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l3'''')
two new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



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




The following remains to be proven:


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




The following remains to be proven:


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




The following remains to be proven:

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