YES
0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
↳5 RelADPP
↳6 RelADPCleverAfsProof (⇒, 54 ms)
↳7 QDP
↳8 MRRProof (⇔, 0 ms)
↳9 QDP
↳10 MRRProof (⇔, 0 ms)
↳11 QDP
↳12 PisEmptyProof (⇔, 0 ms)
↳13 YES
↳14 RelADPP
↳15 RelADPCleverAfsProof (⇒, 46 ms)
↳16 QDP
↳17 MRRProof (⇔, 0 ms)
↳18 QDP
↳19 MRRProof (⇔, 0 ms)
↳20 QDP
↳21 PisEmptyProof (⇔, 0 ms)
↳22 YES
↳23 RelADPP
↳24 RelADPReductionPairProof (⇔, 51 ms)
↳25 RelADPP
↳26 DAbsisEmptyProof (⇔, 0 ms)
↳27 YES
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(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].
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → PRED(minus(x, y))
minus(x, s(y)) → pred(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(x, s(y)) → pred(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, s(y)) → pred(minus(x, y))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(x, 0) → x
pred(s(x)) → x
divL(x, nil) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
MINUS_2 = 0
div_2 = 1
divL_2 =
pred_1 =
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(x2)
s(x1) = s(x1)
div(x1, x2) = div(x1)
minus(x1, x2) = x1
0 = 0
pred(x1) = x1
Recursive path order with status [RPO].
Quasi-Precedence:
[s1, div1]
MINUS1: multiset
s1: multiset
div1: multiset
0: multiset
MINUS(s0(y)) → MINUS(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) → pred0(minus(x))
div(s0(x)) → s0(div(minus(x)))
minus(x) → x
pred0(s0(x)) → x
divL0(x, nil0) → x
divL0(x, cons0(y, xs)) → divL0(div(x), xs)
divL0(x, nil0) → x
POL(00) = 0
POL(MINUS(x1)) = x1
POL(cons0(x1, x2)) = 1 + x1 + x2
POL(div(x1)) = x1
POL(divL0(x1, x2)) = 2 + 2·x1 + 2·x2
POL(minus(x1)) = x1
POL(nil0) = 0
POL(pred0(x1)) = x1
POL(s0(x1)) = x1
MINUS(s0(y)) → MINUS(y)
div(00) → 00
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → pred0(minus(x))
div(s0(x)) → s0(div(minus(x)))
minus(x) → x
pred0(s0(x)) → x
MINUS(s0(y)) → MINUS(y)
div(s0(x)) → s0(div(minus(x)))
pred0(s0(x)) → x
POL(00) = 0
POL(MINUS(x1)) = x1
POL(cons0(x1, x2)) = x1 + x2
POL(div(x1)) = 2·x1
POL(divL0(x1, x2)) = x1 + 2·x2
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(s0(x1)) = 1 + x1
div(00) → 00
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → pred0(minus(x))
minus(x) → x
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, s(y)) → pred(minus(x, y))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(x, 0) → x
pred(s(x)) → x
divL(x, nil) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
div_2 = 1
divL_2 =
0 =
pred_1 =
minus_2 = 1
cons_2 =
DIV_2 = 1
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)
s(x1) = s(x1)
minus(x1, x2) = x1
pred(x1) = x1
0 = 0
div(x1, x2) = div(x1)
Recursive path order with status [RPO].
Quasi-Precedence:
[DIV1, s1, 0, div1]
DIV1: multiset
s1: multiset
0: multiset
div1: multiset
DIV(s0(x)) → DIV(minus(x))
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) → pred0(minus(x))
div(s0(x)) → s0(div(minus(x)))
minus(x) → x
pred0(s0(x)) → x
divL0(x, nil0) → x
divL0(x, cons0(y, xs)) → divL0(div(x), xs)
divL0(x, nil0) → x
POL(00) = 0
POL(DIV(x1)) = x1
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(pred0(x1)) = x1
POL(s0(x1)) = x1
DIV(s0(x)) → DIV(minus(x))
div(00) → 00
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → pred0(minus(x))
div(s0(x)) → s0(div(minus(x)))
minus(x) → x
pred0(s0(x)) → x
DIV(s0(x)) → DIV(minus(x))
minus(x) → x
pred0(s0(x)) → x
POL(00) = 0
POL(DIV(x1)) = x1
POL(cons0(x1, x2)) = x1 + x2
POL(div(x1)) = 2·x1
POL(divL0(x1, x2)) = x1 + 2·x2
POL(minus(x1)) = 1 + x1
POL(pred0(x1)) = x1
POL(s0(x1)) = 2 + x1
div(00) → 00
divL0(z, cons0(x, cons0(y, xs))) → divL0(z, cons0(y, cons0(x, xs)))
minus(x) → pred0(minus(x))
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, s(y)) → pred(minus(x, y))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(x, 0) → x
divL(z, cons(x, cons(y, xs))) → DIVL(z, cons(y, cons(x, xs)))
pred(s(x)) → x
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, s(y)) → pred(minus(x, y))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(x, 0) → x
pred(s(x)) → x
divL(x, nil) → x
POL(0) = 0
POL(DIV(x1, x2)) = 2
POL(DIVL(x1, x2)) = 3·x1 + 3·x2
POL(MINUS(x1, x2)) = 2·x1 + 2·x1·x2
POL(PRED(x1)) = 2 + x1
POL(cons(x1, x2)) = 3 + 2·x2
POL(div(x1, x2)) = 2
POL(divL(x1, x2)) = 2 + 2·x1 + 2·x2
POL(minus(x1, x2)) = 2 + 2·x1 + 2·x2
POL(nil) = 0
POL(pred(x1)) = x1
POL(s(x1)) = x1
div(0, s(y)) → 0
divL(x, cons(y, xs)) → divL(div(x, y), xs)
minus(x, s(y)) → pred(minus(x, y))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(x, 0) → x
divL(z, cons(x, cons(y, xs))) → DIVL(z, cons(y, cons(x, xs)))
pred(s(x)) → x
divL(x, nil) → x