Termination Proof using AProVE

Term Rewriting System R:
[x, n, h, t, m, pid, store]
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)
SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)
LEQ(s(n), s(m)) -> LEQ(n, m)
LENGTH(cons(h, t)) -> LENGTH(t)
APP(cons(h, t), x) -> APP(t, x)
MAP_F(pid, cons(h, t)) -> APP(f(pid, h), map_f(pid, t))
MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
PROCESS(store, m) -> LEQ(m, length(store))
PROCESS(store, m) -> LENGTH(store)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
IF1(store, m, true) -> EMPTY(fstsplit(m, store))
IF1(store, m, true) -> FSTSPLIT(m, store)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF1(store, m, false) -> EMPTY(fstsplit(m, app(map_f(self, nil), store)))
IF1(store, m, false) -> FSTSPLIT(m, app(map_f(self, nil), store))
IF1(store, m, false) -> APP(map_f(self, nil), store)
IF1(store, m, false) -> MAP_F(self, nil)
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF2(store, m, false) -> APP(map_f(self, nil), sndsplit(m, store))
IF2(store, m, false) -> MAP_F(self, nil)
IF2(store, m, false) -> SNDSPLIT(m, store)
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF3(store, m, false) -> SNDSPLIT(m, app(map_f(self, nil), store))
IF3(store, m, false) -> APP(map_f(self, nil), store)
IF3(store, m, false) -> MAP_F(self, nil)

Furthermore, R contains seven SCCs.

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

       →DP Problem 7

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LEQ(s(n), s(m)) -> LEQ(n, m)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LENGTH(cons(h, t)) -> LENGTH(t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
APP(cons(h, t), x) -> APP(t, x)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pairs:
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

       →DP Problem 7

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LEQ(s(n), s(m)) -> LEQ(n, m)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LENGTH(cons(h, t)) -> LENGTH(t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
APP(cons(h, t), x) -> APP(t, x)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pairs:
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

       →DP Problem 7

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LEQ(s(n), s(m)) -> LEQ(n, m)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LENGTH(cons(h, t)) -> LENGTH(t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
APP(cons(h, t), x) -> APP(t, x)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pairs:
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

       →DP Problem 7

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LEQ(s(n), s(m)) -> LEQ(n, m)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LENGTH(cons(h, t)) -> LENGTH(t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
APP(cons(h, t), x) -> APP(t, x)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pairs:
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

       →DP Problem 7

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LEQ(s(n), s(m)) -> LEQ(n, m)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LENGTH(cons(h, t)) -> LENGTH(t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
APP(cons(h, t), x) -> APP(t, x)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pairs:
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

       →DP Problem 7

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LEQ(s(n), s(m)) -> LEQ(n, m)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LENGTH(cons(h, t)) -> LENGTH(t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
APP(cons(h, t), x) -> APP(t, x)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pairs:
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

       →DP Problem 7

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LEQ(s(n), s(m)) -> LEQ(n, m)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
LENGTH(cons(h, t)) -> LENGTH(t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
APP(cons(h, t), x) -> APP(t, x)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pair:
MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
Dependency Pairs:
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))

Rules:

fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
empty(nil) -> true
empty(cons(h, t)) -> false
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)
length(nil) -> 0
length(cons(h, t)) -> s(length(t))
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
process(store, m) -> if1(store, m, leq(m, length(store)))
if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)

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