(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
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:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
(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:
LE(s(x), s(y)) → LE(x, y)
MINUS(x, s(y)) → PRED(minus(x, y))
MINUS(x, s(y)) → MINUS(x, y)
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
GCD(s(x), s(y)) → LE(y, x)
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(true, x, y) → MINUS(x, y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
IF_GCD(false, x, y) → MINUS(y, x)
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 4 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(x, s(y)) → MINUS(x, y)
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, 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:
MINUS(x, s(y)) → MINUS(x, y)
R is empty.
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, 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].
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(x, s(y)) → MINUS(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:
- MINUS(x, s(y)) → MINUS(x, y)
The graph contains the following edges 1 >= 1, 2 > 2
(13) YES
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s(x), s(y)) → LE(x, y)
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
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:
LE(s(x), s(y)) → LE(x, y)
R is empty.
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
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].
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s(x), s(y)) → LE(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:
- LE(s(x), s(y)) → LE(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(20) YES
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
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:
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
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].
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(26) NonInfProof (EQUIVALENT transformation)
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that
final constraints are written in
bold face.
For Pair
GCD(
s(
x),
s(
y)) →
IF_GCD(
le(
y,
x),
s(
x),
s(
y)) the following chains were created:
- We consider the chain IF_GCD(true, x2, x3) → GCD(minus(x2, x3), x3), GCD(s(x4), s(x5)) → IF_GCD(le(x5, x4), s(x4), s(x5)) which results in the following constraint:
| (1) (GCD(minus(x2, x3), x3)=GCD(s(x4), s(x5)) ⇒ GCD(s(x4), s(x5))≥IF_GCD(le(x5, x4), s(x4), s(x5))) |
We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:
| (2) (s(x5)=x26∧minus(x2, x26)=s(x4) ⇒ GCD(s(x4), s(x5))≥IF_GCD(le(x5, x4), s(x4), s(x5))) |
We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on minus(x2, x26)=s(x4) which results in the following new constraints:
| (3) (x27=s(x4)∧s(x5)=0 ⇒ GCD(s(x4), s(x5))≥IF_GCD(le(x5, x4), s(x4), s(x5))) |
| (4) (pred(minus(x29, x28))=s(x4)∧s(x5)=s(x28)∧(∀x30,x31:minus(x29, x28)=s(x30)∧s(x31)=x28 ⇒ GCD(s(x30), s(x31))≥IF_GCD(le(x31, x30), s(x30), s(x31))) ⇒ GCD(s(x4), s(x5))≥IF_GCD(le(x5, x4), s(x4), s(x5))) |
We solved constraint (3) using rules (I), (II).We simplified constraint (4) using rules (I), (II), (III), (VII) which results in the following new constraint:
| (5) (minus(x29, x28)=x32∧pred(x32)=s(x4)∧(∀x30,x31:minus(x29, x28)=s(x30)∧s(x31)=x28 ⇒ GCD(s(x30), s(x31))≥IF_GCD(le(x31, x30), s(x30), s(x31))) ⇒ GCD(s(x4), s(x28))≥IF_GCD(le(x28, x4), s(x4), s(x28))) |
We simplified constraint (5) using rule (V) (with possible (I) afterwards) using induction on pred(x32)=s(x4) which results in the following new constraint:
| (6) (x33=s(x4)∧minus(x29, x28)=s(x33)∧(∀x30,x31:minus(x29, x28)=s(x30)∧s(x31)=x28 ⇒ GCD(s(x30), s(x31))≥IF_GCD(le(x31, x30), s(x30), s(x31))) ⇒ GCD(s(x4), s(x28))≥IF_GCD(le(x28, x4), s(x4), s(x28))) |
We simplified constraint (6) using rules (III), (IV) which results in the following new constraint:
| (7) (minus(x29, x28)=s(s(x4)) ⇒ GCD(s(x4), s(x28))≥IF_GCD(le(x28, x4), s(x4), s(x28))) |
We simplified constraint (7) using rule (V) (with possible (I) afterwards) using induction on minus(x29, x28)=s(s(x4)) which results in the following new constraints:
| (8) (x34=s(s(x4)) ⇒ GCD(s(x4), s(0))≥IF_GCD(le(0, x4), s(x4), s(0))) |
| (9) (pred(minus(x36, x35))=s(s(x4))∧(∀x37:minus(x36, x35)=s(s(x37)) ⇒ GCD(s(x37), s(x35))≥IF_GCD(le(x35, x37), s(x37), s(x35))) ⇒ GCD(s(x4), s(s(x35)))≥IF_GCD(le(s(x35), x4), s(x4), s(s(x35)))) |
We simplified constraint (8) using rule (III) which results in the following new constraint:
| (10) (GCD(s(x4), s(0))≥IF_GCD(le(0, x4), s(x4), s(0))) |
We simplified constraint (9) using rules (IV), (VII) which results in the following new constraint:
| (11) (GCD(s(x4), s(s(x35)))≥IF_GCD(le(s(x35), x4), s(x4), s(s(x35)))) |
- We consider the chain IF_GCD(false, x6, x7) → GCD(minus(x7, x6), x6), GCD(s(x8), s(x9)) → IF_GCD(le(x9, x8), s(x8), s(x9)) which results in the following constraint:
| (1) (GCD(minus(x7, x6), x6)=GCD(s(x8), s(x9)) ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9))) |
We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:
| (2) (s(x9)=x39∧minus(x7, x39)=s(x8) ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9))) |
We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on minus(x7, x39)=s(x8) which results in the following new constraints:
| (3) (x40=s(x8)∧s(x9)=0 ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9))) |
| (4) (pred(minus(x42, x41))=s(x8)∧s(x9)=s(x41)∧(∀x43,x44:minus(x42, x41)=s(x43)∧s(x44)=x41 ⇒ GCD(s(x43), s(x44))≥IF_GCD(le(x44, x43), s(x43), s(x44))) ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9))) |
We solved constraint (3) using rules (I), (II).We simplified constraint (4) using rules (I), (II), (III), (VII) which results in the following new constraint:
| (5) (minus(x42, x41)=x45∧pred(x45)=s(x8)∧(∀x43,x44:minus(x42, x41)=s(x43)∧s(x44)=x41 ⇒ GCD(s(x43), s(x44))≥IF_GCD(le(x44, x43), s(x43), s(x44))) ⇒ GCD(s(x8), s(x41))≥IF_GCD(le(x41, x8), s(x8), s(x41))) |
We simplified constraint (5) using rule (V) (with possible (I) afterwards) using induction on pred(x45)=s(x8) which results in the following new constraint:
| (6) (x46=s(x8)∧minus(x42, x41)=s(x46)∧(∀x43,x44:minus(x42, x41)=s(x43)∧s(x44)=x41 ⇒ GCD(s(x43), s(x44))≥IF_GCD(le(x44, x43), s(x43), s(x44))) ⇒ GCD(s(x8), s(x41))≥IF_GCD(le(x41, x8), s(x8), s(x41))) |
We simplified constraint (6) using rules (III), (IV) which results in the following new constraint:
| (7) (minus(x42, x41)=s(s(x8)) ⇒ GCD(s(x8), s(x41))≥IF_GCD(le(x41, x8), s(x8), s(x41))) |
We simplified constraint (7) using rule (V) (with possible (I) afterwards) using induction on minus(x42, x41)=s(s(x8)) which results in the following new constraints:
| (8) (x47=s(s(x8)) ⇒ GCD(s(x8), s(0))≥IF_GCD(le(0, x8), s(x8), s(0))) |
| (9) (pred(minus(x49, x48))=s(s(x8))∧(∀x50:minus(x49, x48)=s(s(x50)) ⇒ GCD(s(x50), s(x48))≥IF_GCD(le(x48, x50), s(x50), s(x48))) ⇒ GCD(s(x8), s(s(x48)))≥IF_GCD(le(s(x48), x8), s(x8), s(s(x48)))) |
We simplified constraint (8) using rule (III) which results in the following new constraint:
| (10) (GCD(s(x8), s(0))≥IF_GCD(le(0, x8), s(x8), s(0))) |
We simplified constraint (9) using rules (IV), (VII) which results in the following new constraint:
| (11) (GCD(s(x8), s(s(x48)))≥IF_GCD(le(s(x48), x8), s(x8), s(s(x48)))) |
For Pair
IF_GCD(
true,
x,
y) →
GCD(
minus(
x,
y),
y) the following chains were created:
- We consider the chain GCD(s(x10), s(x11)) → IF_GCD(le(x11, x10), s(x10), s(x11)), IF_GCD(true, x12, x13) → GCD(minus(x12, x13), x13) which results in the following constraint:
| (1) (IF_GCD(le(x11, x10), s(x10), s(x11))=IF_GCD(true, x12, x13) ⇒ IF_GCD(true, x12, x13)≥GCD(minus(x12, x13), x13)) |
We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
| (2) (le(x11, x10)=true ⇒ IF_GCD(true, s(x10), s(x11))≥GCD(minus(s(x10), s(x11)), s(x11))) |
We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x11, x10)=true which results in the following new constraints:
| (3) (true=true ⇒ IF_GCD(true, s(x52), s(0))≥GCD(minus(s(x52), s(0)), s(0))) |
| (4) (le(x55, x54)=true∧(le(x55, x54)=true ⇒ IF_GCD(true, s(x54), s(x55))≥GCD(minus(s(x54), s(x55)), s(x55))) ⇒ IF_GCD(true, s(s(x54)), s(s(x55)))≥GCD(minus(s(s(x54)), s(s(x55))), s(s(x55)))) |
We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
| (5) (IF_GCD(true, s(x52), s(0))≥GCD(minus(s(x52), s(0)), s(0))) |
We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (le(x55, x54)=true ⇒ IF_GCD(true, s(x54), s(x55))≥GCD(minus(s(x54), s(x55)), s(x55))) with σ = [ ] which results in the following new constraint:
| (6) (IF_GCD(true, s(x54), s(x55))≥GCD(minus(s(x54), s(x55)), s(x55)) ⇒ IF_GCD(true, s(s(x54)), s(s(x55)))≥GCD(minus(s(s(x54)), s(s(x55))), s(s(x55)))) |
For Pair
IF_GCD(
false,
x,
y) →
GCD(
minus(
y,
x),
x) the following chains were created:
- We consider the chain GCD(s(x18), s(x19)) → IF_GCD(le(x19, x18), s(x18), s(x19)), IF_GCD(false, x20, x21) → GCD(minus(x21, x20), x20) which results in the following constraint:
| (1) (IF_GCD(le(x19, x18), s(x18), s(x19))=IF_GCD(false, x20, x21) ⇒ IF_GCD(false, x20, x21)≥GCD(minus(x21, x20), x20)) |
We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
| (2) (le(x19, x18)=false ⇒ IF_GCD(false, s(x18), s(x19))≥GCD(minus(s(x19), s(x18)), s(x18))) |
We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x19, x18)=false which results in the following new constraints:
| (3) (false=false ⇒ IF_GCD(false, s(0), s(s(x57)))≥GCD(minus(s(s(x57)), s(0)), s(0))) |
| (4) (le(x59, x58)=false∧(le(x59, x58)=false ⇒ IF_GCD(false, s(x58), s(x59))≥GCD(minus(s(x59), s(x58)), s(x58))) ⇒ IF_GCD(false, s(s(x58)), s(s(x59)))≥GCD(minus(s(s(x59)), s(s(x58))), s(s(x58)))) |
We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
| (5) (IF_GCD(false, s(0), s(s(x57)))≥GCD(minus(s(s(x57)), s(0)), s(0))) |
We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (le(x59, x58)=false ⇒ IF_GCD(false, s(x58), s(x59))≥GCD(minus(s(x59), s(x58)), s(x58))) with σ = [ ] which results in the following new constraint:
| (6) (IF_GCD(false, s(x58), s(x59))≥GCD(minus(s(x59), s(x58)), s(x58)) ⇒ IF_GCD(false, s(s(x58)), s(s(x59)))≥GCD(minus(s(s(x59)), s(s(x58))), s(s(x58)))) |
To summarize, we get the following constraints P
≥ for the following pairs.
- GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
- (GCD(s(x4), s(0))≥IF_GCD(le(0, x4), s(x4), s(0)))
- (GCD(s(x4), s(s(x35)))≥IF_GCD(le(s(x35), x4), s(x4), s(s(x35))))
- (GCD(s(x8), s(0))≥IF_GCD(le(0, x8), s(x8), s(0)))
- (GCD(s(x8), s(s(x48)))≥IF_GCD(le(s(x48), x8), s(x8), s(s(x48))))
- IF_GCD(true, x, y) → GCD(minus(x, y), y)
- (IF_GCD(true, s(x52), s(0))≥GCD(minus(s(x52), s(0)), s(0)))
- (IF_GCD(true, s(x54), s(x55))≥GCD(minus(s(x54), s(x55)), s(x55)) ⇒ IF_GCD(true, s(s(x54)), s(s(x55)))≥GCD(minus(s(s(x54)), s(s(x55))), s(s(x55))))
- IF_GCD(false, x, y) → GCD(minus(y, x), x)
- (IF_GCD(false, s(0), s(s(x57)))≥GCD(minus(s(s(x57)), s(0)), s(0)))
- (IF_GCD(false, s(x58), s(x59))≥GCD(minus(s(x59), s(x58)), s(x58)) ⇒ IF_GCD(false, s(s(x58)), s(s(x59)))≥GCD(minus(s(s(x59)), s(s(x58))), s(s(x58))))
The constraints for P
> respective P
bound are constructed from P
≥ where we just replace every occurence of "t ≥ s" in P
≥ by "t > s" respective "t ≥
c". Here
c stands for the fresh constant used for P
bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:
POL(0) = 0
POL(GCD(x1, x2)) = -1 + x2
POL(IF_GCD(x1, x2, x3)) = -x1 + x3
POL(c) = -1
POL(false) = 1
POL(le(x1, x2)) = 1
POL(minus(x1, x2)) = 0
POL(pred(x1)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 1
The following pairs are in P
>:
IF_GCD(false, x, y) → GCD(minus(y, x), x)
The following pairs are in P
bound:
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
The following rules are usable:
true → le(0, y)
false → le(s(x), 0)
le(x, y) → le(s(x), s(y))
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(28) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
GCD(
s(
x),
s(
y)) →
IF_GCD(
le(
y,
x),
s(
x),
s(
y)) at position [0] we obtained the following new rules [LPAR04]:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0)) → GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(0), s(s(x0))) → IF_GCD(false, s(0), s(s(x0))) → GCD(s(0), s(s(x0))) → IF_GCD(false, s(0), s(s(x0)))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0))) → GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
(29) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(true, x, y) → GCD(minus(x, y), y)
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(0), s(s(x0))) → IF_GCD(false, s(0), s(s(x0)))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(30) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(31) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(32) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IF_GCD(
true,
x,
y) →
GCD(
minus(
x,
y),
y) at position [0] we obtained the following new rules [LPAR04]:
IF_GCD(true, x0, 0) → GCD(x0, 0) → IF_GCD(true, x0, 0) → GCD(x0, 0)
IF_GCD(true, x0, s(x1)) → GCD(pred(minus(x0, x1)), s(x1)) → IF_GCD(true, x0, s(x1)) → GCD(pred(minus(x0, x1)), s(x1))
(33) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
IF_GCD(true, x0, 0) → GCD(x0, 0)
IF_GCD(true, x0, s(x1)) → GCD(pred(minus(x0, x1)), s(x1))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(34) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(35) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(true, x0, s(x1)) → GCD(pred(minus(x0, x1)), s(x1))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(36) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF_GCD(
true,
x0,
s(
x1)) →
GCD(
pred(
minus(
x0,
x1)),
s(
x1)) we obtained the following new rules [LPAR04]:
IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0)) → IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(minus(s(s(z0)), s(z1))), s(s(z1))) → IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(minus(s(s(z0)), s(z1))), s(s(z1)))
(37) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(minus(s(s(z0)), s(z1))), s(s(z1)))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(38) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(39) Complex Obligation (AND)
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(minus(s(s(z0)), s(z1))), s(s(z1)))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(41) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF_GCD(
true,
s(
s(
z0)),
s(
s(
z1))) →
GCD(
pred(
minus(
s(
s(
z0)),
s(
z1))),
s(
s(
z1))) at position [0,0] we obtained the following new rules [LPAR04]:
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(pred(minus(s(s(z0)), z1))), s(s(z1))) → IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(pred(minus(s(s(z0)), z1))), s(s(z1)))
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(pred(minus(s(s(z0)), z1))), s(s(z1)))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
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.
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(pred(minus(s(s(z0)), z1))), s(s(z1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
| POL( IF_GCD(x1, ..., x3) ) = max{0, x1 + 2x2 - 2} |
| POL( GCD(x1, x2) ) = max{0, 2x1 - 2} |
| POL( pred(x1) ) = max{0, x1 - 1} |
| POL( minus(x1, x2) ) = x1 + 1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(45) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(46) TRUE
(47) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(48) 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.
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
The TRS R consists of the following rules:
minus(x, 0) → x
pred(s(x)) → x
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(50) 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].
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
The TRS R consists of the following rules:
minus(x, 0) → x
pred(s(x)) → x
The set Q consists of the following terms:
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
We have to consider all minimal (P,Q,R)-chains.
(52) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF_GCD(
true,
s(
z0),
s(
0)) →
GCD(
pred(
minus(
s(
z0),
0)),
s(
0)) at position [0,0] we obtained the following new rules [LPAR04]:
IF_GCD(true, s(z0), s(0)) → GCD(pred(s(z0)), s(0)) → IF_GCD(true, s(z0), s(0)) → GCD(pred(s(z0)), s(0))
(53) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(pred(s(z0)), s(0))
The TRS R consists of the following rules:
minus(x, 0) → x
pred(s(x)) → x
The set Q consists of the following terms:
pred(s(x0))
minus(x0, 0)
minus(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:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(pred(s(z0)), s(0))
The TRS R consists of the following rules:
pred(s(x)) → x
The set Q consists of the following terms:
pred(s(x0))
minus(x0, 0)
minus(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].
minus(x0, 0)
minus(x0, s(x1))
(57) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(pred(s(z0)), s(0))
The TRS R consists of the following rules:
pred(s(x)) → x
The set Q consists of the following terms:
pred(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(58) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF_GCD(
true,
s(
z0),
s(
0)) →
GCD(
pred(
s(
z0)),
s(
0)) at position [0] we obtained the following new rules [LPAR04]:
IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0)) → IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0))
(59) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0))
The TRS R consists of the following rules:
pred(s(x)) → x
The set Q consists of the following terms:
pred(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(60) 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.
(61) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0))
R is empty.
The set Q consists of the following terms:
pred(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(62) 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].
pred(s(x0))
(63) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(64) TransformationProof (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IF_GCD(
true,
s(
z0),
s(
0)) →
GCD(
z0,
s(
0)) we obtained the following new rules [LPAR04]:
IF_GCD(true, s(s(y_0)), s(0)) → GCD(s(y_0), s(0)) → IF_GCD(true, s(s(y_0)), s(0)) → GCD(s(y_0), s(0))
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(s(y_0)), s(0)) → GCD(s(y_0), s(0))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(66) TransformationProof (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
GCD(
s(
x0),
s(
0)) →
IF_GCD(
true,
s(
x0),
s(
0)) we obtained the following new rules [LPAR04]:
GCD(s(s(y_0)), s(0)) → IF_GCD(true, s(s(y_0)), s(0)) → GCD(s(s(y_0)), s(0)) → IF_GCD(true, s(s(y_0)), s(0))
(67) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(true, s(s(y_0)), s(0)) → GCD(s(y_0), s(0))
GCD(s(s(y_0)), s(0)) → IF_GCD(true, s(s(y_0)), s(0))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(68) 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:
- GCD(s(s(y_0)), s(0)) → IF_GCD(true, s(s(y_0)), s(0))
The graph contains the following edges 1 >= 2, 2 >= 3
- IF_GCD(true, s(s(y_0)), s(0)) → GCD(s(y_0), s(0))
The graph contains the following edges 2 > 1, 3 >= 2
(69) YES