(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(f, a(f, x)) → a(x, g)
a(x, g) → a(f, a(g, a(f, 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:
A(f, a(f, x)) → A(x, g)
A(x, g) → A(f, a(g, a(f, x)))
A(x, g) → A(g, a(f, x))
A(x, g) → A(f, x)
The TRS R consists of the following rules:
a(f, a(f, x)) → a(x, g)
a(x, g) → a(f, a(g, a(f, 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 1 SCC with 1 less node.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A(x, g) → A(f, a(g, a(f, x)))
A(f, a(f, x)) → A(x, g)
A(x, g) → A(f, x)
The TRS R consists of the following rules:
a(f, a(f, x)) → a(x, g)
a(x, g) → a(f, a(g, a(f, x)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(5) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
A(
x,
g) →
A(
f,
a(
g,
a(
f,
x))) at position [1] we obtained the following new rules [LPAR04]:
A(a(f, x0), g) → A(f, a(g, a(x0, g))) → A(a(f, x0), g) → A(f, a(g, a(x0, g)))
A(g, g) → A(f, a(g, a(f, a(g, a(f, f))))) → A(g, g) → A(f, a(g, a(f, a(g, a(f, f)))))
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A(f, a(f, x)) → A(x, g)
A(x, g) → A(f, x)
A(a(f, x0), g) → A(f, a(g, a(x0, g)))
A(g, g) → A(f, a(g, a(f, a(g, a(f, f)))))
The TRS R consists of the following rules:
a(f, a(f, x)) → a(x, g)
a(x, g) → a(f, a(g, a(f, x)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A(x, g) → A(f, x)
A(f, a(f, x)) → A(x, g)
A(a(f, x0), g) → A(f, a(g, a(x0, g)))
The TRS R consists of the following rules:
a(f, a(f, x)) → a(x, g)
a(x, g) → a(f, a(g, a(f, x)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(9) SemLabProof (SOUND transformation)
We found the following model for the rules of the TRSs R and P.
Interpretation over the domain with elements from 0 to 1.
a: 0
f: 0
A: 0
g: 1
By semantic labelling [SEMLAB] we obtain the following labelled QDP problem.
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A.0-1(x, g.) → A.0-0(f., x)
A.0-0(f., a.0-0(f., x)) → A.0-1(x, g.)
A.0-0(f., a.0-1(f., x)) → A.1-1(x, g.)
A.1-1(x, g.) → A.0-1(f., x)
A.0-1(a.0-0(f., x0), g.) → A.0-0(f., a.1-0(g., a.0-1(x0, g.)))
A.0-1(a.0-1(f., x0), g.) → A.0-0(f., a.1-0(g., a.1-1(x0, g.)))
The TRS R consists of the following rules:
a.0-0(f., a.0-0(f., x)) → a.0-1(x, g.)
a.0-0(f., a.0-1(f., x)) → a.1-1(x, g.)
a.0-1(x, g.) → a.0-0(f., a.1-0(g., a.0-0(f., x)))
a.1-1(x, g.) → a.0-0(f., a.1-0(g., a.0-1(f., 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 1 SCC with 2 less nodes.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A.0-0(f., a.0-0(f., x)) → A.0-1(x, g.)
A.0-1(x, g.) → A.0-0(f., x)
A.0-0(f., a.0-1(f., x)) → A.1-1(x, g.)
A.1-1(x, g.) → A.0-1(f., x)
The TRS R consists of the following rules:
a.0-0(f., a.0-0(f., x)) → a.0-1(x, g.)
a.0-0(f., a.0-1(f., x)) → a.1-1(x, g.)
a.0-1(x, g.) → a.0-0(f., a.1-0(g., a.0-0(f., x)))
a.1-1(x, g.) → a.0-0(f., a.1-0(g., a.0-1(f., x)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(13) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
A.0-0(f., a.0-0(f., x)) → A.0-1(x, g.)
A.0-0(f., a.0-1(f., x)) → A.1-1(x, g.)
The following rules are removed from R:
a.0-0(f., a.0-0(f., x)) → a.0-1(x, g.)
a.0-0(f., a.0-1(f., x)) → a.1-1(x, g.)
a.0-1(x, g.) → a.0-0(f., a.1-0(g., a.0-0(f., x)))
a.1-1(x, g.) → a.0-0(f., a.1-0(g., a.0-1(f., x)))
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(A.0-0(x1, x2)) = 1 + x1 + x2
POL(A.0-1(x1, x2)) = 1 + x1 + x2
POL(A.1-1(x1, x2)) = 1 + x1 + x2
POL(a.0-0(x1, x2)) = x1 + x2
POL(a.0-1(x1, x2)) = x1 + x2
POL(f.) = 0
POL(g.) = 0
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A.0-1(x, g.) → A.0-0(f., x)
A.1-1(x, g.) → A.0-1(f., x)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(15) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(16) TRUE