Termination w.r.t. Q proof of AProVE_04

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

0 QTRS

↳1 AAECC Innermost (⇔, 0 ms)

↳2 QTRS

↳3 DependencyPairsProof (⇔, 0 ms)

↳4 QDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 QDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 QReductionProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 QDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 QReductionProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 QDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 QDP

        ↳24 QReductionProof (⇔, 0 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 QDP

        ↳29 UsableRulesProof (⇔, 0 ms)

        ↳30 QDP

        ↳31 QReductionProof (⇔, 0 ms)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔, 0 ms)

        ↳34 YES

    ↳35 QDP

        ↳36 UsableRulesProof (⇔, 0 ms)

        ↳37 QDP

        ↳38 QReductionProof (⇔, 0 ms)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔, 0 ms)

        ↳41 YES

    ↳42 QDP

        ↳43 UsableRulesProof (⇔, 0 ms)

        ↳44 QDP

        ↳45 QReductionProof (⇔, 0 ms)

        ↳46 QDP

        ↳47 QDPSizeChangeProof (⇔, 0 ms)

        ↳48 YES

    ↳49 QDP

        ↳50 UsableRulesProof (⇔, 0 ms)

        ↳51 QDP

        ↳52 QReductionProof (⇔, 0 ms)

        ↳53 QDP

        ↳54 TransformationProof (⇔, 0 ms)

        ↳55 QDP

        ↳56 TransformationProof (⇔, 0 ms)

        ↳57 QDP

        ↳58 TransformationProof (⇔, 0 ms)

        ↳59 QDP

        ↳60 UsableRulesProof (⇔, 0 ms)

        ↳61 QDP

        ↳62 QReductionProof (⇔, 0 ms)

        ↳63 QDP

        ↳64 TransformationProof (⇔, 0 ms)

        ↳65 QDP

        ↳66 TransformationProof (⇔, 0 ms)

        ↳67 QDP

        ↳68 TransformationProof (⇔, 0 ms)

        ↳69 QDP

        ↳70 UsableRulesProof (⇔, 0 ms)

        ↳71 QDP

        ↳72 QReductionProof (⇔, 0 ms)

        ↳73 QDP

        ↳74 TransformationProof (⇔, 0 ms)

        ↳75 QDP

        ↳76 DependencyGraphProof (⇔, 0 ms)

        ↳77 QDP

        ↳78 TransformationProof (⇔, 0 ms)

        ↳79 QDP

        ↳80 TransformationProof (⇔, 0 ms)

        ↳81 QDP

        ↳82 DependencyGraphProof (⇔, 0 ms)

        ↳83 QDP

        ↳84 UsableRulesProof (⇔, 0 ms)

        ↳85 QDP

        ↳86 TransformationProof (⇔, 0 ms)

        ↳87 QDP

        ↳88 UsableRulesProof (⇔, 0 ms)

        ↳89 QDP

        ↳90 QReductionProof (⇔, 0 ms)

        ↳91 QDP

        ↳92 TransformationProof (⇔, 0 ms)

        ↳93 QDP

        ↳94 DependencyGraphProof (⇔, 0 ms)

        ↳95 QDP

        ↳96 TransformationProof (⇔, 0 ms)

        ↳97 QDP

        ↳98 DependencyGraphProof (⇔, 0 ms)

        ↳99 QDP

        ↳100 TransformationProof (⇔, 0 ms)

        ↳101 QDP

        ↳102 DependencyGraphProof (⇔, 0 ms)

        ↳103 QDP

        ↳104 TransformationProof (⇔, 0 ms)

        ↳105 QDP

        ↳106 TransformationProof (⇔, 0 ms)

        ↳107 QDP

        ↳108 QDPOrderProof (⇔, 0 ms)

        ↳109 QDP

        ↳110 DependencyGraphProof (⇔, 0 ms)

        ↳111 TRUE

(0) Obligation:

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

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is

sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
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))
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(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)

The TRS R 2 is

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)

The signature Sigma is {process, if1, if2, if3}

(2) Obligation:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

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)

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APP(cons(h, t), x) → APP(t, x)

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

APP(cons(h, t), x) → APP(t, x)

R is empty.
The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

(11) Obligation:

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

