(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R 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, s(x), s(y)) → gcd(minus(x, y), s(y))
if_gcd(false, s(x), s(y)) → gcd(minus(y, x), s(x))
The relative TRS consists of the following S rules:
rand(x) → rand(s(x))
rand(x) → x
(1) RelTRStoRelADPProof (EQUIVALENT transformation)
We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].
(2) Obligation:
Relative ADP Problem with
absolute ADPs:
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))
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))
gcd(s(x), s(y)) → if_gcd(LE(y, x), s(x), s(y))
if_gcd(true, s(x), s(y)) → GCD(minus(x, y), s(y))
if_gcd(true, s(x), s(y)) → gcd(MINUS(x, y), s(y))
if_gcd(false, s(x), s(y)) → GCD(minus(y, x), s(x))
if_gcd(false, s(x), s(y)) → gcd(MINUS(y, x), s(x))
and relative ADPs:
rand(x) → RAND(s(x))
rand(x) → x
(3) RelADPDepGraphProof (EQUIVALENT transformation)
We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
3 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 3 subproblems.
(4) Complex Obligation (AND)
(5) Obligation:
Relative ADP Problem with
absolute ADPs:
minus(x, s(y)) → pred(MINUS(x, y))
gcd(0, y) → y
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
minus(x, s(y)) → pred(minus(x, y))
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
gcd(s(x), 0) → s(x)
le(0, y) → true
minus(x, 0) → x
if_gcd(true, s(x), s(y)) → gcd(minus(x, y), s(y))
if_gcd(false, s(x), s(y)) → gcd(minus(y, x), s(x))
pred(s(x)) → x
and relative ADPs:
rand(x) → rand(s(x))
rand(x) → x
(6) RelADPCleverAfsProof (SOUND transformation)
We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
MINUS_2 = 0
true =
gcd_2 =
pred_1 =
0 =
le_2 = 0, 1
minus_2 = 1
if_gcd_3 = 0
rand_1 =
false =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
MINUS(x1, x2) = x2
s(x1) = s(x1)
le(x1, x2) = le
0 = 0
false = false
gcd(x1, x2) = gcd(x1, x2)
if_gcd(x1, x2, x3) = if_gcd(x2, x3)
true = true
minus(x1, x2) = minus(x1)
pred(x1) = x1
Recursive path order with status [RPO].
Quasi-Precedence:
0 > [s1, le, false, true] > [gcd2, ifgcd2] > minus1
Status:
s1: multiset
le: []
0: multiset
false: multiset
gcd2: multiset
ifgcd2: multiset
true: multiset
minus1: [1]
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s0(y)) → MINUS(y)
The TRS R consists of the following rules:
le → le
le → false0
gcd0(s0(x), 00) → s0(x)
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(00, y) → y
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
le → true0
minus(x) → x
rand0(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(8) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
le → false0
rand0(x) → x
Used ordering: Polynomial interpretation [POLO]:
POL(00) = 0
POL(MINUS(x1)) = x1
POL(false0) = 0
POL(gcd0(x1, x2)) = 2·x1 + 2·x2
POL(if_gcd(x1, x2)) = 2·x1 + 2·x2
POL(le) = 2
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(rand0(x1)) = 2 + x1
POL(s0(x1)) = x1
POL(true0) = 2
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s0(y)) → MINUS(y)
The TRS R consists of the following rules:
le → le
gcd0(s0(x), 00) → s0(x)
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(00, y) → y
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
le → true0
minus(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(10) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
gcd0(s0(x), 00) → s0(x)
gcd0(00, y) → y
le → true0
Used ordering: Polynomial interpretation [POLO]:
POL(00) = 1
POL(MINUS(x1)) = x1
POL(gcd0(x1, x2)) = 2·x1 + 2·x2
POL(if_gcd(x1, x2)) = 2·x1 + 2·x2
POL(le) = 2
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(rand0(x1)) = x1
POL(s0(x1)) = x1
POL(true0) = 1
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s0(y)) → MINUS(y)
The TRS R consists of the following rules:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
minus(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
MINUS(s0(y)) → MINUS(y)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MINUS(
x1) =
x1
s0(
x1) =
s0(
x1)
le =
le
if_gcd(
x1,
x2) =
if_gcd
gcd0(
x1,
x2) =
gcd0
minus(
x1) =
minus(
x1)
rand0(
x1) =
rand0
pred0(
x1) =
x1
Recursive path order with status [RPO].
Quasi-Precedence:
[ifgcd, gcd0] > [s01, rand0]
[ifgcd, gcd0] > minus1
Status:
s01: multiset
le: multiset
ifgcd: multiset
gcd0: multiset
minus1: multiset
rand0: []
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
minus(x) → x
(13) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
minus(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(15) YES
(16) Obligation:
Relative ADP Problem with
absolute ADPs:
gcd(0, y) → y
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
minus(x, s(y)) → pred(minus(x, y))
le(s(x), 0) → false
gcd(s(x), 0) → s(x)
le(0, y) → true
minus(x, 0) → x
if_gcd(true, s(x), s(y)) → gcd(minus(x, y), s(y))
if_gcd(false, s(x), s(y)) → gcd(minus(y, x), s(x))
le(s(x), s(y)) → LE(x, y)
pred(s(x)) → x
and relative ADPs:
rand(x) → rand(s(x))
rand(x) → x
(17) RelADPCleverAfsProof (SOUND transformation)
We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
true =
gcd_2 =
LE_2 = 1
0 =
le_2 = 0, 1
pred_1 =
if_gcd_3 = 0
minus_2 = 1
rand_1 =
false =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
LE(x1, x2) = LE(x1)
s(x1) = s(x1)
le(x1, x2) = le
0 = 0
false = false
gcd(x1, x2) = gcd(x1, x2)
if_gcd(x1, x2, x3) = if_gcd(x2, x3)
true = true
minus(x1, x2) = minus(x1)
pred(x1) = x1
Recursive path order with status [RPO].
Quasi-Precedence:
0 > false > s1 > [LE1, minus1]
0 > true > s1 > [LE1, minus1]
[gcd2, ifgcd2] > le > false > s1 > [LE1, minus1]
[gcd2, ifgcd2] > le > true > s1 > [LE1, minus1]
Status:
LE1: multiset
s1: multiset
le: []
0: multiset
false: multiset
gcd2: multiset
ifgcd2: multiset
true: multiset
minus1: [1]
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s0(x)) → LE(x)
The TRS R consists of the following rules:
le → le
le → false0
gcd0(s0(x), 00) → s0(x)
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(00, y) → y
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
le → true0
minus(x) → x
rand0(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
le → false0
rand0(x) → x
Used ordering: Polynomial interpretation [POLO]:
POL(00) = 0
POL(LE(x1)) = x1
POL(false0) = 0
POL(gcd0(x1, x2)) = 2·x1 + 2·x2
POL(if_gcd(x1, x2)) = 2·x1 + 2·x2
POL(le) = 2
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(rand0(x1)) = 2 + x1
POL(s0(x1)) = x1
POL(true0) = 2
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s0(x)) → LE(x)
The TRS R consists of the following rules:
le → le
gcd0(s0(x), 00) → s0(x)
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(00, y) → y
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
le → true0
minus(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(21) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
gcd0(s0(x), 00) → s0(x)
gcd0(00, y) → y
le → true0
Used ordering: Polynomial interpretation [POLO]:
POL(00) = 1
POL(LE(x1)) = x1
POL(gcd0(x1, x2)) = 2·x1 + 2·x2
POL(if_gcd(x1, x2)) = 2·x1 + 2·x2
POL(le) = 2
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(rand0(x1)) = x1
POL(s0(x1)) = x1
POL(true0) = 1
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s0(x)) → LE(x)
The TRS R consists of the following rules:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
minus(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(23) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
LE(s0(x)) → LE(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( if_gcd(x1, x2) ) = max{0, 2x1 + x2 - 1} |
POL( gcd0(x1, x2) ) = 2x1 + x2 |
POL( minus(x1) ) = x1 + 1 |
POL( rand0(x1) ) = max{0, -2} |
POL( pred0(x1) ) = max{0, x1 - 2} |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
minus(x) → x
(24) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
minus(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(25) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(26) YES
(27) Obligation:
Relative ADP Problem with
absolute ADPs:
le(s(x), s(y)) → le(x, y)
gcd(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
le(s(x), 0) → false
gcd(s(x), 0) → s(x)
if_gcd(true, s(x), s(y)) → gcd(minus(x, y), s(y))
if_gcd(false, s(x), s(y)) → gcd(minus(y, x), s(x))
if_gcd(false, s(x), s(y)) → GCD(minus(y, x), s(x))
pred(s(x)) → x
gcd(0, y) → y
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
minus(x, s(y)) → pred(minus(x, y))
if_gcd(true, s(x), s(y)) → GCD(minus(x, y), s(y))
le(0, y) → true
minus(x, 0) → x
and relative ADPs:
rand(x) → rand(s(x))
rand(x) → x
(28) RelADPCleverAfsProof (SOUND transformation)
We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.
Furthermore, We use an argument filter [LPAR04].
Filtering:true =
IF_GCD_3 = 0
gcd_2 =
pred_1 =
if_gcd_3 = 0
rand_1 =
false =
GCD_2 =
s_1 =
le_2 = 0, 1
0 =
minus_2 = 1
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
IF_GCD(x1, x2, x3) = IF_GCD(x2, x3)
false = false
s(x1) = s(x1)
GCD(x1, x2) = GCD(x1, x2)
minus(x1, x2) = minus(x1)
le(x1, x2) = le
true = true
0 = 0
gcd(x1, x2) = gcd(x1, x2)
if_gcd(x1, x2, x3) = if_gcd(x2, x3)
pred(x1) = x1
Recursive path order with status [RPO].
Quasi-Precedence:
s1 > [IFGCD2, GCD2] > [false, le, true]
s1 > minus1 > [false, le, true]
s1 > [gcd2, ifgcd2] > [false, le, true]
0 > [false, le, true]
Status:
IFGCD2: multiset
false: multiset
s1: multiset
GCD2: multiset
minus1: multiset
le: []
true: multiset
0: multiset
gcd2: multiset
ifgcd2: multiset
(29) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(s0(x), s0(y)) → GCD0(minus(y), s0(x))
GCD0(s0(x), s0(y)) → IF_GCD(s0(x), s0(y))
IF_GCD(s0(x), s0(y)) → GCD0(minus(x), s0(y))
The TRS R consists of the following rules:
le → le
le → false0
gcd0(s0(x), 00) → s0(x)
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(00, y) → y
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
le → true0
minus(x) → x
rand0(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(30) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
le → false0
gcd0(s0(x), 00) → s0(x)
gcd0(00, y) → y
rand0(x) → x
Used ordering: Polynomial interpretation [POLO]:
POL(00) = 0
POL(GCD0(x1, x2)) = 2·x1 + 2·x2
POL(IF_GCD(x1, x2)) = 2·x1 + 2·x2
POL(false0) = 0
POL(gcd0(x1, x2)) = 2 + x1 + x2
POL(if_gcd(x1, x2)) = 2 + x1 + x2
POL(le) = 2
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(rand0(x1)) = 2 + x1
POL(s0(x1)) = x1
POL(true0) = 2
(31) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(s0(x), s0(y)) → GCD0(minus(y), s0(x))
GCD0(s0(x), s0(y)) → IF_GCD(s0(x), s0(y))
IF_GCD(s0(x), s0(y)) → GCD0(minus(x), s0(y))
The TRS R consists of the following rules:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
le → true0
minus(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(32) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
le → true0
Used ordering: Polynomial interpretation [POLO]:
POL(GCD0(x1, x2)) = 2·x1 + 2·x2
POL(IF_GCD(x1, x2)) = 2·x1 + 2·x2
POL(gcd0(x1, x2)) = x1 + x2
POL(if_gcd(x1, x2)) = x1 + x2
POL(le) = 2
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(rand0(x1)) = x1
POL(s0(x1)) = x1
POL(true0) = 0
(33) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_GCD(s0(x), s0(y)) → GCD0(minus(y), s0(x))
GCD0(s0(x), s0(y)) → IF_GCD(s0(x), s0(y))
IF_GCD(s0(x), s0(y)) → GCD0(minus(x), s0(y))
The TRS R consists of the following rules:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
minus(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(34) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
IF_GCD(s0(x), s0(y)) → GCD0(minus(y), s0(x))
GCD0(s0(x), s0(y)) → IF_GCD(s0(x), s0(y))
IF_GCD(s0(x), s0(y)) → GCD0(minus(x), s0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( if_gcd(x1, x2) ) = 0 |
POL( minus(x1) ) = x1 + 1 |
POL( rand0(x1) ) = max{0, -2} |
POL( pred0(x1) ) = max{0, x1 - 2} |
POL( IF_GCD(x1, x2) ) = 2x1 + x2 |
POL( GCD0(x1, x2) ) = 2x1 + x2 + 1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
minus(x) → x
(35) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
le → le
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
rand0(x) → rand0(s0(x))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
minus(x) → pred0(minus(x))
minus(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(36) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(37) YES