(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
Q is empty.
(1) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
+1(x, s(y)) → +1(x, y)
*1(x, s(y)) → +1(*(x, y), x)
*1(x, s(y)) → *1(x, y)
GE(s(x), s(y)) → GE(x, y)
-1(s(x), s(y)) → -1(x, y)
FACT(x) → IFFACT(x, ge(x, s(s(0))))
FACT(x) → GE(x, s(s(0)))
IFFACT(x, true) → *1(x, fact(-(x, s(0))))
IFFACT(x, true) → FACT(-(x, s(0)))
IFFACT(x, true) → -1(x, s(0))
The TRS R consists of the following rules:
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 4 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
-1(s(x), s(y)) → -1(x, y)
The TRS R consists of the following rules:
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
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(s(x), s(y)) → -1(x, y)
R is empty.
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
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].
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
-1(s(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(s(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:
GE(s(x), s(y)) → GE(x, y)
The TRS R consists of the following rules:
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
We have to consider all minimal (P,Q,R)-chains.
(15) 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.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
R is empty.
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
We have to consider all minimal (P,Q,R)-chains.
(17) 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].
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(19) 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:
- GE(s(x), s(y)) → GE(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(20) TRUE
(21) 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:
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
We have to consider all minimal (P,Q,R)-chains.
(22) 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.
(23) 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:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
We have to consider all minimal (P,Q,R)-chains.
(24) 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].
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
(25) 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.
(26) 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
(27) TRUE
(28) 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:
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
We have to consider all minimal (P,Q,R)-chains.
(29) 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.
(30) 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:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
We have to consider all minimal (P,Q,R)-chains.
(31) 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].
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
(32) 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.
(33) 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
(34) TRUE
(35) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(x, true) → FACT(-(x, s(0)))
FACT(x) → IFFACT(x, ge(x, s(s(0))))
The TRS R consists of the following rules:
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
We have to consider all minimal (P,Q,R)-chains.
(36) 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.
(37) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(x, true) → FACT(-(x, s(0)))
FACT(x) → IFFACT(x, ge(x, s(s(0))))
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
The set Q consists of the following terms:
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
We have to consider all minimal (P,Q,R)-chains.
(38) 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].
+(x0, 0)
+(x0, s(x1))
*(x0, 0)
*(x0, s(x1))
fact(x0)
iffact(x0, true)
iffact(x0, false)
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(x, true) → FACT(-(x, s(0)))
FACT(x) → IFFACT(x, ge(x, s(s(0))))
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(40) RemovalProof (SOUND transformation)
In the following pairs the term without variables
s(
s(
0)) is replaced by the fresh variable
x_removed.
Pair:
FACT(
x) →
IFFACT(
x,
ge(
x,
s(
s(
0))))
Positions in right side of the pair:
The new variable was added to all pairs as a new argument[CONREM].
(41) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(x, true, x_removed) → FACT(-(x, s(0)), x_removed)
FACT(x, x_removed) → IFFACT(x, ge(x, x_removed), x_removed)
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(42) RemovalProof (SOUND transformation)
In the following pairs the term without variables
s(
s(
0)) is replaced by the fresh variable
x_removed.
Pair:
FACT(
x) →
IFFACT(
x,
ge(
x,
s(
s(
0))))
Positions in right side of the pair:
The new variable was added to all pairs as a new argument[CONREM].
(43) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(x, true, x_removed) → FACT(-(x, s(0)), x_removed)
FACT(x, x_removed) → IFFACT(x, ge(x, x_removed), x_removed)
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(44) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
FACT(
x) →
IFFACT(
x,
ge(
x,
s(
s(
0)))) at position [1] we obtained the following new rules [LPAR04]:
FACT(0) → IFFACT(0, false)
FACT(s(x0)) → IFFACT(s(x0), ge(x0, s(0)))
(45) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(x, true) → FACT(-(x, s(0)))
FACT(0) → IFFACT(0, false)
FACT(s(x0)) → IFFACT(s(x0), ge(x0, s(0)))
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(46) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(47) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FACT(s(x0)) → IFFACT(s(x0), ge(x0, s(0)))
IFFACT(x, true) → FACT(-(x, s(0)))
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(48) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IFFACT(
x,
true) →
FACT(
-(
x,
s(
0))) at position [0] we obtained the following new rules [LPAR04]:
IFFACT(s(x0), true) → FACT(-(x0, 0))
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FACT(s(x0)) → IFFACT(s(x0), ge(x0, s(0)))
IFFACT(s(x0), true) → FACT(-(x0, 0))
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(50) 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.
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FACT(s(x0)) → IFFACT(s(x0), ge(x0, s(0)))
IFFACT(s(x0), true) → FACT(-(x0, 0))
The TRS R consists of the following rules:
-(x, 0) → x
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(52) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IFFACT(
s(
x0),
true) →
FACT(
-(
x0,
0)) at position [0] we obtained the following new rules [LPAR04]:
IFFACT(s(x0), true) → FACT(x0)
(53) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FACT(s(x0)) → IFFACT(s(x0), ge(x0, s(0)))
IFFACT(s(x0), true) → FACT(x0)
The TRS R consists of the following rules:
-(x, 0) → x
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(54) 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.
(55) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FACT(s(x0)) → IFFACT(s(x0), ge(x0, s(0)))
IFFACT(s(x0), true) → FACT(x0)
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
-(x0, 0)
-(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(56) 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].
-(x0, 0)
-(s(x0), s(x1))
(57) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FACT(s(x0)) → IFFACT(s(x0), ge(x0, s(0)))
IFFACT(s(x0), true) → FACT(x0)
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(58) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IFFACT(
s(
x0),
true) →
FACT(
x0) we obtained the following new rules [LPAR04]:
IFFACT(s(s(y_0)), true) → FACT(s(y_0))
(59) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FACT(s(x0)) → IFFACT(s(x0), ge(x0, s(0)))
IFFACT(s(s(y_0)), true) → FACT(s(y_0))
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(60) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
FACT(
s(
x0)) →
IFFACT(
s(
x0),
ge(
x0,
s(
0))) we obtained the following new rules [LPAR04]:
FACT(s(s(y_0))) → IFFACT(s(s(y_0)), ge(s(y_0), s(0)))
(61) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(s(s(y_0)), true) → FACT(s(y_0))
FACT(s(s(y_0))) → IFFACT(s(s(y_0)), ge(s(y_0), s(0)))
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(62) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
FACT(
s(
s(
y_0))) →
IFFACT(
s(
s(
y_0)),
ge(
s(
y_0),
s(
0))) at position [1] we obtained the following new rules [LPAR04]:
FACT(s(s(y_0))) → IFFACT(s(s(y_0)), ge(y_0, 0))
(63) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(s(s(y_0)), true) → FACT(s(y_0))
FACT(s(s(y_0))) → IFFACT(s(s(y_0)), ge(y_0, 0))
The TRS R consists of the following rules:
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x, 0) → true
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(64) 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.
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(s(s(y_0)), true) → FACT(s(y_0))
FACT(s(s(y_0))) → IFFACT(s(s(y_0)), ge(y_0, 0))
The TRS R consists of the following rules:
ge(x, 0) → true
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(66) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
FACT(
s(
s(
y_0))) →
IFFACT(
s(
s(
y_0)),
ge(
y_0,
0)) at position [1] we obtained the following new rules [LPAR04]:
FACT(s(s(y_0))) → IFFACT(s(s(y_0)), true)
(67) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(s(s(y_0)), true) → FACT(s(y_0))
FACT(s(s(y_0))) → IFFACT(s(s(y_0)), true)
The TRS R consists of the following rules:
ge(x, 0) → true
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(68) 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.
(69) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(s(s(y_0)), true) → FACT(s(y_0))
FACT(s(s(y_0))) → IFFACT(s(s(y_0)), true)
R is empty.
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(70) 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].
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
(71) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFFACT(s(s(y_0)), true) → FACT(s(y_0))
FACT(s(s(y_0))) → IFFACT(s(s(y_0)), true)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(72) 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:
- FACT(s(s(y_0))) → IFFACT(s(s(y_0)), true)
The graph contains the following edges 1 >= 1
- IFFACT(s(s(y_0)), true) → FACT(s(y_0))
The graph contains the following edges 1 > 1
(73) TRUE