Termination w.r.t. Q proof of /tmp/tmpfPvG5X/Ex4_Zan97

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

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

  ↳5 QDP

    ↳6 QDPOrderProof (⇔)

    ↳7 QDP

    ↳8 PisEmptyProof (⇔)

    ↳9 TRUE

  ↳10 QDP

    ↳11 QDPOrderProof (⇔)

    ↳12 QDP

    ↳13 PisEmptyProof (⇔)

    ↳14 TRUE

  ↳15 QDP

    ↳16 QDPOrderProof (⇔)

    ↳17 QDP

    ↳18 PisEmptyProof (⇔)

    ↳19 TRUE

(0) Obligation:

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

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

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:

G(s(X)) → G(X)
SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))
SEL(s(X), cons(Y, Z)) → ACTIVATE(Z)
ACTIVATE(n__f(X)) → F(activate(X))
ACTIVATE(n__f(X)) → ACTIVATE(X)
ACTIVATE(n__g(X)) → G(activate(X))
ACTIVATE(n__g(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

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 3 SCCs with 3 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

G(s(X)) → G(X)

The TRS R consists of the following rules:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

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

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

G(s(X)) → G(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Recursive path order with status [RPO].
Precedence:

G₁ > cons₂
0 > s₁ > cons₂
sel₂ > activate₁ > f₁ > n_{_f₁} > cons₂
sel₂ > activate₁ > f₁ > n_{_g₁} > cons₂
sel₂ > activate₁ > g₁ > s₁ > cons₂
sel₂ > activate₁ > g₁ > n_{_g₁} > cons₂

Status:

G₁: multiset
s₁: multiset
f₁: multiset
cons₂: multiset
n_{_f₁}: multiset
n_{_g₁}: multiset
g₁: multiset
0: multiset
sel₂: [1,2]
activate₁: multiset

The following usable rules [FROCOS05] were oriented:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

(7) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

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

(8) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(9) TRUE

(10) Obligation:

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

ACTIVATE(n__g(X)) → ACTIVATE(X)
ACTIVATE(n__f(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__g(X)) → ACTIVATE(X)
ACTIVATE(n__f(X)) → ACTIVATE(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Recursive path order with status [RPO].
Precedence:

0 > s₁ > ACTIVATE₁
sel₂ > activate₁ > f₁ > n_{_g₁} > ACTIVATE₁
sel₂ > activate₁ > f₁ > n_{_f₁} > ACTIVATE₁
sel₂ > activate₁ > f₁ > cons₂ > ACTIVATE₁
sel₂ > activate₁ > g₁ > n_{_g₁} > ACTIVATE₁
sel₂ > activate₁ > g₁ > s₁ > ACTIVATE₁

Status:

ACTIVATE₁: multiset
n_{_g₁}: multiset
n_{_f₁}: multiset
f₁: multiset
cons₂: multiset
g₁: [1]
0: multiset
s₁: multiset
sel₂: [1,2]
activate₁: [1]

The following usable rules [FROCOS05] were oriented:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

(12) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

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

(13) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(14) TRUE

(15) Obligation:

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

SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))

The TRS R consists of the following rules:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

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

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

SEL(s(X), cons(Y, Z)) → SEL(X, activate(Z))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
SEL(x1, x2) = SEL(x1)
s(x1) = s(x1)
cons(x1, x2) = cons(x1, x2)
activate(x1) = activate(x1)
f(x1) = f(x1)
n__f(x1) = n__f(x1)
n__g(x1) = n__g(x1)
g(x1) = g(x1)
0 = 0
sel(x1, x2) = sel(x1, x2)

Recursive path order with status [RPO].
Precedence:

SEL₁ > n_{_f₁}
0 > s₁ > n_{_f₁}
sel₂ > activate₁ > f₁ > cons₂ > n_{_f₁}
sel₂ > activate₁ > f₁ > n_{_g₁} > n_{_f₁}
sel₂ > activate₁ > g₁ > s₁ > n_{_f₁}
sel₂ > activate₁ > g₁ > n_{_g₁} > n_{_f₁}

Status:

SEL₁: [1]
s₁: multiset
cons₂: multiset
activate₁: [1]
f₁: multiset
n_{_f₁}: multiset
n_{_g₁}: multiset
g₁: [1]
0: multiset
sel₂: [1,2]

The following usable rules [FROCOS05] were oriented:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

(17) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(activate(X))
activate(X) → X

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

(18) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) QDPOrderProof (EQUIVALENT transformation)

(7) Obligation:

(8) PisEmptyProof (EQUIVALENT transformation)

(9) TRUE

(10) Obligation:

(11) QDPOrderProof (EQUIVALENT transformation)

(12) Obligation:

(13) PisEmptyProof (EQUIVALENT transformation)

(14) TRUE

(15) Obligation:

(16) QDPOrderProof (EQUIVALENT transformation)

(17) Obligation:

(18) PisEmptyProof (EQUIVALENT transformation)

(19) TRUE