YES Termination proof of Mixed_relative_TRS_trafic.ari

Termination of the given RelTRS could be proven:

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

(0) Obligation:

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

top(north(old(n), e, s, w)) → top(east(n, e, s, w))
top(north(new(n), old(e), s, w)) → top(east(n, old(e), s, w))
top(north(new(n), e, old(s), w)) → top(east(n, e, old(s), w))
top(north(new(n), e, s, old(w))) → top(east(n, e, s, old(w)))
top(east(n, old(e), s, w)) → top(south(n, e, s, w))
top(east(old(n), new(e), s, w)) → top(south(old(n), e, s, w))
top(east(n, new(e), old(s), w)) → top(south(n, e, old(s), w))
top(east(n, new(e), s, old(w))) → top(south(n, e, s, old(w)))
top(south(n, e, old(s), w)) → top(west(n, e, s, w))
top(south(old(n), e, new(s), w)) → top(west(old(n), e, s, w))
top(south(n, old(e), new(s), w)) → top(west(n, old(e), s, w))
top(south(n, e, new(s), old(w))) → top(west(n, e, s, old(w)))
top(west(n, e, s, old(w))) → top(north(n, e, s, w))
top(west(old(n), e, s, new(w))) → top(north(old(n), e, s, w))
top(west(n, old(e), s, new(w))) → top(north(n, old(e), s, w))
top(west(n, e, old(s), new(w))) → top(north(n, e, old(s), w))
top(north(bot, old(e), s, w)) → top(east(bot, old(e), s, w))
top(north(bot, e, old(s), w)) → top(east(bot, e, old(s), w))
top(north(bot, e, s, old(w))) → top(east(bot, e, s, old(w)))
top(east(old(n), bot, s, w)) → top(south(old(n), bot, s, w))
top(east(n, bot, old(s), w)) → top(south(n, bot, old(s), w))
top(east(n, bot, s, old(w))) → top(south(n, bot, s, old(w)))
top(south(old(n), e, bot, w)) → top(west(old(n), e, bot, w))
top(south(n, old(e), bot, w)) → top(west(n, old(e), bot, w))
top(south(n, e, bot, old(w))) → top(west(n, e, bot, old(w)))
top(west(old(n), e, s, bot)) → top(north(old(n), e, s, bot))
top(west(n, old(e), s, bot)) → top(north(n, old(e), s, bot))
top(west(n, e, old(s), bot)) → top(north(n, e, old(s), bot))

The relative TRS consists of the following S rules:

top(south(n, e, old(s), w)) → top(south(n, e, s, w))
top(south(n, e, new(s), w)) → top(south(n, e, s, w))
top(west(n, e, s, old(w))) → top(west(n, e, s, w))
top(west(n, e, s, new(w))) → top(west(n, e, s, w))
bot → new(bot)
top(north(new(n), e, s, w)) → top(north(n, e, s, w))
top(east(n, old(e), s, w)) → top(east(n, e, s, w))
top(east(n, new(e), s, w)) → top(east(n, e, s, w))
top(north(old(n), e, s, w)) → top(north(n, e, s, w))

