Termination w.r.t. Q proof of /tmp/tmpvwIB7m/AAECC.trs

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

0 QTRS

↳1 AAECC Innermost (⇔)

↳2 QTRS

↳3 DependencyPairsProof (⇔)

↳4 QDP

↳5 DependencyGraphProof (⇔)

↳6 AND

  ↳7 QDP

    ↳8 UsableRulesProof (⇔)

    ↳9 QDP

    ↳10 QReductionProof (⇔)

    ↳11 QDP

    ↳12 QDPSizeChangeProof (⇔)

    ↳13 TRUE

  ↳14 QDP

    ↳15 UsableRulesProof (⇔)

    ↳16 QDP

    ↳17 QReductionProof (⇔)

    ↳18 QDP

    ↳19 QDPSizeChangeProof (⇔)

    ↳20 TRUE

  ↳21 QDP

    ↳22 UsableRulesProof (⇔)

    ↳23 QDP

    ↳24 QReductionProof (⇔)

    ↳25 QDP

    ↳26 QDPSizeChangeProof (⇔)

    ↳27 TRUE

  ↳28 QDP

    ↳29 UsableRulesProof (⇔)

    ↳30 QDP

    ↳31 QReductionProof (⇔)

    ↳32 QDP

    ↳33 QDPSizeChangeProof (⇔)

    ↳34 TRUE

  ↳35 QDP

    ↳36 UsableRulesProof (⇔)

    ↳37 QDP

    ↳38 QReductionProof (⇔)

    ↳39 QDP

    ↳40 QDPSizeChangeProof (⇔)

    ↳41 TRUE

  ↳42 QDP

    ↳43 UsableRulesProof (⇔)

    ↳44 QDP

    ↳45 QReductionProof (⇔)

    ↳46 QDP

    ↳47 QDPSizeChangeProof (⇔)

    ↳48 TRUE

  ↳49 QDP

    ↳50 UsableRulesProof (⇔)

    ↳51 QDP

    ↳52 QReductionProof (⇔)

    ↳53 QDP

    ↳54 Rewriting (⇔)

    ↳55 QDP

    ↳56 Rewriting (⇔)

    ↳57 QDP

    ↳58 Rewriting (⇔)

    ↳59 QDP

    ↳60 UsableRulesProof (⇔)

    ↳61 QDP

    ↳62 QReductionProof (⇔)

    ↳63 QDP

    ↳64 Rewriting (⇔)

    ↳65 QDP

    ↳66 Rewriting (⇔)

    ↳67 QDP

    ↳68 Rewriting (⇔)

    ↳69 QDP

    ↳70 UsableRulesProof (⇔)

    ↳71 QDP

    ↳72 QReductionProof (⇔)

    ↳73 QDP

    ↳74 Narrowing (⇔)

    ↳75 QDP

    ↳76 DependencyGraphProof (⇔)

    ↳77 QDP

    ↳78 Rewriting (⇔)

    ↳79 QDP

    ↳80 Narrowing (⇔)

    ↳81 QDP

    ↳82 DependencyGraphProof (⇔)

    ↳83 QDP

    ↳84 UsableRulesProof (⇔)

    ↳85 QDP

    ↳86 Rewriting (⇔)

    ↳87 QDP

    ↳88 UsableRulesProof (⇔)

    ↳89 QDP

    ↳90 QReductionProof (⇔)

    ↳91 QDP

    ↳92 Narrowing (⇔)

    ↳93 QDP

    ↳94 DependencyGraphProof (⇔)

    ↳95 QDP

    ↳96 Narrowing (⇔)

    ↳97 QDP

    ↳98 DependencyGraphProof (⇔)

    ↳99 QDP

    ↳100 Narrowing (⇔)

    ↳101 QDP

    ↳102 DependencyGraphProof (⇔)

    ↳103 QDP

    ↳104 Instantiation (⇔)

    ↳105 QDP

    ↳106 Rewriting (⇔)

    ↳107 QDP

    ↳108 QDPOrderProof (⇔)

    ↳109 QDP

    ↳110 DependencyGraphProof (⇔)

    ↳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, if2, if3, if1}

(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) TRUE

(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) TRUE

(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) TRUE

(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) TRUE

(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) TRUE

(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) TRUE

(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) Rewriting (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)

(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) Rewriting (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))))

(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) Rewriting (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)

(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) Rewriting (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)

(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) Rewriting (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)))

(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) Rewriting (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)

(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) Narrowing (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(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))))

(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) Rewriting (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)

(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) Narrowing (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(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))))

(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) Rewriting (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)

(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) Narrowing (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(nil, y1) → IF1(nil, y1, leq(y1, 0))
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) Narrowing (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(nil, s(x0), false) → PROCESS(nil, 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) Narrowing (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(nil, s(x0), false) → PROCESS(nil, 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) Instantiation (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))))

(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) Rewriting (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)))

(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].

The following pairs can be oriented strictly and are deleted.

IF2(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))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(IF1(x₁, x₂, x₃)) = x₁
POL(IF2(x₁, x₂, x₃)) = x₁
POL(IF3(x₁, x₂, x₃)) = x₁
POL(PROCESS(x₁, x₂)) = x₁
POL(cons(x₁, x₂)) = 1 + x₂
POL(false) = 0
POL(length(x₁)) = 0
POL(leq(x₁, x₂)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(sndsplit(x₁, x₂)) = x₂
POL(true) = 0

The following usable rules [FROCOS05] were oriented:

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

(109) 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)
IF1(cons(x1, x2), s(x0), false) → IF3(cons(x1, x2), s(x0), false)
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 3 less nodes.