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

(0) Obligation:

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

rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))

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:

REV(cons(x, l)) → REV1(x, l)
REV(cons(x, l)) → REV2(x, l)
REV1(x, cons(y, l)) → REV1(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
REV2(x, cons(y, l)) → REV2(y, l)

The TRS R consists of the following rules:

rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))

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 2 SCCs with 1 less node.

(4) Complex Obligation (AND)

(5) Obligation:

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

REV1(x, cons(y, l)) → REV1(y, l)

The TRS R consists of the following rules:

rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))

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

(6) QDPSizeChangeProof (EQUIVALENT transformation)

We used the following order and afs together with the size-change analysis [AAECC05] to show that there are no infinite chains for this DP problem.

Order:Homeomorphic Embedding Order

AFS:
cons(x1, x2)  =  cons(x2)

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

• REV1(x, cons(y, l)) → REV1(y, l) (allowed arguments on rhs = {1, 2})
  The graph contains the following edges 2 > 2

We oriented the following set of usable rules [AAECC05,FROCOS05]. none

(7) TRUE

(8) Obligation:

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

REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
REV2(x, cons(y, l)) → REV2(y, l)

The TRS R consists of the following rules:

rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))

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

(9) QDPSizeChangeProof (EQUIVALENT transformation)

We used the following order and afs together with the size-change analysis [AAECC05] to show that there are no infinite chains for this DP problem.

Order:Combined order from the following AFS and order.
rev2(x1, x2)  =  x2
nil  =  nil
cons(x1, x2)  =  cons(x2)
rev(x1)  =  x1
rev1(x1, x2)  =  rev1

Recursive path order with status [RPO].
Quasi-Precedence:

trivial

Status:

nil: multiset
cons₁: multiset
rev1: multiset

AFS:
rev2(x1, x2)  =  x2
nil  =  nil
cons(x1, x2)  =  cons(x2)
rev(x1)  =  x1
rev1(x1, x2)  =  rev1

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

• REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l))) (allowed arguments on rhs = {1})
  The graph contains the following edges 2 >= 1

• REV2(x, cons(y, l)) → REV2(y, l) (allowed arguments on rhs = {1, 2})
  The graph contains the following edges 2 > 2

• REV(cons(x, l)) → REV2(x, l) (allowed arguments on rhs = {1, 2})
  The graph contains the following edges 1 > 2

We oriented the following set of usable rules [AAECC05,FROCOS05].

rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))

(10) TRUE