Certification Problem

Input (TPDB SRS_Standard/Zantema_06/09)

The rewrite relation of the following TRS is considered.

a(s(x1))	→	s(a(x1))	(1)
b(a(b(s(x1))))	→	a(b(s(a(x1))))	(2)
b(a(b(b(x1))))	→	c(s(x1))	(3)
c(s(x1))	→	a(b(a(b(x1))))	(4)
a(b(a(a(x1))))	→	b(a(b(a(x1))))	(5)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

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

s(a(x1))	→	a(s(x1))	(6)
s(b(a(b(x1))))	→	a(s(b(a(x1))))	(7)
b(b(a(b(x1))))	→	s(c(x1))	(8)
s(c(x1))	→	b(a(b(a(x1))))	(9)
a(a(b(a(x1))))	→	a(b(a(b(x1))))	(10)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

s^#(b(a(b(x1)))) → s^#(b(a(x1))) (14)

s^#(a(x1)) → s^#(x1) (12)

1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[a(x₁)] = 1 · x₁

[b(x₁)] = 1 · x₁

[s(x₁)] = 1 · x₁

[c(x₁)] = 1 · x₁

[s^#(x₁)] = 1 · x₁

together with the usable rules

a(a(b(a(x1)))) → a(b(a(b(x1)))) (10)

s(c(x1)) → b(a(b(a(x1)))) (9)

b(b(a(b(x1)))) → s(c(x1)) (8)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals

[a(x₁)] = 1 + 1 · x₁

[b(x₁)] = 1 + 1 · x₁

[s(x₁)] = 1 + 1 · x₁

[c(x₁)] = 3 + 1 · x₁

[s^#(x₁)] = 2 · x₁

the pairs

s^#(b(a(b(x1)))) → s^#(b(a(x1))) (14)

s^#(a(x1)) → s^#(x1) (12)

and no rules could be deleted.
1.1.1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

s^#(c(x1))	→	b^#(a(b(a(x1))))	(18)
b^#(b(a(b(x1))))	→	s^#(c(x1))	(17)
s^#(c(x1))	→	a^#(b(a(x1)))	(19)
a^#(a(b(a(x1))))	→	a^#(b(a(b(x1))))	(22)
a^#(a(b(a(x1))))	→	b^#(a(b(x1)))	(23)
a^#(a(b(a(x1))))	→	a^#(b(x1))	(24)
a^#(a(b(a(x1))))	→	b^#(x1)	(25)
s^#(c(x1))	→	b^#(a(x1))	(20)
s^#(c(x1))	→	a^#(x1)	(21)

1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[a(x₁)]	=	1 · x₁
[b(x₁)]	=	1 · x₁
[s(x₁)]	=	1 · x₁
[c(x₁)]	=	1 · x₁
[b^#(x₁)]	=	1 · x₁
[s^#(x₁)]	=	1 · x₁
[a^#(x₁)]	=	1 · x₁

together with the usable rules

a(a(b(a(x1))))	→	a(b(a(b(x1))))	(10)
s(c(x1))	→	b(a(b(a(x1))))	(9)
b(b(a(b(x1))))	→	s(c(x1))	(8)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

1.1.1.2.1 Monotonic Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[a(x₁)]	=	1 + 1 · x₁
[b(x₁)]	=	1 + 1 · x₁
[s(x₁)]	=	2 + 1 · x₁
[c(x₁)]	=	2 + 1 · x₁
[s^#(x₁)]	=	2 + 1 · x₁
[b^#(x₁)]	=	1 + 1 · x₁
[a^#(x₁)]	=	1 · x₁

the pairs

s^#(c(x1))	→	a^#(b(a(x1)))	(19)
a^#(a(b(a(x1))))	→	a^#(b(x1))	(24)
a^#(a(b(a(x1))))	→	b^#(x1)	(25)
s^#(c(x1))	→	b^#(a(x1))	(20)
s^#(c(x1))	→	a^#(x1)	(21)

and no rules could be deleted.

1.1.1.2.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair
a^#(a(b(a(x1)))) → a^#(b(a(b(x1)))) (22)

1.1.1.2.1.1.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[a^#(x₁)] = 1 · x₁

[a(x₁)] = 1

[b(x₁)] = 0

[s(x₁)] = 1 · x₁

[c(x₁)] = 0

together with the usable rules

b(b(a(b(x1)))) → s(c(x1)) (8)

s(c(x1)) → b(a(b(a(x1)))) (9)

(w.r.t. the implicit argument filter of the reduction pair), the pair
a^#(a(b(a(x1)))) → a^#(b(a(b(x1)))) (22)
could be deleted.
1.1.1.2.1.1.1.1 P is empty

There are no pairs anymore.
The 2^nd component contains the pair

b^#(b(a(b(x1)))) → s^#(c(x1)) (17)

s^#(c(x1)) → b^#(a(b(a(x1)))) (18)

1.1.1.2.1.1.2 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[b^#(x₁)] = 1 · x₁

[b(x₁)] = 1

[a(x₁)] = 0

[s^#(x₁)] = 1 · x₁

[c(x₁)] = 0

[s(x₁)] = 1 + 1 · x₁

together with the usable rule
a(a(b(a(x1)))) → a(b(a(b(x1)))) (10)
(w.r.t. the implicit argument filter of the reduction pair), the pair
b^#(b(a(b(x1)))) → s^#(c(x1)) (17)
could be deleted.
1.1.1.2.1.1.2.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals

[a(x₁)] = 1 + 1 · x₁

[b(x₁)] = 1 + 1 · x₁

[s(x₁)] = 2 + 1 · x₁

[c(x₁)] = 2 + 1 · x₁

[s^#(x₁)] = 3 + 3 · x₁

[b^#(x₁)] = 3 + 1 · x₁

the pair
s^#(c(x1)) → b^#(a(b(a(x1)))) (18)
and no rules could be deleted.
1.1.1.2.1.1.2.1.1 P is empty

There are no pairs anymore.

Certification Problem

Input (TPDB SRS_Standard/Zantema_06/09)

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

1.1 Dependency Pair Transformation

1.1.1 Dependency Graph Processor

1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.1 Monotonic Reduction Pair Processor

1.1.1.1.1.1 P is empty

1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.2.1 Monotonic Reduction Pair Processor

1.1.1.2.1.1 Dependency Graph Processor

1.1.1.2.1.1.1 Reduction Pair Processor with Usable Rules

1.1.1.2.1.1.1.1 P is empty

1.1.1.2.1.1.2 Reduction Pair Processor with Usable Rules

1.1.1.2.1.1.2.1 Monotonic Reduction Pair Processor

1.1.1.2.1.1.2.1.1 P is empty