Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/247906)

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(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(4)
1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(0(...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 AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{0(☐), 1(☐), 3(☐), 4(☐), 5(☐), 2(☐)}

We obtain the transformed TRS

0(0(x1))	→	0(x1)	(2)
0(0(x1))	→	0(1(x1))	(6)
1(0(x1))	→	1(1(x1))	(7)
3(0(x1))	→	3(1(x1))	(8)
4(0(x1))	→	4(1(x1))	(9)
5(0(x1))	→	5(1(x1))	(10)
2(0(x1))	→	2(1(x1))	(11)
0(3(4(5(x1))))	→	0(4(3(5(x1))))	(12)
1(3(4(5(x1))))	→	1(4(3(5(x1))))	(13)
3(3(4(5(x1))))	→	3(4(3(5(x1))))	(14)
4(3(4(5(x1))))	→	4(4(3(5(x1))))	(15)
5(3(4(5(x1))))	→	5(4(3(5(x1))))	(16)
2(3(4(5(x1))))	→	2(4(3(5(x1))))	(17)
0(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(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(18)
1(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...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	1(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(19)
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(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	3(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(20)
4(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...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	4(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(21)
5(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(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(22)
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...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	2(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(23)
0(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	0(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...)))))))))))))))))))))))))))))))))))))))))))))))))))	(24)
1(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	1(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...)))))))))))))))))))))))))))))))))))))))))))))))))))	(25)
3(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	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(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(26)
4(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	4(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...)))))))))))))))))))))))))))))))))))))))))))))))))))	(27)
5(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	5(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...)))))))))))))))))))))))))))))))))))))))))))))))))))	(28)
2(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...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...)))))))))))))))))))))))))))))))))))))))))))))))))))	(29)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

There are 150 ruless (increase limit for explicit display).

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[0₀(x₁)]	=	1 · x₁ + 6
[0₁(x₁)]	=	1 · x₁ + 1
[0₃(x₁)]	=	1 · x₁ + 1
[0₄(x₁)]	=	1 · x₁
[0₅(x₁)]	=	1 · x₁ + 4
[0₂(x₁)]	=	1 · x₁ + 6
[1₀(x₁)]	=	1 · x₁ + 2
[1₁(x₁)]	=	1 · x₁ + 1
[1₃(x₁)]	=	1 · x₁
[1₄(x₁)]	=	1 · x₁
[1₅(x₁)]	=	1 · x₁ + 3
[1₂(x₁)]	=	1 · x₁ + 5
[3₀(x₁)]	=	1 · x₁ + 1
[3₁(x₁)]	=	1 · x₁
[4₀(x₁)]	=	1 · x₁ + 2
[4₁(x₁)]	=	1 · x₁
[5₀(x₁)]	=	1 · x₁
[5₁(x₁)]	=	1 · x₁
[2₀(x₁)]	=	1 · x₁ + 1
[2₁(x₁)]	=	1 · x₁
[3₄(x₁)]	=	1 · x₁ + 1
[4₅(x₁)]	=	1 · x₁
[4₃(x₁)]	=	1 · x₁
[3₅(x₁)]	=	1 · x₁
[5₃(x₁)]	=	1 · x₁
[5₄(x₁)]	=	1 · x₁ + 1
[5₅(x₁)]	=	1 · x₁
[5₂(x₁)]	=	1 · x₁ + 4
[3₃(x₁)]	=	1 · x₁ + 1
[4₄(x₁)]	=	1 · x₁ + 1
[2₃(x₁)]	=	1 · x₁
[2₄(x₁)]	=	1 · x₁
[2₂(x₁)]	=	1 · x₁ + 4
[2₅(x₁)]	=	1 · x₁
[3₂(x₁)]	=	1 · x₁ + 5
[4₂(x₁)]	=	1 · x₁ + 3

all of the following rules can be deleted.

There are 132 ruless (increase limit for explicit display).

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[5₀(x₁)]	=	1 · x₁ + 1
[0₁(x₁)]	=	1 · x₁
[5₁(x₁)]	=	1 · x₁
[1₁(x₁)]	=	1 · x₁
[0₄(x₁)]	=	1 · x₁ + 1
[1₄(x₁)]	=	1 · x₁ + 1
[4₃(x₁)]	=	1 · x₁
[3₄(x₁)]	=	1 · x₁
[4₅(x₁)]	=	1 · x₁
[4₄(x₁)]	=	1 · x₁
[3₅(x₁)]	=	1 · x₁
[5₃(x₁)]	=	1 · x₁
[5₄(x₁)]	=	1 · x₁
[5₅(x₁)]	=	1 · x₁
[5₂(x₁)]	=	1 · x₁
[1₀(x₁)]	=	1 · x₁
[0₀(x₁)]	=	1 · x₁
[1₃(x₁)]	=	1 · x₁ + 1
[0₂(x₁)]	=	1 · x₁
[2₂(x₁)]	=	1 · x₁
[2₃(x₁)]	=	1 · x₁
[2₄(x₁)]	=	1 · x₁
[3₁(x₁)]	=	1 · x₁
[3₂(x₁)]	=	1 · x₁

