Certification Problem

Input (TPDB SRS_Standard/Secret_05_SRS/matchbox1)

The rewrite relation of the following TRS is considered.

r(e(x1))	→	w(r(x1))	(1)
i(t(x1))	→	e(r(x1))	(2)
e(w(x1))	→	r(i(x1))	(3)
t(e(x1))	→	r(e(x1))	(4)
w(r(x1))	→	i(t(x1))	(5)
e(r(x1))	→	e(w(x1))	(6)
r(i(t(e(r(x1)))))	→	e(w(r(i(t(e(x1))))))	(7)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

i^#(t(x1))	→	r^#(x1)	(8)
r^#(i(t(e(r(x1)))))	→	w^#(r(i(t(e(x1)))))	(9)
e^#(w(x1))	→	r^#(i(x1))	(10)
r^#(i(t(e(r(x1)))))	→	t^#(e(x1))	(11)
w^#(r(x1))	→	i^#(t(x1))	(12)
w^#(r(x1))	→	t^#(x1)	(13)
e^#(w(x1))	→	i^#(x1)	(14)
r^#(i(t(e(r(x1)))))	→	r^#(i(t(e(x1))))	(15)
r^#(i(t(e(r(x1)))))	→	e^#(x1)	(16)
r^#(i(t(e(r(x1)))))	→	e^#(w(r(i(t(e(x1))))))	(17)
t^#(e(x1))	→	r^#(e(x1))	(18)
r^#(e(x1))	→	r^#(x1)	(19)
e^#(r(x1))	→	e^#(w(x1))	(20)
i^#(t(x1))	→	e^#(r(x1))	(21)
r^#(i(t(e(r(x1)))))	→	i^#(t(e(x1)))	(22)
r^#(e(x1))	→	w^#(r(x1))	(23)
e^#(r(x1))	→	w^#(x1)	(24)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

e^#(r(x1))	→	w^#(x1)	(24)
e^#(w(x1))	→	i^#(x1)	(14)
r^#(e(x1))	→	w^#(r(x1))	(23)
w^#(r(x1))	→	t^#(x1)	(13)
r^#(i(t(e(r(x1)))))	→	i^#(t(e(x1)))	(22)
i^#(t(x1))	→	e^#(r(x1))	(21)
e^#(r(x1))	→	e^#(w(x1))	(20)
r^#(e(x1))	→	r^#(x1)	(19)
w^#(r(x1))	→	i^#(t(x1))	(12)
r^#(i(t(e(r(x1)))))	→	t^#(e(x1))	(11)
e^#(w(x1))	→	r^#(i(x1))	(10)
t^#(e(x1))	→	r^#(e(x1))	(18)
r^#(i(t(e(r(x1)))))	→	w^#(r(i(t(e(x1)))))	(9)
r^#(i(t(e(r(x1)))))	→	e^#(w(r(i(t(e(x1))))))	(17)
r^#(i(t(e(r(x1)))))	→	e^#(x1)	(16)
r^#(i(t(e(r(x1)))))	→	r^#(i(t(e(x1))))	(15)
i^#(t(x1))	→	r^#(x1)	(8)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[w^#(x₁)]	=	x₁ + 15923
[e^#(x₁)]	=	x₁ + 15923
[r(x₁)]	=	x₁ + 31846
[t(x₁)]	=	x₁ + 47769
[w(x₁)]	=	x₁ + 15923
[i(x₁)]	=	x₁ + 0
[r^#(x₁)]	=	x₁ + 31846
[e(x₁)]	=	x₁ + 15923
[t^#(x₁)]	=	x₁ + 47768
[i^#(x₁)]	=	x₁ + 0

together with the usable rules

t(e(x1))	→	r(e(x1))	(4)
r(e(x1))	→	w(r(x1))	(1)
e(w(x1))	→	r(i(x1))	(3)
w(r(x1))	→	i(t(x1))	(5)
r(i(t(e(r(x1)))))	→	e(w(r(i(t(e(x1))))))	(7)
e(r(x1))	→	e(w(x1))	(6)
i(t(x1))	→	e(r(x1))	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

e^#(r(x1))	→	w^#(x1)	(24)
e^#(w(x1))	→	i^#(x1)	(14)
w^#(r(x1))	→	t^#(x1)	(13)
r^#(i(t(e(r(x1)))))	→	i^#(t(e(x1)))	(22)
e^#(r(x1))	→	e^#(w(x1))	(20)
r^#(e(x1))	→	r^#(x1)	(19)
r^#(i(t(e(r(x1)))))	→	t^#(e(x1))	(11)
t^#(e(x1))	→	r^#(e(x1))	(18)
r^#(i(t(e(r(x1)))))	→	w^#(r(i(t(e(x1)))))	(9)
r^#(i(t(e(r(x1)))))	→	e^#(x1)	(16)
r^#(i(t(e(r(x1)))))	→	r^#(i(t(e(x1))))	(15)
i^#(t(x1))	→	r^#(x1)	(8)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

r^#(e(x1))	→	w^#(r(x1))	(23)
e^#(w(x1))	→	r^#(i(x1))	(10)
w^#(r(x1))	→	i^#(t(x1))	(12)
r^#(i(t(e(r(x1)))))	→	e^#(w(r(i(t(e(x1))))))	(17)
i^#(t(x1))	→	e^#(r(x1))	(21)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

[w^#(x₁)]

0	0
0	1

· x₁ +

41651

35841

[e^#(x₁)]

1	1
1	0

· x₁ +

[r(x₁)]

35842

[t(x₁)]

1	1
0	0

· x₁ +

5810

[w(x₁)]

0	1
0	0

· x₁ +

35841

[i(x₁)]

0	1
0	0

· x₁ +

30032

[r^#(x₁)]

1	0
1	0

· x₁ +

5810

5809

[e(x₁)]

35842

[t^#(x₁)]

[i^#(x₁)]

41650

35842

together with the usable rules

t(e(x1))	→	r(e(x1))	(4)
r(e(x1))	→	w(r(x1))	(1)
e(w(x1))	→	r(i(x1))	(3)
w(r(x1))	→	i(t(x1))	(5)
r(i(t(e(r(x1)))))	→	e(w(r(i(t(e(x1))))))	(7)
e(r(x1))	→	e(w(x1))	(6)
i(t(x1))	→	e(r(x1))	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

r^#(e(x1))	→	w^#(r(x1))	(23)
w^#(r(x1))	→	i^#(t(x1))	(12)
r^#(i(t(e(r(x1)))))	→	e^#(w(r(i(t(e(x1))))))	(17)
i^#(t(x1))	→	e^#(r(x1))	(21)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.