APP(cons(h, t), x) → APP(t, x)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APP(cons(h, t), x) → APP(t, x)
The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

MAP_F(pid, cons(h, t)) → MAP_F(pid, t)

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

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

MAP_F(pid, cons(h, t)) → MAP_F(pid, t)

R is empty.
The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(17) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

(18) Obligation:

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

MAP_F(pid, cons(h, t)) → MAP_F(pid, t)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
The graph contains the following edges 1 >= 1, 2 > 2

(20) YES

(21) Obligation:

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

LENGTH(cons(h, t)) → LENGTH(t)

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(22) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(23) Obligation:

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

LENGTH(cons(h, t)) → LENGTH(t)

R is empty.
The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(24) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

(25) Obligation:

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

LENGTH(cons(h, t)) → LENGTH(t)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LENGTH(cons(h, t)) → LENGTH(t)
The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

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

LEQ(s(n), s(m)) → LEQ(n, m)

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(29) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(30) Obligation:

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

LEQ(s(n), s(m)) → LEQ(n, m)

R is empty.
The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(31) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

(32) Obligation:

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

LEQ(s(n), s(m)) → LEQ(n, m)

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

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LEQ(s(n), s(m)) → LEQ(n, m)
The graph contains the following edges 1 > 1, 2 > 2

(34) YES

(35) Obligation:

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

SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(36) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(37) Obligation:

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

SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)

R is empty.
The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(38) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

(39) Obligation:

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

SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)

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

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
The graph contains the following edges 1 > 1, 2 > 2

(41) YES

(42) Obligation:

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

FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(43) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(44) Obligation:

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

FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)

R is empty.
The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(45) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

(46) Obligation:

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

FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)

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

(47) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
The graph contains the following edges 1 > 1, 2 > 2

(48) YES

(49) Obligation:

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

IF1(store, m, true) → IF2(store, m, empty(fstsplit(m, store)))
IF2(store, m, false) → PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF3(store, m, false) → PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(50) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(51) Obligation:

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

IF1(store, m, true) → IF2(store, m, empty(fstsplit(m, store)))
IF2(store, m, false) → PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF3(store, m, false) → PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

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

(52) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

process(x0, x1)
if1(x0, x1, true)
if1(x0, x1, false)
if2(x0, x1, false)
if3(x0, x1, false)

(53) Obligation:

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

IF1(store, m, true) → IF2(store, m, empty(fstsplit(m, store)))
IF2(store, m, false) → PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF3(store, m, false) → PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))

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

(54) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF2(store, m, false) → PROCESS(app(map_f(self, nil), sndsplit(m, store)), m) at position [0,0] we obtained the following new rules [LPAR04]:

IF2(store, m, false) → PROCESS(app(nil, sndsplit(m, store)), m) → IF2(store, m, false) → PROCESS(app(nil, sndsplit(m, store)), m)

(55) Obligation:

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

IF1(store, m, true) → IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
IF3(store, m, false) → PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF2(store, m, false) → PROCESS(app(nil, sndsplit(m, store)), m)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))

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

(56) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) at position [2,0,1,0] we obtained the following new rules [LPAR04]:

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

(57) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))

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

(58) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF3(store, m, false) → PROCESS(sndsplit(m, app(map_f(self, nil), store)), m) at position [0,1,0] we obtained the following new rules [LPAR04]:

IF3(store, m, false) → PROCESS(sndsplit(m, app(nil, store)), m) → IF3(store, m, false) → PROCESS(sndsplit(m, app(nil, store)), m)

(59) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))

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

(60) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(61) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))

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

(62) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

map_f(x0, nil)
map_f(x0, cons(x1, x2))

(63) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)

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

(64) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF2(store, m, false) → PROCESS(app(nil, sndsplit(m, store)), m) at position [0] we obtained the following new rules [LPAR04]:

IF2(store, m, false) → PROCESS(sndsplit(m, store), m) → IF2(store, m, false) → PROCESS(sndsplit(m, store), m)

(65) Obligation:

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

IF1(store, m, true) → IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, app(nil, store))))
IF3(store, m, false) → PROCESS(sndsplit(m, app(nil, store)), m)
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)

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

(66) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, app(nil, store)))) at position [2,0,1] we obtained the following new rules [LPAR04]:

IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, store))) → IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, store)))

(67) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)

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

(68) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF3(store, m, false) → PROCESS(sndsplit(m, app(nil, store)), m) at position [0,1] we obtained the following new rules [LPAR04]:

IF3(store, m, false) → PROCESS(sndsplit(m, store), m) → IF3(store, m, false) → PROCESS(sndsplit(m, store), m)

(69) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)

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

(70) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(71) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)

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

(72) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

app(nil, x0)
app(cons(x0, x1), x2)

(73) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(74) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule IF1(store, m, true) → IF2(store, m, empty(fstsplit(m, store))) at position [2] we obtained the following new rules [LPAR04]:

IF1(x0, 0, true) → IF2(x0, 0, empty(nil)) → IF1(x0, 0, true) → IF2(x0, 0, empty(nil))
IF1(nil, s(x0), true) → IF2(nil, s(x0), empty(nil)) → IF1(nil, s(x0), true) → IF2(nil, s(x0), empty(nil))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2)))) → IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2))))

(75) Obligation:

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

PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, store)))
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(x0, 0, true) → IF2(x0, 0, empty(nil))
IF1(nil, s(x0), true) → IF2(nil, s(x0), empty(nil))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2))))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(76) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(77) Obligation:

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

IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, store)))
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)
PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2))))
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(78) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2)))) at position [2] we obtained the following new rules [LPAR04]:

IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false) → IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)

(79) Obligation:

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

IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, store)))
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)
PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(80) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule IF1(store, m, false) → IF3(store, m, empty(fstsplit(m, store))) at position [2] we obtained the following new rules [LPAR04]:

IF1(x0, 0, false) → IF3(x0, 0, empty(nil)) → IF1(x0, 0, false) → IF3(x0, 0, empty(nil))
IF1(nil, s(x0), false) → IF3(nil, s(x0), empty(nil)) → IF1(nil, s(x0), false) → IF3(nil, s(x0), empty(nil))
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2)))) → IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2))))

(81) Obligation:

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

IF3(store, m, false) → PROCESS(sndsplit(m, store), m)
PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF1(x0, 0, false) → IF3(x0, 0, empty(nil))
IF1(nil, s(x0), false) → IF3(nil, s(x0), empty(nil))
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2))))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(82) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(83) Obligation:

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

PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2))))
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(84) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(85) Obligation:

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

PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2))))
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(86) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), empty(cons(x1, fstsplit(x0, x2)))) at position [2] we obtained the following new rules [LPAR04]:

IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false) → IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)

(87) Obligation:

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

PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(88) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(89) Obligation:

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

PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(90) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))

(91) Obligation:

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

PROCESS(store, m) → IF1(store, m, leq(m, length(store)))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(92) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule PROCESS(store, m) → IF1(store, m, leq(m, length(store))) at position [2] we obtained the following new rules [LPAR04]:

PROCESS(y0, 0) → IF1(y0, 0, true) → PROCESS(y0, 0) → IF1(y0, 0, true)
PROCESS(nil, y1) → IF1(nil, y1, leq(y1, 0)) → PROCESS(nil, y1) → IF1(nil, y1, leq(y1, 0))
PROCESS(cons(x0, x1), y1) → IF1(cons(x0, x1), y1, leq(y1, s(length(x1)))) → PROCESS(cons(x0, x1), y1) → IF1(cons(x0, x1), y1, leq(y1, s(length(x1))))

(93) Obligation:

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

IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
PROCESS(y0, 0) → IF1(y0, 0, true)
PROCESS(nil, y1) → IF1(nil, y1, leq(y1, 0))
PROCESS(cons(x0, x1), y1) → IF1(cons(x0, x1), y1, leq(y1, s(length(x1))))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(94) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(95) Obligation:

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

IF2(store, m, false) → PROCESS(sndsplit(m, store), m)
PROCESS(cons(x0, x1), y1) → IF1(cons(x0, x1), y1, leq(y1, s(length(x1))))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(96) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule IF2(store, m, false) → PROCESS(sndsplit(m, store), m) at position [0] we obtained the following new rules [LPAR04]:

