Termination proof of rtL-me3.trs

Termination of the given RelTRS could be proven:

0 RelTRS

↳1 RelTRS S Cleaner (⇔, 0 ms)

↳2 RelTRS

↳3 RelTRStoRelADPProof (⇔, 0 ms)

↳4 RelADPP

↳5 RelADPDepGraphProof (⇔, 0 ms)

↳6 RelADPP

↳7 RelADPReductionPairProof (⇔, 100 ms)

↳8 RelADPP

↳9 RelADPDepGraphProof (⇔, 0 ms)

↳10 RelADPP

↳11 RelADPReductionPairProof (⇔, 0 ms)

↳12 RelADPP

↳13 DAbsisEmptyProof (⇔, 0 ms)

↳14 YES

(0) Obligation:

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

topB(i, N1(x), y) → topA(1, T1(x), y)
topA(i, x, N2(y)) → topB(0, x, T2(y))
topB(i, S1(x), y) → topA(i, N1(x), y)
topA(i, x, S2(y)) → topB(i, x, N2(y))
topA(i, N1(x), T2(y)) → topB(i, N1(x), S2(y))
topA(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))

The relative TRS consists of the following S rules:

topB(i, x, N2(y)) → topB(i, x, N2(C(y)))
topA(i, S1(x), y) → topA(i, N1(x), y)
topB(i, x, S2(y)) → topB(i, x, N2(y))
topB(i, x, N2(y)) → topB(0, x, T2(y))
topA(i, T1(x), y) → topA(i, T1(x), y)
topB(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topB(i, N1(x), T2(y)) → topB(i, N1(x), S2(y))
topA(i, N1(x), y) → topA(i, N1(C(x)), y)
topB(i, x, T2(y)) → topB(i, x, T2(y))
topB(i, x, S2(y)) → topB(i, x, S2(D(y)))
topA(i, N1(x), y) → topA(1, T1(x), y)

(1) RelTRS S Cleaner (EQUIVALENT transformation)

We have deleted all rules from S that have the shape t → t:

topA(i, T1(x), y) → topA(i, T1(x), y)
topB(i, x, T2(y)) → topB(i, x, T2(y))

(2) Obligation:

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

topB(i, N1(x), y) → topA(1, T1(x), y)
topA(i, x, N2(y)) → topB(0, x, T2(y))
topB(i, S1(x), y) → topA(i, N1(x), y)
topA(i, x, S2(y)) → topB(i, x, N2(y))
topA(i, N1(x), T2(y)) → topB(i, N1(x), S2(y))
topA(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))

The relative TRS consists of the following S rules:

