Certification Problem

Input (TPDB TRS_Relative/Mixed_relative_TRS/trafic)

The relative rewrite relation R/S is considered where R is the following TRS

top(north(old(n),e,s,w))	→	top(east(n,e,s,w))	(1)
top(north(new(n),old(e),s,w))	→	top(east(n,old(e),s,w))	(2)
top(north(new(n),e,old(s),w))	→	top(east(n,e,old(s),w))	(3)
top(north(new(n),e,s,old(w)))	→	top(east(n,e,s,old(w)))	(4)
top(east(n,old(e),s,w))	→	top(south(n,e,s,w))	(5)
top(east(old(n),new(e),s,w))	→	top(south(old(n),e,s,w))	(6)
top(east(n,new(e),old(s),w))	→	top(south(n,e,old(s),w))	(7)
top(east(n,new(e),s,old(w)))	→	top(south(n,e,s,old(w)))	(8)
top(south(n,e,old(s),w))	→	top(west(n,e,s,w))	(9)
top(south(old(n),e,new(s),w))	→	top(west(old(n),e,s,w))	(10)
top(south(n,old(e),new(s),w))	→	top(west(n,old(e),s,w))	(11)
top(south(n,e,new(s),old(w)))	→	top(west(n,e,s,old(w)))	(12)
top(west(n,e,s,old(w)))	→	top(north(n,e,s,w))	(13)
top(west(old(n),e,s,new(w)))	→	top(north(old(n),e,s,w))	(14)
top(west(n,old(e),s,new(w)))	→	top(north(n,old(e),s,w))	(15)
top(west(n,e,old(s),new(w)))	→	top(north(n,e,old(s),w))	(16)
top(north(bot,old(e),s,w))	→	top(east(bot,old(e),s,w))	(17)
top(north(bot,e,old(s),w))	→	top(east(bot,e,old(s),w))	(18)
top(north(bot,e,s,old(w)))	→	top(east(bot,e,s,old(w)))	(19)
top(east(old(n),bot,s,w))	→	top(south(old(n),bot,s,w))	(20)
top(east(n,bot,old(s),w))	→	top(south(n,bot,old(s),w))	(21)
top(east(n,bot,s,old(w)))	→	top(south(n,bot,s,old(w)))	(22)
top(south(old(n),e,bot,w))	→	top(west(old(n),e,bot,w))	(23)
top(south(n,old(e),bot,w))	→	top(west(n,old(e),bot,w))	(24)
top(south(n,e,bot,old(w)))	→	top(west(n,e,bot,old(w)))	(25)
top(west(old(n),e,s,bot))	→	top(north(old(n),e,s,bot))	(26)
top(west(n,old(e),s,bot))	→	top(north(n,old(e),s,bot))	(27)
top(west(n,e,old(s),bot))	→	top(north(n,e,old(s),bot))	(28)

and S is the following TRS.

top(south(n,e,old(s),w))	→	top(south(n,e,s,w))	(29)
top(south(n,e,new(s),w))	→	top(south(n,e,s,w))	(30)
top(west(n,e,s,old(w)))	→	top(west(n,e,s,w))	(31)
top(west(n,e,s,new(w)))	→	top(west(n,e,s,w))	(32)
bot	→	new(bot)	(33)
top(north(new(n),e,s,w))	→	top(north(n,e,s,w))	(34)
top(east(n,old(e),s,w))	→	top(east(n,e,s,w))	(35)
top(east(n,new(e),s,w))	→	top(east(n,e,s,w))	(36)
top(north(old(n),e,s,w))	→	top(north(n,e,s,w))	(37)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals

