YES
0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
↳5 RelADPP
↳6 RelADPCleverAfsProof (⇒, 55 ms)
↳7 QDP
↳8 MRRProof (⇔, 0 ms)
↳9 QDP
↳10 MRRProof (⇔, 0 ms)
↳11 QDP
↳12 MRRProof (⇔, 0 ms)
↳13 QDP
↳14 PisEmptyProof (⇔, 0 ms)
↳15 YES
↳16 RelADPP
↳17 RelADPCleverAfsProof (⇒, 41 ms)
↳18 QDP
↳19 MRRProof (⇔, 0 ms)
↳20 QDP
↳21 MRRProof (⇔, 0 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
↳25 RelADPP
↳26 RelADPReductionPairProof (⇔, 46 ms)
↳27 RelADPP
↳28 DAbsisEmptyProof (⇔, 0 ms)
↳29 YES
minus(x, o) → x
minus(s(x), s(y)) → minus(x, y)
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
divL(x, nil) → x
divL(x, cons(y, xs)) → divL(div(x, y), xs)
divL(z, cons(x, cons(y, xs))) → divL(z, cons(y, cons(x, xs)))
We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].
minus(x, o) → x
minus(s(x), s(y)) → MINUS(x, y)
div(0, s(y)) → 0
div(s(x), s(y)) → s(DIV(minus(x, y), s(y)))
div(s(x), s(y)) → s(div(MINUS(x, y), s(y)))
divL(x, nil) → x
divL(x, cons(y, xs)) → DIVL(div(x, y), xs)
divL(x, cons(y, xs)) → divL(DIV(x, y), xs)
divL(z, cons(x, cons(y, xs))) → DIVL(z, cons(y, cons(x, xs)))
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.
minus(s(x), s(y)) → MINUS(x, y)
div(0, s(y)) → 0
divL(x, cons(y, xs)) → divL(div(x, y), xs)
divL(z, cons(x, cons(y, xs))) → divL(z, cons(y, cons(x, xs)))
minus(x, o) → x
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
divL(x, nil) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
MINUS_2 = 1
o =
div_2 =
divL_2 =
0 =
minus_2 = 1
cons_2 =
nil =
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)
s(x1) = s(x1)
div(x1, x2) = div(x1, x2)
minus(x1, x2) = minus(x1)
0 = 0
o = o
Recursive path order with status [RPO].
Quasi-Precedence:
div2 > s1 > minus1
div2 > 0
MINUS1: multiset
s1: multiset
div2: [2,1]
minus1: multiset
0: multiset
o: multiset
MINUS(s0(x)) → MINUS(x)
div0(00, s0(y)) → 00
divL0(x, cons0(y, xs)) → divL0(div0(x, y), xs)
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → x
div0(s0(x), s0(y)) → s0(div0(minus(x), s0(y)))
minus(s0(x)) → minus(x)
divL0(x, nil0) → x
div0(00, s0(y)) → 00
divL0(x, nil0) → x
POL(00) = 0
POL(MINUS(x1)) = 2·x1
POL(cons0(x1, x2)) = 1 + 2·x1 + x2
POL(div0(x1, x2)) = 1 + x1 + 2·x2
POL(divL0(x1, x2)) = 2 + 2·x1 + 2·x2
POL(minus(x1)) = x1
POL(nil0) = 0
POL(s0(x1)) = x1
MINUS(s0(x)) → MINUS(x)
divL0(x, cons0(y, xs)) → divL0(div0(x, y), xs)
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → x
div0(s0(x), s0(y)) → s0(div0(minus(x), s0(y)))
minus(s0(x)) → minus(x)
divL0(x, cons0(y, xs)) → divL0(div0(x, y), xs)
POL(MINUS(x1)) = x1
POL(cons0(x1, x2)) = 1 + 2·x1 + x2
POL(div0(x1, x2)) = 1 + x1 + 2·x2
POL(divL0(x1, x2)) = x1 + 2·x2
POL(minus(x1)) = x1
POL(s0(x1)) = x1
MINUS(s0(x)) → MINUS(x)
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → x
div0(s0(x), s0(y)) → s0(div0(minus(x), s0(y)))
minus(s0(x)) → minus(x)
MINUS(s0(x)) → MINUS(x)
minus(s0(x)) → minus(x)
POL(MINUS(x1)) = 2·x1
POL(cons0(x1, x2)) = x1 + x2
POL(div0(x1, x2)) = 2 + x1 + 2·x2
POL(divL0(x1, x2)) = x1 + 2·x2
POL(minus(x1)) = x1
POL(s0(x1)) = 2 + x1
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → x
div0(s0(x), s0(y)) → s0(div0(minus(x), s0(y)))
div(s(x), s(y)) → s(DIV(minus(x, y), s(y)))
div(0, s(y)) → 0
divL(x, cons(y, xs)) → divL(div(x, y), xs)
divL(z, cons(x, cons(y, xs))) → divL(z, cons(y, cons(x, xs)))
minus(x, o) → x
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(s(x), s(y)) → minus(x, y)
divL(x, nil) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
o =
div_2 = 1
divL_2 =
0 =
minus_2 = 1
cons_2 =
DIV_2 =
nil =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
DIV(x1, x2) = DIV(x1, x2)
s(x1) = s(x1)
minus(x1, x2) = x1
o = o
div(x1, x2) = div(x1)
0 = 0
Recursive path order with status [RPO].
Quasi-Precedence:
[s1, div1, 0] > DIV2
DIV2: multiset
s1: [1]
o: multiset
div1: [1]
0: multiset
DIV0(s0(x), s0(y)) → DIV0(minus(x), s0(y))
div(00) → 00
divL0(x, cons0(y, xs)) → divL0(div(x), xs)
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → x
div(s0(x)) → s0(div(minus(x)))
minus(s0(x)) → minus(x)
divL0(x, nil0) → x
divL0(x, cons0(y, xs)) → divL0(div(x), xs)
divL0(x, nil0) → x
POL(00) = 0
POL(DIV0(x1, x2)) = x1 + x2
POL(cons0(x1, x2)) = 1 + 2·x1 + x2
POL(div(x1)) = x1
POL(divL0(x1, x2)) = 2 + 2·x1 + 2·x2
POL(minus(x1)) = x1
POL(nil0) = 0
POL(s0(x1)) = x1
DIV0(s0(x), s0(y)) → DIV0(minus(x), s0(y))
div(00) → 00
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → x
div(s0(x)) → s0(div(minus(x)))
minus(s0(x)) → minus(x)
DIV0(s0(x), s0(y)) → DIV0(minus(x), s0(y))
div(00) → 00
minus(x) → x
minus(s0(x)) → minus(x)
POL(00) = 1
POL(DIV0(x1, x2)) = x1 + x2
POL(cons0(x1, x2)) = 2·x1 + x2
POL(div(x1)) = 2·x1
POL(divL0(x1, x2)) = x1 + 2·x2
POL(minus(x1)) = 1 + x1
POL(s0(x1)) = 2 + x1
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
div(s0(x)) → s0(div(minus(x)))
divL(x, cons(y, xs)) → DIVL(div(x, y), xs)
div(0, s(y)) → 0
divL(x, cons(y, xs)) → divL(div(x, y), xs)
minus(x, o) → x
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(s(x), s(y)) → minus(x, y)
divL(z, cons(x, cons(y, xs))) → DIVL(z, cons(y, cons(x, xs)))
divL(x, nil) → 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:
divL(x, cons(y, xs)) → DIVL(div(x, y), xs)
div(0, s(y)) → 0
divL(x, cons(y, xs)) → divL(div(x, y), xs)
minus(x, o) → x
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(s(x), s(y)) → minus(x, y)
divL(x, nil) → x
POL(0) = 0
POL(DIV(x1, x2)) = 2 + x2
POL(DIVL(x1, x2)) = 2 + 3·x1 + 3·x2
POL(MINUS(x1, x2)) = 2
POL(cons(x1, x2)) = 3 + 2·x2
POL(div(x1, x2)) = 2 + x1
POL(divL(x1, x2)) = 2·x1 + 3·x2
POL(minus(x1, x2)) = x1
POL(nil) = 0
POL(o) = 0
POL(s(x1)) = x1
div(0, s(y)) → 0
divL(x, cons(y, xs)) → divL(div(x, y), xs)
minus(x, o) → x
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(s(x), s(y)) → minus(x, y)
divL(z, cons(x, cons(y, xs))) → DIVL(z, cons(y, cons(x, xs)))
divL(x, nil) → x