NO Termination proof of rtL-evo.trs

Termination of the given RelTRS could be disproven:

0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 34 ms)
↳4 AND
    ↳5 RelADPP
        ↳6 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳7 QDP
        ↳8 MRRProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 MRRProof (⇔, 4 ms)
        ↳11 QDP
        ↳12 PisEmptyProof (⇔, 0 ms)
        ↳13 YES
    ↳14 RelADPP
        ↳15 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 MRRProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 PisEmptyProof (⇔, 0 ms)
        ↳20 YES
    ↳21 RelADPP
        ↳22 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳23 QDP
        ↳24 MRRProof (⇔, 0 ms)
        ↳25 QDP
        ↳26 TransformationProof (⇔, 0 ms)
        ↳27 QDP
        ↳28 NonTerminationLoopProof (⇒, 0 ms)
        ↳29 NO
    ↳30 RelADPP
        ↳31 RelADPReductionPairProof (⇔, 94 ms)
        ↳32 RelADPP
        ↳33 RelADPDepGraphProof (⇔, 0 ms)
        ↳34 TRUE
    ↳35 RelADPP
        ↳36 RelADPReductionPairProof (⇔, 126 ms)
        ↳37 RelADPP
        ↳38 RelADPDepGraphProof (⇔, 0 ms)
        ↳39 RelADPP
        ↳40 RelADPCleverAfsProof (⇒, 70 ms)
        ↳41 QDP
        ↳42 MRRProof (⇔, 2 ms)
        ↳43 QDP
        ↳44 PisEmptyProof (⇔, 0 ms)
        ↳45 YES
    ↳46 RelADPP
        ↳47 RelADPReductionPairProof (⇔, 126 ms)
        ↳48 RelADPP
        ↳49 RelADPDepGraphProof (⇔, 0 ms)
        ↳50 TRUE
    ↳51 RelADPP
        ↳52 RelADPReductionPairProof (⇔, 127 ms)
        ↳53 RelADPP
        ↳54 RelADPDepGraphProof (⇔, 0 ms)
        ↳55 TRUE
    ↳56 RelADPP
        ↳57 RelADPReductionPairProof (⇔, 141 ms)
        ↳58 RelADPP
        ↳59 RelADPDepGraphProof (⇔, 0 ms)
        ↳60 RelADPP
        ↳61 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳62 QDP
        ↳63 MRRProof (⇔, 0 ms)
        ↳64 QDP
        ↳65 MRRProof (⇔, 12 ms)
        ↳66 QDP
        ↳67 PisEmptyProof (⇔, 0 ms)
        ↳68 YES
    ↳69 RelADPP
        ↳70 RelADPReductionPairProof (⇔, 119 ms)
        ↳71 RelADPP
        ↳72 RelADPDepGraphProof (⇔, 0 ms)
        ↳73 TRUE
    ↳74 RelADPP
        ↳75 RelADPReductionPairProof (⇔, 104 ms)
        ↳76 RelADPP
        ↳77 RelADPDepGraphProof (⇔, 0 ms)
        ↳78 TRUE
    ↳79 RelADPP
        ↳80 RelADPReductionPairProof (⇔, 111 ms)
        ↳81 RelADPP
        ↳82 RelADPDepGraphProof (⇔, 0 ms)
        ↳83 TRUE
    ↳84 RelADPP
        ↳85 RelADPReductionPairProof (⇔, 98 ms)
        ↳86 RelADPP
        ↳87 RelADPDepGraphProof (⇔, 0 ms)
        ↳88 TRUE
    ↳89 RelADPP
        ↳90 RelADPReductionPairProof (⇔, 116 ms)
        ↳91 RelADPP
        ↳92 RelADPDepGraphProof (⇔, 0 ms)
        ↳93 RelADPP
        ↳94 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳95 QDP
        ↳96 MRRProof (⇔, 13 ms)
        ↳97 QDP
        ↳98 PisEmptyProof (⇔, 0 ms)
        ↳99 YES
    ↳100 RelADPP
        ↳101 RelADPReductionPairProof (⇔, 95 ms)
        ↳102 RelADPP
        ↳103 RelADPDepGraphProof (⇔, 0 ms)
        ↳104 RelADPP
        ↳105 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳106 QDP
        ↳107 MRRProof (⇔, 0 ms)
        ↳108 QDP
        ↳109 PisEmptyProof (⇔, 0 ms)
        ↳110 YES
    ↳111 RelADPP
        ↳112 RelADPReductionPairProof (⇔, 95 ms)
        ↳113 RelADPP
        ↳114 RelADPReductionPairProof (⇔, 13 ms)
        ↳115 RelADPP
        ↳116 RelADPDepGraphProof (⇔, 0 ms)
        ↳117 RelADPP
        ↳118 RelADPCleverAfsProof (⇒, 32 ms)
        ↳119 QDP
        ↳120 MRRProof (⇔, 3 ms)
        ↳121 QDP
        ↳122 MRRProof (⇔, 0 ms)
        ↳123 QDP
        ↳124 PisEmptyProof (⇔, 0 ms)
        ↳125 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

