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

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)
split(nil) → app(nil, nil)
split(cons(x, nil)) → app(cons(x, nil), nil)
split(cons(x, cons(y, xs))) → split1(x, y, split(xs))
split1(x, y, app(xs, ys)) → app(cons(x, xs), cons(y, ys))
merge([], xs) → xs
merge(xs, []) → xs
merge(cons(x, xs), cons(y, ys)) → ifmerge(leq(x, y), x, y, xs, ys)
ifmerge(tt, x, y, xs, ys) → cons(x, merge(xs, cons(y, ys)))
ifmerge(ff, x, y, xs, ys) → cons(y, merge(cons(x, xs), ys))
mergesort(xs) → mergesort1(split(xs))
mergesort1(app(xs, ys)) → merge(mergesort(xs), mergesort(ys))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

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

(2) Obligation:

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

LEQ(s(x), s(y)) → LEQ(x, y)
SPLIT(cons(x, cons(y, xs))) → SPLIT1(x, y, split(xs))
SPLIT(cons(x, cons(y, xs))) → SPLIT(xs)
MERGE(cons(x, xs), cons(y, ys)) → IFMERGE(leq(x, y), x, y, xs, ys)
MERGE(cons(x, xs), cons(y, ys)) → LEQ(x, y)
IFMERGE(tt, x, y, xs, ys) → MERGE(xs, cons(y, ys))
IFMERGE(ff, x, y, xs, ys) → MERGE(cons(x, xs), ys)
MERGESORT(xs) → MERGESORT1(split(xs))
MERGESORT(xs) → SPLIT(xs)
MERGESORT1(app(xs, ys)) → MERGE(mergesort(xs), mergesort(ys))
MERGESORT1(app(xs, ys)) → MERGESORT(xs)
MERGESORT1(app(xs, ys)) → MERGESORT(ys)

The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)
split(nil) → app(nil, nil)
split(cons(x, nil)) → app(cons(x, nil), nil)
split(cons(x, cons(y, xs))) → split1(x, y, split(xs))
split1(x, y, app(xs, ys)) → app(cons(x, xs), cons(y, ys))
merge([], xs) → xs
merge(xs, []) → xs
merge(cons(x, xs), cons(y, ys)) → ifmerge(leq(x, y), x, y, xs, ys)
ifmerge(tt, x, y, xs, ys) → cons(x, merge(xs, cons(y, ys)))
ifmerge(ff, x, y, xs, ys) → cons(y, merge(cons(x, xs), ys))
mergesort(xs) → mergesort1(split(xs))
mergesort1(app(xs, ys)) → merge(mergesort(xs), mergesort(ys))

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

SPLIT(cons(x, cons(y, xs))) → SPLIT(xs)

The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)
split(nil) → app(nil, nil)
split(cons(x, nil)) → app(cons(x, nil), nil)
split(cons(x, cons(y, xs))) → split1(x, y, split(xs))
split1(x, y, app(xs, ys)) → app(cons(x, xs), cons(y, ys))
merge([], xs) → xs
merge(xs, []) → xs
merge(cons(x, xs), cons(y, ys)) → ifmerge(leq(x, y), x, y, xs, ys)
ifmerge(tt, x, y, xs, ys) → cons(x, merge(xs, cons(y, ys)))
ifmerge(ff, x, y, xs, ys) → cons(y, merge(cons(x, xs), ys))
mergesort(xs) → mergesort1(split(xs))
mergesort1(app(xs, ys)) → merge(mergesort(xs), mergesort(ys))

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

(6) 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:

• SPLIT(cons(x, cons(y, xs))) → SPLIT(xs)
  The graph contains the following edges 1 > 1

(7) YES

(8) Obligation:

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

LEQ(s(x), s(y)) → LEQ(x, y)

The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)
split(nil) → app(nil, nil)
split(cons(x, nil)) → app(cons(x, nil), nil)
split(cons(x, cons(y, xs))) → split1(x, y, split(xs))
split1(x, y, app(xs, ys)) → app(cons(x, xs), cons(y, ys))
merge([], xs) → xs
merge(xs, []) → xs
merge(cons(x, xs), cons(y, ys)) → ifmerge(leq(x, y), x, y, xs, ys)
ifmerge(tt, x, y, xs, ys) → cons(x, merge(xs, cons(y, ys)))
ifmerge(ff, x, y, xs, ys) → cons(y, merge(cons(x, xs), ys))
mergesort(xs) → mergesort1(split(xs))
mergesort1(app(xs, ys)) → merge(mergesort(xs), mergesort(ys))

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

