YES
0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
↳5 RelADPP
↳6 RelADPCleverAfsProof (⇒, 44 ms)
↳7 QDP
↳8 MRRProof (⇔, 0 ms)
↳9 QDP
↳10 QDPOrderProof (⇔, 6 ms)
↳11 QDP
↳12 PisEmptyProof (⇔, 0 ms)
↳13 YES
↳14 RelADPP
↳15 RelADPCleverAfsProof (⇒, 28 ms)
↳16 QDP
↳17 MRRProof (⇔, 0 ms)
↳18 QDP
↳19 PisEmptyProof (⇔, 0 ms)
↳20 YES
↳21 RelADPP
↳22 RelADPReductionPairProof (⇔, 41 ms)
↳23 RelADPP
↳24 DAbsisEmptyProof (⇔, 0 ms)
↳25 YES
↳26 RelADPP
↳27 RelADPReductionPairProof (⇔, 33 ms)
↳28 RelADPP
↳29 DAbsisEmptyProof (⇔, 0 ms)
↳30 YES
↳31 RelADPP
↳32 RelADPReductionPairProof (⇔, 36 ms)
↳33 RelADPP
↳34 DAbsisEmptyProof (⇔, 0 ms)
↳35 YES
l(m(x)) → m(l(x))
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
f(x, y) → f(x, r(y))
b → l(b)
We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].
l(m(x)) → M(l(x))
l(m(x)) → m(L(x))
m(r(x)) → r(M(x))
f(m(x), y) → F(x, m(y))
f(m(x), y) → f(x, M(y))
f(x, y) → F(x, r(y))
b → L(B)
We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
3 SCCs with nodes from P_abs,
2 Lassos,
Result: This relative DT problem is equivalent to 5 subproblems.
m(r(x)) → r(M(x))
f(m(x), y) → f(x, m(y))
f(x, y) → f(x, r(y))
l(m(x)) → m(l(x))
b → l(b)
Furthermore, We use an argument filter [LPAR04].
Filtering:r_1 =
M_1 =
b =
m_1 =
f_2 =
l_1 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
M(x1) = x1
r(x1) = r(x1)
Recursive path order with status [RPO].
Quasi-Precedence:
trivial
r1: multiset
M0(r0(x)) → M0(x)
m0(r0(x)) → r0(m0(x))
f0(m0(x), y) → f0(x, m0(y))
f0(x, y) → f0(x, r0(y))
l0(m0(x)) → m0(l0(x))
b0 → l0(b0)
f0(m0(x), y) → f0(x, m0(y))
l0(m0(x)) → m0(l0(x))
POL(M0(x1)) = 2·x1
POL(b0) = 0
POL(f0(x1, x2)) = 2·x1 + x2
POL(l0(x1)) = 2·x1
POL(m0(x1)) = 1 + x1
POL(r0(x1)) = x1
M0(r0(x)) → M0(x)
m0(r0(x)) → r0(m0(x))
f0(x, y) → f0(x, r0(y))
b0 → l0(b0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
M0(r0(x)) → M0(x)
[M01, r01, m01]
M01: [1]
r01: [1]
m01: [1]
f01: multiset
b0: multiset
m0(r0(x)) → r0(m0(x))
f0(x, y) → f0(x, r0(y))
b0 → l0(b0)
m0(r0(x)) → r0(m0(x))
f0(x, y) → f0(x, r0(y))
b0 → l0(b0)
l(m(x)) → m(L(x))
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
f(x, y) → f(x, r(y))
l(m(x)) → m(l(x))
b → l(b)
Furthermore, We use an argument filter [LPAR04].
Filtering:L_1 =
r_1 =
b =
m_1 =
f_2 =
l_1 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
L(x1) = x1
m(x1) = m(x1)
Recursive path order with status [RPO].
Quasi-Precedence:
trivial
m1: multiset
L0(m0(x)) → L0(x)
m0(r0(x)) → r0(m0(x))
f0(m0(x), y) → f0(x, m0(y))
f0(x, y) → f0(x, r0(y))
l0(m0(x)) → m0(l0(x))
b0 → l0(b0)
L0(m0(x)) → L0(x)
f0(m0(x), y) → f0(x, m0(y))
l0(m0(x)) → m0(l0(x))
POL(L0(x1)) = x1
POL(b0) = 0
POL(f0(x1, x2)) = 2·x1 + x2
POL(l0(x1)) = 2·x1
POL(m0(x1)) = 2 + x1
POL(r0(x1)) = x1
m0(r0(x)) → r0(m0(x))
f0(x, y) → f0(x, r0(y))
b0 → l0(b0)
f(m(x), y) → F(x, m(y))
f(x, y) → F(x, r(y))
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
l(m(x)) → m(l(x))
b → l(b)
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:
f(m(x), y) → F(x, m(y))
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
l(m(x)) → m(l(x))
b → l(b)
POL(B) = 3
POL(F(x1, x2)) = 2 + 3·x1
POL(L(x1)) = 2 + 3·x12
POL(M(x1)) = 3
POL(b) = 0
POL(f(x1, x2)) = 2·x1
POL(l(x1)) = x1
POL(m(x1)) = 1 + 2·x1
POL(r(x1)) = 1
f(x, y) → F(x, r(y))
f(m(x), y) → f(x, m(y))
m(r(x)) → r(m(x))
l(m(x)) → m(l(x))
b → l(b)
l(m(x)) → m(L(x))
b → L(B)
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
f(x, y) → f(x, r(y))
l(m(x)) → m(l(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:
l(m(x)) → m(L(x))
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
f(x, y) → f(x, r(y))
l(m(x)) → m(l(x))
POL(B) = 0
POL(F(x1, x2)) = 2
POL(L(x1)) = 3·x1
POL(M(x1)) = 2
POL(b) = 0
POL(f(x1, x2)) = 2·x1
POL(l(x1)) = x1
POL(m(x1)) = 3 + 2·x1
POL(r(x1)) = 0
b → L(B)
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
f(x, y) → f(x, r(y))
l(m(x)) → m(l(x))
l(m(x)) → M(l(x))
b → L(B)
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
f(x, y) → f(x, r(y))
l(m(x)) → m(l(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:
l(m(x)) → M(l(x))
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
f(x, y) → f(x, r(y))
l(m(x)) → m(l(x))
POL(B) = 0
POL(F(x1, x2)) = 2
POL(L(x1)) = 3·x1
POL(M(x1)) = 1
POL(b) = 0
POL(f(x1, x2)) = 3·x1
POL(l(x1)) = 2·x1
POL(m(x1)) = 2 + 2·x1
POL(r(x1)) = 1
b → L(B)
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
f(x, y) → f(x, r(y))
l(m(x)) → m(l(x))