top(U(x, y)) → top(check(D(x, y)))
D(x, B) → U(x, B)
F(x, U(O(y), z)) → U(x, F(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
F(x, U(E, y)) → U(x, F(E, y))
D(E, F(x, y)) → F(E, D(x, y))

The relative TRS consists of the following S rules:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
check(F(x, y)) → F(check(x), y)
check(N(x)) → N(check(x))
check(D(x, y)) → D(x, check(y))

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].

(2) Obligation:

Relative ADP Problem with
absolute ADPs:

top(U(x, y)) → TOP(check(D(x, y)))
top(U(x, y)) → top(CHECK(D(x, y)))
top(U(x, y)) → top(check(D1(x, y)))
D(x, B) → U(x, B)
F(x, U(O(y), z)) → U(x, F1(y, z))
F(x, U(N(y), z)) → U(x, F1(y, z))
D(O(x), F(y, z)) → F1(x, D(y, z))
D(O(x), F(y, z)) → F(x, D1(y, z))
D(N(x), F(y, z)) → F1(x, D(y, z))
D(N(x), F(y, z)) → F(x, D1(y, z))
F(x, U(E, y)) → U(x, F1(E, y))
F(x, U(E, y)) → U(x, F(E1, y))
D(E, F(x, y)) → F1(E, D(x, y))
D(E, F(x, y)) → F(E1, D(x, y))
D(E, F(x, y)) → F(E, D1(x, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
E → N(E1)
check(F(x, y)) → F1(x, CHECK(y))
check(U(x, y)) → U(x, CHECK(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))

(3) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
3 SCCs with nodes from P_abs,
12 Lassos,
Result: This relative DT problem is equivalent to 15 subproblems.

(4) Complex Obligation (AND)

(5) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(O(y), z)) → U(x, F1(y, z))
F(x, U(E, y)) → U(x, F1(E, y))
F(x, U(N(y), z)) → U(x, F1(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
check(F(x, y)) → F(check(x), y)
check(N(x)) → N(check(x))
check(D(x, y)) → D(x, check(y))

(6) RelADPDerelatifyingProof (EQUIVALENT 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.

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F1(x, U(O(y), z)) → F1(y, z)
F1(x, U(E, y)) → F1(E, y)
F1(x, U(N(y), z)) → F1(y, z)

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
F(x, U(O(y), z)) → U(x, F(y, z))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

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 dependency pairs:

F1(x, U(O(y), z)) → F1(y, z)

Strictly oriented rules of the TRS R:

F(x, U(O(y), z)) → U(x, F(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))

Used ordering: Polynomial interpretation [POLO]:

POL(B) = 0   
POL(D(x1, x2)) = x1 + x2   
POL(E) = 1   
POL(F(x1, x2)) = 2 + x1 + x2   
POL(F1(x1, x2)) = x1 + x2   
POL(N(x1)) = x1   
POL(O(x1)) = 1 + x1   
POL(U(x1, x2)) = x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = 2·x1   

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F1(x, U(E, y)) → F1(E, y)
F1(x, U(N(y), z)) → F1(y, z)

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(10) 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:

F1(x, U(E, y)) → F1(E, y)
F1(x, U(N(y), z)) → F1(y, z)


Used ordering: Polynomial interpretation [POLO]:

POL(B) = 1   
POL(D(x1, x2)) = 1 + 2·x1 + x2   
POL(E) = 2   
POL(F(x1, x2)) = 2·x1 + x2   
POL(F1(x1, x2)) = x1 + x2   
POL(N(x1)) = x1   
POL(O(x1)) = 2 + 2·x1   
POL(U(x1, x2)) = 1 + 2·x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = x1   

(11) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

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:

D(O(x), F(y, z)) → F(x, D1(y, z))
D(E, F(x, y)) → F(E, D1(x, y))
D(N(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
check(F(x, y)) → F(check(x), y)
check(N(x)) → N(check(x))
check(D(x, y)) → D(x, check(y))

(15) RelADPDerelatifyingProof (EQUIVALENT 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.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(O(x), F(y, z)) → D1(y, z)
D1(E, F(x, y)) → D1(x, y)
D1(N(x), F(y, z)) → D1(y, z)

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
F(x, U(O(y), z)) → U(x, F(y, z))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

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 dependency pairs:

D1(O(x), F(y, z)) → D1(y, z)
D1(E, F(x, y)) → D1(x, y)
D1(N(x), F(y, z)) → D1(y, z)

Strictly oriented rules of the TRS R:

F(x, U(O(y), z)) → U(x, F(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))

Used ordering: Polynomial interpretation [POLO]:

POL(B) = 0   
POL(D(x1, x2)) = 2 + x1 + x2   
POL(D1(x1, x2)) = x1 + x2   
POL(E) = 0   
POL(F(x1, x2)) = 2 + x1 + x2   
POL(N(x1)) = x1   
POL(O(x1)) = 1 + 2·x1   
POL(U(x1, x2)) = 2 + x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = x1   

(18) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(19) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(20) YES

(21) Obligation:

Relative ADP Problem with
absolute ADPs:

top(U(x, y)) → TOP(check(D(x, y)))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
check(F(x, y)) → F(check(x), y)
check(N(x)) → N(check(x))
check(D(x, y)) → D(x, check(y))

(22) RelADPDerelatifyingProof (EQUIVALENT 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.

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TOP(U(x, y)) → TOP(check(D(x, y)))

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
F(x, U(O(y), z)) → U(x, F(y, z))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(24) 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:

F(x, U(O(y), z)) → U(x, F(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))

Used ordering: Polynomial interpretation [POLO]:

POL(B) = 2   
POL(D(x1, x2)) = x1 + 2·x2   
POL(E) = 1   
POL(F(x1, x2)) = x1 + 2·x2   
POL(N(x1)) = x1   
POL(O(x1)) = 1 + 2·x1   
POL(TOP(x1)) = 2·x1   
POL(U(x1, x2)) = x1 + 2·x2   
POL(check(x1)) = x1   
POL(top(x1)) = x1   

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TOP(U(x, y)) → TOP(check(D(x, y)))

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(26) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TOP(U(x, y)) → TOP(check(D(x, y))) at position [0] we obtained the following new rules [LPAR04]:

TOP(U(x0, x1)) → TOP(D(check(x0), x1)) → TOP(U(x0, x1)) → TOP(D(check(x0), x1))
TOP(U(x0, x1)) → TOP(D(x0, check(x1))) → TOP(U(x0, x1)) → TOP(D(x0, check(x1)))
TOP(U(x0, B)) → TOP(check(U(x0, B))) → TOP(U(x0, B)) → TOP(check(U(x0, B)))
TOP(U(E, F(x0, x1))) → TOP(check(F(E, D(x0, x1)))) → TOP(U(E, F(x0, x1))) → TOP(check(F(E, D(x0, x1))))
TOP(U(N(x0), F(x1, x2))) → TOP(check(F(x0, D(x1, x2)))) → TOP(U(N(x0), F(x1, x2))) → TOP(check(F(x0, D(x1, x2))))

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TOP(U(x0, x1)) → TOP(D(check(x0), x1))
TOP(U(x0, x1)) → TOP(D(x0, check(x1)))
TOP(U(x0, B)) → TOP(check(U(x0, B)))
TOP(U(E, F(x0, x1))) → TOP(check(F(E, D(x0, x1))))
TOP(U(N(x0), F(x1, x2))) → TOP(check(F(x0, D(x1, x2))))

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(28) NonTerminationLoopProof (COMPLETE transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = TOP(D(x, B)) evaluates to t =TOP(D(check(x), B))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [x / check(x)]
  • Semiunifier: [ ]



Rewriting sequence

TOP(D(x, B)) → TOP(U(x, B))
with rule D(x', B) → U(x', B) at position [0] and matcher [x' / x]

TOP(U(x, B)) → TOP(D(check(x), B))
with rule TOP(U(x0, x1)) → TOP(D(check(x0), x1))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(29) NO

(30) Obligation:

Relative ADP Problem with
absolute ADPs:

D(O(x), F(y, z)) → F1(x, D(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(31) RelADPReductionPairProof (EQUIVALENT transformation)

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:


D(O(x), F(y, z)) → F1(x, D(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))

Relative ADPs:

check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 2 + 2·x1   
POL(D(x1, x2)) = 3 + 3·x1 + 3·x2   
POL(D1(x1, x2)) = 2·x2   
POL(E) = 2   
POL(E1) = 3   
POL(F(x1, x2)) = 3 + 3·x1 + 3·x2   
POL(F1(x1, x2)) = 0   
POL(N(x1)) = x1   
POL(O(x1)) = 2 + x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = 3 + 2·x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = 0   

(32) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
E → N(E)
check(N(x)) → N(CHECK(x))
check(U(x, y)) → U(check(x), y)
D(E, F(x, y)) → F(E, D(x, y))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(33) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.

(34) TRUE

(35) Obligation:

Relative ADP Problem with
absolute ADPs:

D(O(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(36) RelADPReductionPairProof (EQUIVALENT transformation)

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:
Relative ADPs:


check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

D(O(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(U(x, y)) → U(x, CHECK(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 1   
POL(CHECK(x1)) = 2·x1   
POL(D(x1, x2)) = 3 + 2·x1 + 2·x2   
POL(D1(x1, x2)) = 0   
POL(E) = 0   
POL(E1) = 3   
POL(F(x1, x2)) = 3 + 3·x1 + 2·x2   
POL(F1(x1, x2)) = 2·x1   
POL(N(x1)) = 2·x1   
POL(O(x1)) = 2·x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = 0   

(37) Obligation:

Relative ADP Problem with
absolute ADPs:

D(O(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(F(x, y)) → F(x, check(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(38) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
1 SCC with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 1 subproblem.

(39) Obligation:

Relative ADP Problem with
absolute ADPs:

D(O(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
check(N(x)) → N(check(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(40) 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:O_1 = N_1 = E = top_1 = 0 check_1 = B = D^1_2 = 0 U_2 = 0 F_2 = 0 D_2 = 0
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
D1(x1, x2)  =  x2
O(x1)  =  O(x1)
F(x1, x2)  =  F(x2)
U(x1, x2)  =  x2
N(x1)  =  N(x1)
D(x1, x2)  =  D(x2)
B  =  B
E  =  E
top(x1)  =  top
check(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:

O1 > [N1, D1] > E > F1
top > [N1, D1] > E > F1

Status:
O1: [1]
F1: multiset
N1: multiset
D1: [1]
B: multiset
E: multiset
top: multiset

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(F(z)) → D1(z)

The TRS R consists of the following rules:

check0(O0(x)) → O0(x)
E0 → N0(E0)
F(U(z)) → U(F(z))
check0(U(y)) → U(y)
D(B0) → U(B0)
D(F(y)) → F(D(y))
check0(N0(x)) → N0(check0(x))
top → top
check0(D(y)) → D(y)
check0(F(y)) → F(check0(y))
check0(U(y)) → U(check0(y))
check0(O0(x)) → O0(check0(x))
check0(F(y)) → F(y)
check0(D(y)) → D(check0(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(42) 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:

D1(F(z)) → D1(z)

Strictly oriented rules of the TRS R:

check0(O0(x)) → O0(x)
F(U(z)) → U(F(z))
check0(U(y)) → U(y)
D(B0) → U(B0)
check0(D(y)) → D(y)
check0(F(y)) → F(check0(y))
check0(U(y)) → U(check0(y))
check0(O0(x)) → O0(check0(x))
check0(F(y)) → F(y)
check0(D(y)) → D(check0(y))

Used ordering: Polynomial interpretation [POLO]:

POL(B0) = 1   
POL(D(x1)) = 1 + 2·x1   
POL(D1(x1)) = x1   
POL(E0) = 2   
POL(F(x1)) = 1 + 2·x1   
POL(N0(x1)) = x1   
POL(O0(x1)) = 2 + x1   
POL(U(x1)) = 1 + x1   
POL(check0(x1)) = 2·x1   
POL(top) = 0   

(43) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

E0 → N0(E0)
D(F(y)) → F(D(y))
check0(N0(x)) → N0(check0(x))
top → top

Q is empty.
We have to consider all (P,Q,R)-chains.

(44) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(45) YES

(46) Obligation:

Relative ADP Problem with
absolute ADPs:

D(N(x), F(y, z)) → F1(x, D(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(47) RelADPReductionPairProof (EQUIVALENT transformation)

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:


D(N(x), F(y, z)) → F1(x, D(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))

Relative ADPs:

check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 2 + 2·x1   
POL(D(x1, x2)) = 3 + 3·x1 + 3·x2   
POL(D1(x1, x2)) = 2·x2   
POL(E) = 2   
POL(E1) = 3   
POL(F(x1, x2)) = 3 + 3·x1 + 3·x2   
POL(F1(x1, x2)) = 0   
POL(N(x1)) = x1   
POL(O(x1)) = 1 + 3·x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = 2 + 3·x1 + 2·x2   
POL(check(x1)) = x1   
POL(top(x1)) = 0   

(48) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
E → N(E)
check(N(x)) → N(CHECK(x))
check(U(x, y)) → U(check(x), y)
D(E, F(x, y)) → F(E, D(x, y))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(49) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.

(50) TRUE

(51) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(E, y)) → U(x, F1(E, y))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(52) RelADPReductionPairProof (EQUIVALENT transformation)

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(x, U(E, y)) → U(x, F1(E, y))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(U(x, y)) → U(CHECK(x), y)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))

Relative ADPs:

check(O(x)) → O(CHECK(x))
check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 2 + 3·x1   
POL(D(x1, x2)) = 2 + 3·x1 + 3·x2   
POL(D1(x1, x2)) = 0   
POL(E) = 3   
POL(E1) = 3   
POL(F(x1, x2)) = 2 + 3·x1 + 3·x2   
POL(F1(x1, x2)) = 3·x1 + 2·x2   
POL(N(x1)) = x1   
POL(O(x1)) = 3·x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = 2 + 3·x1 + 2·x2   
POL(check(x1)) = 2·x1   
POL(top(x1)) = 0   

(53) Obligation:

Relative ADP Problem with
absolute ADPs:

D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))

and relative ADPs:

check(O(x)) → O(x)
E → N(E)
check(O(x)) → O(CHECK(x))
F(x, U(N(y), z)) → U(x, F(y, z))
check(N(x)) → N(CHECK(x))
check(U(x, y)) → U(check(x), y)
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
F(x, U(O(y), z)) → U(x, F(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

(54) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.

(55) TRUE

(56) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F1(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(57) RelADPReductionPairProof (EQUIVALENT transformation)

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:
Relative ADPs:


check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

F(x, U(N(y), z)) → U(x, F1(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(U(x, y)) → U(x, CHECK(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 2 + 3·x1   
POL(D(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(D1(x1, x2)) = x1   
POL(E) = 0   
POL(E1) = 3   
POL(F(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(F1(x1, x2)) = x1 + x2   
POL(N(x1)) = x1   
POL(O(x1)) = 2·x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = 0   

(58) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F1(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(F(x, y)) → F(x, check(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(59) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
1 SCC with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 1 subproblem.

(60) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F1(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
check(N(x)) → N(check(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(61) RelADPDerelatifyingProof (EQUIVALENT 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.

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F1(x, U(N(y), z)) → F1(y, z)

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
F(x, U(O(y), z)) → U(x, F(y, z))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(63) 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:

F(x, U(O(y), z)) → U(x, F(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))

Used ordering: Polynomial interpretation [POLO]:

POL(B) = 2   
POL(D(x1, x2)) = 2·x1 + 2·x2   
POL(E) = 2   
POL(F(x1, x2)) = 2·x1 + 2·x2   
POL(F1(x1, x2)) = x1 + x2   
POL(N(x1)) = x1   
POL(O(x1)) = 2 + 2·x1   
POL(U(x1, x2)) = 2·x1 + 2·x2   
POL(check(x1)) = x1   
POL(top(x1)) = x1   

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F1(x, U(N(y), z)) → F1(y, z)

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(65) 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:

F1(x, U(N(y), z)) → F1(y, z)


Used ordering: Polynomial interpretation [POLO]:

POL(B) = 1   
POL(D(x1, x2)) = 1 + 2·x1 + x2   
POL(E) = 2   
POL(F(x1, x2)) = 1 + 2·x1 + x2   
POL(F1(x1, x2)) = x1 + 2·x2   
POL(N(x1)) = x1   
POL(O(x1)) = 1 + x1   
POL(U(x1, x2)) = 1 + 2·x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = x1   

(66) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(67) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(68) YES

(69) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(70) RelADPReductionPairProof (EQUIVALENT transformation)

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:
Relative ADPs:


check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(U(x, y)) → U(x, CHECK(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 3·x1   
POL(D(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(D1(x1, x2)) = x1   
POL(E) = 0   
POL(E1) = 3   
POL(F(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(F1(x1, x2)) = x1 + x2   
POL(N(x1)) = 2·x1   
POL(O(x1)) = 2·x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = 0   

(71) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(F(x, y)) → F(x, check(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(72) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.

(73) TRUE

(74) Obligation:

Relative ADP Problem with
absolute ADPs:

D(E, F(x, y)) → F1(E, D(x, y))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(75) RelADPReductionPairProof (EQUIVALENT transformation)

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:


D(E, F(x, y)) → F1(E, D(x, y))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(D(x, y)))

Relative ADPs:

check(U(x, y)) → U(x, CHECK(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 2 + 2·x1   
POL(D(x1, x2)) = 3 + 3·x1 + 3·x2   
POL(D1(x1, x2)) = 3·x1 + 3·x2   
POL(E) = 3   
POL(E1) = 3   
POL(F(x1, x2)) = 3 + 2·x1 + 2·x2   
POL(F1(x1, x2)) = x1 + 2·x2   
POL(N(x1)) = x1   
POL(O(x1)) = 3·x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = 0   

(76) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(D(x, y)))

and relative ADPs:

check(O(x)) → O(x)
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(E, F(x, y)) → F(E, D(x, y))
check(D(x, y)) → D(check(x), y)
check(U(x, y)) → U(x, CHECK(y))
check(F(x, y)) → F(x, check(y))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

(77) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.

(78) TRUE

(79) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(E, y)) → U(x, F(E1, y))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(80) RelADPReductionPairProof (EQUIVALENT transformation)

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(x, U(E, y)) → U(x, F(E1, y))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))

Relative ADPs:

check(U(x, y)) → U(x, CHECK(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 2 + 3·x1   
POL(D(x1, x2)) = 2 + x1 + 3·x2   
POL(D1(x1, x2)) = 0   
POL(E) = 2   
POL(E1) = 1   
POL(F(x1, x2)) = 2 + x1 + 2·x2   
POL(F1(x1, x2)) = x2   
POL(N(x1)) = x1   
POL(O(x1)) = x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = 0   

(81) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(F(x, y)) → F(x, check(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

(82) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.

(83) TRUE

(84) Obligation:

Relative ADP Problem with
absolute ADPs:

D(E, F(x, y)) → F(E1, D(x, y))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(85) RelADPReductionPairProof (EQUIVALENT transformation)

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:


D(E, F(x, y)) → F(E1, D(x, y))
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))

Relative ADPs:

check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 2 + 2·x1   
POL(D(x1, x2)) = 3 + 2·x1 + 2·x2   
POL(D1(x1, x2)) = x1   
POL(E) = 3   
POL(E1) = 0   
POL(F(x1, x2)) = 3 + 2·x1 + 2·x2   
POL(F1(x1, x2)) = 2·x1   
POL(N(x1)) = x1   
POL(O(x1)) = 1 + x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = 3 + x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = 0   

(86) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(N(x)) → N(CHECK(x))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
D(E, F(x, y)) → F(E, D(x, y))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(87) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.

(88) TRUE

(89) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(O(y), z)) → U(x, F1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(90) RelADPReductionPairProof (EQUIVALENT transformation)

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:
Relative ADPs:


check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

F(x, U(O(y), z)) → U(x, F1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(U(x, y)) → U(x, CHECK(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 1   
POL(CHECK(x1)) = 2 + 3·x1   
POL(D(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(D1(x1, x2)) = x1   
POL(E) = 0   
POL(E1) = 3   
POL(F(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(F1(x1, x2)) = x1 + x2   
POL(N(x1)) = 2·x1   
POL(O(x1)) = x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = 0   

(91) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(O(y), z)) → U(x, F1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(F(x, y)) → F(x, check(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(92) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
1 SCC with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 1 subproblem.

(93) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(O(y), z)) → U(x, F1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
check(N(x)) → N(check(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(94) RelADPDerelatifyingProof (EQUIVALENT 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.

(95) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F1(x, U(O(y), z)) → F1(y, z)

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
F(x, U(O(y), z)) → U(x, F(y, z))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(96) 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:

F1(x, U(O(y), z)) → F1(y, z)

Strictly oriented rules of the TRS R:

F(x, U(O(y), z)) → U(x, F(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))

Used ordering: Polynomial interpretation [POLO]:

POL(B) = 2   
POL(D(x1, x2)) = 2·x1 + 2·x2   
POL(E) = 0   
POL(F(x1, x2)) = 2·x1 + 2·x2   
POL(F1(x1, x2)) = x1 + x2   
POL(N(x1)) = x1   
POL(O(x1)) = 2 + x1   
POL(U(x1, x2)) = 2·x1 + 2·x2   
POL(check(x1)) = x1   
POL(top(x1)) = x1   

(97) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(98) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(99) YES

(100) Obligation:

Relative ADP Problem with
absolute ADPs:

D(E, F(x, y)) → F(E, D1(x, y))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(101) RelADPReductionPairProof (EQUIVALENT transformation)

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:
Relative ADPs:


check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

D(E, F(x, y)) → F(E, D1(x, y))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(U(x, y)) → U(x, CHECK(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 2 + 2·x1   
POL(D(x1, x2)) = 3 + 2·x1 + 2·x2   
POL(D1(x1, x2)) = 0   
POL(E) = 0   
POL(E1) = 3   
POL(F(x1, x2)) = 3 + 3·x1 + 2·x2   
POL(F1(x1, x2)) = x1   
POL(N(x1)) = 2·x1   
POL(O(x1)) = 2·x1   
POL(TOP(x1)) = 0   
POL(U(x1, x2)) = x1 + x2   
POL(check(x1)) = 2·x1   
POL(top(x1)) = 0   

(102) Obligation:

Relative ADP Problem with
absolute ADPs:

D(E, F(x, y)) → F(E, D1(x, y))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(F(x, y)) → F(x, check(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(103) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
1 SCC with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 1 subproblem.

(104) Obligation:

Relative ADP Problem with
absolute ADPs:

D(E, F(x, y)) → F(E, D1(x, y))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
check(N(x)) → N(check(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))

(105) RelADPDerelatifyingProof (EQUIVALENT 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.

(106) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(E, F(x, y)) → D1(x, y)

The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
F(x, U(O(y), z)) → U(x, F(y, z))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(107) 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:

D1(E, F(x, y)) → D1(x, y)

Strictly oriented rules of the TRS R:

F(x, U(O(y), z)) → U(x, F(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))

Used ordering: Polynomial interpretation [POLO]:

POL(B) = 1   
POL(D(x1, x2)) = 1 + x1 + x2   
POL(D1(x1, x2)) = x1 + x2   
POL(E) = 1   
POL(F(x1, x2)) = 2 + x1 + x2   
POL(N(x1)) = x1   
POL(O(x1)) = 2 + 2·x1   
POL(U(x1, x2)) = 1 + x1 + x2   
POL(check(x1)) = x1   
POL(top(x1)) = x1   

(108) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(check(x), y)
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(N(x)) → N(check(x))
top(U(x, y)) → top(check(D(x, y)))
check(D(x, y)) → D(check(x), y)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(109) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(110) YES

(111) Obligation:

Relative ADP Problem with
absolute ADPs:

D(N(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))

(112) RelADPReductionPairProof (EQUIVALENT transformation)

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:


top(U(x, y)) → top(check(D(x, y)))

Relative ADPs:

check(O(x)) → O(x)
E → N(E)


The remaining rules can at least be oriented weakly:
Absolute ADPs:

D(N(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 0   
POL(CHECK(x1)) = 0   
POL(D(x1, x2)) = 3   
POL(D1(x1, x2)) = 0   
POL(E) = 1   
POL(E1) = 3   
POL(F(x1, x2)) = x2   
POL(F1(x1, x2)) = 0   
POL(N(x1)) = 1   
POL(O(x1)) = 2·x1   
POL(TOP(x1)) = 1   
POL(U(x1, x2)) = 3 + 3·x2   
POL(check(x1)) = 2·x1   
POL(top(x1)) = 0   

(113) Obligation:

Relative ADP Problem with
absolute ADPs:

D(N(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))
top(U(x, y)) → top(check(D(x, y)))

(114) RelADPReductionPairProof (EQUIVALENT transformation)

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:
Relative ADPs:


check(D(x, y)) → D1(CHECK(x), y)
check(F(x, y)) → F1(CHECK(x), y)
check(O(x)) → O(x)
check(U(x, y)) → U(x, CHECK(y))
E → N(E)
check(U(x, y)) → U(CHECK(x), y)
check(D(x, y)) → D1(x, CHECK(y))
check(F(x, y)) → F1(x, CHECK(y))
top(U(x, y)) → top(check(D(x, y)))


The remaining rules can at least be oriented weakly:
Absolute ADPs:

D(N(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
F(x, U(E, y)) → U(x, F(E, y))

Relative ADPs:

check(O(x)) → O(CHECK(x))
check(N(x)) → N(CHECK(x))


Ordered with Polynomial interpretation [POLO]:

POL(B) = 1   
POL(CHECK(x1)) = 2 + 2·x1   
POL(D(x1, x2)) = 3 + 2·x1 + 2·x2   
POL(D1(x1, x2)) = 0   
POL(E) = 0   
POL(E1) = 3   
POL(F(x1, x2)) = 3 + 3·x1 + 2·x2   
POL(F1(x1, x2)) = x1   
POL(N(x1)) = 2·x1   
POL(O(x1)) = 2·x1   
POL(TOP(x1)) = 3·x12   
POL(U(x1, x2)) = 3 + x1 + x2   
POL(check(x1)) = 2·x1   
POL(top(x1)) = 0   

(115) Obligation:

Relative ADP Problem with
absolute ADPs:

D(N(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(O(x)) → O(CHECK(x))
check(U(x, y)) → U(x, check(y))
check(N(x)) → N(CHECK(x))
check(U(x, y)) → U(check(x), y)
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))
top(U(x, y)) → top(check(D(x, y)))

(116) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
1 SCC with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 1 subproblem.

(117) Obligation:

Relative ADP Problem with
absolute ADPs:

D(N(x), F(y, z)) → F(x, D1(y, z))
F(x, U(N(y), z)) → U(x, F(y, z))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(x, B) → U(x, B)
D(O(x), F(y, z)) → F(x, D(y, z))
D(E, F(x, y)) → F(E, D(x, y))
F(x, U(E, y)) → U(x, F(E, y))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D(check(x), y)
E → N(E)
check(F(x, y)) → F(x, check(y))
check(U(x, y)) → U(x, check(y))
check(O(x)) → O(check(x))
check(U(x, y)) → U(check(x), y)
check(N(x)) → N(check(x))
check(F(x, y)) → F(check(x), y)
check(D(x, y)) → D(x, check(y))
top(U(x, y)) → top(check(D(x, y)))

(118) 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:O_1 = N_1 = E = top_1 = check_1 = B = D^1_2 = 0 U_2 = 0 F_2 = 0 D_2 = 0
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
D1(x1, x2)  =  D1(x2)
N(x1)  =  N(x1)
F(x1, x2)  =  F(x2)
U(x1, x2)  =  x2
D(x1, x2)  =  x2
B  =  B
E  =  E
O(x1)  =  O(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

E > [D^11, F1]

Status:
D^11: [1]
N1: multiset
F1: multiset
B: multiset
E: multiset
O1: multiset

(119) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(F(z)) → D1(z)

The TRS R consists of the following rules:

check0(O0(x)) → O0(x)
E0 → N0(E0)
F(U(z)) → U(F(z))
check0(U(y)) → U(y)
D(B0) → U(B0)
D(F(y)) → F(D(y))
check0(N0(x)) → N0(check0(x))
top0(U(y)) → top0(check0(D(y)))
check0(D(y)) → D(y)
check0(F(y)) → F(check0(y))
check0(U(y)) → U(check0(y))
check0(O0(x)) → O0(check0(x))
check0(F(y)) → F(y)
check0(D(y)) → D(check0(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(120) 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:

check0(O0(x)) → O0(x)
check0(O0(x)) → O0(check0(x))

Used ordering: Polynomial interpretation [POLO]:

POL(B0) = 0   
POL(D(x1)) = x1   
POL(D1(x1)) = x1   
POL(E0) = 1   
POL(F(x1)) = x1   
POL(N0(x1)) = x1   
POL(O0(x1)) = 2 + x1   
POL(U(x1)) = 2·x1   
POL(check0(x1)) = 2·x1   
POL(top0(x1)) = x1   

(121) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(F(z)) → D1(z)

The TRS R consists of the following rules:

E0 → N0(E0)
F(U(z)) → U(F(z))
check0(U(y)) → U(y)
D(B0) → U(B0)
D(F(y)) → F(D(y))
check0(N0(x)) → N0(check0(x))
top0(U(y)) → top0(check0(D(y)))
check0(D(y)) → D(y)
check0(F(y)) → F(check0(y))
check0(U(y)) → U(check0(y))
check0(F(y)) → F(y)
check0(D(y)) → D(check0(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(122) 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:

D1(F(z)) → D1(z)


Used ordering: Polynomial interpretation [POLO]:

POL(B0) = 2   
POL(D(x1)) = 1 + 2·x1   
POL(D1(x1)) = x1   
POL(E0) = 0   
POL(F(x1)) = 1 + 2·x1   
POL(N0(x1)) = x1   
POL(U(x1)) = 1 + 2·x1   
POL(check0(x1)) = x1   
POL(top0(x1)) = x1   

(123) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

E0 → N0(E0)
F(U(z)) → U(F(z))
check0(U(y)) → U(y)
D(B0) → U(B0)
D(F(y)) → F(D(y))
check0(N0(x)) → N0(check0(x))
top0(U(y)) → top0(check0(D(y)))
check0(D(y)) → D(y)
check0(F(y)) → F(check0(y))
check0(U(y)) → U(check0(y))
check0(F(y)) → F(y)
check0(D(y)) → D(check0(y))

Q is empty.
We have to consider all (P,Q,R)-chains.

(124) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(125) YES