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

0 QTRS
↳1 QTRSRRRProof (⇔)
↳2 QTRS
↳3 Overlay + Local Confluence (⇔)
↳4 QTRS
↳5 DependencyPairsProof (⇔)
↳6 QDP
↳7 DependencyGraphProof (⇔)
↳8 AND
  ↳9 QDP
    ↳10 UsableRulesProof (⇔)
    ↳11 QDP
    ↳12 ATransformationProof (⇔)
    ↳13 QDP
    ↳14 QReductionProof (⇔)
    ↳15 QDP
    ↳16 MRRProof (⇔)
    ↳17 QDP
    ↳18 DependencyGraphProof (⇔)
    ↳19 TRUE
  ↳20 QDP
    ↳21 UsableRulesProof (⇔)
    ↳22 QDP
    ↳23 ATransformationProof (⇔)
    ↳24 QDP
    ↳25 QReductionProof (⇔)
    ↳26 QDP
    ↳27 MRRProof (⇔)
    ↳28 QDP
    ↳29 DependencyGraphProof (⇔)
    ↳30 TRUE

(0) Obligation:

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

a(f, 0) → a(s, 0)
a(d, 0) → 0
a(d, a(s, x)) → a(s, a(s, a(d, a(p, a(s, x)))))
a(f, a(s, x)) → a(d, a(f, a(p, a(s, x))))
a(p, a(s, x)) → x

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(a(x1, x2)) = x1 + x2   
POL(d) = 0   
POL(f) = 1   
POL(p) = 0   
POL(s) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

a(f, 0) → a(s, 0)


(2) Obligation:

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

a(d, 0) → 0
a(d, a(s, x)) → a(s, a(s, a(d, a(p, a(s, x)))))
a(f, a(s, x)) → a(d, a(f, a(p, a(s, x))))
a(p, a(s, x)) → x

Q is empty.

(3) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(4) Obligation:

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

a(d, 0) → 0
a(d, a(s, x)) → a(s, a(s, a(d, a(p, a(s, x)))))
a(f, a(s, x)) → a(d, a(f, a(p, a(s, x))))
a(p, a(s, x)) → x

The set Q consists of the following terms:

a(d, 0)
a(d, a(s, x0))
a(f, a(s, x0))
a(p, a(s, x0))

(5) DependencyPairsProof (EQUIVALENT transformation)

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

(6) Obligation:

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

A(d, a(s, x)) → A(s, a(s, a(d, a(p, a(s, x)))))
A(d, a(s, x)) → A(s, a(d, a(p, a(s, x))))
A(d, a(s, x)) → A(d, a(p, a(s, x)))
A(d, a(s, x)) → A(p, a(s, x))
A(f, a(s, x)) → A(d, a(f, a(p, a(s, x))))
A(f, a(s, x)) → A(f, a(p, a(s, x)))
A(f, a(s, x)) → A(p, a(s, x))

The TRS R consists of the following rules:

a(d, 0) → 0
a(d, a(s, x)) → a(s, a(s, a(d, a(p, a(s, x)))))
a(f, a(s, x)) → a(d, a(f, a(p, a(s, x))))
a(p, a(s, x)) → x

The set Q consists of the following terms:

a(d, 0)
a(d, a(s, x0))
a(f, a(s, x0))
a(p, a(s, x0))

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

A(d, a(s, x)) → A(d, a(p, a(s, x)))

The TRS R consists of the following rules:

a(d, 0) → 0
a(d, a(s, x)) → a(s, a(s, a(d, a(p, a(s, x)))))
a(f, a(s, x)) → a(d, a(f, a(p, a(s, x))))
a(p, a(s, x)) → x

The set Q consists of the following terms:

a(d, 0)
a(d, a(s, x0))
a(f, a(s, x0))
a(p, a(s, x0))

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

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

(11) Obligation:

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

A(d, a(s, x)) → A(d, a(p, a(s, x)))

The TRS R consists of the following rules:

a(p, a(s, x)) → x

The set Q consists of the following terms:

a(d, 0)
a(d, a(s, x0))
a(f, a(s, x0))
a(p, a(s, x0))

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

(12) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(13) Obligation:

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

d1(s(x)) → d1(p(s(x)))

The TRS R consists of the following rules:

p(s(x)) → x

The set Q consists of the following terms:

d(0)
d(s(x0))
f(s(x0))
p(s(x0))

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

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

d(0)
d(s(x0))
f(s(x0))

(15) Obligation:

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

d1(s(x)) → d1(p(s(x)))

The TRS R consists of the following rules:

p(s(x)) → x

The set Q consists of the following terms:

p(s(x0))

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

(16) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

p(s(x)) → x

Used ordering: Polynomial interpretation [POLO]:

POL(d1(x1)) = x1   
POL(p(x1)) = x1   
POL(s(x1)) = 1 + x1   

(17) Obligation:

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

d1(s(x)) → d1(p(s(x)))

R is empty.
The set Q consists of the following terms:

p(s(x0))

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

(18) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(19) TRUE

(20) Obligation:

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

A(f, a(s, x)) → A(f, a(p, a(s, x)))

The TRS R consists of the following rules:

a(d, 0) → 0
a(d, a(s, x)) → a(s, a(s, a(d, a(p, a(s, x)))))
a(f, a(s, x)) → a(d, a(f, a(p, a(s, x))))
a(p, a(s, x)) → x

The set Q consists of the following terms:

a(d, 0)
a(d, a(s, x0))
a(f, a(s, x0))
a(p, a(s, x0))

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

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

(22) Obligation:

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

A(f, a(s, x)) → A(f, a(p, a(s, x)))

The TRS R consists of the following rules:

a(p, a(s, x)) → x

The set Q consists of the following terms:

a(d, 0)
a(d, a(s, x0))
a(f, a(s, x0))
a(p, a(s, x0))

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

(23) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(24) Obligation:

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

f1(s(x)) → f1(p(s(x)))

The TRS R consists of the following rules:

p(s(x)) → x

The set Q consists of the following terms:

d(0)
d(s(x0))
f(s(x0))
p(s(x0))

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

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

d(0)
d(s(x0))
f(s(x0))

(26) Obligation:

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

f1(s(x)) → f1(p(s(x)))

The TRS R consists of the following rules:

p(s(x)) → x

The set Q consists of the following terms:

p(s(x0))

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

(27) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

p(s(x)) → x

Used ordering: Polynomial interpretation [POLO]:

POL(f1(x1)) = x1   
POL(p(x1)) = x1   
POL(s(x1)) = 1 + x1   

(28) Obligation:

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

f1(s(x)) → f1(p(s(x)))

R is empty.
The set Q consists of the following terms:

p(s(x0))

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

(29) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(30) TRUE