topB(i, x, N2(y)) → topB(i, x, N2(C(y)))
topA(i, S1(x), y) → topA(i, N1(x), y)
topB(i, x, S2(y)) → topB(i, x, N2(y))
topB(i, x, N2(y)) → topB(0, x, T2(y))
topB(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topB(i, N1(x), T2(y)) → topB(i, N1(x), S2(y))
topA(i, N1(x), y) → topA(i, N1(C(x)), y)
topB(i, x, S2(y)) → topB(i, x, S2(D(y)))
topA(i, N1(x), y) → topA(1, T1(x), y)

(3) RelTRStoRelADPProof (EQUIVALENT transformation)

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

(4) Obligation:

Relative ADP Problem with
absolute ADPs:

topB(i, N1(x), y) → TOPA(1, T1(x), y)
topA(i, x, N2(y)) → TOPB(0, x, T2(y))
topB(i, S1(x), y) → TOPA(i, N1(x), y)
topA(i, x, S2(y)) → TOPB(i, x, N2(y))
topA(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topA(1, T1(x), T2(y)) → TOPB(1, T1(x), S2(y))

and relative ADPs:

topB(i, x, N2(y)) → TOPB(i, x, N2(C(y)))
topA(i, S1(x), y) → TOPA(i, N1(x), y)
topB(i, x, S2(y)) → TOPB(i, x, N2(y))
topB(i, x, N2(y)) → TOPB(0, x, T2(y))
topB(1, T1(x), T2(y)) → TOPB(1, T1(x), S2(y))
topB(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topA(i, N1(x), y) → TOPA(i, N1(C(x)), y)
topB(i, x, S2(y)) → TOPB(i, x, S2(D(y)))
topA(i, N1(x), y) → TOPA(1, T1(x), y)

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

(6) Obligation:

Relative ADP Problem with
absolute ADPs:

topA(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, S1(x), y) → TOPA(i, N1(x), y)
topA(1, T1(x), T2(y)) → TOPB(1, T1(x), S2(y))
topB(i, N1(x), y) → TOPA(1, T1(x), y)
topA(i, x, S2(y)) → TOPB(i, x, N2(y))
topA(i, x, N2(y)) → TOPB(0, x, T2(y))

and relative ADPs:

topA(i, S1(x), y) → topA(i, N1(x), y)
topB(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, x, S2(y)) → TOPB(i, x, N2(y))
topB(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topA(i, N1(x), y) → TOPA(1, T1(x), y)
topA(i, N1(x), y) → TOPA(i, N1(C(x)), y)
topB(i, x, N2(y)) → TOPB(0, x, T2(y))
topB(i, x, S2(y)) → TOPB(i, x, S2(D(y)))
topB(i, x, N2(y)) → TOPB(i, x, N2(C(y)))

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

topB(i, N1(x), y) → TOPA(1, T1(x), y)

Relative ADPs:

topA(i, S1(x), y) → topA(i, N1(x), y)
topA(i, N1(x), y) → TOPA(1, T1(x), y)
topB(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))

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

topA(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, S1(x), y) → TOPA(i, N1(x), y)
topA(1, T1(x), T2(y)) → TOPB(1, T1(x), S2(y))
topA(i, x, S2(y)) → TOPB(i, x, N2(y))
topA(i, x, N2(y)) → TOPB(0, x, T2(y))

Relative ADPs:

topB(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, x, S2(y)) → TOPB(i, x, N2(y))
topA(i, N1(x), y) → TOPA(i, N1(C(x)), y)
topB(i, x, N2(y)) → TOPB(0, x, T2(y))
topB(i, x, S2(y)) → TOPB(i, x, S2(D(y)))
topB(i, x, N2(y)) → TOPB(i, x, N2(C(y)))

Ordered with Polynomial interpretation [POLO]:

POL(0) = 0
POL(1) = 0
POL(C(x₁)) = 0
POL(D(x₁)) = x₁
POL(N1(x₁)) = 3 + 2·x₁
POL(N2(x₁)) = 3·x₁
POL(S1(x₁)) = 3 + 3·x₁
POL(S2(x₁)) = 3·x₁
POL(T1(x₁)) = x₁
POL(T2(x₁)) = 3·x₁
POL(TOPA(x₁, x₂, x₃)) = x₁ + 2·x₂ + 3·x₃
POL(TOPB(x₁, x₂, x₃)) = x₁ + 2·x₂ + 3·x₃
POL(topA(x₁, x₂, x₃)) = 2 + 3·x₂
POL(topB(x₁, x₂, x₃)) = 2 + 3·x₂

(8) Obligation:

Relative ADP Problem with
absolute ADPs:

topA(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, S1(x), y) → TOPA(i, N1(x), y)
topA(1, T1(x), T2(y)) → TOPB(1, T1(x), S2(y))
topA(i, x, S2(y)) → TOPB(i, x, N2(y))
topA(i, x, N2(y)) → TOPB(0, x, T2(y))

and relative ADPs:

topA(i, S1(x), y) → topA(i, N1(x), y)
topB(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, x, S2(y)) → TOPB(i, x, N2(y))
topB(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topB(i, N1(x), y) → topA(1, T1(x), y)
topA(i, N1(x), y) → TOPA(i, N1(C(x)), y)
topB(i, x, N2(y)) → TOPB(0, x, T2(y))
topB(i, x, S2(y)) → TOPB(i, x, S2(D(y)))
topB(i, x, N2(y)) → TOPB(i, x, N2(C(y)))
topA(i, N1(x), y) → topA(1, T1(x), y)

(9) RelADPDepGraphProof (EQUIVALENT transformation)

(10) Obligation:

Relative ADP Problem with
absolute ADPs:

topA(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topA(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, S1(x), y) → TOPA(i, N1(x), y)
topA(i, x, S2(y)) → TOPB(i, x, N2(y))
topA(i, x, N2(y)) → TOPB(0, x, T2(y))

and relative ADPs:

topA(i, S1(x), y) → topA(i, N1(x), y)
topB(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, x, S2(y)) → TOPB(i, x, N2(y))
topB(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topB(i, N1(x), y) → topA(1, T1(x), y)
topA(i, N1(x), y) → TOPA(i, N1(C(x)), y)
topB(i, x, N2(y)) → TOPB(0, x, T2(y))
topB(i, x, S2(y)) → TOPB(i, x, S2(D(y)))
topB(i, x, N2(y)) → TOPB(i, x, N2(C(y)))
topA(i, N1(x), y) → topA(1, T1(x), y)

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

topA(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topA(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, S1(x), y) → TOPA(i, N1(x), y)
topA(i, x, S2(y)) → TOPB(i, x, N2(y))
topA(i, x, N2(y)) → TOPB(0, x, T2(y))

Relative ADPs:

topA(i, S1(x), y) → topA(i, N1(x), y)
topB(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topB(i, N1(x), y) → topA(1, T1(x), y)
topA(i, N1(x), y) → topA(1, T1(x), y)

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(0) = 0
POL(1) = 0
POL(C(x₁)) = 0
POL(D(x₁)) = 0
POL(N1(x₁)) = 2·x₁
POL(N2(x₁)) = 3·x₁
POL(S1(x₁)) = 2 + 3·x₁
POL(S2(x₁)) = 3·x₁
POL(T1(x₁)) = 2
POL(T2(x₁)) = 3·x₁
POL(TOPA(x₁, x₂, x₃)) = 2 + 3·x₁ + 3·x₂ + 3·x₃
POL(TOPB(x₁, x₂, x₃)) = 3·x₁ + 2·x₂ + 3·x₃
POL(topA(x₁, x₂, x₃)) = 3·x₃
POL(topB(x₁, x₂, x₃)) = 3·x₃

(12) Obligation:

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

topA(i, x, S2(y)) → topB(i, x, N2(y))
topB(i, N1(x), T2(y)) → TOPB(i, N1(x), S2(y))
topB(i, N1(x), y) → topA(1, T1(x), y)
topB(i, x, N2(y)) → TOPB(i, x, N2(C(y)))
topA(i, N1(x), y) → topA(1, T1(x), y)
topA(i, x, N2(y)) → topB(0, x, T2(y))
topA(i, S1(x), y) → topA(i, N1(x), y)
topA(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topB(i, x, S2(y)) → TOPB(i, x, N2(y))
topB(1, T1(x), T2(y)) → topB(1, T1(x), S2(y))
topA(i, N1(x), y) → TOPA(i, N1(C(x)), y)
topA(i, N1(x), T2(y)) → topB(i, N1(x), S2(y))
topB(i, x, N2(y)) → TOPB(0, x, T2(y))
topB(i, x, S2(y)) → TOPB(i, x, S2(D(y)))
topB(i, S1(x), y) → topA(i, N1(x), y)

(13) DAbsisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) RelTRS S Cleaner (EQUIVALENT transformation)

(2) Obligation:

(3) RelTRStoRelADPProof (EQUIVALENT transformation)

(4) Obligation:

(5) RelADPDepGraphProof (EQUIVALENT transformation)

(6) Obligation:

(7) RelADPReductionPairProof (EQUIVALENT transformation)

(8) Obligation:

(9) RelADPDepGraphProof (EQUIVALENT transformation)

(10) Obligation:

(11) RelADPReductionPairProof (EQUIVALENT transformation)

(12) Obligation:

(13) DAbsisEmptyProof (EQUIVALENT transformation)

(14) YES