Certification Problem

Input (TPDB SRS_Standard/Secret_05_SRS/matchbox2)

The rewrite relation of the following TRS is considered.

t(o(x1))	→	m(a(x1))	(1)
t(e(x1))	→	n(s(x1))	(2)
a(l(x1))	→	a(t(x1))	(3)
o(m(a(x1)))	→	t(e(n(x1)))	(4)
s(a(x1))	→	l(a(t(o(m(a(t(e(x1))))))))	(5)
n(s(x1))	→	a(l(a(t(x1))))	(6)

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.

t^#(e(x1))	→	s^#(x1)	(7)
s^#(a(x1))	→	a^#(t(o(m(a(t(e(x1)))))))	(8)
t^#(o(x1))	→	a^#(x1)	(9)
s^#(a(x1))	→	a^#(t(e(x1)))	(10)
a^#(l(x1))	→	a^#(t(x1))	(11)
a^#(l(x1))	→	t^#(x1)	(12)
o^#(m(a(x1)))	→	t^#(e(n(x1)))	(13)
s^#(a(x1))	→	t^#(o(m(a(t(e(x1))))))	(14)
s^#(a(x1))	→	t^#(e(x1))	(15)
n^#(s(x1))	→	t^#(x1)	(16)
n^#(s(x1))	→	a^#(l(a(t(x1))))	(17)
t^#(e(x1))	→	n^#(s(x1))	(18)
s^#(a(x1))	→	o^#(m(a(t(e(x1)))))	(19)
o^#(m(a(x1)))	→	n^#(x1)	(20)
n^#(s(x1))	→	a^#(t(x1))	(21)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

n^#(s(x1))	→	a^#(t(x1))	(21)
o^#(m(a(x1)))	→	t^#(e(n(x1)))	(13)
o^#(m(a(x1)))	→	n^#(x1)	(20)
a^#(l(x1))	→	t^#(x1)	(12)
s^#(a(x1))	→	o^#(m(a(t(e(x1)))))	(19)
t^#(e(x1))	→	n^#(s(x1))	(18)
n^#(s(x1))	→	a^#(l(a(t(x1))))	(17)
a^#(l(x1))	→	a^#(t(x1))	(11)
s^#(a(x1))	→	a^#(t(e(x1)))	(10)
t^#(o(x1))	→	a^#(x1)	(9)
s^#(a(x1))	→	a^#(t(o(m(a(t(e(x1)))))))	(8)
n^#(s(x1))	→	t^#(x1)	(16)
s^#(a(x1))	→	t^#(e(x1))	(15)
s^#(a(x1))	→	t^#(o(m(a(t(e(x1))))))	(14)
t^#(e(x1))	→	s^#(x1)	(7)

1.1.1 Reduction Pair Processor with Usable Rules

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

[a(x₁)]

0	0
1	0

· x₁ +

[s(x₁)]

[n(x₁)]

[t(x₁)]

x₁ +

[l(x₁)]

1	0
0	0

· x₁ +

[o(x₁)]

0	0
1	0

· x₁ +

44542

