(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(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:
S(s(0)) → F(0)
S(s(s(0))) → F(s(0))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(s(s(s(0))))))
F(s(s(0))) → S(s(s(s(s(0)))))
F(s(s(0))) → S(s(s(s(0))))
F(s(s(0))) → S(s(s(0)))
G(x) → H(x, x)
S(x) → H(x, 0)
S(x) → H(0, x)
F(g(x)) → G(g(f(x)))
F(g(x)) → G(f(x))
F(g(x)) → F(x)
G(s(x)) → S(s(g(x)))
G(s(x)) → S(g(x))
G(s(x)) → G(x)
H(f(x), g(x)) → F(s(x))
H(f(x), g(x)) → S(x)
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(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 3 less nodes.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(0))) → F(s(0))
F(s(s(0))) → S(s(s(s(s(s(0))))))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(s(s(0)))))
F(s(s(0))) → S(s(s(s(0))))
F(s(s(0))) → S(s(s(0)))
F(g(x)) → G(g(f(x)))
G(x) → H(x, x)
H(f(x), g(x)) → F(s(x))
F(g(x)) → G(f(x))
G(s(x)) → S(s(g(x)))
G(s(x)) → S(g(x))
G(s(x)) → G(x)
F(g(x)) → F(x)
H(f(x), g(x)) → S(x)
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(5) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
S(
s(
s(
0))) →
F(
s(
0)) at position [0] we obtained the following new rules [LPAR04]:
S(s(s(0))) → F(h(0, 0)) → S(s(s(0))) → F(h(0, 0))
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(s(s(s(s(0))))))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(s(s(0)))))
F(s(s(0))) → S(s(s(s(0))))
F(s(s(0))) → S(s(s(0)))
F(g(x)) → G(g(f(x)))
G(x) → H(x, x)
H(f(x), g(x)) → F(s(x))
F(g(x)) → G(f(x))
G(s(x)) → S(s(g(x)))
G(s(x)) → S(g(x))
G(s(x)) → G(x)
F(g(x)) → F(x)
H(f(x), g(x)) → S(x)
S(s(s(0))) → F(h(0, 0))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(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:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(s(s(s(0))))))
F(s(s(0))) → S(s(s(s(s(0)))))
F(s(s(0))) → S(s(s(s(0))))
F(s(s(0))) → S(s(s(0)))
F(g(x)) → G(g(f(x)))
G(x) → H(x, x)
H(f(x), g(x)) → F(s(x))
F(g(x)) → G(f(x))
G(s(x)) → S(s(g(x)))
G(s(x)) → S(g(x))
G(s(x)) → G(x)
F(g(x)) → F(x)
H(f(x), g(x)) → S(x)
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(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.
G(x) → H(x, x)
G(s(x)) → S(s(g(x)))
G(s(x)) → S(g(x))
F(g(x)) → F(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( s(x1) ) = max{0, -1} |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(s(s(s(0))))))
F(s(s(0))) → S(s(s(s(s(0)))))
F(s(s(0))) → S(s(s(s(0))))
F(s(s(0))) → S(s(s(0)))
F(g(x)) → G(g(f(x)))
H(f(x), g(x)) → F(s(x))
F(g(x)) → G(f(x))
G(s(x)) → G(x)
H(f(x), g(x)) → S(x)
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(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 2 SCCs with 4 less nodes.
(12) Complex Obligation (AND)
(13) 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:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(14) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(15) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(s(x)) → G(x)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(16) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- G(s(x)) → G(x)
The graph contains the following edges 1 > 1
(17) YES
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(s(s(s(s(0))))))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(s(s(0)))))
F(s(s(0))) → S(s(s(s(0))))
F(s(s(0))) → S(s(s(0)))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(19) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
s(
s(
0))) →
S(
s(
s(
s(
s(
s(
0)))))) at position [0] we obtained the following new rules [LPAR04]:
F(s(s(0))) → S(h(s(s(s(s(0)))), 0)) → F(s(s(0))) → S(h(s(s(s(s(0)))), 0))
F(s(s(0))) → S(h(0, s(s(s(s(0)))))) → F(s(s(0))) → S(h(0, s(s(s(s(0))))))
F(s(s(0))) → S(s(h(s(s(s(0))), 0))) → F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0)))))) → F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0))))) → F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0)))) → F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0)))))) → F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0))))) → F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0))))) → F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0)))))) → F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0)))))) → F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(s(s(0)))))
F(s(s(0))) → S(s(s(s(0))))
F(s(s(0))) → S(s(s(0)))
F(s(s(0))) → S(h(s(s(s(s(0)))), 0))
F(s(s(0))) → S(h(0, s(s(s(s(0))))))
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(21) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(s(s(s(0)))))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(s(0))))
F(s(s(0))) → S(s(s(0)))
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(23) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
s(
s(
0))) →
S(
s(
s(
s(
s(
0))))) at position [0] we obtained the following new rules [LPAR04]:
F(s(s(0))) → S(h(s(s(s(0))), 0)) → F(s(s(0))) → S(h(s(s(s(0))), 0))
F(s(s(0))) → S(h(0, s(s(s(0))))) → F(s(s(0))) → S(h(0, s(s(s(0)))))
F(s(s(0))) → S(s(f(s(0)))) → F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0))) → F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0))))) → F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0)))) → F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0)))) → F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0))))) → F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0))))) → F(s(s(0))) → S(s(s(s(h(0, 0)))))
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(s(0))))
F(s(s(0))) → S(s(s(0)))
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(h(s(s(s(0))), 0))
F(s(s(0))) → S(h(0, s(s(s(0)))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(25) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(s(s(0))))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(0)))
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(27) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
s(
s(
0))) →
S(
s(
s(
s(
0)))) at position [0] we obtained the following new rules [LPAR04]:
F(s(s(0))) → S(f(s(0))) → F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(h(s(s(0)), 0)) → F(s(s(0))) → S(h(s(s(0)), 0))
F(s(s(0))) → S(h(0, s(s(0)))) → F(s(s(0))) → S(h(0, s(s(0))))
F(s(s(0))) → S(s(f(0))) → F(s(s(0))) → S(s(f(0)))
F(s(s(0))) → S(s(h(s(0), 0))) → F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0)))) → F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0)))) → F(s(s(0))) → S(s(s(h(0, 0))))
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(0)))
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(h(s(s(0)), 0))
F(s(s(0))) → S(h(0, s(s(0))))
F(s(s(0))) → S(s(f(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(29) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(s(0)))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(f(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(31) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
s(
s(
0))) →
S(
s(
s(
0))) at position [0] we obtained the following new rules [LPAR04]:
F(s(s(0))) → S(f(0)) → F(s(s(0))) → S(f(0))
F(s(s(0))) → S(h(s(0), 0)) → F(s(s(0))) → S(h(s(0), 0))
F(s(s(0))) → S(h(0, s(0))) → F(s(s(0))) → S(h(0, s(0)))
F(s(s(0))) → S(s(h(0, 0))) → F(s(s(0))) → S(s(h(0, 0)))
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(f(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0))))
F(s(s(0))) → S(f(0))
F(s(s(0))) → S(h(s(0), 0))
F(s(s(0))) → S(h(0, s(0)))
F(s(s(0))) → S(s(h(0, 0)))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(33) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(f(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0))))
F(s(s(0))) → S(f(0))
F(s(s(0))) → S(s(h(0, 0)))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(35) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
s(
s(
0))) →
S(
f(
0)) at position [0] we obtained the following new rules [LPAR04]:
F(s(s(0))) → S(0) → F(s(s(0))) → S(0)
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(f(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0))))
F(s(s(0))) → S(s(h(0, 0)))
F(s(s(0))) → S(0)
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(37) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(f(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0))))
F(s(s(0))) → S(s(h(0, 0)))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(39) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
s(
s(
0))) →
S(
s(
h(
0,
0))) at position [0] we obtained the following new rules [LPAR04]:
F(s(s(0))) → S(h(h(0, 0), 0)) → F(s(s(0))) → S(h(h(0, 0), 0))
F(s(s(0))) → S(h(0, h(0, 0))) → F(s(s(0))) → S(h(0, h(0, 0)))
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(f(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0))))
F(s(s(0))) → S(h(h(0, 0), 0))
F(s(s(0))) → S(h(0, h(0, 0)))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(41) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(f(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(43) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(s(s(0))) → S(s(f(0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :
POL(h(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(h(0, s(0))))
F(s(s(0))) → S(s(s(h(0, 0))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(45) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(s(s(0))) → S(s(h(0, s(0))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(s(x1)) = | | + | / | -I | 0A | 1A | \ |
| | 0A | 0A | 2A | | |
\ | -I | -I | 1A | / |
| · | x1 |
POL(h(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | -I | 0A | -I | | |
\ | -I | -I | -I | / |
| · | x1 | + | / | -I | 0A | -I | \ |
| | 0A | -I | 2A | | |
\ | -I | -I | -I | / |
| · | x2 |
POL(f(x1)) = | | + | / | 0A | -I | 2A | \ |
| | 0A | -I | 2A | | |
\ | -I | -I | -I | / |
| · | x1 |
POL(g(x1)) = | | + | / | 0A | 0A | 3A | \ |
| | 0A | 0A | 3A | | |
\ | -I | -I | -I | / |
| · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(h(s(0), 0)))
F(s(s(0))) → S(s(s(h(0, 0))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(47) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(s(s(0))) → S(s(h(s(s(s(0))), 0)))
F(s(s(0))) → S(s(h(s(s(0)), 0)))
F(s(s(0))) → S(s(h(s(0), 0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(s(x1)) = | | + | / | 0A | -I | -I | \ |
| | 3A | 0A | 3A | | |
\ | -I | -I | 3A | / |
| · | x1 |
POL(h(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | -I | -I | -I | | |
\ | -I | -I | -I | / |
| · | x1 | + | / | 0A | -I | -I | \ |
| | 3A | -I | 0A | | |
\ | -I | -I | -I | / |
| · | x2 |
POL(f(x1)) = | | + | / | 0A | -I | -I | \ |
| | 3A | -I | -I | | |
\ | -I | -I | -I | / |
| · | x1 |
POL(g(x1)) = | | + | / | 0A | -I | -I | \ |
| | 3A | -I | 0A | | |
\ | -I | -I | -I | / |
| · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(h(0, s(s(0)))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(s(h(0, 0))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(49) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(s(s(0))) → S(s(h(0, s(s(s(0))))))
F(s(s(0))) → S(s(h(0, s(s(0)))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(s(x1)) = | | + | / | -I | -I | -I | \ |
| | 0A | -I | -I | | |
\ | 2A | 3A | 0A | / |
| · | x1 |
POL(h(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | 0A | -I | -I | | |
\ | -I | 3A | -I | / |
| · | x1 | + | / | -I | -I | -I | \ |
| | -I | -I | -I | | |
\ | 2A | 0A | -I | / |
| · | x2 |
POL(f(x1)) = | | + | / | 0A | -I | -I | \ |
| | 0A | 0A | -I | | |
\ | 3A | 3A | -I | / |
| · | x1 |
POL(g(x1)) = | | + | / | 0A | 0A | -I | \ |
| | 0A | -I | -I | | |
\ | 3A | 3A | 0A | / |
| · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(f(s(0)))
F(s(s(0))) → S(s(s(h(0, 0))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(51) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(s(s(0))) → S(s(s(h(s(s(0)), 0))))
F(s(s(0))) → S(s(s(h(0, s(s(0))))))
F(s(s(0))) → S(s(s(s(h(s(0), 0)))))
F(s(s(0))) → S(s(s(s(h(0, s(0))))))
F(s(s(0))) → S(s(s(s(s(h(0, 0))))))
F(s(s(0))) → S(s(s(h(s(0), 0))))
F(s(s(0))) → S(s(s(h(0, s(0)))))
F(s(s(0))) → S(s(s(s(h(0, 0)))))
F(s(s(0))) → S(s(s(h(0, 0))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(s(x1)) = | | + | / | 0A | 0A | -I | \ |
| | -I | 0A | -I | | |
\ | -I | -I | -I | / |
| · | x1 |
POL(f(x1)) = | | + | / | 0A | -I | -I | \ |
| | -I | 0A | -I | | |
\ | -I | -I | -I | / |
| · | x1 |
POL(h(x1, x2)) = | | + | / | -I | 0A | -I | \ |
| | -I | 0A | -I | | |
\ | -I | -I | -I | / |
| · | x1 | + | / | -I | 0A | -I | \ |
| | -I | -I | -I | | |
\ | -I | -I | -I | / |
| · | x2 |
POL(g(x1)) = | | + | / | 0A | 0A | -I | \ |
| | 0A | 0A | -I | | |
\ | -I | -I | 2A | / |
| · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(s(f(0))))
F(s(s(0))) → S(f(s(0)))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(53) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(s(s(0))) → S(f(s(0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(s(x1)) = | | + | / | -I | -I | -I | \ |
| | 0A | 0A | 3A | | |
\ | 0A | -I | -I | / |
| · | x1 |
POL(f(x1)) = | | + | / | 0A | -I | -I | \ |
| | 1A | 0A | -I | | |
\ | -I | -I | -I | / |
| · | x1 |
POL(h(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | -I | 0A | -I | | |
\ | -I | -I | -I | / |
| · | x1 | + | / | -I | -I | -I | \ |
| | 0A | -I | 3A | | |
\ | -I | -I | -I | / |
| · | x2 |
POL(g(x1)) = | | + | / | -I | -I | 0A | \ |
| | 2A | 0A | 3A | | |
\ | -I | -I | 0A | / |
| · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(f(s(0))))
F(s(s(0))) → S(s(s(f(0))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(55) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(s(s(0))) → S(s(f(s(0))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(s(x1)) = | | + | / | -I | -I | 2A | \ |
| | -I | -I | 0A | | |
\ | -I | 0A | 0A | / |
| · | x1 |
POL(f(x1)) = | | + | / | 0A | 2A | 2A | \ |
| | -I | 0A | 0A | | |
\ | -I | -I | 0A | / |
| · | x1 |
POL(h(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | -I | -I | -I | | |
\ | -I | -I | -I | / |
| · | x1 | + | / | -I | -I | 2A | \ |
| | -I | -I | 0A | | |
\ | -I | 0A | 0A | / |
| · | x2 |
POL(g(x1)) = | | + | / | 0A | 2A | 2A | \ |
| | -I | -I | 0A | | |
\ | -I | 0A | 0A | / |
| · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(s(f(0)))))
F(s(s(0))) → S(s(s(f(0))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(57) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(s(s(0))) → S(s(s(f(0))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(s(x1)) = | | + | / | 0A | -I | -I | \ |
| | -I | 0A | 2A | | |
\ | 0A | -I | 0A | / |
| · | x1 |
POL(f(x1)) = | | + | / | 0A | -I | 0A | \ |
| | -I | 1A | -I | | |
\ | 0A | -I | 0A | / |
| · | x1 |
POL(h(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | -I | 0A | 2A | | |
\ | -I | -I | -I | / |
| · | x1 | + | / | 0A | -I | -I | \ |
| | -I | 0A | 2A | | |
\ | -I | -I | 0A | / |
| · | x2 |
POL(g(x1)) = | | + | / | 0A | -I | 0A | \ |
| | 3A | 0A | 3A | | |
\ | 0A | -I | 0A | / |
| · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(s(f(0)))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(59) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
S(s(s(s(s(s(s(s(0)))))))) → F(s(s(0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(s(x1)) = | | + | / | 0A | -I | 0A | \ |
| | -I | -I | 0A | | |
\ | 0A | 0A | -I | / |
| · | x1 |
POL(f(x1)) = | | + | / | 0A | -I | -I | \ |
| | 0A | 0A | -I | | |
\ | 0A | -I | 0A | / |
| · | x1 |
POL(h(x1, x2)) = | | + | / | -I | -I | -I | \ |
| | -I | -I | 0A | | |
\ | 0A | -I | -I | / |
| · | x1 | + | / | 0A | -I | -I | \ |
| | -I | -I | -I | | |
\ | 0A | -I | -I | / |
| · | x2 |
POL(g(x1)) = | | + | / | 0A | 0A | 0A | \ |
| | 0A | -I | 0A | | |
\ | 0A | 0A | 0A | / |
| · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
s(x) → h(x, 0)
s(x) → h(0, x)
s(s(0)) → f(0)
s(s(s(0))) → f(s(0))
f(s(s(0))) → s(s(s(s(s(s(0))))))
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(g(x)) → g(g(f(x)))
g(x) → h(x, x)
h(f(x), g(x)) → f(s(x))
g(s(x)) → s(s(g(x)))
f(0) → 0
f(s(0)) → s(0)
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(s(0))) → S(s(s(f(s(0)))))
F(s(s(0))) → S(s(s(s(f(0)))))
The TRS R consists of the following rules:
s(s(0)) → f(0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
s(s(s(s(s(s(s(s(0)))))))) → f(s(s(0)))
f(s(s(0))) → s(s(s(s(s(s(0))))))
g(x) → h(x, x)
s(x) → h(x, 0)
s(x) → h(0, x)
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
h(f(x), g(x)) → f(s(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(61) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(62) TRUE