(9) 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(x), s(y)) → LEQ(x, y)
  The graph contains the following edges 1 > 1, 2 > 2

(10) YES

(11) Obligation:

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

MERGE(cons(x, xs), cons(y, ys)) → IFMERGE(leq(x, y), x, y, xs, ys)
IFMERGE(tt, x, y, xs, ys) → MERGE(xs, cons(y, ys))
IFMERGE(ff, x, y, xs, ys) → MERGE(cons(x, xs), ys)

The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)
split(nil) → app(nil, nil)
split(cons(x, nil)) → app(cons(x, nil), nil)
split(cons(x, cons(y, xs))) → split1(x, y, split(xs))
split1(x, y, app(xs, ys)) → app(cons(x, xs), cons(y, ys))
merge([], xs) → xs
merge(xs, []) → xs
merge(cons(x, xs), cons(y, ys)) → ifmerge(leq(x, y), x, y, xs, ys)
ifmerge(tt, x, y, xs, ys) → cons(x, merge(xs, cons(y, ys)))
ifmerge(ff, x, y, xs, ys) → cons(y, merge(cons(x, xs), ys))
mergesort(xs) → mergesort1(split(xs))
mergesort1(app(xs, ys)) → merge(mergesort(xs), mergesort(ys))

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

(12) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(13) Obligation:

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

MERGE(cons(x, xs), cons(y, ys)) → IFMERGE(leq(x, y), x, y, xs, ys)
IFMERGE(tt, x, y, xs, ys) → MERGE(xs, cons(y, ys))
IFMERGE(ff, x, y, xs, ys) → MERGE(cons(x, xs), ys)

The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)
split(nil) → app(nil, nil)
split(cons(x, nil)) → app(cons(x, nil), nil)
split(cons(x, cons(y, xs))) → split1(x, y, split(xs))
split1(x, y, app(xs, ys)) → app(cons(x, xs), cons(y, ys))
merge([], xs) → xs
merge(xs, []) → xs
merge(cons(x, xs), cons(y, ys)) → ifmerge(leq(x, y), x, y, xs, ys)
ifmerge(tt, x, y, xs, ys) → cons(x, merge(xs, cons(y, ys)))
ifmerge(ff, x, y, xs, ys) → cons(y, merge(cons(x, xs), ys))
mergesort(xs) → mergesort1(split(xs))
mergesort1(app(xs, ys)) → merge(mergesort(xs), mergesort(ys))

The set Q consists of the following terms:

leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
split(nil)
split(cons(x0, nil))
split(cons(x0, cons(x1, x2)))
split1(x0, x1, app(x2, x3))
merge([], x0)
merge(x0, [])
merge(cons(x0, x1), cons(x2, x3))
ifmerge(tt, x0, x1, x2, x3)
ifmerge(ff, x0, x1, x2, x3)
mergesort(x0)
mergesort1(app(x0, x1))

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

(14) 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.

(15) Obligation:

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

MERGE(cons(x, xs), cons(y, ys)) → IFMERGE(leq(x, y), x, y, xs, ys)
IFMERGE(tt, x, y, xs, ys) → MERGE(xs, cons(y, ys))
IFMERGE(ff, x, y, xs, ys) → MERGE(cons(x, xs), ys)

The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)

The set Q consists of the following terms:

leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
split(nil)
split(cons(x0, nil))
split(cons(x0, cons(x1, x2)))
split1(x0, x1, app(x2, x3))
merge([], x0)
merge(x0, [])
merge(cons(x0, x1), cons(x2, x3))
ifmerge(tt, x0, x1, x2, x3)
ifmerge(ff, x0, x1, x2, x3)
mergesort(x0)
mergesort1(app(x0, x1))

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

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

split(nil)
split(cons(x0, nil))
split(cons(x0, cons(x1, x2)))
split1(x0, x1, app(x2, x3))
merge([], x0)
merge(x0, [])
merge(cons(x0, x1), cons(x2, x3))
ifmerge(tt, x0, x1, x2, x3)
ifmerge(ff, x0, x1, x2, x3)
mergesort(x0)
mergesort1(app(x0, x1))