all of the following rules can be deleted.

5₀(0₁(x1))	→	5₁(1₁(x1))	(61)
5₀(0₄(x1))	→	5₁(1₄(x1))	(63)
0₁(1₁(1₁(1₁(1₁(1₁(1₀(0₁(1₁(1₁(1₁(1₁(1₁(1₀(0₀(0₀(0₁(1₀(0₁(1₁(1₁(1₀(0₁(1₁(1₁(1₀(0₁(1₀(0₁(1₀(0₁(1₁(1₀(0₁(1₀(0₀(0₁(1₁(1₀(0₁(1₀(0₁(1₀(0₁(1₀(0₀(0₀(0₀(0₀(0₀(0₀(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	0₂(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...)))))))))))))))))))))))))))))))))))))))))))))))))))	(146)
0₁(1₁(1₁(1₁(1₁(1₁(1₀(0₁(1₁(1₁(1₁(1₁(1₁(1₀(0₀(0₀(0₁(1₀(0₁(1₁(1₁(1₀(0₁(1₁(1₁(1₀(0₁(1₀(0₁(1₀(0₁(1₁(1₀(0₁(1₀(0₀(0₁(1₁(1₀(0₁(1₀(0₁(1₀(0₁(1₀(0₀(0₀(0₀(0₀(0₀(0₀(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	0₂(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...)))))))))))))))))))))))))))))))))))))))))))))))))))	(147)
3₁(1₁(1₁(1₁(1₁(1₁(1₀(0₁(1₁(1₁(1₁(1₁(1₁(1₀(0₀(0₀(0₁(1₀(0₁(1₁(1₁(1₀(0₁(1₁(1₁(1₀(0₁(1₀(0₁(1₀(0₁(1₁(1₀(0₁(1₀(0₀(0₁(1₁(1₀(0₁(1₀(0₁(1₀(0₁(1₀(0₀(0₀(0₀(0₀(0₀(0₀(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	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₂(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(158)
3₁(1₁(1₁(1₁(1₁(1₁(1₀(0₁(1₁(1₁(1₁(1₁(1₁(1₀(0₀(0₀(0₁(1₀(0₁(1₁(1₁(1₀(0₁(1₁(1₁(1₀(0₁(1₀(0₁(1₀(0₁(1₁(1₀(0₁(1₀(0₀(0₁(1₁(1₀(0₁(1₀(0₁(1₀(0₁(1₀(0₀(0₀(0₀(0₀(0₀(0₀(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	→	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₂(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(159)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[4₃(x₁)]	=	1 · x₁ + 1
[3₄(x₁)]	=	1 · x₁
[4₅(x₁)]	=	1 · x₁ + 1
[5₀(x₁)]	=	1 · x₁
[4₄(x₁)]	=	1 · x₁
[3₅(x₁)]	=	1 · x₁
[5₁(x₁)]	=	1 · x₁
[5₃(x₁)]	=	1 · x₁
[5₄(x₁)]	=	1 · x₁
[5₅(x₁)]	=	1 · x₁
[5₂(x₁)]	=	1 · x₁

all of the following rules can be deleted.

4₃(3₄(4₅(5₀(x1))))	→	4₄(4₃(3₅(5₀(x1))))	(90)
4₃(3₄(4₅(5₁(x1))))	→	4₄(4₃(3₅(5₁(x1))))	(91)
4₃(3₄(4₅(5₃(x1))))	→	4₄(4₃(3₅(5₃(x1))))	(92)
4₃(3₄(4₅(5₄(x1))))	→	4₄(4₃(3₅(5₄(x1))))	(93)
4₃(3₄(4₅(5₅(x1))))	→	4₄(4₃(3₅(5₅(x1))))	(94)
4₃(3₄(4₅(5₂(x1))))	→	4₄(4₃(3₅(5₂(x1))))	(95)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[5₃(x₁)]	=	1 · x₁
[3₄(x₁)]	=	1 · x₁ + 1
[4₅(x₁)]	=	1 · x₁
[5₀(x₁)]	=	1 · x₁
[5₄(x₁)]	=	1 · x₁
[4₃(x₁)]	=	1 · x₁
[3₅(x₁)]	=	1 · x₁
[5₁(x₁)]	=	1 · x₁
[5₅(x₁)]	=	1 · x₁
[5₂(x₁)]	=	1 · x₁

all of the following rules can be deleted.

5₃(3₄(4₅(5₀(x1))))	→	5₄(4₃(3₅(5₀(x1))))	(96)
5₃(3₄(4₅(5₁(x1))))	→	5₄(4₃(3₅(5₁(x1))))	(97)
5₃(3₄(4₅(5₃(x1))))	→	5₄(4₃(3₅(5₃(x1))))	(98)
5₃(3₄(4₅(5₄(x1))))	→	5₄(4₃(3₅(5₄(x1))))	(99)
5₃(3₄(4₅(5₅(x1))))	→	5₄(4₃(3₅(5₅(x1))))	(100)
5₃(3₄(4₅(5₂(x1))))	→	5₄(4₃(3₅(5₂(x1))))	(101)

1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.