YES Termination proof of trafic.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRSRRRProof (⇔, 95 ms)
↳2 RelTRS
↳3 RelTRSRRRProof (⇔, 102 ms)
↳4 RelTRS
↳5 RelTRSRRRProof (⇔, 9 ms)
↳6 RelTRS
↳7 RelTRSRRRProof (⇔, 0 ms)
↳8 RelTRS
↳9 RIsEmptyProof (⇔, 0 ms)
↳10 YES

(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) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(bot) = 0   
POL(east(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(new(x1)) = x1   
POL(north(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(old(x1)) = 1 + x1   
POL(south(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(top(x1)) = x1   
POL(west(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

top(north(old(n), e, s, w)) → top(east(n, e, s, w))
top(east(n, old(e), s, w)) → top(south(n, e, s, w))
top(south(n, e, old(s), w)) → top(west(n, e, s, w))
top(west(n, e, s, old(w))) → top(north(n, e, s, w))
Rules from S:

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


(2) Obligation:

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

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

(3) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(top(x1)) =
/1\
\1/
 +
/11\
\00/
·x1

POL(north(x1, x2, x3, x4)) =
/0\
\1/
 +
/11\
\00/
·x1 +
/10\
\11/
·x2 +
/11\
\10/
·x3 +
/10\
\11/
·x4

POL(new(x1)) =
/0\
\0/
 +
/10\
\11/
·x1

POL(old(x1)) =
/1\
\1/
 +
/10\
\00/
·x1

POL(east(x1, x2, x3, x4)) =
/0\
\0/
 +
/10\
\11/
·x1 +
/10\
\01/
·x2 +
/11\
\10/
·x3 +
/11\
\10/
·x4

POL(south(x1, x2, x3, x4)) =
/1\
\0/
 +
/10\
\01/
·x1 +
/10\
\11/
·x2 +
/11\
\00/
·x3 +
/10\
\01/
·x4

POL(west(x1, x2, x3, x4)) =
/0\
\1/
 +
/10\
\01/
·x1 +
/10\
\11/
·x2 +
/11\
\10/
·x3 +
/10\
\01/
·x4

POL(bot) =
/0\
\1/
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

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(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)))
Rules from S:
none


(4) Obligation:

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

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

(5) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(bot) = 0   
POL(east(x1, x2, x3, x4)) = 1 + x1 + x2 + x3 + x4   
POL(new(x1)) = x1   
POL(north(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(old(x1)) = x1   
POL(south(x1, x2, x3, x4)) = 1 + x1 + x2 + x3 + x4   
POL(top(x1)) = x1   
POL(west(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

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(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)))
Rules from S:
none


(6) Obligation:

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

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

(7) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(bot) = 0   
POL(east(x1, x2, x3, x4)) = 1 + x1 + x2 + x3 + x4   
POL(new(x1)) = x1   
POL(north(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(old(x1)) = x1   
POL(south(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(top(x1)) = x1   
POL(west(x1, x2, x3, x4)) = 1 + x1 + x2 + x3 + x4   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

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(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(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(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))
Rules from S:
none


(8) Obligation:

Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:

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

(9) RIsEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(10) YES