Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nosorts_noand_iGM)

The rewrite relation of the following TRS is considered.

active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(X,nil))	→	mark(X)	(2)
active(__(nil,X))	→	mark(X)	(3)
active(U11(tt))	→	mark(U12(tt))	(4)
active(U12(tt))	→	mark(tt)	(5)
active(isNePal(__(I,__(P,I))))	→	mark(U11(tt))	(6)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(7)
mark(nil)	→	active(nil)	(8)
mark(U11(X))	→	active(U11(mark(X)))	(9)
mark(tt)	→	active(tt)	(10)
mark(U12(X))	→	active(U12(mark(X)))	(11)
mark(isNePal(X))	→	active(isNePal(mark(X)))	(12)
__(mark(X1),X2)	→	__(X1,X2)	(13)
__(X1,mark(X2))	→	__(X1,X2)	(14)
__(active(X1),X2)	→	__(X1,X2)	(15)
__(X1,active(X2))	→	__(X1,X2)	(16)
U11(mark(X))	→	U11(X)	(17)
U11(active(X))	→	U11(X)	(18)
U12(mark(X))	→	U12(X)	(19)
U12(active(X))	→	U12(X)	(20)
isNePal(mark(X))	→	isNePal(X)	(21)
isNePal(active(X))	→	isNePal(X)	(22)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[tt]

0	0	0
0	0	0
0	0	0

[active(x₁)]

1	0	0
0	0	0
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

1	0	0
1	0	0
0	0	0

[U11(x₁)]

1	0	0
0	1	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	0	0
0	1	1
0	0	0

· x₁ +

1	0	0
0	0	0
0	1	1

· x₂ +

0	0	0
0	0	0
0	0	0

[isNePal(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[U12(x₁)]

1	1	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	0	0
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

active(__(X,nil))	→	mark(X)	(2)
active(__(nil,X))	→	mark(X)	(3)
active(isNePal(__(I,__(P,I))))	→	mark(U11(tt))	(6)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[tt]

1	0	0
0	0	0
0	0	0

[active(x₁)]

1	0	0
1	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	0	0
0	0	1
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[isNePal(x₁)]

1	0	1
0	0	1
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[U12(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
1	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

active(U11(tt))

→

mark(U12(tt))

(4)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[tt]

1	0	0
0	0	0
0	0	0

[active(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
1	0	0

[__(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[isNePal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[U12(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
1	0	0

[mark(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

active(U12(tt))

→

mark(tt)

(5)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[tt]

0	0	0
0	0	0
0	0	0

[active(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	1	0
0	1	0
0	0	0

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

0	0	0
1	0	0
0	0	0

[isNePal(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[U12(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

active(__(__(X,Y),Z))

→

mark(__(X,__(Y,Z)))

(1)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[tt]

1	0	0
0	0	0
1	0	0

[active(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

1	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	1
1	0	1
1	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	0	0
0	0	0
0	0	1

· x₁ +

1	0	1
0	0	0
1	0	1

· x₂ +

0	0	0
0	0	0
0	0	0

[isNePal(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[U12(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
1	0	0

[mark(x₁)]

1	0	1
1	0	0
1	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

mark(tt)	→	active(tt)	(10)
mark(U12(X))	→	active(U12(mark(X)))	(11)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[active(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
1	0	0
0	1	1

· x₂ +

0	0	0
0	0	0
0	0	0

[isNePal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[U12(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[mark(x₁)]

1	0	0
1	0	0
1	1	1

· x₁ +

0	0	0
0	0	0
1	0	0

all of the following rules can be deleted.

U12(mark(X))

→

U12(X)

(19)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[active(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

1	0	0
1	0	0
0	0	0

[nil]

0	0	0
0	0	0
1	0	0

[U11(x₁)]

1	1	1
1	1	1
0	0	0

· x₁ +

1	0	0
1	0	0
1	0	0

[__(x₁, x₂)]

1	0	1
0	1	0
0	0	0

· x₁ +

1	0	0
0	1	1
0	0	0

· x₂ +

1	0	0
1	0	0
1	0	0

[isNePal(x₁)]

1	1	1
1	1	1
0	0	0

· x₁ +

1	0	0
1	0	0
1	0	0

[U12(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[mark(x₁)]

1	1	1
1	1	1
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

all of the following rules can be deleted.

__(mark(X1),X2)	→	__(X1,X2)	(13)
__(active(X1),X2)	→	__(X1,X2)	(15)
__(X1,active(X2))	→	__(X1,X2)	(16)
U11(mark(X))	→	U11(X)	(17)
U11(active(X))	→	U11(X)	(18)
U12(active(X))	→	U12(X)	(20)
isNePal(mark(X))	→	isNePal(X)	(21)
isNePal(active(X))	→	isNePal(X)	(22)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[active(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	0	0
0	0	0
0	0	1

· x₁ +

1	1	1
0	0	0
1	0	1

· x₂ +

1	0	0
0	0	0
1	0	0

[isNePal(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	1
1	0	1
0	1	0

· x₁ +

0	0	0
1	0	0
0	0	0

all of the following rules can be deleted.

__(X1,mark(X2))

→

__(X1,X2)

(14)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[active(x₁)]

1	1	0
0	1	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	0
0	1	1
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	0	0
0	0	1
0	1	0

· x₁ +

1	1	1
0	0	0
0	1	1

· x₂ +

0	0	0
0	0	0
0	0	0

[isNePal(x₁)]

1	1	1
0	0	0
0	1	1

· x₁ +

0	0	0
0	0	0
1	0	0

[mark(x₁)]

1	1	1
0	1	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

mark(isNePal(X))

→

active(isNePal(mark(X)))

(12)

1.1.1.1.1.1.1.1.1.1 Bounds

The given TRS is match-(raise)-bounded by 1. This is shown by the following automaton.

final states:

{6}

transitions:

mark₁(6)	→	10
mark₁(6)	→	11
__₁(11,10)	→	12
active₀(6)	→	6
nil₀	→	6
__₀(6,6)	→	6
U11₀(6)	→	6
active₁(12)	→	6
active₁(12)	→	11
active₁(12)	→	10
mark₀(6)	→	6
nil₁	→	12
U11₁(10)	→	12

The automaton is closed under rewriting as it is compatible.