Termination proof of Relative_05

Termination of the given RelTRS could be disproven:

0 RelTRS

↳1 RelTRStoRelADPProof (⇔, 0 ms)

↳2 RelADPP

↳3 RelADPDepGraphProof (⇔, 0 ms)

↳4 AND

    ↳5 RelADPP

        ↳6 RelADPDerelatifyingProof (⇔, 0 ms)

        ↳7 QDP

        ↳8 MRRProof (⇔, 23 ms)

        ↳9 QDP

        ↳10 MRRProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 PisEmptyProof (⇔, 0 ms)

        ↳13 YES

    ↳14 RelADPP

        ↳15 RelADPDerelatifyingProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 MRRProof (⇔, 19 ms)

        ↳18 QDP

        ↳19 PisEmptyProof (⇔, 0 ms)

        ↳20 YES

    ↳21 RelADPP

        ↳22 RelADPDerelatifyingProof (⇔, 0 ms)

        ↳23 QDP

        ↳24 MRRProof (⇔, 15 ms)

        ↳25 QDP

        ↳26 TransformationProof (⇔, 0 ms)

        ↳27 QDP

        ↳28 NonTerminationLoopProof (⇒, 0 ms)

        ↳29 NO

    ↳30 RelADPP

        ↳31 RelADPReductionPairProof (⇔, 107 ms)

        ↳32 RelADPP

        ↳33 DAbsisEmptyProof (⇔, 0 ms)

        ↳34 YES

    ↳35 RelADPP

        ↳36 RelADPReductionPairProof (⇔, 97 ms)

        ↳37 RelADPP

        ↳38 DAbsisEmptyProof (⇔, 0 ms)

        ↳39 YES

    ↳40 RelADPP

        ↳41 RelADPReductionPairProof (⇔, 91 ms)

        ↳42 RelADPP

        ↳43 DAbsisEmptyProof (⇔, 0 ms)

        ↳44 YES

    ↳45 RelADPP

        ↳46 RelADPReductionPairProof (⇔, 112 ms)

        ↳47 RelADPP

        ↳48 DAbsisEmptyProof (⇔, 0 ms)

        ↳49 YES

    ↳50 RelADPP

        ↳51 RelADPReductionPairProof (⇔, 88 ms)

        ↳52 RelADPP

        ↳53 RelADPDepGraphProof (⇔, 0 ms)

        ↳54 RelADPP

        ↳55 RelADPDerelatifyingProof (⇔, 0 ms)

        ↳56 QDP

        ↳57 MRRProof (⇔, 10 ms)

        ↳58 QDP

        ↳59 MRRProof (⇔, 0 ms)

        ↳60 QDP

        ↳61 PisEmptyProof (⇔, 0 ms)

        ↳62 YES

    ↳63 RelADPP

        ↳64 RelADPReductionPairProof (⇔, 103 ms)

        ↳65 RelADPP

        ↳66 DAbsisEmptyProof (⇔, 0 ms)

        ↳67 YES

    ↳68 RelADPP

        ↳69 RelADPReductionPairProof (⇔, 107 ms)

        ↳70 RelADPP

        ↳71 RelADPDepGraphProof (⇔, 0 ms)

        ↳72 TRUE

    ↳73 RelADPP

        ↳74 RelADPReductionPairProof (⇔, 101 ms)

        ↳75 RelADPP

        ↳76 DAbsisEmptyProof (⇔, 0 ms)

        ↳77 YES

    ↳78 RelADPP

        ↳79 RelADPReductionPairProof (⇔, 108 ms)

        ↳80 RelADPP

        ↳81 DAbsisEmptyProof (⇔, 0 ms)

        ↳82 YES

    ↳83 RelADPP

        ↳84 RelADPReductionPairProof (⇔, 98 ms)

        ↳85 RelADPP

        ↳86 DAbsisEmptyProof (⇔, 0 ms)

        ↳87 YES

    ↳88 RelADPP

        ↳89 RelADPReductionPairProof (⇔, 99 ms)

        ↳90 RelADPP

        ↳91 RelADPDepGraphProof (⇔, 0 ms)

        ↳92 TRUE

    ↳93 RelADPP

        ↳94 RelADPReductionPairProof (⇔, 97 ms)

        ↳95 RelADPP

        ↳96 RelADPDepGraphProof (⇔, 0 ms)

        ↳97 RelADPP

        ↳98 RelADPDerelatifyingProof (⇔, 0 ms)

        ↳99 QDP

        ↳100 MRRProof (⇔, 23 ms)

        ↳101 QDP

        ↳102 PisEmptyProof (⇔, 0 ms)

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

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

