YES
0 RelTRS
↳1 RelTRSSCleanerProof (⇒, 0 ms)
↳2 RelTRS
↳3 RelTRStoRelADPProof (⇔, 0 ms)
↳4 RelADPP
↳5 RelADPDepGraphProof (⇔, 0 ms)
↳6 AND
↳7 RelADPP
↳8 RelADPReductionPairProof (⇔, 60 ms)
↳9 RelADPP
↳10 DAbsisEmptyProof (⇔, 0 ms)
↳11 YES
↳12 RelADPP
↳13 RelADPCleverAfsProof (⇒, 58 ms)
↳14 QDP
↳15 MRRProof (⇔, 4 ms)
↳16 QDP
↳17 DependencyGraphProof (⇔, 0 ms)
↳18 TRUE
le(s(s(x)), s(s(y))) → le(s(x), s(y))
le(s(s(x)), s(s(y))) → le(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))
if_gcd(error, x, y) → if_gcd(error, 0, 0)
pred(s(x)) → 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))
le(s(s(x)), s(s(y))) → le(s(x), s(y))
le(s(s(x)), s(s(y))) → le(x, 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(false, s(x), s(y)) → gcd(minus(y, x), s(x))
gcd(0, y) → 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(error, x, y) → if_gcd(error, 0, 0)
pred(s(x)) → x
We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].
le(s(s(x)), s(s(y))) → LE(s(x), s(y))
le(s(s(x)), s(s(y))) → LE(x, y)
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))
gcd(0, y) → 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(error, x, y) → IF_GCD(error, 0, 0)
pred(s(x)) → x
We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
2 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 2 subproblems.
le(s(s(x)), s(s(y))) → LE(s(x), s(y))
le(s(s(x)), s(s(y))) → LE(x, y)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcd(0, y) → y
minus(x, s(y)) → pred(minus(x, y))
le(s(x), 0) → false
gcd(s(x), 0) → s(x)
le(0, y) → true
if_gcd(true, s(x), s(y)) → gcd(minus(x, y), s(y))
minus(x, 0) → x
if_gcd(false, s(x), s(y)) → gcd(minus(y, x), s(x))
if_gcd(error, x, y) → if_gcd(error, 0, 0)
le(s(x), s(y)) → LE(x, y)
pred(s(x)) → x
We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:
le(s(s(x)), s(s(y))) → LE(s(x), s(y))
le(s(s(x)), s(s(y))) → LE(x, y)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcd(0, y) → y
minus(x, s(y)) → pred(minus(x, y))
le(s(x), 0) → false
gcd(s(x), 0) → s(x)
le(0, y) → true
if_gcd(true, s(x), s(y)) → gcd(minus(x, y), s(y))
minus(x, 0) → x
if_gcd(false, s(x), s(y)) → gcd(minus(y, x), s(x))
if_gcd(error, x, y) → if_gcd(error, 0, 0)
le(s(x), s(y)) → LE(x, y)
pred(s(x)) → x
POL(0) = 0
POL(GCD(x1, x2)) = 2
POL(IF_GCD(x1, x2, x3)) = 2
POL(LE(x1, x2)) = 2 + x1
POL(MINUS(x1, x2)) = 2·x1 + 2·x1·x2
POL(PRED(x1)) = 2
POL(error) = 0
POL(false) = 0
POL(gcd(x1, x2)) = 2 + 3·x1 + 2·x2
POL(if_gcd(x1, x2, x3)) = 2 + 3·x1 + 2·x2 + 2·x3
POL(le(x1, x2)) = 0
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(s(x1)) = 1 + 2·x1
POL(true) = 0
le(s(s(x)), s(s(y))) → le(s(x), s(y))
le(s(x), s(y)) → le(x, y)
le(s(s(x)), s(s(y))) → le(x, 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(error, x, y) → if_gcd(error, 0, 0)
pred(s(x)) → x
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcd(0, y) → y
minus(x, s(y)) → pred(minus(x, y))
le(0, y) → true
minus(x, 0) → x
if_gcd(true, s(x), s(y)) → GCD(minus(x, y), s(y))
gcd(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
if_gcd(false, s(x), s(y)) → GCD(minus(y, x), s(x))
le(s(s(x)), s(s(y))) → le(s(x), s(y))
le(s(x), s(y)) → le(x, y)
le(s(s(x)), s(s(y))) → le(x, 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(error, x, y) → if_gcd(error, 0, 0)
pred(s(x)) → x
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcd(0, y) → y
minus(x, s(y)) → pred(minus(x, y))
le(0, y) → true
minus(x, 0) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
true =
IF_GCD_3 = 0
error =
gcd_2 =
le_2 = 0, 1
0 =
pred_1 =
if_gcd_3 = 0
minus_2 = 1
GCD_2 =
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.
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
pred(x1) = x1
0 = 0
gcd(x1, x2) = gcd(x1, x2)
if_gcd(x1, x2, x3) = if_gcd(x2, x3)
error = error
Recursive path order with status [RPO].
Quasi-Precedence:
[IFGCD2, GCD2] > s1 > [false, minus1, le, true] > [gcd2, ifgcd2] > error > 0
IFGCD2: multiset
false: multiset
s1: [1]
GCD2: multiset
minus1: [1]
le: multiset
true: multiset
0: multiset
gcd2: multiset
ifgcd2: multiset
error: multiset
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))
le → le
le → false0
gcd0(s0(x), 00) → s0(x)
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
if_gcd(x, y) → if_gcd(00, 00)
pred0(s0(x)) → x
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
gcd0(00, y) → y
minus(x) → pred0(minus(x))
le → true0
minus(x) → x
GCD0(s0(x), s0(y)) → IF_GCD(s0(x), s0(y))
le → false0
gcd0(s0(x), 00) → s0(x)
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
pred0(s0(x)) → x
le → true0
minus(x) → x
POL(00) = 0
POL(GCD0(x1, x2)) = 2 + 2·x1 + x2
POL(IF_GCD(x1, x2)) = 2·x1 + x2
POL(false0) = 1
POL(gcd0(x1, x2)) = 2·x1 + x2
POL(if_gcd(x1, x2)) = 2·x1 + x2
POL(le) = 2
POL(minus(x1)) = 1 + x1
POL(pred0(x1)) = x1
POL(s0(x1)) = 2 + 2·x1
POL(true0) = 0
IF_GCD(s0(x), s0(y)) → GCD0(minus(y), s0(x))
IF_GCD(s0(x), s0(y)) → GCD0(minus(x), s0(y))
le → le
if_gcd(x, y) → if_gcd(00, 00)
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
gcd0(00, y) → y
minus(x) → pred0(minus(x))