Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z100)

The rewrite relation of the following TRS is considered.

r1(a(x1))	→	a(a(a(r1(x1))))	(1)
r2(a(x1))	→	a(a(a(r2(x1))))	(2)
a(l1(x1))	→	l1(a(a(a(x1))))	(3)
a(a(l2(x1)))	→	l2(a(a(x1)))	(4)
r1(b(x1))	→	l1(b(x1))	(5)
r2(b(x1))	→	l2(a(b(x1)))	(6)
b(l1(x1))	→	b(r2(x1))	(7)
b(l2(x1))	→	b(r1(x1))	(8)
a(a(x1))	→	x1	(9)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

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

a(r1(x1))	→	r1(a(a(a(x1))))	(10)
a(r2(x1))	→	r2(a(a(a(x1))))	(11)
l1(a(x1))	→	a(a(a(l1(x1))))	(12)
l2(a(a(x1)))	→	a(a(l2(x1)))	(13)
b(r1(x1))	→	b(l1(x1))	(14)
b(r2(x1))	→	b(a(l2(x1)))	(15)
l1(b(x1))	→	r2(b(x1))	(16)
l2(b(x1))	→	r1(b(x1))	(17)
a(a(x1))	→	x1	(9)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[l2(x₁)]

1	0	0
0	1	0
0	1	0

· x₁ +

0	0	0
0	0	0
1	0	0

[r1(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
1	0	0
1	0	0

[l1(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[b(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[a(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[r2(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

b(r1(x1))

→

b(l1(x1))

(14)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[l2(x₁)]	=	2 · x₁ + -∞
[r1(x₁)]	=	2 · x₁ + -∞
[l1(x₁)]	=	15 · x₁ + -∞
[b(x₁)]	=	1 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[r2(x₁)]	=	2 · x₁ + -∞

all of the following rules can be deleted.

l1(b(x1))

→

r2(b(x1))

(16)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[l2(x₁)]	=	15 · x₁ + -∞
[r1(x₁)]	=	4 · x₁ + -∞
[l1(x₁)]	=	0 · x₁ + -∞
[b(x₁)]	=	12 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[r2(x₁)]	=	15 · x₁ + -∞

all of the following rules can be deleted.

l2(b(x1))

→

r1(b(x1))

(17)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[l2(x₁)]	=	4 · x₁ + -∞
[r1(x₁)]	=	0 · x₁ + -∞
[l1(x₁)]	=	12 · x₁ + -∞
[b(x₁)]	=	2 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[r2(x₁)]	=	8 · x₁ + -∞

all of the following rules can be deleted.

b(r2(x1))

→

b(a(l2(x1)))

(15)

1.1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a^#(r1(x1))	→	a^#(x1)	(18)
a^#(r1(x1))	→	a^#(a(x1))	(19)
a^#(r1(x1))	→	a^#(a(a(x1)))	(20)
a^#(r2(x1))	→	a^#(x1)	(21)
a^#(r2(x1))	→	a^#(a(x1))	(22)
a^#(r2(x1))	→	a^#(a(a(x1)))	(23)
l1^#(a(x1))	→	l1^#(x1)	(24)
l1^#(a(x1))	→	a^#(l1(x1))	(25)
l1^#(a(x1))	→	a^#(a(l1(x1)))	(26)
l1^#(a(x1))	→	a^#(a(a(l1(x1))))	(27)
l2^#(a(a(x1)))	→	l2^#(x1)	(28)
l2^#(a(a(x1)))	→	a^#(l2(x1))	(29)
l2^#(a(a(x1)))	→	a^#(a(l2(x1)))	(30)

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair
l1^#(a(x1)) → l1^#(x1) (24)

1.1.1.1.1.1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

l1^#(a(x1)) → l1^#(x1) (24)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair
l2^#(a(a(x1))) → l2^#(x1) (28)

1.1.1.1.1.1.1.2 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

l2^#(a(a(x1))) → l2^#(x1) (28)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.

The 3^rd component contains the pair

a^#(r1(x1))	→	a^#(x1)	(18)
a^#(r1(x1))	→	a^#(a(x1))	(19)
a^#(r1(x1))	→	a^#(a(a(x1)))	(20)
a^#(r2(x1))	→	a^#(x1)	(21)
a^#(r2(x1))	→	a^#(a(x1))	(22)
a^#(r2(x1))	→	a^#(a(a(x1)))	(23)

1.1.1.1.1.1.1.3 Subterm Criterion Processor

We use the projection to multisets

π(a^#)	=	{ 1, 1 }
π(r2)	=	{ 1, 1 }
π(r1)	=	{ 1, 1 }
π(a)	=	{ 1 }

to remove the pairs:

a^#(r1(x1))	→	a^#(x1)	(18)
a^#(r1(x1))	→	a^#(a(x1))	(19)
a^#(r1(x1))	→	a^#(a(a(x1)))	(20)
a^#(r2(x1))	→	a^#(x1)	(21)
a^#(r2(x1))	→	a^#(a(x1))	(22)
a^#(r2(x1))	→	a^#(a(a(x1)))	(23)

1.1.1.1.1.1.1.3.1 P is empty

There are no pairs anymore.

Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z100)

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

1.1 Rule Removal

1.1.1 Rule Removal

1.1.1.1 Rule Removal

1.1.1.1.1 Rule Removal

1.1.1.1.1.1 Dependency Pair Transformation

1.1.1.1.1.1.1 Dependency Graph Processor

1.1.1.1.1.1.1.1 Size-Change Termination

1.1.1.1.1.1.1.2 Size-Change Termination

1.1.1.1.1.1.1.3 Subterm Criterion Processor

1.1.1.1.1.1.1.3.1 P is empty