YES
0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
↳5 RelADPP
↳6 RelADPCleverAfsProof (⇒, 51 ms)
↳7 QDP
↳8 MRRProof (⇔, 0 ms)
↳9 QDP
↳10 MRRProof (⇔, 7 ms)
↳11 QDP
↳12 PisEmptyProof (⇔, 0 ms)
↳13 YES
↳14 RelADPP
↳15 RelADPCleverAfsProof (⇒, 39 ms)
↳16 QDP
↳17 MRRProof (⇔, 0 ms)
↳18 QDP
↳19 MRRProof (⇔, 8 ms)
↳20 QDP
↳21 PisEmptyProof (⇔, 0 ms)
↳22 YES
↳23 RelADPP
↳24 RelADPCleverAfsProof (⇒, 42 ms)
↳25 QDP
↳26 MRRProof (⇔, 0 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 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)
cons(x, cons(y, xs)) → 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)
cons(x, cons(y, xs)) → 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)
minus(x, o) → x
cons(x, cons(y, xs)) → cons(y, cons(x, xs))
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)
minus(x) → x
cons0(x, cons0(y, xs)) → cons0(y, cons0(x, xs))
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) = 1
POL(MINUS(x1)) = 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)
minus(x) → x
cons0(x, cons0(y, xs)) → cons0(y, cons0(x, xs))
div0(s0(x), s0(y)) → s0(div0(minus(x), s0(y)))
minus(s0(x)) → minus(x)
MINUS(s0(x)) → MINUS(x)
divL0(x, cons0(y, xs)) → divL0(div0(x, y), xs)
minus(s0(x)) → minus(x)
POL(MINUS(x1)) = x1
POL(cons0(x1, x2)) = 2 + 2·x1 + x2
POL(div0(x1, x2)) = 1 + x1 + x2
POL(divL0(x1, x2)) = 2·x1 + 2·x2
POL(minus(x1)) = x1
POL(s0(x1)) = 1 + x1
minus(x) → x
cons0(x, cons0(y, xs)) → cons0(y, cons0(x, xs))
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)
minus(x, o) → x
cons(x, cons(y, xs)) → cons(y, cons(x, xs))
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)
minus(x) → x
cons0(x, cons0(y, xs)) → cons0(y, cons0(x, xs))
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)) = 2 + x1 + x2
POL(div(x1)) = x1
POL(divL0(x1, x2)) = 2 + 2·x1 + 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
minus(x) → x
cons0(x, cons0(y, xs)) → cons0(y, cons0(x, xs))
div(s0(x)) → s0(div(minus(x)))
minus(s0(x)) → minus(x)
DIV0(s0(x), s0(y)) → DIV0(minus(x), s0(y))
minus(s0(x)) → minus(x)
POL(00) = 2
POL(DIV0(x1, x2)) = x1 + x2
POL(cons0(x1, x2)) = x1 + x2
POL(div(x1)) = x1
POL(minus(x1)) = x1
POL(s0(x1)) = 1 + 2·x1
div(00) → 00
minus(x) → x
cons0(x, cons0(y, xs)) → 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
cons(x, cons(y, xs)) → cons(y, cons(x, xs))
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 = 0
divL_2 =
0 =
minus_2 = 1
cons_2 =
DIVL_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.
DIVL(x1, x2) = DIVL(x1, x2)
cons(x1, x2) = cons(x1, x2)
div(x1, x2) = x2
0 = 0
s(x1) = x1
minus(x1, x2) = x1
o = o
Recursive path order with status [RPO].
Quasi-Precedence:
cons2 > DIVL2 > 0
o > 0
DIVL2: multiset
cons2: [1,2]
0: multiset
o: multiset
DIVL0(x, cons0(y, xs)) → DIVL0(div(y), xs)
div(s0(y)) → 00
divL0(x, cons0(y, xs)) → divL0(div(y), xs)
minus(x) → x
cons0(x, cons0(y, xs)) → cons0(y, cons0(x, xs))
div(s0(y)) → s0(div(s0(y)))
minus(s0(x)) → minus(x)
divL0(x, nil0) → x
DIVL0(x, cons0(y, xs)) → DIVL0(div(y), xs)
divL0(x, cons0(y, xs)) → divL0(div(y), xs)
minus(x) → x
divL0(x, nil0) → x
POL(00) = 0
POL(DIVL0(x1, x2)) = 2·x1 + 2·x2
POL(cons0(x1, x2)) = 1 + 2·x1 + x2
POL(div(x1)) = x1
POL(divL0(x1, x2)) = 2 + x1 + 2·x2
POL(minus(x1)) = 2 + 2·x1
POL(nil0) = 0
POL(s0(x1)) = x1
div(s0(y)) → 00
cons0(x, cons0(y, xs)) → cons0(y, cons0(x, xs))
div(s0(y)) → s0(div(s0(y)))
minus(s0(x)) → minus(x)