(17) Obligation:

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

MERGE(cons(x, xs), cons(y, ys)) → IFMERGE(leq(x, y), x, y, xs, ys)
IFMERGE(tt, x, y, xs, ys) → MERGE(xs, cons(y, ys))
IFMERGE(ff, x, y, xs, ys) → MERGE(cons(x, xs), ys)

The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)

The set Q consists of the following terms:

leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))

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

(18) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

IFMERGE(ff, x, y, xs, ys) → MERGE(cons(x, xs), ys)

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

POL(0) = 0   
POL(IFMERGE(x₁, x₂, x₃, x₄, x₅)) = 1 + x₅   
POL(MERGE(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = 1 + x₂   
POL(ff) = 0   
POL(leq(x₁, x₂)) = 0   
POL(s(x₁)) = 0   
POL(tt) = 0   

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

(19) Obligation:

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

MERGE(cons(x, xs), cons(y, ys)) → IFMERGE(leq(x, y), x, y, xs, ys)
IFMERGE(tt, x, y, xs, ys) → MERGE(xs, cons(y, ys))

The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)

The set Q consists of the following terms:

leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))

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

(20) 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:

• IFMERGE(tt, x, y, xs, ys) → MERGE(xs, cons(y, ys))
  The graph contains the following edges 4 >= 1

• MERGE(cons(x, xs), cons(y, ys)) → IFMERGE(leq(x, y), x, y, xs, ys)
  The graph contains the following edges 1 > 2, 2 > 3, 1 > 4, 2 > 5

(21) YES

(22) Obligation:

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

MERGESORT1(app(xs, ys)) → MERGESORT(xs)
MERGESORT(xs) → MERGESORT1(split(xs))
MERGESORT1(app(xs, ys)) → MERGESORT(ys)

The TRS R consists of the following rules:

leq(0, x) → tt
leq(s(x), 0) → ff
leq(s(x), s(y)) → leq(x, y)
split(nil) → app(nil, nil)
split(cons(x, nil)) → app(cons(x, nil), nil)
split(cons(x, cons(y, xs))) → split1(x, y, split(xs))
split1(x, y, app(xs, ys)) → app(cons(x, xs), cons(y, ys))
merge([], xs) → xs
merge(xs, []) → xs
merge(cons(x, xs), cons(y, ys)) → ifmerge(leq(x, y), x, y, xs, ys)
ifmerge(tt, x, y, xs, ys) → cons(x, merge(xs, cons(y, ys)))
ifmerge(ff, x, y, xs, ys) → cons(y, merge(cons(x, xs), ys))
mergesort(xs) → mergesort1(split(xs))
mergesort1(app(xs, ys)) → merge(mergesort(xs), mergesort(ys))

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

(23) NonLoopProof (EQUIVALENT transformation)

By Theorem 8 [NONLOOP] we deduce infiniteness of the QDP.
We apply the theorem with m = 1, b = 0,
σ' = [ ], and μ' = [x0 / nil] on the rule
MERGESORT1(app(nil, nil))[ ]ⁿ[ ] → MERGESORT1(app(nil, nil))[ ]ⁿ[x0 / nil]
This rule is correct for the QDP as the following derivation shows:

intermediate steps: Equivalent (Simplify mu) - Instantiate mu - Instantiation
MERGESORT1(app(nil, x1))[ ]ⁿ[ ] → MERGESORT1(app(nil, nil))[ ]ⁿ[ ]
    by Narrowing at position: [0]
        intermediate steps: Instantiation
        MERGESORT1(app(x0, x1))[ ]ⁿ[ ] → MERGESORT1(split(x0))[ ]ⁿ[ ]
            by Narrowing at position: []
                intermediate steps: Instantiation
                MERGESORT1(app(xs, ys))[ ]ⁿ[ ] → MERGESORT(xs)[ ]ⁿ[ ]
                    by OriginalRule from TRS P

                intermediate steps: Instantiation - Instantiation
                MERGESORT(xs)[ ]ⁿ[ ] → MERGESORT1(split(xs))[ ]ⁿ[ ]
                    by OriginalRule from TRS P

        split(nil)[ ]ⁿ[ ] → app(nil, nil)[ ]ⁿ[ ]
            by OriginalRule from TRS R

(24) NO