Certification Problem

Input (TPDB SRS_Standard/Secret_07_SRS/x06)

The rewrite relation of the following TRS is considered.

a(b(x1))	→	c(b(x1))	(1)
c(c(x1))	→	d(b(x1))	(2)
d(x1)	→	c(e(x1))	(3)
b(b(x1))	→	f(x1)	(4)
c(b(x1))	→	g(x1)	(5)
e(x1)	→	f(x1)	(6)
e(x1)	→	b(b(x1))	(7)
f(g(x1))	→	a(c(x1))	(8)
g(f(x1))	→	e(x1)	(9)
a(x1)	→	b(c(x1))	(10)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

g^#(f(x1))	→	e^#(x1)	(11)
f^#(g(x1))	→	c^#(x1)	(12)
f^#(g(x1))	→	a^#(c(x1))	(13)
e^#(x1)	→	f^#(x1)	(14)
e^#(x1)	→	b^#(x1)	(15)
e^#(x1)	→	b^#(b(x1))	(16)
d^#(x1)	→	e^#(x1)	(17)
d^#(x1)	→	c^#(e(x1))	(18)
c^#(c(x1))	→	d^#(b(x1))	(19)
c^#(c(x1))	→	b^#(x1)	(20)
c^#(b(x1))	→	g^#(x1)	(21)
b^#(b(x1))	→	f^#(x1)	(22)
a^#(x1)	→	c^#(x1)	(23)
a^#(x1)	→	b^#(c(x1))	(24)
a^#(b(x1))	→	c^#(b(x1))	(25)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

g^#(f(x1))	→	e^#(x1)	(11)
e^#(x1)	→	f^#(x1)	(14)
f^#(g(x1))	→	c^#(x1)	(12)
c^#(c(x1))	→	d^#(b(x1))	(19)
d^#(x1)	→	e^#(x1)	(17)
e^#(x1)	→	b^#(x1)	(15)
b^#(b(x1))	→	f^#(x1)	(22)
f^#(g(x1))	→	a^#(c(x1))	(13)
a^#(x1)	→	c^#(x1)	(23)
c^#(c(x1))	→	b^#(x1)	(20)
c^#(b(x1))	→	g^#(x1)	(21)
a^#(x1)	→	b^#(c(x1))	(24)
a^#(b(x1))	→	c^#(b(x1))	(25)
e^#(x1)	→	b^#(b(x1))	(16)
d^#(x1)	→	c^#(e(x1))	(18)

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

[g(x₁)]

2	2
0	0

· x₁ +

-∞

[f(x₁)]

0	0
0	0

· x₁ +

-∞

[e(x₁)]

0	0
0	0

· x₁ +

-∞

[d(x₁)]

2	2
0	0

· x₁ +

-∞

[c(x₁)]

0	2
0	0

· x₁ +

-∞

[b(x₁)]

0	0
0	0

· x₁ +

-∞

[a(x₁)]

0	2
0	2

· x₁ +

-∞

