Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExProp7_Luc06_iGM)

The rewrite relation of the following TRS is considered.

active(f(0))	→	mark(cons(0,f(s(0))))	(1)
active(f(s(0)))	→	mark(f(p(s(0))))	(2)
active(p(s(X)))	→	mark(X)	(3)
mark(f(X))	→	active(f(mark(X)))	(4)
mark(0)	→	active(0)	(5)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(6)
mark(s(X))	→	active(s(mark(X)))	(7)
mark(p(X))	→	active(p(mark(X)))	(8)
f(mark(X))	→	f(X)	(9)
f(active(X))	→	f(X)	(10)
cons(mark(X1),X2)	→	cons(X1,X2)	(11)
cons(X1,mark(X2))	→	cons(X1,X2)	(12)
cons(active(X1),X2)	→	cons(X1,X2)	(13)
cons(X1,active(X2))	→	cons(X1,X2)	(14)
s(mark(X))	→	s(X)	(15)
s(active(X))	→	s(X)	(16)
p(mark(X))	→	p(X)	(17)
p(active(X))	→	p(X)	(18)

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

[cons(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	1
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[f(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[s(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	0	1
0	0	1

· x₁ +

0	0	0
1	0	0
1	0	0

[0]

0	0	0
1	0	0
0	0	0

[p(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
1	0	0

[active(x₁)]

1	0	0
0	1	1
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

cons(X1,mark(X2))

→

cons(X1,X2)

(12)

1.1 Rule Removal

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

[cons(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	1	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
1	0	0

[f(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[s(x₁)]

1	0	0
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	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[0]

0	0	0
0	0	0
0	0	0

[p(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[active(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

all of the following rules can be deleted.

cons(X1,active(X2))

→

cons(X1,X2)

(14)

1.1.1 Rule Removal

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

[cons(x₁, x₂)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	1	0

· x₂ +

0	0	0
0	0	0
0	0	0

[f(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[s(x₁)]

1	1	0
1	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[0]

0	0	0
0	0	0
0	0	0

[p(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[active(x₁)]

1	1	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(f(0))

→

mark(cons(0,f(s(0))))

(1)

1.1.1.1 Rule Removal

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

[cons(x₁, x₂)]

1	0	1
0	0	0
0	0	0

· x₁ +

1	0	1
0	0	0
1	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[f(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[mark(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[0]

1	0	0
0	0	0
0	0	0

[p(x₁)]

1	0	1
1	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[active(x₁)]

1	0	1
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(p(s(X)))

→

mark(X)

(3)

1.1.1.1.1 Rule Removal

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

[cons(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	1	0
0	1	1

· x₂ +

0	0	0
0	0	0
1	0	0

[f(x₁)]

1	1	1
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[s(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[0]

1	0	0
1	0	0
0	0	0

[p(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[active(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

active(f(s(0)))

→

mark(f(p(s(0))))

(2)

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

[cons(x₁, x₂)]

1	0	0
0	0	0
1	1	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[f(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[0]

0	0	0
1	0	0
0	0	0

[p(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[active(x₁)]

1	1	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.

f(mark(X))	→	f(X)	(9)
cons(mark(X1),X2)	→	cons(X1,X2)	(11)
s(mark(X))	→	s(X)	(15)
p(mark(X))	→	p(X)	(17)

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

[cons(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

1	0	0
0	0	0
0	0	0

[f(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[mark(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
1	0	0
0	0	0

[0]

1	0	0
0	0	0
0	0	0

[p(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[active(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

all of the following rules can be deleted.

mark(0)

→

active(0)

(5)

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

[cons(x₁, x₂)]

1	0	1
0	0	0
1	0	0

· x₁ +

1	0	0
0	0	0
1	0	0

· x₂ +

1	0	0
0	0	0
1	0	0

[f(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

1	0	0
0	0	0
1	0	0

[s(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
1	0	0
0	0	0

[mark(x₁)]

1	0	1
0	0	1
1	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[p(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
1	0	0
0	0	0

[active(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

mark(f(X))

→

active(f(mark(X)))

(4)

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

[cons(x₁, x₂)]

1	1	1
0	0	0
1	1	1

· x₁ +

1	1	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[f(x₁)]

1	1	1
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[s(x₁)]

1	1	1
0	0	0
1	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	1	1
1	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[p(x₁)]

1	0	0
0	0	0
0	1	1

· x₁ +

0	0	0
0	0	0
1	0	0

[active(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

mark(p(X))

→

active(p(mark(X)))

(8)

1.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

[cons(x₁, x₂)]

1	0	0
0	1	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

1	0	0
0	0	0
1	0	0

[f(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

1	0	0
0	0	0
1	0	0

[mark(x₁)]

1	0	1
0	0	0
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[p(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

[active(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

f(active(X))	→	f(X)	(10)
cons(active(X1),X2)	→	cons(X1,X2)	(13)
s(active(X))	→	s(X)	(16)
p(active(X))	→	p(X)	(18)

1.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:

{5}
transitions:

s₀(5) → 5

active₁(9) → 5

active₁(9) → 8

active₀(5) → 5

s₁(8) → 9

mark₁(5) → 8

mark₀(5) → 5

cons₀(5,5) → 5

cons₁(8,5) → 9

The automaton is closed under rewriting as it is compatible.

s₀(5)	→	5
active₁(9)	→	5
active₁(9)	→	8
active₀(5)	→	5
s₁(8)	→	9
mark₁(5)	→	8
mark₀(5)	→	5
cons₀(5,5)	→	5
cons₁(8,5)	→	9