0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
↳5 RelADPP
↳6 RelADPCleverAfsProof (⇒, 38 ms)
↳7 QDP
↳8 MRRProof (⇔, 9 ms)
↳9 QDP
↳10 PisEmptyProof (⇔, 0 ms)
↳11 YES
↳12 RelADPP
↳13 RelADPCleverAfsProof (⇒, 38 ms)
↳14 QDP
↳15 MRRProof (⇔, 7 ms)
↳16 QDP
↳17 MRRProof (⇔, 0 ms)
↳18 QDP
↳19 PisEmptyProof (⇔, 0 ms)
↳20 YES
↳21 RelADPP
↳22 RelADPReductionPairProof (⇔, 36 ms)
↳23 RelADPP
↳24 DAbsisEmptyProof (⇔, 0 ms)
↳25 YES
↳26 RelADPP
↳27 RelADPReductionPairProof (⇔, 39 ms)
↳28 RelADPP
↳29 DAbsisEmptyProof (⇔, 0 ms)
↳30 YES
↳31 RelADPP
↳32 RelADPReductionPairProof (⇔, 41 ms)
↳33 RelADPP
↳34 DAbsisEmptyProof (⇔, 0 ms)
↳35 YES
↳36 RelADPP
↳37 RelADPReductionPairProof (⇔, 39 ms)
↳38 RelADPP
↳39 DAbsisEmptyProof (⇔, 0 ms)
↳40 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)
consSwap(x, xs) → cons(x, xs)
divL(z, cons(x, xs)) → divL(z, consSwap(x, xs))
consSwap(x, cons(y, xs)) → cons(y, consSwap(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)
consSwap(x, xs) → cons(x, xs)
divL(z, cons(x, xs)) → DIVL(z, CONSSWAP(x, xs))
consSwap(x, cons(y, xs)) → cons(y, CONSSWAP(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,
3 Lassos,
Result: This relative DT problem is equivalent to 6 subproblems.
minus(s(x), s(y)) → MINUS(x, y)
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
divL(x, cons(y, xs)) → divL(div(x, y), xs)
minus(x, o) → x
divL(z, cons(x, xs)) → divL(z, consSwap(x, xs))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
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 =
consSwap_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
consSwap0(x, xs) → cons0(x, xs)
divL0(x, cons0(y, xs)) → divL0(div0(x, y), xs)
minus(x) → x
divL0(z, cons0(x, xs)) → divL0(z, consSwap0(x, xs))
div0(s0(x), s0(y)) → s0(div0(minus(x), s0(y)))
minus(s0(x)) → minus(x)
consSwap0(x, cons0(y, xs)) → cons0(y, consSwap0(x, xs))
divL0(x, nil0) → x
MINUS(s0(x)) → MINUS(x)
div0(00, s0(y)) → 00
divL0(x, cons0(y, xs)) → divL0(div0(x, y), xs)
minus(s0(x)) → minus(x)
divL0(x, nil0) → x
POL(00) = 0
POL(MINUS(x1)) = x1
POL(cons0(x1, x2)) = 2 + x1 + x2
POL(consSwap0(x1, x2)) = 2 + x1 + x2
POL(div0(x1, x2)) = x1 + 2·x2
POL(divL0(x1, x2)) = 2 + x1 + 2·x2
POL(minus(x1)) = x1
POL(nil0) = 0
POL(s0(x1)) = 1 + x1
consSwap0(x, xs) → cons0(x, xs)
minus(x) → x
divL0(z, cons0(x, xs)) → divL0(z, consSwap0(x, xs))
div0(s0(x), s0(y)) → s0(div0(minus(x), s0(y)))
consSwap0(x, cons0(y, xs)) → cons0(y, consSwap0(x, xs))
div(s(x), s(y)) → s(DIV(minus(x, y), s(y)))
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
divL(x, cons(y, xs)) → divL(div(x, y), xs)
minus(x, o) → x
divL(z, cons(x, xs)) → divL(z, consSwap(x, xs))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
minus(s(x), s(y)) → minus(x, y)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
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 =
consSwap_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
consSwap0(x, xs) → cons0(x, xs)
divL0(x, cons0(y, xs)) → divL0(div(x), xs)
minus(x) → x
divL0(z, cons0(x, xs)) → divL0(z, consSwap0(x, xs))
div(s0(x)) → s0(div(minus(x)))
minus(s0(x)) → minus(x)
consSwap0(x, cons0(y, xs)) → cons0(y, consSwap0(x, xs))
divL0(x, nil0) → x
divL0(x, nil0) → x
POL(00) = 0
POL(DIV0(x1, x2)) = x1 + x2
POL(cons0(x1, x2)) = x1 + x2
POL(consSwap0(x1, x2)) = x1 + x2
POL(div(x1)) = x1
POL(divL0(x1, x2)) = 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
consSwap0(x, xs) → cons0(x, xs)
divL0(x, cons0(y, xs)) → divL0(div(x), xs)
minus(x) → x
divL0(z, cons0(x, xs)) → divL0(z, consSwap0(x, xs))
div(s0(x)) → s0(div(minus(x)))
minus(s0(x)) → minus(x)
consSwap0(x, cons0(y, xs)) → cons0(y, consSwap0(x, xs))
DIV0(s0(x), s0(y)) → DIV0(minus(x), s0(y))
div(00) → 00
minus(s0(x)) → minus(x)
POL(00) = 2
POL(DIV0(x1, x2)) = 2·x1 + x2
POL(cons0(x1, x2)) = 1 + x1 + x2
POL(consSwap0(x1, x2)) = 1 + x1 + x2
POL(div(x1)) = 1 + x1
POL(divL0(x1, x2)) = 2·x1 + 2·x2
POL(minus(x1)) = x1
POL(s0(x1)) = 1 + x1
consSwap0(x, xs) → cons0(x, xs)
divL0(x, cons0(y, xs)) → divL0(div(x), xs)
minus(x) → x
divL0(z, cons0(x, xs)) → divL0(z, consSwap0(x, xs))
div(s0(x)) → s0(div(minus(x)))
consSwap0(x, cons0(y, xs)) → cons0(y, consSwap0(x, xs))
divL(x, cons(y, xs)) → DIVL(div(x, y), xs)
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(z, cons(x, xs)) → DIVL(z, CONSSWAP(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
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(x, nil) → x
POL(0) = 0
POL(CONSSWAP(x1, x2)) = 0
POL(DIV(x1, x2)) = 2 + 2·x1·x2
POL(DIVL(x1, x2)) = 2 + x1 + 3·x2
POL(MINUS(x1, x2)) = 0
POL(cons(x1, x2)) = 3 + 3·x1 + x2
POL(consSwap(x1, x2)) = 3 + 3·x1 + x2
POL(div(x1, x2)) = x1
POL(divL(x1, x2)) = 2·x1
POL(minus(x1, x2)) = x1
POL(nil) = 0
POL(o) = 2
POL(s(x1)) = 1 + x1
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(z, cons(x, xs)) → DIVL(z, CONSSWAP(x, xs))
divL(x, nil) → x
divL(x, cons(y, xs)) → DIVL(div(x, y), xs)
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(z, cons(x, xs)) → DIVL(z, CONSSWAP(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
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(x, nil) → x
POL(0) = 0
POL(CONSSWAP(x1, x2)) = 0
POL(DIV(x1, x2)) = 2 + 2·x1·x2
POL(DIVL(x1, x2)) = 2 + x1 + 3·x2
POL(MINUS(x1, x2)) = 0
POL(cons(x1, x2)) = 3 + 3·x1 + x2
POL(consSwap(x1, x2)) = 3 + 3·x1 + x2
POL(div(x1, x2)) = x1
POL(divL(x1, x2)) = 2·x1
POL(minus(x1, x2)) = x1
POL(nil) = 0
POL(o) = 2
POL(s(x1)) = 1 + x1
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(z, cons(x, xs)) → DIVL(z, CONSSWAP(x, xs))
divL(x, nil) → x
divL(x, cons(y, xs)) → divL(DIV(x, y), xs)
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(z, cons(x, xs)) → DIVL(z, CONSSWAP(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
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(x, nil) → x
POL(0) = 0
POL(CONSSWAP(x1, x2)) = 0
POL(DIV(x1, x2)) = 1
POL(DIVL(x1, x2)) = 2 + 2·x1 + x2
POL(MINUS(x1, x2)) = 2·x1·x2
POL(cons(x1, x2)) = 2 + 3·x2
POL(consSwap(x1, x2)) = 2 + 3·x2
POL(div(x1, x2)) = 2 + x1
POL(divL(x1, x2)) = 2 + 2·x1 + 2·x2
POL(minus(x1, x2)) = x1
POL(nil) = 0
POL(o) = 0
POL(s(x1)) = 3 + x1
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(z, cons(x, xs)) → DIVL(z, CONSSWAP(x, xs))
divL(x, nil) → x
divL(x, nil) → x
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(z, cons(x, xs)) → DIVL(z, CONSSWAP(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:
divL(x, nil) → x
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
POL(0) = 0
POL(CONSSWAP(x1, x2)) = 0
POL(DIV(x1, x2)) = 0
POL(DIVL(x1, x2)) = 1 + 3·x1 + x2
POL(MINUS(x1, x2)) = 2
POL(cons(x1, x2)) = 2 + 3·x2
POL(consSwap(x1, x2)) = 2 + 3·x2
POL(div(x1, x2)) = x1
POL(divL(x1, x2)) = 2 + 2·x1
POL(minus(x1, x2)) = x1
POL(nil) = 0
POL(o) = 0
POL(s(x1)) = 2 + 3·x1
div(0, s(y)) → 0
consSwap(x, xs) → cons(x, xs)
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)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
divL(z, cons(x, xs)) → DIVL(z, CONSSWAP(x, xs))
divL(x, nil) → x