YES Termination proof of carbridge.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 (⇔, 124 ms)
↳6 RelADPP
↳7 RelADPReductionPairProof (⇔, 35 ms)
↳8 RelADPP
↳9 RelADPReductionPairProof (⇔, 0 ms)
↳10 RelADPP
↳11 RelADPReductionPairProof (⇔, 19 ms)
↳12 RelADPP
↳13 DAbsisEmptyProof (⇔, 0 ms)
↳14 YES

(0) Obligation:

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

top(left(car(x, y), car(old, z))) → top(right(y, car(old, z)))
top(left(car(x, car(old, y)), z)) → top(right(car(old, y), z))
top(right(x, car(y, car(old, z)))) → top(left(x, car(old, z)))
top(right(car(old, x), car(y, z))) → top(left(car(old, x), z))
top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))

The relative TRS consists of the following S rules:

bot → car(new, bot)
top(right(x, car(y, z))) → top(right(x, z))
top(left(car(x, y), z)) → top(left(y, z))

(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(left(car(x, y), car(old, z))) → TOP(right(y, car(old, z)))
top(left(car(x, car(old, y)), z)) → TOP(right(car(old, y), z))
top(right(x, car(y, car(old, z)))) → TOP(left(x, car(old, z)))
top(right(car(old, x), car(y, z))) → TOP(left(car(old, x), z))
top(left(bot, car(old, x))) → TOP(right(bot, car(old, x)))
top(left(bot, car(old, x))) → top(right(BOT, car(old, x)))
top(right(car(old, x), bot)) → TOP(left(car(old, x), bot))
top(right(car(old, x), bot)) → top(left(car(old, x), BOT))

and relative ADPs:

bot → car(new, BOT)
top(right(x, car(y, z))) → TOP(right(x, z))
top(left(car(x, y), z)) → TOP(left(y, z))

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

top(right(car(old, x), bot)) → TOP(left(car(old, x), bot))
top(right(x, car(y, car(old, z)))) → TOP(left(x, car(old, z)))
top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(left(bot, car(old, x))) → TOP(right(bot, car(old, x)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))
top(left(car(x, y), car(old, z))) → TOP(right(y, car(old, z)))
top(right(car(old, x), car(y, z))) → TOP(left(car(old, x), z))
top(left(car(x, car(old, y)), z)) → TOP(right(car(old, y), z))

and relative ADPs:

bot → car(new, bot)
top(right(x, car(y, z))) → TOP(right(x, z))
top(left(car(x, y), z)) → TOP(left(y, z))

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


top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))

Relative ADPs:

bot → car(new, bot)


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

top(right(car(old, x), bot)) → TOP(left(car(old, x), bot))
top(right(x, car(y, car(old, z)))) → TOP(left(x, car(old, z)))
top(left(bot, car(old, x))) → TOP(right(bot, car(old, x)))
top(left(car(x, y), car(old, z))) → TOP(right(y, car(old, z)))
top(right(car(old, x), car(y, z))) → TOP(left(car(old, x), z))
top(left(car(x, car(old, y)), z)) → TOP(right(car(old, y), z))

Relative ADPs:

top(right(x, car(y, z))) → TOP(right(x, z))
top(left(car(x, y), z)) → TOP(left(y, z))


Ordered with Polynomial interpretation [POLO]:

POL(BOT) = 3   
POL(TOP(x1)) = 2 + 3·x1   
POL(bot) = 1   
POL(car(x1, x2)) = 3·x1 + x2   
POL(left(x1, x2)) = 2 + x1 + x2   
POL(new) = 0   
POL(old) = 2   
POL(right(x1, x2)) = 2 + x1 + x2   
POL(top(x1)) = 0   

(6) Obligation:

Relative ADP Problem with
absolute ADPs:

top(right(car(old, x), bot)) → TOP(left(car(old, x), bot))
top(right(x, car(y, car(old, z)))) → TOP(left(x, car(old, z)))
top(left(bot, car(old, x))) → TOP(right(bot, car(old, x)))
top(left(car(x, y), car(old, z))) → TOP(right(y, car(old, z)))
top(right(car(old, x), car(y, z))) → TOP(left(car(old, x), z))
top(left(car(x, car(old, y)), z)) → TOP(right(car(old, y), z))

and relative ADPs:

top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))
bot → car(new, bot)
top(right(x, car(y, z))) → TOP(right(x, z))
top(left(car(x, y), z)) → TOP(left(y, z))

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


top(left(bot, car(old, x))) → TOP(right(bot, car(old, x)))
top(left(car(x, y), car(old, z))) → TOP(right(y, car(old, z)))

Relative ADPs:

top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))
bot → car(new, bot)


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