and relative ADPs:

check(O(x)) → O(x)
E → N(E)
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))
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))

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

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

F¹(x, U(O(y), z)) → F¹(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(x₁, x₂)) = x₁ + x₂
POL(E) = 1
POL(F(x₁, x₂)) = 2 + x₁ + x₂
POL(F¹(x₁, x₂)) = x₁ + x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 1 + x₁
POL(U(x₁, x₂)) = x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 2·x₁

(9) Obligation:

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

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

F¹(x, U(E, y)) → F¹(E, y)
F¹(x, U(N(y), z)) → F¹(y, z)

Used ordering: Polynomial interpretation [POLO]:

POL(B) = 1
POL(D(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(E) = 2
POL(F(x₁, x₂)) = 2·x₁ + x₂
POL(F¹(x₁, x₂)) = x₁ + x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 2 + 2·x₁
POL(U(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = x₁

(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, D¹(y, z))
D(E, F(x, y)) → F(E, D¹(x, y))
D(N(x), F(y, z)) → F(x, D¹(y, z))

and relative ADPs:

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))

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

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

D¹(O(x), F(y, z)) → D¹(y, z)
D¹(E, F(x, y)) → D¹(x, y)
D¹(N(x), F(y, z)) → D¹(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(x₁, x₂)) = 2 + x₁ + x₂
POL(D¹(x₁, x₂)) = x₁ + x₂
POL(E) = 0
POL(F(x₁, x₂)) = 2 + x₁ + x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 1 + 2·x₁
POL(U(x₁, x₂)) = 2 + x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = x₁

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

and relative ADPs:

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))

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

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(x₁, x₂)) = x₁ + 2·x₂
POL(E) = 1
POL(F(x₁, x₂)) = x₁ + 2·x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 1 + 2·x₁
POL(TOP(x₁)) = 2·x₁
POL(U(x₁, x₂)) = x₁ + 2·x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = x₁

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

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(O(x)) → O(CHECK(x))
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(F(x, y)) → F¹(x, CHECK(y))
top(U(x, y)) → top(check(D(x, y)))
check(F(x, y)) → F¹(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
check(D(x, y)) → D¹(x, CHECK(y))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
F(x, U(E, y)) → U(x, F(E, 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:

F(x, U(E, y)) → U(x, F(E¹, y))

Relative ADPs:

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

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(B) = 3
POL(CHECK(x₁)) = 2 + 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = 2·x₁ + 2·x₂
POL(E) = 1
POL(E¹) = 0
POL(F(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(F¹(x₁, x₂)) = 2·x₁ + 3·x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 3·x₁
POL(TOP(x₁)) = 2
POL(U(x₁, x₂)) = x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(32) Obligation:

Relative ADP Problem with
No absolute ADPs, 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(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(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))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
D(O(x), F(y, z)) → F(x, D(y, z))
F(x, U(E, y)) → U(x, F(E, y))
check(D(x, y)) → D(x, check(y))

(33) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(34) YES

(35) Obligation:

Relative ADP Problem with
absolute ADPs:

D(N(x), F(y, z)) → F¹(x, D(y, z))

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D¹(CHECK(x), y)
E → N(E)
check(O(x)) → O(CHECK(x))
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(F(x, y)) → F¹(x, CHECK(y))
top(U(x, y)) → top(check(D(x, y)))
check(F(x, y)) → F¹(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
check(D(x, y)) → D¹(x, CHECK(y))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
F(x, U(E, y)) → U(x, F(E, 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:
Absolute ADPs:

D(N(x), F(y, z)) → F¹(x, D(y, z))

Relative ADPs:

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

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(B) = 0
POL(CHECK(x₁)) = 2 + 3·x₁
POL(D(x₁, x₂)) = 3 + 2·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = 2 + 3·x₂
POL(E) = 1
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 2·x₁ + 2·x₂
POL(F¹(x₁, x₂)) = 1 + x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 2·x₁
POL(TOP(x₁)) = 0
POL(U(x₁, x₂)) = 2·x₁ + x₂
POL(check(x₁)) = 2·x₁
POL(top(x₁)) = 0

(37) Obligation:

Relative ADP Problem with
No absolute ADPs, 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(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(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))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
D(O(x), F(y, z)) → F(x, D(y, z))
check(D(x, y)) → D(x, check(y))
F(x, U(E, y)) → U(x, F(E, y))

(38) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(39) YES

(40) Obligation:

Relative ADP Problem with
absolute ADPs:

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(O(x)) → O(CHECK(x))
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(F(x, y)) → F¹(x, CHECK(y))
top(U(x, y)) → top(check(D(x, y)))
check(F(x, y)) → F¹(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
check(D(x, y)) → D¹(x, CHECK(y))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
F(x, U(E, y)) → U(x, F(E, y))

(41) 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¹(E, y))

Relative ADPs:

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

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(B) = 0
POL(CHECK(x₁)) = 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 2·x₂
POL(D¹(x₁, x₂)) = 2·x₁ + 2·x₂
POL(E) = 3
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 3·x₁ + 2·x₂
POL(F¹(x₁, x₂)) = 3·x₁ + 2·x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 3 + 3·x₁
POL(TOP(x₁)) = 2 + 2·x₁
POL(U(x₁, x₂)) = 2 + 3·x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(42) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

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

(43) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(44) YES

(45) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

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

(46) 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)) → F(x, D¹(y, z))

Relative ADPs:

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

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(B) = 1
POL(CHECK(x₁)) = 2 + 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = 2·x₁ + 3·x₂
POL(E) = 3
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(F¹(x₁, x₂)) = 2·x₁ + 2·x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 3·x₁
POL(TOP(x₁)) = 2
POL(U(x₁, x₂)) = 3·x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(47) Obligation:

Relative ADP Problem with
No absolute ADPs, 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(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(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))
F(x, U(O(y), z)) → U(x, F(y, z))
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))
F(x, U(E, y)) → U(x, F(E, y))

(48) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(49) YES

(50) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F¹(y, z))

and relative ADPs:

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

(51) 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)) → D¹(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
check(F(x, y)) → F¹(x, CHECK(y))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
check(F(x, y)) → F¹(CHECK(x), y)
check(D(x, y)) → D¹(x, CHECK(y))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
F(x, U(E, y)) → U(x, F(E, y))

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

F(x, U(N(y), z)) → U(x, F¹(y, z))

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) = 2
POL(CHECK(x₁)) = 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 2·x₂
POL(D¹(x₁, x₂)) = 2·x₁
POL(E) = 0
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 3·x₁ + 2·x₂
POL(F¹(x₁, x₂)) = 0
POL(N(x₁)) = 3·x₁
POL(O(x₁)) = 3·x₁
POL(TOP(x₁)) = 2 + 2·x₁ + x₁²
POL(U(x₁, x₂)) = x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(52) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F¹(y, z))

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

