(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → f'(y, x, s(x))
The relative TRS consists of the following S rules:
rand(x) → rand(s(x))
rand(x) → x
(1) RelTRStoRelADPProof (EQUIVALENT transformation)
We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].
(2) Obligation:
Relative ADP Problem with
absolute ADPs:
f(g(x)) → g(F(f(x)))
f(g(x)) → g(f(F(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → F'(y, x, s(x))
and relative ADPs:
rand(x) → RAND(s(x))
rand(x) → x
(3) RelADPDepGraphProof (EQUIVALENT transformation)
We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
2 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 2 subproblems.
(4) Complex Obligation (AND)
(5) Obligation:
Relative ADP Problem with
absolute ADPs:
f'(s(x), y, y) → F'(y, x, s(x))
and relative ADPs:
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
rand(x) → rand(s(x))
rand(x) → x
(6) RelADPCleverAfsProof (SOUND transformation)
We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
F'_3 = 2
f_1 =
h_1 =
rand_1 =
f'_3 = 2
g_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.
F'(x1, x2, x3) = F'(x1, x2)
s(x1) = s(x1)
f'(x1, x2, x3) = f'(x1, x2)
Recursive path order with status [RPO].
Quasi-Precedence:
F'2 > s1
f'2 > s1
Status:
F'2: multiset
s1: [1]
f'2: multiset
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F'(s0(x), y) → F'(y, x)
The TRS R consists of the following rules:
f0(g0(x)) → g0(f0(f0(x)))
f'(s0(x), y) → f'(y, x)
f0(h0(x)) → h0(g0(x))
rand0(x) → rand0(s0(x))
rand0(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(8) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
rand0(x) → x
Used ordering: Polynomial interpretation [POLO]:
POL(F'(x1, x2)) = 2·x1 + 2·x2
POL(f'(x1, x2)) = x1 + x2
POL(f0(x1)) = x1
POL(g0(x1)) = x1
POL(h0(x1)) = 2·x1
POL(rand0(x1)) = 2 + x1
POL(s0(x1)) = x1
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F'(s0(x), y) → F'(y, x)
The TRS R consists of the following rules:
f0(g0(x)) → g0(f0(f0(x)))
f'(s0(x), y) → f'(y, x)
f0(h0(x)) → h0(g0(x))
rand0(x) → rand0(s0(x))
Q is empty.
We have to consider all (P,Q,R)-chains.
(10) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F'(s0(x), y) → F'(y, x)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
| POL( g0(x1) ) = max{0, -2} |
| POL( rand0(x1) ) = max{0, -2} |
| POL( F'(x1, x2) ) = x1 + x2 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
f0(g0(x)) → g0(f0(f0(x)))
f'(s0(x), y) → f'(y, x)
f0(h0(x)) → h0(g0(x))
rand0(x) → rand0(s0(x))
(11) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
f0(g0(x)) → g0(f0(f0(x)))
f'(s0(x), y) → f'(y, x)
f0(h0(x)) → h0(g0(x))
rand0(x) → rand0(s0(x))
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(13) YES
(14) Obligation:
Relative ADP Problem with
absolute ADPs:
f(g(x)) → g(F(f(x)))
f(g(x)) → g(f(F(x)))
and relative ADPs:
f'(s(x), y, y) → f'(y, x, s(x))
f(h(x)) → h(g(x))
rand(x) → rand(s(x))
rand(x) → x
(15) RelADPCleverAfsProof (SOUND transformation)
We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
f_1 =
h_1 = 0
F_1 =
rand_1 =
g_1 =
f'_3 = 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.
F(x1) = x1
g(x1) = g(x1)
f(x1) = x1
h(x1) = h
f'(x1, x2, x3) = f'(x1, x3)
s(x1) = s(x1)
Recursive path order with status [RPO].
Quasi-Precedence:
g1 > h
s1 > f'2 > h
Status:
g1: [1]
h: multiset
f'2: multiset
s1: multiset
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F0(g0(x)) → F0(x)
F0(g0(x)) → F0(f0(x))
The TRS R consists of the following rules:
f0(g0(x)) → g0(f0(f0(x)))
f'(s0(x), y) → f'(y, s0(x))
f0(h) → h
rand0(x) → rand0(s0(x))
rand0(x) → x
Q is empty.
We have to consider all (P,Q,R)-chains.
(17) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
rand0(x) → x
Used ordering: Polynomial interpretation [POLO]:
POL(F0(x1)) = x1
POL(f'(x1, x2)) = x1 + x2
POL(f0(x1)) = x1
POL(g0(x1)) = 2·x1
POL(h) = 0
POL(rand0(x1)) = 2 + x1
POL(s0(x1)) = x1
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F0(g0(x)) → F0(x)
F0(g0(x)) → F0(f0(x))
The TRS R consists of the following rules:
f0(g0(x)) → g0(f0(f0(x)))
f'(s0(x), y) → f'(y, s0(x))
f0(h) → h
rand0(x) → rand0(s0(x))
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
F0(g0(x)) → F0(x)
F0(g0(x)) → F0(f0(x))
Used ordering: Polynomial interpretation [POLO]:
POL(F0(x1)) = 2·x1
POL(f'(x1, x2)) = x1 + x2
POL(f0(x1)) = x1
POL(g0(x1)) = 1 + 2·x1
POL(h) = 2
POL(rand0(x1)) = x1
POL(s0(x1)) = x1
(20) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
f0(g0(x)) → g0(f0(f0(x)))
f'(s0(x), y) → f'(y, s0(x))
f0(h) → h
rand0(x) → rand0(s0(x))
Q is empty.
We have to consider all (P,Q,R)-chains.
(21) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(22) YES