YES Termination proof of rtL-me2.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 RelADPP
↳5 RelADPReductionPairProof (⇔, 47 ms)
↳6 RelADPP
↳7 RelADPDepGraphProof (⇔, 0 ms)
↳8 RelADPP
↳9 RelADPReductionPairProof (⇔, 0 ms)
↳10 RelADPP
↳11 RelADPDepGraphProof (⇔, 0 ms)
↳12 TRUE

(0) Obligation:

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

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

The relative TRS consists of the following S rules:

topB(i, N1, T2) → topB(i, N1, S2)
topA(i, S1, y) → topA(i, N1, y)
topB(1, T1, T2) → topB(1, T1, S2)
topB(i, x, S2) → topB(i, x, N2)
topB(i, x, N2) → topB(0, x, T2)
topA(i, N1, y) → topA(1, T1, 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:

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

and relative ADPs:

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

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

(4) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

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

(5) 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, S1, y) → TOPA(i, N1, y)

Relative ADPs:

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


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

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

Relative ADPs:

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


Ordered with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(1) = 2   
POL(N1) = 2   
POL(N2) = 2   
POL(S1) = 3   
POL(S2) = 2   
POL(T1) = 0   
POL(T2) = 2   
POL(TOPA(x1, x2, x3)) = 1 + 3·x1 + 3·x2 + 3·x3   
POL(TOPB(x1, x2, x3)) = 1 + 3·x1 + 3·x2 + 3·x3   
POL(topA(x1, x2, x3)) = 2 + 2·x2 + 3·x3   
POL(topB(x1, x2, x3)) = 2·x2 + 3·x3   

(6) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

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

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

(8) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

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

(9) 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(i, N1, T2) → topB(i, N1, S2)
topB(i, N1, y) → TOPA(1, T1, y)

Relative ADPs:

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


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

topA(i, x, N2) → TOPB(0, x, T2)
topA(i, x, S2) → TOPB(i, x, N2)
topA(1, T1, T2) → TOPB(1, T1, S2)

Relative ADPs:

topB(i, x, N2) → TOPB(0, x, T2)
topB(i, x, S2) → TOPB(i, x, N2)
topB(i, N1, T2) → TOPB(i, N1, S2)


Ordered with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(1) = 3   
POL(N1) = 2   
POL(N2) = 0   
POL(S1) = 0   
POL(S2) = 0   
POL(T1) = 0   
POL(T2) = 0   
POL(TOPA(x1, x2, x3)) = 3·x2   
POL(TOPB(x1, x2, x3)) = 3·x2 + 2·x3   
POL(topA(x1, x2, x3)) = 0   
POL(topB(x1, x2, x3)) = 0   

(10) Obligation:

Relative ADP Problem with
absolute ADPs:

topA(i, x, N2) → TOPB(0, x, T2)
topA(i, x, S2) → TOPB(i, x, N2)
topA(1, T1, T2) → TOPB(1, T1, S2)

and relative ADPs:

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

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

(12) TRUE