(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(0) → 0
f(s(0)) → s(0)
f(s(s(x))) → p(h(g(x)))
g(0) → pair(s(0), s(0))
g(s(x)) → h(g(x))
h(x) → pair(+(p(x), q(x)), p(x))
p(pair(x, y)) → x
q(pair(x, y)) → y
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
f(s(s(x))) → +(p(g(x)), q(g(x)))
g(s(x)) → pair(+(p(g(x)), q(g(x))), p(g(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:
F(s(s(x))) → P(h(g(x)))
F(s(s(x))) → H(g(x))
F(s(s(x))) → G(x)
G(s(x)) → H(g(x))
G(s(x)) → G(x)
H(x) → +1(p(x), q(x))
H(x) → P(x)
H(x) → Q(x)
+1(x, s(y)) → +1(x, y)
F(s(s(x))) → +1(p(g(x)), q(g(x)))
F(s(s(x))) → P(g(x))
F(s(s(x))) → Q(g(x))
G(s(x)) → +1(p(g(x)), q(g(x)))
G(s(x)) → P(g(x))
G(s(x)) → Q(g(x))
The TRS R consists of the following rules:
f(0) → 0
f(s(0)) → s(0)
f(s(s(x))) → p(h(g(x)))
g(0) → pair(s(0), s(0))
g(s(x)) → h(g(x))
h(x) → pair(+(p(x), q(x)), p(x))
p(pair(x, y)) → x
q(pair(x, y)) → y
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
f(s(s(x))) → +(p(g(x)), q(g(x)))
g(s(x)) → pair(+(p(g(x)), q(g(x))), p(g(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 2 SCCs with 13 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
+1(x, s(y)) → +1(x, y)
The TRS R consists of the following rules:
f(0) → 0
f(s(0)) → s(0)
f(s(s(x))) → p(h(g(x)))
g(0) → pair(s(0), s(0))
g(s(x)) → h(g(x))
h(x) → pair(+(p(x), q(x)), p(x))
p(pair(x, y)) → x
q(pair(x, y)) → y
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
f(s(s(x))) → +(p(g(x)), q(g(x)))
g(s(x)) → pair(+(p(g(x)), q(g(x))), p(g(x)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(6) MNOCProof (EQUIVALENT transformation)
We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
+1(x, s(y)) → +1(x, y)
The TRS R consists of the following rules:
f(0) → 0
f(s(0)) → s(0)
f(s(s(x))) → p(h(g(x)))
g(0) → pair(s(0), s(0))
g(s(x)) → h(g(x))
h(x) → pair(+(p(x), q(x)), p(x))
p(pair(x, y)) → x
q(pair(x, y)) → y
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
f(s(s(x))) → +(p(g(x)), q(g(x)))
g(s(x)) → pair(+(p(g(x)), q(g(x))), p(g(x)))
The set Q consists of the following terms:
f(0)
f(s(0))
f(s(s(x0)))
g(0)
g(s(x0))
h(x0)
p(pair(x0, x1))
q(pair(x0, x1))
+(x0, 0)
+(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(8) 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.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
+1(x, s(y)) → +1(x, y)
R is empty.
The set Q consists of the following terms:
f(0)
f(s(0))
f(s(s(x0)))
g(0)
g(s(x0))
h(x0)
p(pair(x0, x1))
q(pair(x0, x1))
+(x0, 0)
+(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(10) 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].
f(0)
f(s(0))
f(s(s(x0)))
g(0)
g(s(x0))
h(x0)
p(pair(x0, x1))
q(pair(x0, x1))
+(x0, 0)
+(x0, s(x1))
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
+1(x, s(y)) → +1(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(12) 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:
- +1(x, s(y)) → +1(x, y)
The graph contains the following edges 1 >= 1, 2 > 2
(13) TRUE
(14) 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(0) → 0
f(s(0)) → s(0)
f(s(s(x))) → p(h(g(x)))
g(0) → pair(s(0), s(0))
g(s(x)) → h(g(x))
h(x) → pair(+(p(x), q(x)), p(x))
p(pair(x, y)) → x
q(pair(x, y)) → y
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
f(s(s(x))) → +(p(g(x)), q(g(x)))
g(s(x)) → pair(+(p(g(x)), q(g(x))), p(g(x)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(15) MNOCProof (EQUIVALENT transformation)
We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.
(16) 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(0) → 0
f(s(0)) → s(0)
f(s(s(x))) → p(h(g(x)))
g(0) → pair(s(0), s(0))
g(s(x)) → h(g(x))
h(x) → pair(+(p(x), q(x)), p(x))
p(pair(x, y)) → x
q(pair(x, y)) → y
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
f(s(s(x))) → +(p(g(x)), q(g(x)))
g(s(x)) → pair(+(p(g(x)), q(g(x))), p(g(x)))
The set Q consists of the following terms:
f(0)
f(s(0))
f(s(s(x0)))
g(0)
g(s(x0))
h(x0)
p(pair(x0, x1))
q(pair(x0, x1))
+(x0, 0)
+(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(17) 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.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(s(x)) → G(x)
R is empty.
The set Q consists of the following terms:
f(0)
f(s(0))
f(s(s(x0)))
g(0)
g(s(x0))
h(x0)
p(pair(x0, x1))
q(pair(x0, x1))
+(x0, 0)
+(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(19) 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].
f(0)
f(s(0))
f(s(s(x0)))
g(0)
g(s(x0))
h(x0)
p(pair(x0, x1))
q(pair(x0, x1))
+(x0, 0)
+(x0, s(x1))
(20) 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.
(21) 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
(22) TRUE