0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
↳5 RelADPP
↳6 RelADPCleverAfsProof (⇒, 109 ms)
↳7 QDP
↳8 MRRProof (⇔, 0 ms)
↳9 QDP
↳10 PisEmptyProof (⇔, 0 ms)
↳11 YES
↳12 RelADPP
↳13 RelADPCleverAfsProof (⇒, 87 ms)
↳14 QDP
↳15 MRRProof (⇔, 0 ms)
↳16 QDP
↳17 MRRProof (⇔, 0 ms)
↳18 QDP
↳19 PisEmptyProof (⇔, 0 ms)
↳20 YES
↳21 RelADPP
↳22 RelADPCleverAfsProof (⇒, 100 ms)
↳23 QDP
↳24 MRRProof (⇔, 0 ms)
↳25 QDP
↳26 PisEmptyProof (⇔, 0 ms)
↳27 YES
↳28 RelADPP
↳29 RelADPReductionPairProof (⇔, 108 ms)
↳30 RelADPP
↳31 DAbsisEmptyProof (⇔, 0 ms)
↳32 YES
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → 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))
gcdL(nil) → 0
gcdL(cons(x, nil)) → x
gcdL(cons(x, cons(y, xs))) → gcdL(cons(gcd(x, y), xs))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(y, cons(x, xs)))
We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → LE(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → 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))
gcdL(nil) → 0
gcdL(cons(x, nil)) → x
gcdL(cons(x, cons(y, xs))) → GCDL(cons(gcd(x, y), xs))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(GCD(x, y), xs))
gcdL(cons(x, cons(y, xs))) → GCDL(cons(y, cons(x, xs)))
We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
4 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 4 subproblems.
minus(s(x), s(y)) → MINUS(x, y)
gcdL(cons(x, nil)) → x
gcdL(nil) → 0
le(s(x), 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))
gcd(0, y) → y
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(gcd(x, y), xs))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(y, cons(x, xs)))
le(0, y) → true
minus(x, 0) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
MINUS_2 =
gcdL_1 =
true =
gcd_2 =
0 =
le_2 = 0, 1
minus_2 = 1
if_gcd_3 = 0
cons_2 =
nil =
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) = MINUS(x1, x2)
s(x1) = s(x1)
if_gcd(x1, x2, x3) = if_gcd(x2, x3)
false = false
gcd(x1, x2) = gcd(x1, x2)
minus(x1, x2) = x1
true = true
le(x1, x2) = le
0 = 0
Recursive path order with status [RPO].
Quasi-Precedence:
[ifgcd2, false, gcd2, true, le, 0] > s1
MINUS2: [2,1]
s1: [1]
ifgcd2: multiset
false: multiset
gcd2: multiset
true: multiset
le: []
0: multiset
MINUS0(s0(x), s0(y)) → MINUS0(x, y)
gcdL0(cons0(x, nil0)) → x
gcdL0(nil0) → 00
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))
gcd0(00, y) → y
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(gcd0(x, y), xs))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(y, cons0(x, xs)))
le → true0
minus(s0(x)) → minus(x)
minus(x) → x
MINUS0(s0(x), s0(y)) → MINUS0(x, y)
gcdL0(cons0(x, nil0)) → x
gcdL0(nil0) → 00
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))
gcd0(00, y) → y
le → true0
minus(s0(x)) → minus(x)
POL(00) = 2
POL(MINUS0(x1, x2)) = 2·x1 + 2·x2
POL(cons0(x1, x2)) = x1 + x2
POL(false0) = 1
POL(gcd0(x1, x2)) = x1 + x2
POL(gcdL0(x1)) = 2 + x1
POL(if_gcd(x1, x2)) = x1 + x2
POL(le) = 2
POL(minus(x1)) = x1
POL(nil0) = 1
POL(s0(x1)) = 2 + x1
POL(true0) = 0
le → le
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(gcd0(x, y), xs))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(y, cons0(x, xs)))
minus(x) → x
le(s(x), s(y)) → LE(x, y)
gcdL(cons(x, nil)) → x
gcdL(nil) → 0
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))
gcd(0, y) → y
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(gcd(x, y), xs))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(y, cons(x, xs)))
le(0, y) → true
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
gcdL_1 =
true =
LE_2 =
gcd_2 =
le_2 = 1
0 =
if_gcd_3 = 0
minus_2 = 1
cons_2 =
nil =
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, x2)
s(x1) = s(x1)
gcd(x1, x2) = gcd(x1, x2)
if_gcd(x1, x2, x3) = if_gcd(x2, x3)
le(x1, x2) = le(x1)
true = true
minus(x1, x2) = minus(x1)
false = false
0 = 0
Recursive path order with status [RPO].
Quasi-Precedence:
[gcd2, ifgcd2] > [s1, le1, false] > minus1 > LE2
0 > true > [s1, le1, false] > minus1 > LE2
LE2: [1,2]
s1: multiset
gcd2: multiset
ifgcd2: multiset
le1: [1]
true: multiset
minus1: [1]
false: multiset
0: multiset
LE0(s0(x), s0(y)) → LE0(x, y)
gcdL0(cons0(x, nil0)) → x
gcdL0(nil0) → 00
le(s0(x)) → le(x)
le(s0(x)) → 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))
gcd0(00, y) → y
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(gcd0(x, y), xs))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(y, cons0(x, xs)))
le(00) → true0
minus(s0(x)) → minus(x)
minus(x) → x
gcdL0(cons0(x, nil0)) → x
gcdL0(nil0) → 00
le(s0(x)) → false0
gcd0(s0(x), 00) → s0(x)
gcd0(00, y) → y
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(gcd0(x, y), xs))
le(00) → true0
POL(00) = 1
POL(LE0(x1, x2)) = x1 + x2
POL(cons0(x1, x2)) = 2 + x1 + x2
POL(false0) = 1
POL(gcd0(x1, x2)) = 1 + x1 + x2
POL(gcdL0(x1)) = 2 + x1
POL(if_gcd(x1, x2)) = 1 + x1 + x2
POL(le(x1)) = 2 + x1
POL(minus(x1)) = x1
POL(nil0) = 2
POL(s0(x1)) = 2·x1
POL(true0) = 0
LE0(s0(x), s0(y)) → LE0(x, y)
le(s0(x)) → le(x)
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(y, cons0(x, xs)))
minus(s0(x)) → minus(x)
minus(x) → x
LE0(s0(x), s0(y)) → LE0(x, y)
le(s0(x)) → le(x)
if_gcd(s0(x), s0(y)) → gcd0(minus(x), s0(y))
if_gcd(s0(x), s0(y)) → gcd0(minus(y), s0(x))
minus(s0(x)) → minus(x)
POL(LE0(x1, x2)) = x1 + x2
POL(cons0(x1, x2)) = 2·x1 + x2
POL(gcd0(x1, x2)) = 2 + x1 + x2
POL(gcdL0(x1)) = 2·x1
POL(if_gcd(x1, x2)) = 2 + x1 + x2
POL(le(x1)) = 2·x1
POL(minus(x1)) = x1
POL(s0(x1)) = 1 + 2·x1
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(y, cons0(x, xs)))
minus(x) → 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))
gcdL(cons(x, nil)) → x
gcdL(nil) → 0
le(s(x), 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))
gcd(0, y) → y
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(gcd(x, y), xs))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(y, cons(x, xs)))
le(0, y) → true
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:true =
IF_GCD_3 = 0
gcd_2 =
if_gcd_3 = 0
GCD_2 =
false =
nil =
s_1 =
gcdL_1 =
le_2 = 0
0 =
minus_2 = 1
cons_2 =
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) = x1
le(x1, x2) = le(x2)
true = true
0 = 0
if_gcd(x1, x2, x3) = if_gcd(x2, x3)
gcd(x1, x2) = gcd(x1, x2)
Recursive path order with status [RPO].
Quasi-Precedence:
[s1, le1] > [false, true, 0] > [ifgcd2, gcd2] > [IFGCD2, GCD2]
IFGCD2: multiset
false: multiset
s1: [1]
GCD2: multiset
le1: [1]
true: multiset
0: multiset
ifgcd2: multiset
gcd2: 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))
gcdL0(cons0(x, nil0)) → x
gcdL0(nil0) → 00
le(s0(y)) → le(y)
le(00) → 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))
gcd0(00, y) → y
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(gcd0(x, y), xs))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(y, cons0(x, xs)))
le(y) → true0
minus(s0(x)) → minus(x)
minus(x) → x
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))
gcdL0(cons0(x, nil0)) → x
gcdL0(nil0) → 00
le(s0(y)) → le(y)
le(00) → 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))
gcd0(00, y) → y
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(gcd0(x, y), xs))
le(y) → true0
minus(s0(x)) → minus(x)
minus(x) → x
POL(00) = 2
POL(GCD0(x1, x2)) = 2·x1 + x2
POL(IF_GCD(x1, x2)) = 1 + x1 + x2
POL(cons0(x1, x2)) = 1 + 2·x1 + x2
POL(false0) = 1
POL(gcd0(x1, x2)) = x1 + x2
POL(gcdL0(x1)) = 1 + 2·x1
POL(if_gcd(x1, x2)) = x1 + x2
POL(le(x1)) = 2 + 2·x1
POL(minus(x1)) = 1 + x1
POL(nil0) = 2
POL(s0(x1)) = 2 + 2·x1
POL(true0) = 1
gcd0(s0(x), s0(y)) → if_gcd(s0(x), s0(y))
gcdL0(cons0(x, cons0(y, xs))) → gcdL0(cons0(y, cons0(x, xs)))
gcdL(cons(x, cons(y, xs))) → GCDL(cons(gcd(x, y), xs))
gcdL(cons(x, nil)) → x
gcdL(nil) → 0
le(s(x), 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))
gcd(0, y) → y
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(gcd(x, y), xs))
le(0, y) → true
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
gcdL(cons(x, cons(y, xs))) → GCDL(cons(y, cons(x, xs)))
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:
gcdL(cons(x, cons(y, xs))) → GCDL(cons(gcd(x, y), xs))
gcdL(cons(x, nil)) → x
gcdL(nil) → 0
le(s(x), 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))
gcd(0, y) → y
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(gcd(x, y), xs))
le(0, y) → true
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
POL(0) = 0
POL(GCD(x1, x2)) = 2
POL(GCDL(x1)) = 3 + 3·x1
POL(IF_GCD(x1, x2, x3)) = 2
POL(LE(x1, x2)) = 2
POL(MINUS(x1, x2)) = 2
POL(cons(x1, x2)) = 3 + 3·x1 + x2
POL(false) = 0
POL(gcd(x1, x2)) = x1 + x2
POL(gcdL(x1)) = x1
POL(if_gcd(x1, x2, x3)) = 3·x1 + x2 + x3
POL(le(x1, x2)) = 0
POL(minus(x1, x2)) = x1
POL(nil) = 0
POL(s(x1)) = 3 + x1
POL(true) = 0
gcdL(cons(x, nil)) → x
gcdL(nil) → 0
le(s(x), 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))
gcd(0, y) → y
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
gcdL(cons(x, cons(y, xs))) → gcdL(cons(gcd(x, y), xs))
le(0, y) → true
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
gcdL(cons(x, cons(y, xs))) → GCDL(cons(y, cons(x, xs)))