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.

     ↳Overlay and local confluence Check

The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.

     ↳OC

       →TRS2

         ↳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.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Usable Rules (Innermost)

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

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)

Strategy:

innermost

As we are in the innermost case, we can delete all 22 non-usable-rules.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

...

               →DP Problem 8

                 ↳Size-Change Principle

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1
2	>	2

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1
2	>	2

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

cons(x₁, x₂) -> cons(x₁, x₂)
s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳Usable Rules (Innermost)

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

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)

Strategy:

innermost

As we are in the innermost case, we can delete all 22 non-usable-rules.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

...

               →DP Problem 9

                 ↳Size-Change Principle

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1
2	>	2

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1
2	>	2

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

cons(x₁, x₂) -> cons(x₁, x₂)
s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳Usable Rules (Innermost)

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

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)

Strategy:

innermost

As we are in the innermost case, we can delete all 22 non-usable-rules.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

               →DP Problem 10

                 ↳Size-Change Principle

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1
2	>	2

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1
2	>	2

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳Usable Rules (Innermost)

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

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)

Strategy:

innermost

As we are in the innermost case, we can delete all 22 non-usable-rules.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

...

               →DP Problem 11

                 ↳Size-Change Principle

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

cons(x₁, x₂) -> cons(x₁, x₂)

We obtain no new DP problems.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳Usable Rules (Innermost)

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

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)

Strategy:

innermost

As we are in the innermost case, we can delete all 22 non-usable-rules.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

...

               →DP Problem 12

                 ↳Size-Change Principle

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1
2	=	2

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1
2	=	2

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

cons(x₁, x₂) -> cons(x₁, x₂)

We obtain no new DP problems.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳Usable Rules (Innermost)

           →DP Problem 7

             ↳UsableRules

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)

Strategy:

innermost

As we are in the innermost case, we can delete all 22 non-usable-rules.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

...

               →DP Problem 13

                 ↳Size-Change Principle

           →DP Problem 7

             ↳UsableRules

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1}	,	{1}
1	=	1
2	>	2

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	=	1
2	>	2

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

cons(x₁, x₂) -> cons(x₁, x₂)

We obtain no new DP problems.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳Usable Rules (Innermost)

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)

Strategy:

innermost

As we are in the innermost case, we can delete all 6 non-usable-rules.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 14

                 ↳Rewriting Transformation

Dependency Pairs:

Rules:

map_f(pid, nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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(map_f(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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 15

                 ↳Rewriting Transformation

Dependency Pairs:

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)))
IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))

Rules:

map_f(pid, nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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(map_f(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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →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(map_f(self, nil), sndsplit(m, store)), m)

Rules:

map_f(pid, nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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(map_f(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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 17

                 ↳Rewriting Transformation

Dependency Pairs:

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, 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:

map_f(pid, nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 18

                 ↳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, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))

Rules:

map_f(pid, nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 19

                 ↳Rewriting 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(app(nil, sndsplit(m, store)), m)

Rules:

map_f(pid, nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 20

                 ↳Usable Rules (Innermost)

Dependency Pairs:

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
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, store), m)

Rules:

map_f(pid, nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)

Strategy:

innermost

As we are in the innermost case, we can delete all 3 non-usable-rules.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 21

                 ↳Narrowing Transformation

Dependency Pairs:

Rules:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
IF1(store', 0, false) -> IF3(store', 0, empty(nil))
IF1(nil, s(n'), false) -> IF3(nil, s(n'), empty(nil))

The transformation is resulting in one new DP problem:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 22

                 ↳Rewriting 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'), empty(cons(h', fstsplit(n', t'))))
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:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 23

                 ↳Narrowing Transformation

Dependency Pairs:

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
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, store), m)

Rules:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
IF1(store', 0, true) -> IF2(store', 0, empty(nil))
IF1(nil, s(n'), true) -> IF2(nil, s(n'), empty(nil))

The transformation is resulting in one new DP problem:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 24

                 ↳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(store, m) -> IF1(store, m, leq(m, length(store)))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)

Rules:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 25

                 ↳Narrowing Transformation

Dependency Pairs:

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

Rules:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))

The transformation is resulting in one new DP problem:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 26

                 ↳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)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)

Rules:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 27

                 ↳Narrowing 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)
IF1(cons(h', t'), s(n'), false) -> IF3(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:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 28

                 ↳Instantiation Transformation

Dependency Pairs:

IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
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)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

Rules:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 29

                 ↳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)
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'))
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)

Rules:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, 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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 30

                 ↳Usable Rules (Innermost)

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)
IF1(cons(h', t'), s(n'), false) -> IF3(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:

empty(cons(h, t)) -> false
empty(nil) -> true
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)

Strategy:

innermost

As we are in the innermost case, we can delete all 5 non-usable-rules.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 31

                 ↳Negative Polynomial Order

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)
IF1(cons(h', t'), s(n'), false) -> IF3(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:

sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)

Strategy:

innermost

The following Dependency Pairs can be strictly oriented using the given order.

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'))

Moreover, the following usable rules (regarding the implicit AFS) are oriented.

sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)

Used ordering:
Polynomial Order with Interpretation:

POL( IF2(x₁, ..., x₃) ) = x₁

POL( cons(x₁, x₂) ) = x₂ + 1

POL( PROCESS(x₁, x₂) ) = x₁

POL( sndsplit(x₁, x₂) ) = x₂

POL( IF3(x₁, ..., x₃) ) = x₁

POL( IF1(x₁, ..., x₃) ) = x₁

POL( nil ) = 0

POL( length(x₁) ) = 0

POL( s(x₁) ) = 0

POL( 0 ) = 0

POL( leq(x₁, x₂) ) = 0

POL( true ) = 0

POL( false ) = 0

This results in one new DP problem.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

           →DP Problem 4

             ↳UsableRules

           →DP Problem 5

             ↳UsableRules

           →DP Problem 6

             ↳UsableRules

           →DP Problem 7

             ↳UsableRules

...

               →DP Problem 32

                 ↳Dependency Graph

Dependency Pairs:

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

Rules:

sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:16 minutes