Termination w.r.t. Q proof of /tmp/tmp5j34BW/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: Lexicographic path order with status [LPO].
Precedence:

G₁ > 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₁}
sel₂ > activate₁ > g₁ > 0 > n_{_f₁}

Status:

G₁: [1]
s₁: [1]
f₁: [1]
cons₂: [1,2]
n_{_f₁}: [1]
n_{_g₁}: [1]
g₁: [1]
0: []
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

(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: Lexicographic path order with status [LPO].
Precedence:

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

Status:

ACTIVATE₁: [1]
n_{_g₁}: [1]
n_{_f₁}: [1]
f₁: [1]
cons₂: [1,2]
g₁: [1]
0: []
s₁: [1]
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: Lexicographic path order with status [LPO].
Precedence:

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

Status:

SEL₂: [1,2]
s₁: [1]
cons₂: [1,2]
activate₁: [1]
f₁: [1]
n_{_f₁}: [1]
n_{_g₁}: [1]
g₁: [1]
0: []
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