[s^#(x₁)]

12300

[o^#(x₁)]

0	1
0	0

· x₁ +

[e(x₁)]

0	0
1	1

· x₁ +

44541

[a^#(x₁)]

12300

[t^#(x₁)]

12300

[n^#(x₁)]

1	0
0	0

· x₁ +

12299

[m(x₁)]

0	0
1	1

· x₁ +

12299

together with the usable rules

o(m(a(x1)))	→	t(e(n(x1)))	(4)
t(o(x1))	→	m(a(x1))	(1)
a(l(x1))	→	a(t(x1))	(3)
s(a(x1))	→	l(a(t(o(m(a(t(e(x1))))))))	(5)
n(s(x1))	→	a(l(a(t(x1))))	(6)
t(e(x1))	→	n(s(x1))	(2)

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

o^#(m(a(x1)))

→

n^#(x1)

(20)

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

o^#(m(a(x1)))	→	t^#(e(n(x1)))	(13)
t^#(o(x1))	→	a^#(x1)	(9)
a^#(l(x1))	→	t^#(x1)	(12)
a^#(l(x1))	→	a^#(t(x1))	(11)
s^#(a(x1))	→	t^#(e(x1))	(15)
s^#(a(x1))	→	a^#(t(e(x1)))	(10)
s^#(a(x1))	→	o^#(m(a(t(e(x1)))))	(19)
s^#(a(x1))	→	t^#(o(m(a(t(e(x1))))))	(14)
s^#(a(x1))	→	a^#(t(o(m(a(t(e(x1)))))))	(8)
n^#(s(x1))	→	t^#(x1)	(16)
n^#(s(x1))	→	a^#(t(x1))	(21)
n^#(s(x1))	→	a^#(l(a(t(x1))))	(17)
t^#(e(x1))	→	s^#(x1)	(7)
t^#(e(x1))	→	n^#(s(x1))	(18)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[n(x₁)]	=	0
[t(x₁)]	=	0
[l(x₁)]	=	x₁ + 0
[o(x₁)]	=	x₁ + 26643
[s^#(x₁)]	=	x₁ + 28884
[o^#(x₁)]	=	28884
[e(x₁)]	=	x₁ + 28884
[a^#(x₁)]	=	x₁ + 1
[t^#(x₁)]	=	x₁ + 0
[n^#(x₁)]	=	x₁ + 1
[m(x₁)]	=	0

together with the usable rules

o(m(a(x1)))	→	t(e(n(x1)))	(4)
t(o(x1))	→	m(a(x1))	(1)
a(l(x1))	→	a(t(x1))	(3)
s(a(x1))	→	l(a(t(o(m(a(t(e(x1))))))))	(5)
n(s(x1))	→	a(l(a(t(x1))))	(6)
t(e(x1))	→	n(s(x1))	(2)

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

t^#(o(x1))	→	a^#(x1)	(9)
a^#(l(x1))	→	t^#(x1)	(12)
s^#(a(x1))	→	a^#(t(e(x1)))	(10)
s^#(a(x1))	→	t^#(o(m(a(t(e(x1))))))	(14)
s^#(a(x1))	→	a^#(t(o(m(a(t(e(x1)))))))	(8)
n^#(s(x1))	→	t^#(x1)	(16)
n^#(s(x1))	→	a^#(t(x1))	(21)
n^#(s(x1))	→	a^#(l(a(t(x1))))	(17)
t^#(e(x1))	→	n^#(s(x1))	(18)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a^#(l(x1))

→

a^#(t(x1))

(11)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	0
[s(x₁)]	=	2
[n(x₁)]	=	1
[t(x₁)]	=	1
[l(x₁)]	=	2
[o(x₁)]	=	x₁ + 26643
[s^#(x₁)]	=	28884
[o^#(x₁)]	=	28884
[e(x₁)]	=	28884
[a^#(x₁)]	=	x₁ + 1
[t^#(x₁)]	=	x₁ + 0
[n^#(x₁)]	=	x₁ + 1
[m(x₁)]	=	1

together with the usable rules

o(m(a(x1)))	→	t(e(n(x1)))	(4)
t(o(x1))	→	m(a(x1))	(1)
a(l(x1))	→	a(t(x1))	(3)
s(a(x1))	→	l(a(t(o(m(a(t(e(x1))))))))	(5)
n(s(x1))	→	a(l(a(t(x1))))	(6)
t(e(x1))	→	n(s(x1))	(2)

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

a^#(l(x1))

→

a^#(t(x1))

(11)

could be deleted.

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

o^#(m(a(x1)))	→	t^#(e(n(x1)))	(13)
s^#(a(x1))	→	t^#(e(x1))	(15)
s^#(a(x1))	→	o^#(m(a(t(e(x1)))))	(19)
t^#(e(x1))	→	s^#(x1)	(7)

1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

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

[a(x₁)]

0	0
0	1

· x₁ +

[s(x₁)]

0	1
0	0

· x₁ +

[n(x₁)]

1	0
0	0

· x₁ +

[t(x₁)]

0	1
1	0

· x₁ +

[l(x₁)]

0	0
1	0

· x₁ +

[o(x₁)]

0	1
1	1

· x₁ +

37542

25201

[s^#(x₁)]

0	1
0	0

· x₁ +

57539

[o^#(x₁)]

57540

[e(x₁)]

0	0
0	1

· x₁ +

4751

40487

[a^#(x₁)]

12300

[t^#(x₁)]

1	1
0	0

· x₁ +

12301

[n^#(x₁)]

12299

[m(x₁)]

0	1
0	1

· x₁ +

3967

2946

together with the usable rules

o(m(a(x1)))	→	t(e(n(x1)))	(4)
t(o(x1))	→	m(a(x1))	(1)
a(l(x1))	→	a(t(x1))	(3)
s(a(x1))	→	l(a(t(o(m(a(t(e(x1))))))))	(5)
n(s(x1))	→	a(l(a(t(x1))))	(6)
t(e(x1))	→	n(s(x1))	(2)

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

s^#(a(x1))

→

t^#(e(x1))

(15)

could be deleted.

1.1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

o^#(m(a(x1)))	→	t^#(e(n(x1)))	(13)
s^#(a(x1))	→	o^#(m(a(t(e(x1)))))	(19)
t^#(e(x1))	→	s^#(x1)	(7)

1.1.1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

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

[a(x₁)]

0	0
0	1

· x₁ +

30787

[s(x₁)]

[n(x₁)]

0	1
1	0

· x₁ +

30783

[t(x₁)]

1	0
0	0

· x₁ +

30787

[l(x₁)]

[o(x₁)]

1	1
0	1

· x₁ +

61570

[s^#(x₁)]

1	0
0	0

· x₁ +

12300

[o^#(x₁)]

1	0
0	0

· x₁ +

43085

[e(x₁)]

x₁ +

[a^#(x₁)]

12300

[t^#(x₁)]

1	0
0	0

· x₁ +

12301

[n^#(x₁)]

12299

[m(x₁)]

0	1
0	0

· x₁ +

together with the usable rules

o(m(a(x1)))	→	t(e(n(x1)))	(4)
t(o(x1))	→	m(a(x1))	(1)
a(l(x1))	→	a(t(x1))	(3)
s(a(x1))	→	l(a(t(o(m(a(t(e(x1))))))))	(5)
n(s(x1))	→	a(l(a(t(x1))))	(6)
t(e(x1))	→	n(s(x1))	(2)

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

o^#(m(a(x1)))	→	t^#(e(n(x1)))	(13)
s^#(a(x1))	→	o^#(m(a(t(e(x1)))))	(19)
t^#(e(x1))	→	s^#(x1)	(7)

could be deleted.

1.1.1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.