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 matchbox @ termCOMP 2023)

1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

[i(x₁)]

x₁ +

[e(x₁)]

x₁ +

1/3

[w(x₁)]

x₁ +

1/3

[t(x₁)]

x₁ +

[r(x₁)]

x₁ +

2/3

all of the following rules can be deleted.

t(e(x1))	→	r(e(x1))	(4)
e(r(x1))	→	e(w(x1))	(6)

1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

e(r(x1))	→	r(w(x1))	(8)
t(i(x1))	→	r(e(x1))	(9)
w(e(x1))	→	i(r(x1))	(10)
r(w(x1))	→	t(i(x1))	(11)
r(e(t(i(r(x1)))))	→	e(t(i(r(w(e(x1))))))	(12)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

e^#(r(x1))	→	w^#(x1)	(13)
e^#(r(x1))	→	r^#(w(x1))	(14)
w^#(e(x1))	→	r^#(x1)	(15)
t^#(i(x1))	→	e^#(x1)	(16)
t^#(i(x1))	→	r^#(e(x1))	(17)
r^#(e(t(i(r(x1)))))	→	e^#(x1)	(18)
r^#(e(t(i(r(x1)))))	→	e^#(t(i(r(w(e(x1))))))	(19)
r^#(e(t(i(r(x1)))))	→	w^#(e(x1))	(20)
r^#(e(t(i(r(x1)))))	→	t^#(i(r(w(e(x1)))))	(21)
r^#(e(t(i(r(x1)))))	→	r^#(w(e(x1)))	(22)
r^#(w(x1))	→	t^#(i(x1))	(23)

1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

[i(x₁)]

x₁ +

[e(x₁)]

x₁ +

[w(x₁)]

x₁ +

[t(x₁)]

x₁ +

[r(x₁)]

x₁ +

[e^#(x₁)]

x₁ +

[w^#(x₁)]

x₁ +

[t^#(x₁)]

x₁ +

[r^#(x₁)]

x₁ +

together with the usable rules

e(r(x1))	→	r(w(x1))	(8)
t(i(x1))	→	r(e(x1))	(9)
w(e(x1))	→	i(r(x1))	(10)
r(w(x1))	→	t(i(x1))	(11)
r(e(t(i(r(x1)))))	→	e(t(i(r(w(e(x1))))))	(12)

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

e^#(r(x1))	→	w^#(x1)	(13)
w^#(e(x1))	→	r^#(x1)	(15)
t^#(i(x1))	→	e^#(x1)	(16)
r^#(e(t(i(r(x1)))))	→	e^#(x1)	(18)
r^#(e(t(i(r(x1)))))	→	w^#(e(x1))	(20)
r^#(e(t(i(r(x1)))))	→	t^#(i(r(w(e(x1)))))	(21)
r^#(e(t(i(r(x1)))))	→	r^#(w(e(x1)))	(22)

and no rules could be deleted.

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

e^#(r(x1))	→	r^#(w(x1))	(14)
r^#(e(t(i(r(x1)))))	→	e^#(t(i(r(w(e(x1))))))	(19)
r^#(w(x1))	→	t^#(i(x1))	(23)
t^#(i(x1))	→	r^#(e(x1))	(17)

1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

[i(x₁)]

0	0	0
-3	-3	0
-3	-3	-3

· x₁ +

-∞

[e(x₁)]

0	0	0
-3	-3	0
-3	-3	0

· x₁ +

-∞

[w(x₁)]

0	0	3
0	0	3
-3	-3	0

· x₁ +

-∞

[t(x₁)]

0	3	3
0	3	3
0	3	3

· x₁ +

-∞

[r(x₁)]

0	0	3
0	0	3
0	0	3

· x₁ +

-∞

[e^#(x₁)]

1	1	4
1	1	4
1	1	4

· x₁ +

-∞

[t^#(x₁)]

2	5	5
2	5	5
2	5	5

· x₁ +

-∞

[r^#(x₁)]

2	2	4
2	2	4
2	2	4

· x₁ +

-∞

together with the usable rules

e(r(x1))	→	r(w(x1))	(8)
t(i(x1))	→	r(e(x1))	(9)
w(e(x1))	→	i(r(x1))	(10)
r(w(x1))	→	t(i(x1))	(11)
r(e(t(i(r(x1)))))	→	e(t(i(r(w(e(x1))))))	(12)

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

e^#(r(x1))

→

r^#(w(x1))

(14)

could be deleted.

1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

[i(x₁)]

x₁ +

[e(x₁)]

x₁ +

[w(x₁)]

x₁ +

[t(x₁)]

x₁ +

[r(x₁)]

x₁ +

[e^#(x₁)]

x₁ +

[t^#(x₁)]

x₁ +

[r^#(x₁)]

x₁ +

together with the usable rules

e(r(x1))	→	r(w(x1))	(8)
t(i(x1))	→	r(e(x1))	(9)
w(e(x1))	→	i(r(x1))	(10)
r(w(x1))	→	t(i(x1))	(11)
r(e(t(i(r(x1)))))	→	e(t(i(r(w(e(x1))))))	(12)

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

r^#(e(t(i(r(x1)))))

→

e^#(t(i(r(w(e(x1))))))

(19)

and no rules could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

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

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

[i(x₁)]

0	0
-2	-2

· x₁ +

-∞

[e(x₁)]

0	0
-2	-2

· x₁ +

-∞

[w(x₁)]

0	0
0	0

· x₁ +

-∞

[t(x₁)]

0	2
-2	0

· x₁ +

-∞

[r(x₁)]

0	0
-2	-2

· x₁ +

-∞

[t^#(x₁)]

7	9
7	9

· x₁ +

-∞

[r^#(x₁)]

5	7
5	7

· x₁ +

-∞

together with the usable rules

e(r(x1))	→	r(w(x1))	(8)
t(i(x1))	→	r(e(x1))	(9)
w(e(x1))	→	i(r(x1))	(10)
r(w(x1))	→	t(i(x1))	(11)
r(e(t(i(r(x1)))))	→	e(t(i(r(w(e(x1))))))	(12)

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

t^#(i(x1))

→

r^#(e(x1))

(17)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

[i(x₁)]

x₁ +

[e(x₁)]

x₁ +

[w(x₁)]

x₁ +

[t(x₁)]

x₁ +

[r(x₁)]

x₁ +

[t^#(x₁)]

x₁ +

[r^#(x₁)]

x₁ +

together with the usable rules

e(r(x1))	→	r(w(x1))	(8)
t(i(x1))	→	r(e(x1))	(9)
w(e(x1))	→	i(r(x1))	(10)
r(w(x1))	→	t(i(x1))	(11)
r(e(t(i(r(x1)))))	→	e(t(i(r(w(e(x1))))))	(12)

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

r^#(w(x1))

→

t^#(i(x1))

(23)

and no rules could be deleted.

1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.