(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
P(x) → Q(Q(p(x)))
p(p(x)) → q(q(x))
p(Q(Q(x))) → Q(Q(p(x)))
Q(p(q(x))) → q(p(Q(x)))
q(q(p(x))) → p(q(q(x)))
q(Q(x)) → x
Q(q(x)) → x
p(P(x)) → x
P(p(x)) → x
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(P(x1)) = 2 + x1
POL(Q(x1)) = 1 + x1
POL(p(x1)) = x1
POL(q(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
q(Q(x)) → x
Q(q(x)) → x
p(P(x)) → x
P(p(x)) → x
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
P(x) → Q(Q(p(x)))
p(p(x)) → q(q(x))
p(Q(Q(x))) → Q(Q(p(x)))
Q(p(q(x))) → q(p(Q(x)))
q(q(p(x))) → p(q(q(x)))
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(P(x1)) = 2 + x1
POL(Q(x1)) = x1
POL(p(x1)) = 1 + x1
POL(q(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
P(x) → Q(Q(p(x)))
p(p(x)) → q(q(x))
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
p(Q(Q(x))) → Q(Q(p(x)))
Q(p(q(x))) → q(p(Q(x)))
q(q(p(x))) → p(q(q(x)))
Q is empty.
(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:
P(Q(Q(x))) → Q1(Q(p(x)))
P(Q(Q(x))) → Q1(p(x))
P(Q(Q(x))) → P(x)
Q1(p(q(x))) → Q2(p(Q(x)))
Q1(p(q(x))) → P(Q(x))
Q1(p(q(x))) → Q1(x)
Q2(q(p(x))) → P(q(q(x)))
Q2(q(p(x))) → Q2(q(x))
Q2(q(p(x))) → Q2(x)
The TRS R consists of the following rules:
p(Q(Q(x))) → Q(Q(p(x)))
Q(p(q(x))) → q(p(Q(x)))
q(q(p(x))) → p(q(q(x)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
Q1(p(q(x))) → Q1(x)
Q2(q(p(x))) → Q2(q(x))
Q2(q(p(x))) → Q2(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
Q(p(q(x))) → q(p(Q(x)))
q(q(p(x))) → p(q(q(x)))
p(Q(Q(x))) → Q(Q(p(x)))
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P(Q(Q(x))) → Q1(Q(p(x)))
P(Q(Q(x))) → Q1(p(x))
P(Q(Q(x))) → P(x)
Q1(p(q(x))) → Q2(p(Q(x)))
Q1(p(q(x))) → P(Q(x))
Q2(q(p(x))) → P(q(q(x)))
The TRS R consists of the following rules:
p(Q(Q(x))) → Q(Q(p(x)))
Q(p(q(x))) → q(p(Q(x)))
q(q(p(x))) → p(q(q(x)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(9) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
P(Q(Q(x))) → Q1(Q(p(x)))
P(Q(Q(x))) → Q1(p(x))
P(Q(Q(x))) → P(x)
Q1(p(q(x))) → P(Q(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
| POL( P(x1) ) = max{0, x1 - 2} |
| POL( Q1(x1) ) = max{0, 2x1 - 2} |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
Q(p(q(x))) → q(p(Q(x)))
q(q(p(x))) → p(q(q(x)))
p(Q(Q(x))) → Q(Q(p(x)))
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
Q1(p(q(x))) → Q2(p(Q(x)))
Q2(q(p(x))) → P(q(q(x)))
The TRS R consists of the following rules:
p(Q(Q(x))) → Q(Q(p(x)))
Q(p(q(x))) → q(p(Q(x)))
q(q(p(x))) → p(q(q(x)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(11) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(12) TRUE