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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Innermost Termination of R to be shown.

R
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)
MAPF(pid, cons(h, t)) -> APP(f(pid, h), mapf(pid, t))
MAPF(pid, cons(h, t)) -> MAPF(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(mapf(self, nil), store))))
IF1(store, m, false) -> EMPTY(fstsplit(m, app(mapf(self, nil), store)))
IF1(store, m, false) -> FSTSPLIT(m, app(mapf(self, nil), store))
IF1(store, m, false) -> APP(mapf(self, nil), store)
IF1(store, m, false) -> MAPF(self, nil)
IF2(store, m, false) -> PROCESS(app(mapf(self, nil), sndsplit(m, store)), m)
IF2(store, m, false) -> APP(mapf(self, nil), sndsplit(m, store))
IF2(store, m, false) -> MAPF(self, nil)
IF2(store, m, false) -> SNDSPLIT(m, store)
IF3(store, m, false) -> PROCESS(sndsplit(m, app(mapf(self, nil), store)), m)
IF3(store, m, false) -> SNDSPLIT(m, app(mapf(self, nil), store))
IF3(store, m, false) -> APP(mapf(self, nil), store)
IF3(store, m, false) -> MAPF(self, nil)

Furthermore, R contains seven SCCs.

R
DPs
→DP Problem 1
Polynomial Ordering
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

The following dependency pair can be strictly oriented:

FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(cons(x1, x2)) =  0 POL(FSTSPLIT(x1, x2)) =  x1 POL(s(x1)) =  1 + x1

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 8
Dependency Graph
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw

Dependency Pair:

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polynomial Ordering
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

The following dependency pair can be strictly oriented:

SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(SNDSPLIT(x1, x2)) =  x1 POL(cons(x1, x2)) =  0 POL(s(x1)) =  1 + x1

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 9
Dependency Graph
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw

Dependency Pair:

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polynomial Ordering
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

The following dependency pair can be strictly oriented:

LEQ(s(n), s(m)) -> LEQ(n, m)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(LEQ(x1, x2)) =  x1 POL(s(x1)) =  1 + x1

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 10
Dependency Graph
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw

Dependency Pair:

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polynomial Ordering
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

The following dependency pair can be strictly oriented:

LENGTH(cons(h, t)) -> LENGTH(t)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(cons(x1, x2)) =  1 + x2 POL(LENGTH(x1)) =  x1

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 11
Dependency Graph
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw

Dependency Pair:

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polynomial Ordering
→DP Problem 6
Polo
→DP Problem 7
Rw

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

The following dependency pair can be strictly oriented:

APP(cons(h, t), x) -> APP(t, x)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(cons(x1, x2)) =  1 + x2 POL(APP(x1, x2)) =  x1

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 12
Dependency Graph
→DP Problem 6
Polo
→DP Problem 7
Rw

Dependency Pair:

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polynomial Ordering
→DP Problem 7
Rw

Dependency Pair:

MAPF(pid, cons(h, t)) -> MAPF(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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

The following dependency pair can be strictly oriented:

MAPF(pid, cons(h, t)) -> MAPF(pid, t)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(MAP_F(x1, x2)) =  x2 POL(cons(x1, x2)) =  1 + x2

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 13
Dependency Graph
→DP Problem 7
Rw

Dependency Pair:

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rewriting Transformation

Dependency Pairs:

IF3(store, m, false) -> PROCESS(sndsplit(m, app(mapf(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(mapf(self, nil), store))))
IF2(store, m, false) -> PROCESS(app(mapf(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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(mapf(self, nil), store))))
one new Dependency Pair is created:

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rewriting Transformation

Dependency Pairs:

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))
IF2(store, m, false) -> PROCESS(app(mapf(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)))
IF3(store, m, false) -> PROCESS(sndsplit(m, app(mapf(self, nil), store)), 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF2(store, m, false) -> PROCESS(app(mapf(self, nil), sndsplit(m, store)), m)
one new Dependency Pair is created:

IF2(store, m, false) -> PROCESS(app(nil, sndsplit(m, store)), m)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 15
Rewriting Transformation

Dependency Pairs:

IF2(store, m, false) -> PROCESS(app(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)))
IF3(store, m, false) -> PROCESS(sndsplit(m, app(mapf(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF3(store, m, false) -> PROCESS(sndsplit(m, app(mapf(self, nil), store)), m)
one new Dependency Pair is created:

IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 16
Rewriting Transformation

Dependency Pairs:

IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF2(store, m, false) -> PROCESS(app(nil, sndsplit(m, store)), 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))
one new Dependency Pair is created:

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 17
Rewriting Transformation

Dependency Pairs:

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
IF2(store, m, false) -> PROCESS(app(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)))
IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF2(store, m, false) -> PROCESS(app(nil, sndsplit(m, store)), m)
one new Dependency Pair is created:

IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 18
Rewriting Transformation

Dependency Pairs:

IF2(store, m, false) -> PROCESS(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)))
IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)
one new Dependency Pair is created:

IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 19
Narrowing Transformation

Dependency Pairs:

IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
three new Dependency Pairs are created:

PROCESS(store', 0) -> IF1(store', 0, true)
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 20
Narrowing Transformation

Dependency Pairs:

PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store', 0) -> IF1(store', 0, true)
IF3(store, m, false) -> PROCESS(sndsplit(m, store), 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
three new Dependency Pairs are created:

IF1(store', 0, true) -> IF2(store', 0, empty(nil))
IF1(nil, s(n'), true) -> IF2(nil, s(n'), empty(nil))
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 21
Rewriting Transformation

Dependency Pairs:

IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
IF1(nil, s(n'), true) -> IF2(nil, s(n'), empty(nil))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store', 0, true) -> IF2(store', 0, empty(nil))
PROCESS(store', 0) -> IF1(store', 0, true)
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(store', 0, true) -> IF2(store', 0, empty(nil))
one new Dependency Pair is created:

IF1(store', 0, true) -> IF2(store', 0, true)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 22
Rewriting Transformation

Dependency Pairs:

IF1(nil, s(n'), true) -> IF2(nil, s(n'), empty(nil))
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(nil, s(n'), true) -> IF2(nil, s(n'), empty(nil))
one new Dependency Pair is created:

IF1(nil, s(n'), true) -> IF2(nil, s(n'), true)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 23
Rewriting Transformation

Dependency Pairs:

IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
one new Dependency Pair is created:

IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 24
Narrowing Transformation

Dependency Pairs:

IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
three new Dependency Pairs are created:

IF1(store', 0, false) -> IF3(store', 0, empty(nil))
IF1(nil, s(n'), false) -> IF3(nil, s(n'), empty(nil))
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 25
Rewriting Transformation

Dependency Pairs:

IF1(nil, s(n'), false) -> IF3(nil, s(n'), empty(nil))
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store', 0, false) -> IF3(store', 0, empty(nil))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(store', 0, false) -> IF3(store', 0, empty(nil))
one new Dependency Pair is created:

IF1(store', 0, false) -> IF3(store', 0, true)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 26
Rewriting Transformation

Dependency Pairs:

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(nil, s(n'), false) -> IF3(nil, s(n'), empty(nil))

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(nil, s(n'), false) -> IF3(nil, s(n'), empty(nil))
one new Dependency Pair is created:

IF1(nil, s(n'), false) -> IF3(nil, s(n'), true)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 27
Rewriting Transformation

Dependency Pairs:

IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
one new Dependency Pair is created:

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 28
Narrowing Transformation

Dependency Pairs:

IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
three new Dependency Pairs are created:

IF2(store', 0, false) -> PROCESS(store', 0)
IF2(nil, s(n'), false) -> PROCESS(nil, s(n'))
IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 29
Narrowing Transformation

Dependency Pairs:

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
three new Dependency Pairs are created:

IF3(store', 0, false) -> PROCESS(store', 0)
IF3(nil, s(n'), false) -> PROCESS(nil, s(n'))
IF3(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 30
Instantiation Transformation

Dependency Pairs:

IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
one new Dependency Pair is created:

PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(s(n'''), s(length(t''))))

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 31
Rewriting Transformation

Dependency Pairs:

IF3(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(s(n'''), s(length(t''))))
IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

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

PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(s(n'''), s(length(t''))))
one new Dependency Pair is created:

PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(n''', length(t'')))

The transformation is resulting in one new DP problem:

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 32
Polynomial Ordering

Dependency Pairs:

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(n''', length(t'')))
IF3(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF3(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(IF3(x1, x2, x3)) =  x1 POL(PROCESS(x1, x2)) =  x1 POL(sndsplit(x1, x2)) =  x2 POL(false) =  0 POL(true) =  0 POL(IF2(x1, x2, x3)) =  x1 POL(0) =  0 POL(IF1(x1, x2, x3)) =  x1 POL(cons(x1, x2)) =  1 + x2 POL(leq(x1, x2)) =  0 POL(nil) =  0 POL(s(x1)) =  0 POL(length(x1)) =  0

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
→DP Problem 3
Polo
→DP Problem 4
Polo
→DP Problem 5
Polo
→DP Problem 6
Polo
→DP Problem 7
Rw
→DP Problem 14
Rw
...
→DP Problem 33
Dependency Graph

Dependency Pairs:

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(n''', 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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(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(mapf(self, nil), store))))
if2(store, m, false) -> process(app(mapf(self, nil), sndsplit(m, store)), m)
if3(store, m, false) -> process(sndsplit(m, app(mapf(self, nil), store)), m)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:06 minutes