IF2(x0, 0, false) → PROCESS(x0, 0) → IF2(x0, 0, false) → PROCESS(x0, 0)
IF2(nil, s(x0), false) → PROCESS(nil, s(x0)) → IF2(nil, s(x0), false) → PROCESS(nil, s(x0))
IF2(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0)) → IF2(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))

(97) Obligation:

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

PROCESS(cons(x0, x1), y1) → IF1(cons(x0, x1), y1, leq(y1, s(length(x1))))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)
IF2(x0, 0, false) → PROCESS(x0, 0)
IF2(nil, s(x0), false) → PROCESS(nil, s(x0))
IF2(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(98) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(99) Obligation:

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

IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF2(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))
PROCESS(cons(x0, x1), y1) → IF1(cons(x0, x1), y1, leq(y1, s(length(x1))))
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
IF3(store, m, false) → PROCESS(sndsplit(m, store), m)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(100) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule IF3(store, m, false) → PROCESS(sndsplit(m, store), m) at position [0] we obtained the following new rules [LPAR04]:

IF3(x0, 0, false) → PROCESS(x0, 0) → IF3(x0, 0, false) → PROCESS(x0, 0)
IF3(nil, s(x0), false) → PROCESS(nil, s(x0)) → IF3(nil, s(x0), false) → PROCESS(nil, s(x0))
IF3(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0)) → IF3(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))

(101) Obligation:

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

IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF2(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))
PROCESS(cons(x0, x1), y1) → IF1(cons(x0, x1), y1, leq(y1, s(length(x1))))
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
IF3(x0, 0, false) → PROCESS(x0, 0)
IF3(nil, s(x0), false) → PROCESS(nil, s(x0))
IF3(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(102) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(103) Obligation:

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

IF2(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))
PROCESS(cons(x0, x1), y1) → IF1(cons(x0, x1), y1, leq(y1, s(length(x1))))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
IF3(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(104) TransformationProof (EQUIVALENT transformation)

By instantiating [LPAR04] the rule PROCESS(cons(x0, x1), y1) → IF1(cons(x0, x1), y1, leq(y1, s(length(x1)))) we obtained the following new rules [LPAR04]:

PROCESS(cons(x0, x1), s(z2)) → IF1(cons(x0, x1), s(z2), leq(s(z2), s(length(x1)))) → PROCESS(cons(x0, x1), s(z2)) → IF1(cons(x0, x1), s(z2), leq(s(z2), s(length(x1))))

(105) Obligation:

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

IF2(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
IF3(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))
PROCESS(cons(x0, x1), s(z2)) → IF1(cons(x0, x1), s(z2), leq(s(z2), s(length(x1))))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(106) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PROCESS(cons(x0, x1), s(z2)) → IF1(cons(x0, x1), s(z2), leq(s(z2), s(length(x1)))) at position [2] we obtained the following new rules [LPAR04]:

PROCESS(cons(x0, x1), s(z2)) → IF1(cons(x0, x1), s(z2), leq(z2, length(x1))) → PROCESS(cons(x0, x1), s(z2)) → IF1(cons(x0, x1), s(z2), leq(z2, length(x1)))

(107) Obligation:

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

IF2(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))
IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
IF3(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))
PROCESS(cons(x0, x1), s(z2)) → IF1(cons(x0, x1), s(z2), leq(z2, length(x1)))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(108) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

IF1(cons(x1, x2), s(x0), true) → IF2(cons(x1, x2), s(x0), false)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
IF3(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

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

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

POL( 0 ) = 0

POL( s(x₁) ) = x₁ + 2

POL( nil ) = 1

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

POL( IF1(x₁, ..., x₃) ) = 2x₁ + 2x₂ + x₃ + 1

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

POL( length(x₁) ) = 2

POL( true ) = 1

POL( false ) = 1

POL( IF2(x₁, ..., x₃) ) = max{0, 2x₁ + 2x₂ + 2x₃ - 2}

POL( IF3(x₁, ..., x₃) ) = x₁ + 2x₂ + 2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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

(109) Obligation:

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

IF2(cons(x1, x2), s(x0), false) → PROCESS(sndsplit(x0, x2), s(x0))
PROCESS(cons(x0, x1), s(z2)) → IF1(cons(x0, x1), s(z2), leq(z2, length(x1)))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))

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

(110) DependencyGraphProof (EQUIVALENT transformation)

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