Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/230819)

The rewrite relation of the following TRS is considered.

0(x1)	→	1(x1)	(1)
0(0(x1))	→	0(x1)	(2)
3(4(5(x1)))	→	4(3(5(x1)))	(3)
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	0(1(0(1(0(0(1(0(0(0(0(0(0(1(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(0(0(0(1(1(1(1(1(1(0(1(0(0(0(1(1(0(0(0(1(0(1(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(4)
0(0(1(1(0(0(1(1(1(0(0(0(1(1(1(0(1(0(1(1(1(1(0(0(0(1(0(1(1(0(0(1(1(0(0(0(1(1(1(0(1(0(1(0(0(1(0(0(0(1(1(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(5)

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

[5(x₁)]

=

x₁ +

0

[4(x₁)]

=

x₁ +

0

[3(x₁)]

=

x₁ +

0

[2(x₁)]

=

x₁ +

1

[1(x₁)]

=

x₁ +

5/14

[0(x₁)]

=

x₁ +

1

all of the following rules can be deleted.

0(x1)	→	1(x1)	(1)
0(0(x1))	→	0(x1)	(2)
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	0(1(0(1(0(0(1(0(0(0(0(0(0(1(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(0(0(0(1(1(1(1(1(1(0(1(0(0(0(1(1(0(0(0(1(0(1(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(4)
0(0(1(1(0(0(1(1(1(0(0(0(1(1(1(0(1(0(1(1(1(1(0(0(0(1(0(1(1(0(0(1(1(0(0(0(1(1(1(0(1(0(1(0(0(1(0(0(0(1(1(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(5)

1.1 String Reversal

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

5(4(3(x1)))

→

5(3(4(x1)))

(6)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

5^#(4(3(x1)))

→

5^#(3(4(x1)))

(7)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.