top(right(car(old, x), bot)) → TOP(left(car(old, x), bot))
top(right(x, car(y, car(old, z)))) → TOP(left(x, car(old, z)))
top(right(car(old, x), car(y, z))) → TOP(left(car(old, x), z))
top(left(car(x, car(old, y)), z)) → TOP(right(car(old, y), z))

Relative ADPs:

top(right(x, car(y, z))) → TOP(right(x, z))
top(left(car(x, y), z)) → TOP(left(y, z))


Ordered with Polynomial interpretation [POLO]:

POL(BOT) = 3   
POL(TOP(x1)) = 3·x1   
POL(bot) = 0   
POL(car(x1, x2)) = x1 + 3·x2   
POL(left(x1, x2)) = 2 + 3·x2   
POL(new) = 0   
POL(old) = 3   
POL(right(x1, x2)) = 2 + x2   
POL(top(x1)) = 0   

(8) Obligation:

Relative ADP Problem with
absolute ADPs:

top(right(car(old, x), bot)) → TOP(left(car(old, x), bot))
top(right(x, car(y, car(old, z)))) → TOP(left(x, car(old, z)))
top(right(car(old, x), car(y, z))) → TOP(left(car(old, x), z))
top(left(car(x, car(old, y)), z)) → TOP(right(car(old, y), z))

and relative ADPs:

top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(left(car(x, y), car(old, z))) → top(right(y, car(old, z)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))
bot → car(new, bot)
top(right(x, car(y, z))) → TOP(right(x, z))
top(left(car(x, y), z)) → TOP(left(y, z))

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


top(right(x, car(y, car(old, z)))) → TOP(left(x, car(old, z)))

Relative ADPs:

top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(left(car(x, y), car(old, z))) → top(right(y, car(old, z)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))
bot → car(new, bot)


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

top(right(car(old, x), bot)) → TOP(left(car(old, x), bot))
top(right(car(old, x), car(y, z))) → TOP(left(car(old, x), z))
top(left(car(x, car(old, y)), z)) → TOP(right(car(old, y), z))

Relative ADPs:

top(right(x, car(y, z))) → TOP(right(x, z))
top(left(car(x, y), z)) → TOP(left(y, z))


Ordered with Polynomial interpretation [POLO]:

POL(BOT) = 3   
POL(TOP(x1)) = 3·x1   
POL(bot) = 0   
POL(car(x1, x2)) = 2·x1 + 2·x2   
POL(left(x1, x2)) = 2 + 3·x2   
POL(new) = 0   
POL(old) = 2   
POL(right(x1, x2)) = 2 + 2·x2   
POL(top(x1)) = 0   

(10) Obligation:

Relative ADP Problem with
absolute ADPs:

top(right(car(old, x), bot)) → TOP(left(car(old, x), bot))
top(right(car(old, x), car(y, z))) → TOP(left(car(old, x), z))
top(left(car(x, car(old, y)), z)) → TOP(right(car(old, y), z))

and relative ADPs:

top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(left(car(x, y), car(old, z))) → top(right(y, car(old, z)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))
bot → car(new, bot)
top(right(x, car(y, z))) → TOP(right(x, z))
top(right(x, car(y, car(old, z)))) → top(left(x, car(old, z)))
top(left(car(x, y), z)) → TOP(left(y, z))

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


top(right(car(old, x), bot)) → TOP(left(car(old, x), bot))
top(right(car(old, x), car(y, z))) → TOP(left(car(old, x), z))
top(left(car(x, car(old, y)), z)) → TOP(right(car(old, y), z))

Relative ADPs:

top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(left(car(x, y), car(old, z))) → top(right(y, car(old, z)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))
bot → car(new, bot)
top(right(x, car(y, car(old, z)))) → top(left(x, car(old, z)))


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(BOT) = 3   
POL(TOP(x1)) = 3·x1   
POL(bot) = 0   
POL(car(x1, x2)) = x1 + 3·x2   
POL(left(x1, x2)) = 2 + x1 + 3·x2   
POL(new) = 0   
POL(old) = 1   
POL(right(x1, x2)) = 1 + 3·x1 + 3·x2   
POL(top(x1)) = 0   

(12) Obligation:

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

top(right(car(old, x), car(y, z))) → top(left(car(old, x), z))
top(left(bot, car(old, x))) → top(right(bot, car(old, x)))
top(right(car(old, x), bot)) → top(left(car(old, x), bot))
top(left(car(x, y), car(old, z))) → top(right(y, car(old, z)))
bot → car(new, bot)
top(right(x, car(y, z))) → TOP(right(x, z))
top(left(car(x, car(old, y)), z)) → top(right(car(old, y), z))
top(right(x, car(y, car(old, z)))) → top(left(x, car(old, z)))
top(left(car(x, y), z)) → TOP(left(y, z))

(13) DAbsisEmptyProof (EQUIVALENT transformation)

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

(14) YES