(53) 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.

(54) Obligation:

Relative ADP Problem with
absolute ADPs:

F(x, U(N(y), z)) → U(x, F¹(y, z))

and relative ADPs:

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

(55) 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.

(56) Obligation:

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

F¹(x, U(N(y), z)) → F¹(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.

(57) MRRProof (EQUIVALENT transformation)

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(x₁, x₂)) = 2·x₁ + 2·x₂
POL(E) = 2
POL(F(x₁, x₂)) = 2·x₁ + 2·x₂
POL(F¹(x₁, x₂)) = x₁ + x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 2 + 2·x₁
POL(U(x₁, x₂)) = 2·x₁ + 2·x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = x₁

(58) Obligation:

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

F¹(x, U(N(y), z)) → F¹(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.

(59) MRRProof (EQUIVALENT transformation)

F¹(x, U(N(y), z)) → F¹(y, z)

Used ordering: Polynomial interpretation [POLO]:

POL(B) = 1
POL(D(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(E) = 2
POL(F(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(F¹(x₁, x₂)) = x₁ + 2·x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 1 + x₁
POL(U(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = x₁

(60) 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.

(61) PisEmptyProof (EQUIVALENT transformation)

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

(62) YES

(63) Obligation:

Relative ADP Problem with
absolute ADPs:

D(N(x), F(y, z)) → F(x, D¹(y, z))

and relative ADPs:

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

(64) 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)) → F(x, D¹(y, z))

Relative ADPs:

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

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(B) = 0
POL(CHECK(x₁)) = 2 + 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = 2·x₁ + 3·x₂
POL(E) = 3
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(F¹(x₁, x₂)) = 2·x₁ + 2·x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 3·x₁
POL(TOP(x₁)) = 0
POL(U(x₁, x₂)) = 3·x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(65) Obligation:

Relative ADP Problem with
No absolute ADPs, 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(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(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))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
D(O(x), F(y, z)) → F(x, D(y, z))
check(D(x, y)) → D(x, check(y))
F(x, U(E, y)) → U(x, F(E, y))

(66) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(67) YES

(68) Obligation:

Relative ADP Problem with
absolute ADPs:

D(E, F(x, y)) → F¹(E, D(x, y))

and relative ADPs:

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

(69) 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)) → D¹(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
check(U(x, y)) → U(CHECK(x), y)
F(x, U(N(y), z)) → U(x, F(y, z))
check(F(x, y)) → F¹(x, CHECK(y))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
check(F(x, y)) → F¹(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
check(D(x, y)) → D¹(x, CHECK(y))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
F(x, U(E, y)) → U(x, F(E, y))

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

D(E, F(x, y)) → F¹(E, D(x, 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(x₁)) = 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = 3·x₁ + 2·x₂
POL(E) = 1
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(F¹(x₁, x₂)) = 3·x₁ + 2·x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 3·x₁
POL(TOP(x₁)) = x₁
POL(U(x₁, x₂)) = 3 + 2·x₁ + 2·x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(70) Obligation:

Relative ADP Problem with
absolute ADPs:

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

(71) 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.

(72) TRUE

(73) Obligation:

Relative ADP Problem with
absolute ADPs:

D(E, F(x, y)) → F(E, D¹(x, y))

and relative ADPs:

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

(74) 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(E, D¹(x, y))

Relative ADPs:

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

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(B) = 0
POL(CHECK(x₁)) = 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = 2·x₁ + 3·x₂
POL(E) = 0
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(F¹(x₁, x₂)) = 2·x₁ + 2·x₂
POL(N(x₁)) = 3·x₁
POL(O(x₁)) = 3·x₁
POL(TOP(x₁)) = 0
POL(U(x₁, x₂)) = x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(75) Obligation:

Relative ADP Problem with
No absolute ADPs, 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(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(E, F(x, y)) → F(E, D(x, y))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(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))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
D(O(x), F(y, z)) → F(x, D(y, z))
check(D(x, y)) → D(x, check(y))
F(x, U(E, y)) → U(x, F(E, y))

(76) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(77) YES

(78) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

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

(79) 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)) → F¹(x, D(y, z))

Relative ADPs:

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

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(B) = 1
POL(CHECK(x₁)) = 2 + 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = 2·x₁ + 3·x₂
POL(E) = 1
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(F¹(x₁, x₂)) = 2·x₁ + 2·x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 3·x₁
POL(TOP(x₁)) = 2
POL(U(x₁, x₂)) = 2·x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(80) Obligation:

Relative ADP Problem with
No absolute ADPs, 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(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(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))
F(x, U(O(y), z)) → U(x, F(y, z))
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))
F(x, U(E, y)) → U(x, F(E, y))

(81) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(82) YES

(83) Obligation:

Relative ADP Problem with
absolute ADPs:

D(E, F(x, y)) → F(E¹, D(x, y))

and relative ADPs:

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

(84) 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(E¹, D(x, y))

Relative ADPs:

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

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(B) = 0
POL(CHECK(x₁)) = 2 + 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = 3·x₁ + x₂
POL(E) = 0
POL(E¹) = 0
POL(F(x₁, x₂)) = 3 + 3·x₁ + x₂
POL(F¹(x₁, x₂)) = 2·x₁
POL(N(x₁)) = 3·x₁
POL(O(x₁)) = 3·x₁
POL(TOP(x₁)) = x₁ + x₁²
POL(U(x₁, x₂)) = 3·x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(85) Obligation:

Relative ADP Problem with
No absolute ADPs, 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(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(E, F(x, y)) → F(E, D(x, y))
D(x, B) → U(x, B)
top(U(x, y)) → top(check(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))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
check(F(x, y)) → F(check(x), y)
D(O(x), F(y, z)) → F(x, D(y, z))
check(D(x, y)) → D(x, check(y))
F(x, U(E, y)) → U(x, F(E, y))

(86) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(87) YES

(88) Obligation:

Relative ADP Problem with
absolute ADPs:

D(x, B) → U(x, B)

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D¹(CHECK(x), y)
E → N(E)
check(O(x)) → O(CHECK(x))
F(x, U(N(y), z)) → U(x, F(y, z))
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(F(x, y)) → F¹(x, CHECK(y))
top(U(x, y)) → top(check(D(x, y)))
check(F(x, y)) → F¹(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
check(D(x, y)) → D¹(x, CHECK(y))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
F(x, U(E, y)) → U(x, F(E, y))

(89) 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)) → D¹(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(F(x, y)) → F¹(x, CHECK(y))
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
check(F(x, y)) → F¹(CHECK(x), y)
check(D(x, y)) → D¹(x, CHECK(y))
F(x, U(O(y), z)) → U(x, F(y, z))
D(N(x), F(y, z)) → F(x, D(y, z))
D(O(x), F(y, z)) → F(x, D(y, z))
F(x, U(E, y)) → U(x, F(E, y))

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

D(x, B) → U(x, B)

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(x₁)) = 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = x₁
POL(E) = 0
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(F¹(x₁, x₂)) = 1 + x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = x₁
POL(TOP(x₁)) = 2 + 2·x₁
POL(U(x₁, x₂)) = x₁ + x₂
POL(check(x₁)) = 3 + 3·x₁
POL(top(x₁)) = 0

(90) Obligation:

Relative ADP Problem with
absolute ADPs:

D(x, B) → U(x, B)

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

(91) RelADPDepGraphProof (EQUIVALENT transformation)

(92) TRUE

(93) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

check(O(x)) → O(x)
check(D(x, y)) → D¹(CHECK(x), y)
E → N(E)
check(O(x)) → O(CHECK(x))
F(x, U(N(y), z)) → U(x, F(y, z))
check(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
check(F(x, y)) → F¹(x, CHECK(y))
top(U(x, y)) → top(check(D(x, y)))
check(F(x, y)) → F¹(CHECK(x), y)
check(U(x, y)) → U(x, CHECK(y))
check(D(x, y)) → D¹(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))
F(x, U(E, y)) → U(x, F(E, y))

(94) 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)) → D¹(CHECK(x), y)
check(O(x)) → O(x)
E → N(E)
F(x, U(N(y), z)) → U(x, F(y, z))
check(F(x, y)) → F¹(x, CHECK(y))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(D(x, y)))
check(F(x, y)) → F¹(CHECK(x), y)
check(D(x, y)) → D¹(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))
F(x, U(E, y)) → U(x, F(E, y))

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

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

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) = 2
POL(CHECK(x₁)) = 2·x₁
POL(D(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(D¹(x₁, x₂)) = 2·x₁ + 2·x₂
POL(E) = 0
POL(E¹) = 3
POL(F(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(F¹(x₁, x₂)) = 0
POL(N(x₁)) = x₁
POL(O(x₁)) = 3·x₁
POL(TOP(x₁)) = 2 + 2·x₁²
POL(U(x₁, x₂)) = x₁ + x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = 0

(95) Obligation:

Relative ADP Problem with
absolute ADPs:

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

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(U(x, y)) → U(CHECK(x), y)
check(N(x)) → N(CHECK(x))
D(x, B) → U(x, B)
D(E, F(x, y)) → F(E, D(x, y))
top(U(x, y)) → top(check(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))
check(F(x, y)) → F(check(x), y)
D(O(x), F(y, z)) → F(x, D(y, z))
check(D(x, y)) → D(x, check(y))
F(x, U(E, y)) → U(x, F(E, y))

(96) RelADPDepGraphProof (EQUIVALENT transformation)

(97) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

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

(98) 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.

(99) Obligation:

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

F¹(x, U(O(y), z)) → F¹(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.

(100) MRRProof (EQUIVALENT transformation)

F¹(x, U(O(y), z)) → F¹(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(x₁, x₂)) = 2·x₁ + 2·x₂
POL(E) = 0
POL(F(x₁, x₂)) = 2·x₁ + 2·x₂
POL(F¹(x₁, x₂)) = x₁ + x₂
POL(N(x₁)) = x₁
POL(O(x₁)) = 2 + x₁
POL(U(x₁, x₂)) = 2·x₁ + 2·x₂
POL(check(x₁)) = x₁
POL(top(x₁)) = x₁

(101) 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.

(102) PisEmptyProof (EQUIVALENT transformation)

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