(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(north(old(n), e, s, w)) → TOP(east(n, e, s, w))
top(north(new(n), old(e), s, w)) → TOP(east(n, old(e), s, w))
top(north(new(n), e, old(s), w)) → TOP(east(n, e, old(s), w))
top(north(new(n), e, s, old(w))) → TOP(east(n, e, s, old(w)))
top(east(n, old(e), s, w)) → TOP(south(n, e, s, w))
top(east(old(n), new(e), s, w)) → TOP(south(old(n), e, s, w))
top(east(n, new(e), old(s), w)) → TOP(south(n, e, old(s), w))
top(east(n, new(e), s, old(w))) → TOP(south(n, e, s, old(w)))
top(south(n, e, old(s), w)) → TOP(west(n, e, s, w))
top(south(old(n), e, new(s), w)) → TOP(west(old(n), e, s, w))
top(south(n, old(e), new(s), w)) → TOP(west(n, old(e), s, w))
top(south(n, e, new(s), old(w))) → TOP(west(n, e, s, old(w)))
top(west(n, e, s, old(w))) → TOP(north(n, e, s, w))
top(west(old(n), e, s, new(w))) → TOP(north(old(n), e, s, w))
top(west(n, old(e), s, new(w))) → TOP(north(n, old(e), s, w))
top(west(n, e, old(s), new(w))) → TOP(north(n, e, old(s), w))
top(north(bot, old(e), s, w)) → TOP(east(bot, old(e), s, w))
top(north(bot, old(e), s, w)) → top(east(BOT, old(e), s, w))
top(north(bot, e, old(s), w)) → TOP(east(bot, e, old(s), w))
top(north(bot, e, old(s), w)) → top(east(BOT, e, old(s), w))
top(north(bot, e, s, old(w))) → TOP(east(bot, e, s, old(w)))
top(north(bot, e, s, old(w))) → top(east(BOT, e, s, old(w)))
top(east(old(n), bot, s, w)) → TOP(south(old(n), bot, s, w))
top(east(old(n), bot, s, w)) → top(south(old(n), BOT, s, w))
top(east(n, bot, old(s), w)) → TOP(south(n, bot, old(s), w))
top(east(n, bot, old(s), w)) → top(south(n, BOT, old(s), w))
top(east(n, bot, s, old(w))) → TOP(south(n, bot, s, old(w)))
top(east(n, bot, s, old(w))) → top(south(n, BOT, s, old(w)))
top(south(old(n), e, bot, w)) → TOP(west(old(n), e, bot, w))
top(south(old(n), e, bot, w)) → top(west(old(n), e, BOT, w))
top(south(n, old(e), bot, w)) → TOP(west(n, old(e), bot, w))
top(south(n, old(e), bot, w)) → top(west(n, old(e), BOT, w))
top(south(n, e, bot, old(w))) → TOP(west(n, e, bot, old(w)))
top(south(n, e, bot, old(w))) → top(west(n, e, BOT, old(w)))
top(west(old(n), e, s, bot)) → TOP(north(old(n), e, s, bot))
top(west(old(n), e, s, bot)) → top(north(old(n), e, s, BOT))
top(west(n, old(e), s, bot)) → TOP(north(n, old(e), s, bot))
top(west(n, old(e), s, bot)) → top(north(n, old(e), s, BOT))
top(west(n, e, old(s), bot)) → TOP(north(n, e, old(s), bot))
top(west(n, e, old(s), bot)) → top(north(n, e, old(s), BOT))

and relative ADPs:

top(south(n, e, old(s), w)) → TOP(south(n, e, s, w))
top(south(n, e, new(s), w)) → TOP(south(n, e, s, w))
top(west(n, e, s, old(w))) → TOP(west(n, e, s, w))
top(west(n, e, s, new(w))) → TOP(west(n, e, s, w))
bot → new(BOT)
top(north(new(n), e, s, w)) → TOP(north(n, e, s, w))
top(east(n, old(e), s, w)) → TOP(east(n, e, s, w))
top(east(n, new(e), s, w)) → TOP(east(n, e, s, w))
top(north(old(n), e, s, w)) → TOP(north(n, e, s, w))

(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(east(n, bot, old(s), w)) → TOP(south(n, bot, old(s), w))
top(east(n, bot, s, old(w))) → TOP(south(n, bot, s, old(w)))
top(east(n, old(e), s, w)) → TOP(south(n, e, s, w))
top(east(old(n), bot, s, w)) → TOP(south(old(n), bot, s, w))
top(east(n, new(e), old(s), w)) → TOP(south(n, e, old(s), w))
top(east(old(n), new(e), s, w)) → TOP(south(old(n), e, s, w))
top(south(n, old(e), bot, w)) → TOP(west(n, old(e), bot, w))
top(south(old(n), e, new(s), w)) → TOP(west(old(n), e, s, w))
top(south(n, old(e), new(s), w)) → TOP(west(n, old(e), s, w))
top(east(n, new(e), s, old(w))) → TOP(south(n, e, s, old(w)))
top(north(bot, e, s, old(w))) → TOP(east(bot, e, s, old(w)))
top(south(old(n), e, bot, w)) → TOP(west(old(n), e, bot, w))
top(west(n, e, s, old(w))) → TOP(north(n, e, s, w))
top(west(n, old(e), s, new(w))) → TOP(north(n, old(e), s, w))
top(west(old(n), e, s, new(w))) → TOP(north(old(n), e, s, w))
top(west(n, e, old(s), new(w))) → TOP(north(n, e, old(s), w))
top(west(n, old(e), s, bot)) → TOP(north(n, old(e), s, bot))
top(west(n, e, old(s), bot)) → TOP(north(n, e, old(s), bot))
top(west(old(n), e, s, bot)) → TOP(north(old(n), e, s, bot))
top(north(bot, e, old(s), w)) → TOP(east(bot, e, old(s), w))
top(north(new(n), e, s, old(w))) → TOP(east(n, e, s, old(w)))
top(north(new(n), old(e), s, w)) → TOP(east(n, old(e), s, w))
top(south(n, e, new(s), old(w))) → TOP(west(n, e, s, old(w)))
top(north(old(n), e, s, w)) → TOP(east(n, e, s, w))
top(south(n, e, bot, old(w))) → TOP(west(n, e, bot, old(w)))
top(north(new(n), e, old(s), w)) → TOP(east(n, e, old(s), w))
top(north(bot, old(e), s, w)) → TOP(east(bot, old(e), s, w))
top(south(n, e, old(s), w)) → TOP(west(n, e, s, w))

and relative ADPs:

top(east(old(n), bot, s, w)) → top(south(old(n), bot, s, w))
top(west(n, e, s, new(w))) → TOP(west(n, e, s, w))
top(east(n, bot, s, old(w))) → top(south(n, bot, s, old(w)))
top(south(n, e, old(s), w)) → TOP(south(n, e, s, w))
bot → new(bot)
top(east(n, bot, old(s), w)) → top(south(n, bot, old(s), w))
top(north(new(n), e, s, w)) → TOP(north(n, e, s, w))
top(north(old(n), e, s, w)) → TOP(north(n, e, s, w))
top(west(n, old(e), s, bot)) → top(north(n, old(e), s, bot))
top(north(bot, e, old(s), w)) → top(east(bot, e, old(s), w))
top(east(n, old(e), s, w)) → TOP(east(n, e, s, w))
top(east(n, new(e), s, w)) → TOP(east(n, e, s, w))
top(west(n, e, s, old(w))) → TOP(west(n, e, s, w))
top(south(n, e, new(s), w)) → TOP(south(n, e, s, w))
top(south(n, old(e), bot, w)) → top(west(n, old(e), bot, w))
top(south(n, e, bot, old(w))) → top(west(n, e, bot, old(w)))
top(south(old(n), e, bot, w)) → top(west(old(n), e, bot, w))
top(west(n, e, old(s), bot)) → top(north(n, e, old(s), bot))
top(north(bot, e, s, old(w))) → top(east(bot, e, s, old(w)))
top(north(bot, old(e), s, w)) → top(east(bot, old(e), s, w))
top(west(old(n), e, s, bot)) → top(north(old(n), e, s, bot))

(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(north(old(n), e, s, w)) → TOP(east(n, e, s, w))
top(south(n, e, old(s), w)) → TOP(west(n, e, s, w))

Relative ADPs:

top(east(old(n), bot, s, w)) → top(south(old(n), bot, s, w))
top(south(n, e, old(s), w)) → TOP(south(n, e, s, w))
top(east(n, bot, s, old(w))) → top(south(n, bot, s, old(w)))
bot → new(bot)
top(east(n, bot, old(s), w)) → top(south(n, bot, old(s), w))
top(north(old(n), e, s, w)) → TOP(north(n, e, s, w))
top(west(n, old(e), s, bot)) → top(north(n, old(e), s, bot))
top(north(bot, e, old(s), w)) → top(east(bot, e, old(s), w))
top(south(n, old(e), bot, w)) → top(west(n, old(e), bot, w))
top(south(n, e, bot, old(w))) → top(west(n, e, bot, old(w)))
top(south(old(n), e, bot, w)) → top(west(old(n), e, bot, w))
top(west(n, e, old(s), bot)) → top(north(n, e, old(s), bot))
top(north(bot, e, s, old(w))) → top(east(bot, e, s, old(w)))
top(north(bot, old(e), s, w)) → top(east(bot, old(e), s, w))
top(west(old(n), e, s, bot)) → top(north(old(n), e, s, bot))


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

top(east(n, bot, old(s), w)) → TOP(south(n, bot, old(s), w))
top(east(n, bot, s, old(w))) → TOP(south(n, bot, s, old(w)))
top(east(n, old(e), s, w)) → TOP(south(n, e, s, w))
top(east(old(n), bot, s, w)) → TOP(south(old(n), bot, s, w))
top(east(n, new(e), old(s), w)) → TOP(south(n, e, old(s), w))
top(east(old(n), new(e), s, w)) → TOP(south(old(n), e, s, w))
top(south(n, old(e), bot, w)) → TOP(west(n, old(e), bot, w))
top(south(old(n), e, new(s), w)) → TOP(west(old(n), e, s, w))
top(south(n, old(e), new(s), w)) → TOP(west(n, old(e), s, w))
top(east(n, new(e), s, old(w))) → TOP(south(n, e, s, old(w)))
top(north(bot, e, s, old(w))) → TOP(east(bot, e, s, old(w)))
top(south(old(n), e, bot, w)) → TOP(west(old(n), e, bot, w))
top(west(n, e, s, old(w))) → TOP(north(n, e, s, w))
top(west(n, old(e), s, new(w))) → TOP(north(n, old(e), s, w))
top(west(old(n), e, s, new(w))) → TOP(north(old(n), e, s, w))
top(west(n, e, old(s), new(w))) → TOP(north(n, e, old(s), w))
top(west(n, old(e), s, bot)) → TOP(north(n, old(e), s, bot))
top(west(n, e, old(s), bot)) → TOP(north(n, e, old(s), bot))
top(west(old(n), e, s, bot)) → TOP(north(old(n), e, s, bot))
top(north(bot, e, old(s), w)) → TOP(east(bot, e, old(s), w))
top(north(new(n), e, s, old(w))) → TOP(east(n, e, s, old(w)))
top(north(new(n), old(e), s, w)) → TOP(east(n, old(e), s, w))
top(south(n, e, new(s), old(w))) → TOP(west(n, e, s, old(w)))
top(south(n, e, bot, old(w))) → TOP(west(n, e, bot, old(w)))
top(north(new(n), e, old(s), w)) → TOP(east(n, e, old(s), w))
top(north(bot, old(e), s, w)) → TOP(east(bot, old(e), s, w))

Relative ADPs:

top(west(n, e, s, new(w))) → TOP(west(n, e, s, w))
top(west(n, e, s, old(w))) → TOP(west(n, e, s, w))
top(south(n, e, new(s), w)) → TOP(south(n, e, s, w))
top(north(new(n), e, s, w)) → TOP(north(n, e, s, w))
top(east(n, old(e), s, w)) → TOP(east(n, e, s, w))
top(east(n, new(e), s, w)) → TOP(east(n, e, s, w))


Ordered with Polynomial interpretation [POLO]:

POL(BOT) = 3   
POL(TOP(x1)) = 2 + 2·x1   
POL(bot) = 3   
POL(east(x1, x2, x3, x4)) = 3 + 3·x1 + 3·x3   
POL(new(x1)) = x1   
POL(north(x1, x2, x3, x4)) = 3 + 3·x1 + 3·x3   
POL(old(x1)) = 3 + 2·x1   
POL(south(x1, x2, x3, x4)) = 3 + 3·x1 + 3·x3   
POL(top(x1)) = 3·x1   
POL(west(x1, x2, x3, x4)) = 3 + 3·x1 + 3·x3   

(6) Obligation:

Relative ADP Problem with
absolute ADPs:

top(east(n, bot, old(s), w)) → TOP(south(n, bot, old(s), w))
top(east(n, bot, s, old(w))) → TOP(south(n, bot, s, old(w)))
top(east(n, old(e), s, w)) → TOP(south(n, e, s, w))
top(east(old(n), bot, s, w)) → TOP(south(old(n), bot, s, w))
top(east(n, new(e), old(s), w)) → TOP(south(n, e, old(s), w))
top(east(old(n), new(e), s, w)) → TOP(south(old(n), e, s, w))
top(south(n, old(e), bot, w)) → TOP(west(n, old(e), bot, w))
top(south(old(n), e, new(s), w)) → TOP(west(old(n), e, s, w))
top(south(n, old(e), new(s), w)) → TOP(west(n, old(e), s, w))
top(east(n, new(e), s, old(w))) → TOP(south(n, e, s, old(w)))
top(north(bot, e, s, old(w))) → TOP(east(bot, e, s, old(w)))
top(south(old(n), e, bot, w)) → TOP(west(old(n), e, bot, w))
top(west(n, e, s, old(w))) → TOP(north(n, e, s, w))
top(west(n, old(e), s, new(w))) → TOP(north(n, old(e), s, w))
top(west(old(n), e, s, new(w))) → TOP(north(old(n), e, s, w))
top(west(n, e, old(s), new(w))) → TOP(north(n, e, old(s), w))
top(west(n, old(e), s, bot)) → TOP(north(n, old(e), s, bot))
top(west(n, e, old(s), bot)) → TOP(north(n, e, old(s), bot))
top(west(old(n), e, s, bot)) → TOP(north(old(n), e, s, bot))
top(north(bot, e, old(s), w)) → TOP(east(bot, e, old(s), w))
top(north(new(n), e, s, old(w))) → TOP(east(n, e, s, old(w)))
top(north(new(n), old(e), s, w)) → TOP(east(n, old(e), s, w))
top(south(n, e, new(s), old(w))) → TOP(west(n, e, s, old(w)))
top(south(n, e, bot, old(w))) → TOP(west(n, e, bot, old(w)))
top(north(new(n), e, old(s), w)) → TOP(east(n, e, old(s), w))
top(north(bot, old(e), s, w)) → TOP(east(bot, old(e), s, w))

and relative ADPs:

top(east(old(n), bot, s, w)) → top(south(old(n), bot, s, w))
top(west(n, e, s, new(w))) → TOP(west(n, e, s, w))
top(south(n, e, old(s), w)) → top(south(n, e, s, w))
top(east(n, bot, s, old(w))) → top(south(n, bot, s, old(w)))
bot → new(bot)
top(east(n, bot, old(s), w)) → top(south(n, bot, old(s), w))
top(north(new(n), e, s, w)) → TOP(north(n, e, s, w))
top(west(n, old(e), s, bot)) → top(north(n, old(e), s, bot))
top(north(bot, e, old(s), w)) → top(east(bot, e, old(s), w))
top(east(n, old(e), s, w)) → TOP(east(n, e, s, w))
top(east(n, new(e), s, w)) → TOP(east(n, e, s, w))
top(north(old(n), e, s, w)) → top(north(n, e, s, w))
top(west(n, e, s, old(w))) → TOP(west(n, e, s, w))
top(south(n, e, new(s), w)) → TOP(south(n, e, s, w))
top(north(old(n), e, s, w)) → top(east(n, e, s, w))
top(south(n, old(e), bot, w)) → top(west(n, old(e), bot, w))
top(south(n, e, bot, old(w))) → top(west(n, e, bot, old(w)))
top(south(old(n), e, bot, w)) → top(west(old(n), e, bot, w))
top(west(n, e, old(s), bot)) → top(north(n, e, old(s), bot))
top(north(bot, e, s, old(w))) → top(east(bot, e, s, old(w)))
top(north(bot, old(e), s, w)) → top(east(bot, old(e), s, w))
top(west(old(n), e, s, bot)) → top(north(old(n), e, s, bot))
top(south(n, e, old(s), w)) → top(west(n, e, s, w))

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

top(west(n, old(e), s, new(w))) → TOP(north(n, old(e), s, w))
top(east(n, bot, s, old(w))) → TOP(south(n, bot, s, old(w)))
top(west(n, e, old(s), new(w))) → TOP(north(n, e, old(s), w))
top(west(n, old(e), s, bot)) → TOP(north(n, old(e), s, bot))
top(west(n, e, old(s), bot)) → TOP(north(n, e, old(s), bot))
top(east(n, old(e), s, w)) → TOP(south(n, e, s, w))
top(east(old(n), bot, s, w)) → TOP(south(old(n), bot, s, w))
top(north(bot, e, old(s), w)) → TOP(east(bot, e, old(s), w))
top(east(old(n), new(e), s, w)) → TOP(south(old(n), e, s, w))
top(north(new(n), e, s, old(w))) → TOP(east(n, e, s, old(w)))
top(south(n, old(e), bot, w)) → TOP(west(n, old(e), bot, w))
top(north(new(n), old(e), s, w)) → TOP(east(n, old(e), s, w))
top(south(n, e, new(s), old(w))) → TOP(west(n, e, s, old(w)))
top(south(old(n), e, new(s), w)) → TOP(west(old(n), e, s, w))
top(south(n, old(e), new(s), w)) → TOP(west(n, old(e), s, w))
top(east(n, new(e), s, old(w))) → TOP(south(n, e, s, old(w)))
top(north(bot, e, s, old(w))) → TOP(east(bot, e, s, old(w)))
top(south(n, e, bot, old(w))) → TOP(west(n, e, bot, old(w)))
top(south(old(n), e, bot, w)) → TOP(west(old(n), e, bot, w))
top(north(new(n), e, old(s), w)) → TOP(east(n, e, old(s), w))
top(north(bot, old(e), s, w)) → TOP(east(bot, old(e), s, w))
top(west(n, e, s, old(w))) → TOP(north(n, e, s, w))

and relative ADPs:

top(west(old(n), e, s, new(w))) → top(north(old(n), e, s, w))
bot → new(bot)
top(north(new(n), e, s, w)) → TOP(north(n, e, s, w))
top(west(n, old(e), s, bot)) → top(north(n, old(e), s, bot))
top(north(bot, e, old(s), w)) → top(east(bot, e, old(s), w))
top(east(n, new(e), s, w)) → TOP(east(n, e, s, w))
top(north(old(n), e, s, w)) → top(north(n, e, s, w))
top(south(n, e, new(s), w)) → TOP(south(n, e, s, w))
top(north(old(n), e, s, w)) → top(east(n, e, s, w))
top(south(n, old(e), bot, w)) → top(west(n, old(e), bot, w))
top(south(n, e, bot, old(w))) → top(west(n, e, bot, old(w)))
top(west(n, e, old(s), bot)) → top(north(n, e, old(s), bot))
top(north(bot, old(e), s, w)) → top(east(bot, old(e), s, w))
top(south(n, e, old(s), w)) → top(west(n, e, s, w))
top(east(old(n), bot, s, w)) → top(south(old(n), bot, s, w))
top(west(n, e, s, new(w))) → TOP(west(n, e, s, w))
top(south(n, e, old(s), w)) → top(south(n, e, s, w))
top(east(n, bot, s, old(w))) → top(south(n, bot, s, old(w)))
top(east(n, bot, old(s), w)) → top(south(n, bot, old(s), w))
top(east(n, old(e), s, w)) → TOP(east(n, e, s, w))
top(west(n, e, s, old(w))) → TOP(west(n, e, s, w))
top(south(old(n), e, bot, w)) → top(west(old(n), e, bot, w))
top(east(n, new(e), old(s), w)) → top(south(n, e, old(s), w))
top(north(bot, e, s, old(w))) → top(east(bot, e, s, old(w)))
top(west(old(n), e, s, bot)) → top(north(old(n), e, s, bot))

(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(east(n, old(e), s, w)) → TOP(south(n, e, s, w))
top(north(bot, e, s, old(w))) → TOP(east(bot, e, s, old(w)))
top(north(bot, e, old(s), w)) → TOP(east(bot, e, old(s), w))
top(north(new(n), e, s, old(w))) → TOP(east(n, e, s, old(w)))
top(north(new(n), e, old(s), w)) → TOP(east(n, e, old(s), w))
top(north(new(n), old(e), s, w)) → TOP(east(n, old(e), s, w))
top(north(bot, old(e), s, w)) → TOP(east(bot, old(e), s, w))
top(west(n, e, s, old(w))) → TOP(north(n, e, s, w))

Relative ADPs:

top(east(old(n), bot, s, w)) → top(south(old(n), bot, s, w))
top(south(n, e, old(s), w)) → top(south(n, e, s, w))
top(west(old(n), e, s, new(w))) → top(north(old(n), e, s, w))
bot → new(bot)
top(east(n, bot, s, old(w))) → top(south(n, bot, s, old(w)))
top(east(n, bot, old(s), w)) → top(south(n, bot, old(s), w))
top(west(n, old(e), s, bot)) → top(north(n, old(e), s, bot))
top(east(n, old(e), s, w)) → TOP(east(n, e, s, w))
top(north(bot, e, old(s), w)) → top(east(bot, e, old(s), w))
top(north(old(n), e, s, w)) → top(north(n, e, s, w))
top(west(n, e, s, old(w))) → TOP(west(n, e, s, w))
top(north(old(n), e, s, w)) → top(east(n, e, s, w))
top(south(n, old(e), bot, w)) → top(west(n, old(e), bot, w))
top(south(n, e, bot, old(w))) → top(west(n, e, bot, old(w)))
top(south(old(n), e, bot, w)) → top(west(old(n), e, bot, w))
top(east(n, new(e), old(s), w)) → top(south(n, e, old(s), w))
top(west(n, e, old(s), bot)) → top(north(n, e, old(s), bot))
top(north(bot, e, s, old(w))) → top(east(bot, e, s, old(w)))
top(north(bot, old(e), s, w)) → top(east(bot, old(e), s, w))
top(west(old(n), e, s, bot)) → top(north(old(n), e, s, bot))
top(south(n, e, old(s), w)) → top(west(n, e, s, w))


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

top(west(n, old(e), s, new(w))) → TOP(north(n, old(e), s, w))
top(east(n, bot, s, old(w))) → TOP(south(n, bot, s, old(w)))
top(west(n, e, old(s), new(w))) → TOP(north(n, e, old(s), w))
top(west(n, old(e), s, bot)) → TOP(north(n, old(e), s, bot))
top(west(n, e, old(s), bot)) → TOP(north(n, e, old(s), bot))
top(east(old(n), bot, s, w)) → TOP(south(old(n), bot, s, w))
top(east(old(n), new(e), s, w)) → TOP(south(old(n), e, s, w))
top(south(n, old(e), bot, w)) → TOP(west(n, old(e), bot, w))
top(south(n, e, new(s), old(w))) → TOP(west(n, e, s, old(w)))
top(south(old(n), e, new(s), w)) → TOP(west(old(n), e, s, w))
top(south(n, old(e), new(s), w)) → TOP(west(n, old(e), s, w))
top(east(n, new(e), s, old(w))) → TOP(south(n, e, s, old(w)))
top(south(n, e, bot, old(w))) → TOP(west(n, e, bot, old(w)))
top(south(old(n), e, bot, w)) → TOP(west(old(n), e, bot, w))

Relative ADPs:

top(west(n, e, s, new(w))) → TOP(west(n, e, s, w))
top(south(n, e, new(s), w)) → TOP(south(n, e, s, w))
top(north(new(n), e, s, w)) → TOP(north(n, e, s, w))
top(east(n, new(e), s, w)) → TOP(east(n, e, s, w))


Ordered with Polynomial interpretation [POLO]:

POL(BOT) = 3   
POL(TOP(x1)) = 2 + 3·x1   
POL(bot) = 0   
POL(east(x1, x2, x3, x4)) = 3·x1 + 2·x2 + x3 + 3·x4   
POL(new(x1)) = 2·x1   
POL(north(x1, x2, x3, x4)) = 2 + 2·x1 + 2·x2 + x3 + 3·x4   
POL(old(x1)) = 1 + 2·x1   
POL(south(x1, x2, x3, x4)) = 1 + 2·x1 + 3·x2 + x3 + 2·x4   
POL(top(x1)) = 0   
POL(west(x1, x2, x3, x4)) = 1 + 2·x1 + 3·x2 + 2·x3 + 2·x4   

(10) Obligation:

Relative ADP Problem with
absolute ADPs:

top(west(n, old(e), s, new(w))) → TOP(north(n, old(e), s, w))
top(east(n, bot, s, old(w))) → TOP(south(n, bot, s, old(w)))
top(west(n, e, old(s), new(w))) → TOP(north(n, e, old(s), w))
top(west(n, old(e), s, bot)) → TOP(north(n, old(e), s, bot))
top(west(n, e, old(s), bot)) → TOP(north(n, e, old(s), bot))
top(east(old(n), bot, s, w)) → TOP(south(old(n), bot, s, w))
top(east(old(n), new(e), s, w)) → TOP(south(old(n), e, s, w))
top(south(n, old(e), bot, w)) → TOP(west(n, old(e), bot, w))
top(south(n, e, new(s), old(w))) → TOP(west(n, e, s, old(w)))
top(south(old(n), e, new(s), w)) → TOP(west(old(n), e, s, w))
top(south(n, old(e), new(s), w)) → TOP(west(n, old(e), s, w))
top(east(n, new(e), s, old(w))) → TOP(south(n, e, s, old(w)))
top(south(n, e, bot, old(w))) → TOP(west(n, e, bot, old(w)))
top(south(old(n), e, bot, w)) → TOP(west(old(n), e, bot, w))

and relative ADPs:

top(west(n, e, s, old(w))) → top(north(n, e, s, w))
top(west(old(n), e, s, new(w))) → top(north(old(n), e, s, w))
bot → new(bot)
top(north(new(n), e, s, old(w))) → top(east(n, e, s, old(w)))
top(north(new(n), e, s, w)) → TOP(north(n, e, s, w))
top(east(n, old(e), s, w)) → top(east(n, e, s, w))
top(north(new(n), old(e), s, w)) → top(east(n, old(e), s, w))
top(west(n, old(e), s, bot)) → top(north(n, old(e), s, bot))
top(north(bot, e, old(s), w)) → top(east(bot, e, old(s), w))
top(east(n, new(e), s, w)) → TOP(east(n, e, s, w))
top(north(old(n), e, s, w)) → top(north(n, e, s, w))
top(south(n, e, new(s), w)) → TOP(south(n, e, s, w))
top(west(n, e, s, old(w))) → top(west(n, e, s, w))
top(north(old(n), e, s, w)) → top(east(n, e, s, w))
top(south(n, old(e), bot, w)) → top(west(n, old(e), bot, w))
top(south(n, e, bot, old(w))) → top(west(n, e, bot, old(w)))
top(north(new(n), e, old(s), w)) → top(east(n, e, old(s), w))
top(west(n, e, old(s), bot)) → top(north(n, e, old(s), bot))
top(north(bot, old(e), s, w)) → top(east(bot, old(e), s, w))
top(south(n, e, old(s), w)) → top(west(n, e, s, w))
top(east(old(n), bot, s, w)) → top(south(old(n), bot, s, w))
top(west(n, e, s, new(w))) → TOP(west(n, e, s, w))
top(south(n, e, old(s), w)) → top(south(n, e, s, w))
top(east(n, bot, s, old(w))) → top(south(n, bot, s, old(w)))
top(east(n, bot, old(s), w)) → top(south(n, bot, old(s), w))
top(south(old(n), e, bot, w)) → top(west(old(n), e, bot, w))
top(east(n, new(e), old(s), w)) → top(south(n, e, old(s), w))
top(east(n, old(e), s, w)) → top(south(n, e, s, w))
top(north(bot, e, s, old(w))) → top(east(bot, e, s, old(w)))
top(west(old(n), e, s, bot)) → top(north(old(n), e, s, bot))

(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