Termination proof of trafic.trs

Termination of the given RelTRS could be proven:

0 RelTRS

↳1 RelTRStoRelADPProof (⇔, 0 ms)

↳2 RelADPP

↳3 RelADPDepGraphProof (⇔, 20 ms)

↳4 RelADPP

↳5 RelADPReductionPairProof (⇔, 119 ms)

↳6 RelADPP

↳7 RelADPDepGraphProof (⇔, 0 ms)

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

and relative ADPs:

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))
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))
bot → new(bot)
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(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))

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

Relative ADPs:

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

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(south(n, e, new(s), old(w))) → TOP(west(n, e, s, old(w)))
top(south(n, old(e), new(s), w)) → TOP(west(n, old(e), s, w))
top(east(old(n), bot, s, w)) → TOP(south(old(n), bot, s, w))
top(east(n, new(e), s, old(w))) → TOP(south(n, e, s, old(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, e, bot, old(w))) → TOP(west(n, e, bot, 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(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(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(x₁)) = 3·x₁
POL(bot) = 0
POL(east(x₁, x₂, x₃, x₄)) = 1 + 3·x₁ + 3·x₂ + 2·x₃ + 2·x₄
POL(new(x₁)) = 3·x₁
POL(north(x₁, x₂, x₃, x₄)) = 1 + x₁ + 3·x₂ + 3·x₃ + 3·x₄
POL(old(x₁)) = 1 + 3·x₁
POL(south(x₁, x₂, x₃, x₄)) = 2 + 2·x₁ + 3·x₂ + x₃ + x₄
POL(top(x₁)) = 0
POL(west(x₁, x₂, x₃, x₄)) = 2 + x₁ + 3·x₂ + 3·x₃ + x₄

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

and relative ADPs:

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

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

(0) Obligation:

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

(2) Obligation:

(3) RelADPDepGraphProof (EQUIVALENT transformation)

(4) Obligation:

(5) RelADPReductionPairProof (EQUIVALENT transformation)

(6) Obligation:

(7) RelADPDepGraphProof (EQUIVALENT transformation)

(8) TRUE