[top(x₁)]	=	1 · x₁
[north(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[old(x₁)]	=	1 + 1 · x₁
[east(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[new(x₁)]	=	1 · x₁
[south(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[west(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[bot]	=	0

all of the following rules can be deleted.

top(north(old(n),e,s,w))	→	top(east(n,e,s,w))	(1)
top(east(n,old(e),s,w))	→	top(south(n,e,s,w))	(5)
top(south(n,e,old(s),w))	→	top(west(n,e,s,w))	(9)
top(west(n,e,s,old(w)))	→	top(north(n,e,s,w))	(13)
top(south(n,e,old(s),w))	→	top(south(n,e,s,w))	(29)
top(west(n,e,s,old(w)))	→	top(west(n,e,s,w))	(31)
top(east(n,old(e),s,w))	→	top(east(n,e,s,w))	(35)
top(north(old(n),e,s,w))	→	top(north(n,e,s,w))	(37)

1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

[top(x₁)]

1	0
1	0

· x₁

[north(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
0	0

· x₃ +

1	1
0	0

· x₄

[new(x₁)]

1	1
1	1

· x₁

[old(x₁)]

1	0
1	0

· x₁

[east(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄

[south(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄

[west(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄

[bot]

all of the following rules can be deleted.

top(north(new(n),e,s,old(w)))	→	top(east(n,e,s,old(w)))	(4)
top(north(bot,e,s,old(w)))	→	top(east(bot,e,s,old(w)))	(19)

1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

[top(x₁)]

1	0
1	0

· x₁

[north(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
0	0

· x₃ +

1	1
1	1

· x₄

[new(x₁)]

1	1
1	1

· x₁

[old(x₁)]

1	0
0	0

· x₁

[east(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
0	0

· x₃ +

1	1
0	0

· x₄

[south(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄

[west(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄

[bot]

all of the following rules can be deleted.

top(east(n,new(e),s,old(w)))	→	top(south(n,e,s,old(w)))	(8)
top(east(n,bot,s,old(w)))	→	top(south(n,bot,s,old(w)))	(22)

1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

[top(x₁)]

1	1
1	1

· x₁

[north(x₁,...,x₄)]

1	0
0	1

· x₁ +

1	0
0	1

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[new(x₁)]

1	1
1	1

· x₁

[old(x₁)]

1	0
0	0

· x₁

[east(x₁,...,x₄)]

1	1
1	1

· x₁ +

1	0
0	1

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[south(x₁,...,x₄)]

1	1
1	0

· x₁ +

1	0
1	1

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[west(x₁,...,x₄)]

1	1
1	0

· x₁ +

1	0
0	1

· x₂ +

1	0
1	0

· x₃ +

1	0
1	0

· x₄

[bot]

all of the following rules can be deleted.

top(east(old(n),new(e),s,w))	→	top(south(old(n),e,s,w))	(6)
top(south(n,e,new(s),old(w)))	→	top(west(n,e,s,old(w)))	(12)
top(east(old(n),bot,s,w))	→	top(south(old(n),bot,s,w))	(20)
top(south(n,e,bot,old(w)))	→	top(west(n,e,bot,old(w)))	(25)

1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

[top(x₁)]

1	1
1	1

· x₁

[north(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[new(x₁)]

1	1
1	1

· x₁

[old(x₁)]

1	0
0	0

· x₁

[east(x₁,...,x₄)]

1	1
0	1

· x₁ +

1	0
0	1

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[south(x₁,...,x₄)]

1	1
0	1

· x₁ +

1	0
1	1

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[west(x₁,...,x₄)]

1	1
0	1

· x₁ +

1	1
0	0

· x₂ +

1	0
1	0

· x₃ +

1	1
0	0

· x₄

[bot]

all of the following rules can be deleted.

top(south(n,old(e),new(s),w))	→	top(west(n,old(e),s,w))	(11)
top(south(n,old(e),bot,w))	→	top(west(n,old(e),bot,w))	(24)

1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

[top(x₁)]

1	1
1	0

· x₁

[north(x₁,...,x₄)]

1	0
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[new(x₁)]

1	1
1	1

· x₁

[old(x₁)]

1	0
0	0

· x₁

[east(x₁,...,x₄)]

1	0
0	0

· x₁ +

1	1
0	0

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[south(x₁,...,x₄)]

1	0
0	0

· x₁ +

1	1
1	1

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[west(x₁,...,x₄)]

1	0
0	0

· x₁ +

1	1
0	1

· x₂ +

1	0
1	0

· x₃ +

1	1
1	1

· x₄

[bot]

all of the following rules can be deleted.

top(west(n,old(e),s,new(w)))	→	top(north(n,old(e),s,w))	(15)
top(west(n,old(e),s,bot))	→	top(north(n,old(e),s,bot))	(27)

1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

[top(x₁)]

1	0
1	1

· x₁

[north(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	0

· x₂ +

1	1
1	1

· x₃ +

1	1
0	0

· x₄

[new(x₁)]

1	1
1	1

· x₁

[old(x₁)]

1	0
0	0

· x₁

[east(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	0
0	1

· x₂ +

1	1
1	1

· x₃ +

1	1
0	0

· x₄

[south(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	1

· x₂ +

1	1
1	1

· x₃ +

1	1
0	0

· x₄

[west(x₁,...,x₄)]

1	1
0	0

· x₁ +

1	1
0	1

· x₂ +

1	1
1	1

· x₃ +

1	1
0	0

· x₄

[bot]

all of the following rules can be deleted.

top(north(new(n),old(e),s,w))	→	top(east(n,old(e),s,w))	(2)
top(north(bot,old(e),s,w))	→	top(east(bot,old(e),s,w))	(17)

1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

[top(x₁)]

1	1
1	1

· x₁

[north(x₁,...,x₄)]

1	0
0	1

· x₁ +

1	1
0	0

· x₂ +

1	0
1	0

· x₃ +

1	1
0	1

· x₄

[new(x₁)]

1	1
1	1

· x₁

[old(x₁)]

1	0
0	0

· x₁

[east(x₁,...,x₄)]

1	1
1	1

· x₁ +

1	0
0	1

· x₂ +

1	0
1	0

· x₃ +

1	1
0	1

· x₄

[south(x₁,...,x₄)]

1	1
1	1

· x₁ +

1	0
0	1

· x₂ +

1	0
1	0

· x₃ +

1	1
0	1

· x₄

[west(x₁,...,x₄)]

1	0
1	1

· x₁ +

1	0
0	1

· x₂ +

1	0
1	0

· x₃ +

1	0
0	1

· x₄

[bot]

all of the following rules can be deleted.

top(south(old(n),e,new(s),w))	→	top(west(old(n),e,s,w))	(10)
top(south(old(n),e,bot,w))	→	top(west(old(n),e,bot,w))	(23)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[top(x₁)]	=	1 · x₁
[north(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[new(x₁)]	=	1 · x₁
[old(x₁)]	=	1 · x₁
[east(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[south(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[west(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[bot]	=	0

all of the following rules can be deleted.

top(east(n,new(e),old(s),w))	→	top(south(n,e,old(s),w))	(7)
top(east(n,bot,old(s),w))	→	top(south(n,bot,old(s),w))	(21)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[top(x₁)]	=	1 · x₁
[north(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[new(x₁)]	=	1 · x₁
[old(x₁)]	=	1 · x₁
[east(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[west(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[bot]	=	0
[south(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄

all of the following rules can be deleted.

top(north(new(n),e,old(s),w))	→	top(east(n,e,old(s),w))	(3)
top(north(bot,e,old(s),w))	→	top(east(bot,e,old(s),w))	(18)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[top(x₁)]	=	1 · x₁
[west(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[old(x₁)]	=	1 · x₁
[new(x₁)]	=	1 · x₁
[north(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[bot]	=	0
[south(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[east(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄

all of the following rules can be deleted.

top(west(old(n),e,s,new(w)))	→	top(north(old(n),e,s,w))	(14)
top(west(n,e,old(s),new(w)))	→	top(north(n,e,old(s),w))	(16)
top(west(old(n),e,s,bot))	→	top(north(old(n),e,s,bot))	(26)
top(west(n,e,old(s),bot))	→	top(north(n,e,old(s),bot))	(28)

1.1.1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.