[g^#(x₁)]

1	1
1	1

· x₁ +

-∞

[f^#(x₁)]

1	1
1	1

· x₁ +

-∞

[e^#(x₁)]

1	1
1	1

· x₁ +

-∞

[d^#(x₁)]

1	1
1	1

· x₁ +

-∞

[c^#(x₁)]

1	1
1	1

· x₁ +

-∞

[b^#(x₁)]

1	1
1	1

· x₁ +

-∞

[a^#(x₁)]

1	3
1	3

· x₁ +

-∞

together with the usable rules

a(b(x1))	→	c(b(x1))	(1)
c(c(x1))	→	d(b(x1))	(2)
d(x1)	→	c(e(x1))	(3)
b(b(x1))	→	f(x1)	(4)
c(b(x1))	→	g(x1)	(5)
e(x1)	→	f(x1)	(6)
e(x1)	→	b(b(x1))	(7)
f(g(x1))	→	a(c(x1))	(8)
g(f(x1))	→	e(x1)	(9)
a(x1)	→	b(c(x1))	(10)

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

f^#(g(x1))	→	c^#(x1)	(12)
a^#(b(x1))	→	c^#(b(x1))	(25)

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

g^#(f(x1))	→	e^#(x1)	(11)
e^#(x1)	→	f^#(x1)	(14)
f^#(g(x1))	→	a^#(c(x1))	(13)
a^#(x1)	→	c^#(x1)	(23)
c^#(c(x1))	→	d^#(b(x1))	(19)
d^#(x1)	→	e^#(x1)	(17)
e^#(x1)	→	b^#(x1)	(15)
b^#(b(x1))	→	f^#(x1)	(22)
e^#(x1)	→	b^#(b(x1))	(16)
d^#(x1)	→	c^#(e(x1))	(18)
c^#(c(x1))	→	b^#(x1)	(20)
c^#(b(x1))	→	g^#(x1)	(21)
a^#(x1)	→	b^#(c(x1))	(24)

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

[g(x₁)]

0	2
0	2

· x₁ +

-∞

[f(x₁)]

0	2
-2	0

· x₁ +

-∞

[e(x₁)]

0	2
-2	0

· x₁ +

-∞

[d(x₁)]

0	2
0	2

· x₁ +

-∞

[c(x₁)]

0	2
0	0

· x₁ +

-∞

[b(x₁)]

0	2
-2	0

· x₁ +

-∞

[a(x₁)]

2	2
0	0

· x₁ +

-∞

[g^#(x₁)]

13	15
13	15

· x₁ +

-∞

[f^#(x₁)]

11	13
11	13

· x₁ +

-∞

[e^#(x₁)]

13	15
13	15

· x₁ +

-∞

[d^#(x₁)]

13	15
13	15

· x₁ +

-∞

[c^#(x₁)]

13	13
13	13

· x₁ +

-∞

[b^#(x₁)]

11	13
11	13

· x₁ +

-∞

[a^#(x₁)]

13	13
13	13

· x₁ +

-∞

together with the usable rules

a(b(x1))	→	c(b(x1))	(1)
c(c(x1))	→	d(b(x1))	(2)
d(x1)	→	c(e(x1))	(3)
b(b(x1))	→	f(x1)	(4)
c(b(x1))	→	g(x1)	(5)
e(x1)	→	f(x1)	(6)
e(x1)	→	b(b(x1))	(7)
f(g(x1))	→	a(c(x1))	(8)
g(f(x1))	→	e(x1)	(9)
a(x1)	→	b(c(x1))	(10)

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

e^#(x1)	→	f^#(x1)	(14)
e^#(x1)	→	b^#(x1)	(15)
e^#(x1)	→	b^#(b(x1))	(16)
c^#(c(x1))	→	b^#(x1)	(20)

could be deleted.

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

[g(x₁)]

x₁ +

[f(x₁)]

x₁ +

[e(x₁)]

x₁ +

[d(x₁)]

x₁ +

[c(x₁)]

x₁ +

[b(x₁)]

x₁ +

[a(x₁)]

x₁ +

[g^#(x₁)]

x₁ +

[f^#(x₁)]

x₁ +

[e^#(x₁)]

x₁ +

[d^#(x₁)]

x₁ +

[c^#(x₁)]

x₁ +

[b^#(x₁)]

x₁ +

[a^#(x₁)]

x₁ +

together with the usable rules

a(b(x1))	→	c(b(x1))	(1)
c(c(x1))	→	d(b(x1))	(2)
d(x1)	→	c(e(x1))	(3)
b(b(x1))	→	f(x1)	(4)
c(b(x1))	→	g(x1)	(5)
e(x1)	→	f(x1)	(6)
e(x1)	→	b(b(x1))	(7)
f(g(x1))	→	a(c(x1))	(8)
g(f(x1))	→	e(x1)	(9)
a(x1)	→	b(c(x1))	(10)

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

g^#(f(x1))	→	e^#(x1)	(11)
a^#(x1)	→	c^#(x1)	(23)
d^#(x1)	→	e^#(x1)	(17)
c^#(b(x1))	→	g^#(x1)	(21)

and no rules could be deleted.

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

f^#(g(x1))	→	a^#(c(x1))	(13)
a^#(x1)	→	b^#(c(x1))	(24)
b^#(b(x1))	→	f^#(x1)	(22)

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

[g(x₁)]

3	3	3
0	0	0
0	0	0

· x₁ +

-∞

[f(x₁)]

0	0	0
0	0	0
0	0	0

· x₁ +

-∞

[e(x₁)]

0	0	0
0	0	0
0	0	0

· x₁ +

-∞

[d(x₁)]

3	3	3
0	0	0
0	0	0

· x₁ +

-∞

[c(x₁)]

0	3	3
0	0	0
-3	0	0

· x₁ +

-∞

[b(x₁)]

0	0	0
0	0	0
0	0	0

· x₁ +

-∞

[a(x₁)]

0	3	3
0	3	3
0	3	3

· x₁ +

-∞

[f^#(x₁)]

20	22	22
20	22	22
20	22	22

· x₁ +

-∞

[b^#(x₁)]

20	20	23
20	20	23
20	20	23

· x₁ +

-∞

[a^#(x₁)]

20	23	23
20	23	23
20	23	23

· x₁ +

-∞

together with the usable rules

a(b(x1))	→	c(b(x1))	(1)
c(c(x1))	→	d(b(x1))	(2)
d(x1)	→	c(e(x1))	(3)
b(b(x1))	→	f(x1)	(4)
c(b(x1))	→	g(x1)	(5)
e(x1)	→	f(x1)	(6)
e(x1)	→	b(b(x1))	(7)
f(g(x1))	→	a(c(x1))	(8)
g(f(x1))	→	e(x1)	(9)
a(x1)	→	b(c(x1))	(10)

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

b^#(b(x1))

→

f^#(x1)

(22)

could be deleted.

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

[g(x₁)]

x₁ +

[f(x₁)]

x₁ +

[e(x₁)]

x₁ +

[d(x₁)]

x₁ +

[c(x₁)]

x₁ +

[b(x₁)]

x₁ +

[a(x₁)]

x₁ +

[f^#(x₁)]

x₁ +

[b^#(x₁)]

x₁ +

[a^#(x₁)]

x₁ +

together with the usable rules

a(b(x1))	→	c(b(x1))	(1)
c(c(x1))	→	d(b(x1))	(2)
d(x1)	→	c(e(x1))	(3)
b(b(x1))	→	f(x1)	(4)
c(b(x1))	→	g(x1)	(5)
e(x1)	→	f(x1)	(6)
e(x1)	→	b(b(x1))	(7)
f(g(x1))	→	a(c(x1))	(8)
g(f(x1))	→	e(x1)	(9)
a(x1)	→	b(c(x1))	(10)

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

f^#(g(x1))	→	a^#(c(x1))	(13)
a^#(x1)	→	b^#(c(x1))	(24)

and no rules could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

c^#(c(x1))	→	d^#(b(x1))	(19)
d^#(x1)	→	c^#(e(x1))	(18)

1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

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

[g(x₁)]

3	3	3
0	0	0
0	0	0

· x₁ +

-∞

[f(x₁)]

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

· x₁ +

-∞

[e(x₁)]

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

· x₁ +

-∞

[d(x₁)]

3	3	3
0	0	3
0	0	0

· x₁ +

-∞

[c(x₁)]

0	3	3
0	0	0
0	0	0

· x₁ +

-∞

[b(x₁)]

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

· x₁ +

-∞

[a(x₁)]

0	3	3
0	3	3
-3	0	0

· x₁ +

-∞

[d^#(x₁)]

24	24	24
24	24	24
24	24	24

· x₁ +

-∞

[c^#(x₁)]

21	22	24
21	22	24
21	22	24

· x₁ +

-∞

together with the usable rules

a(b(x1))	→	c(b(x1))	(1)
c(c(x1))	→	d(b(x1))	(2)
d(x1)	→	c(e(x1))	(3)
b(b(x1))	→	f(x1)	(4)
c(b(x1))	→	g(x1)	(5)
e(x1)	→	f(x1)	(6)
e(x1)	→	b(b(x1))	(7)
f(g(x1))	→	a(c(x1))	(8)
g(f(x1))	→	e(x1)	(9)
a(x1)	→	b(c(x1))	(10)

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

d^#(x1)

→

c^#(e(x1))

(18)

could be deleted.

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

[g(x₁)]

x₁ +

[f(x₁)]

x₁ +

[e(x₁)]

x₁ +

[d(x₁)]

x₁ +

[c(x₁)]

x₁ +

[b(x₁)]

x₁ +

[a(x₁)]

x₁ +

[d^#(x₁)]

x₁ +

[c^#(x₁)]

x₁ +

together with the usable rules

a(b(x1))	→	c(b(x1))	(1)
c(c(x1))	→	d(b(x1))	(2)
d(x1)	→	c(e(x1))	(3)
b(b(x1))	→	f(x1)	(4)
c(b(x1))	→	g(x1)	(5)
e(x1)	→	f(x1)	(6)
e(x1)	→	b(b(x1))	(7)
f(g(x1))	→	a(c(x1))	(8)
g(f(x1))	→	e(x1)	(9)
a(x1)	→	b(c(x1))	(10)

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

c^#(c(x1))

→

d^#(b(x1))

(19)

and no rules could be deleted.

1.1.1.1.1.1.1.2.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.