Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/212480)

The rewrite relation of the following TRS is considered.

0(1(1(x1)))	→	1(2(1(2(0(x1)))))	(1)
0(3(1(x1)))	→	1(3(2(2(0(x1)))))	(2)
0(3(1(x1)))	→	3(2(1(2(0(x1)))))	(3)
0(3(1(x1)))	→	1(3(3(3(2(0(x1))))))	(4)
0(4(1(x1)))	→	2(1(2(0(4(x1)))))	(5)
0(0(4(5(x1))))	→	0(0(2(5(4(x1)))))	(6)
0(1(4(1(x1))))	→	0(1(2(2(4(1(x1))))))	(7)
0(1(4(5(x1))))	→	4(0(1(2(5(4(x1))))))	(8)
0(1(5(1(x1))))	→	1(2(2(5(0(1(x1))))))	(9)
0(1(5(3(x1))))	→	0(5(3(2(1(x1)))))	(10)
0(2(4(1(x1))))	→	1(3(3(2(0(4(x1))))))	(11)
0(2(4(1(x1))))	→	4(2(1(2(0(4(x1))))))	(12)
0(2(4(5(x1))))	→	0(2(2(5(0(4(x1))))))	(13)
0(3(1(5(x1))))	→	0(1(2(5(3(x1)))))	(14)
0(3(1(5(x1))))	→	1(2(5(3(0(4(x1))))))	(15)
0(3(5(1(x1))))	→	1(2(5(3(0(x1)))))	(16)
0(3(5(1(x1))))	→	0(5(2(1(2(3(x1))))))	(17)
0(3(5(5(x1))))	→	0(3(2(5(5(x1)))))	(18)
0(4(0(1(x1))))	→	2(0(4(4(0(1(x1))))))	(19)
0(4(1(5(x1))))	→	1(2(5(0(4(x1)))))	(20)
0(4(3(5(x1))))	→	0(4(3(2(5(4(x1))))))	(21)
0(4(5(1(x1))))	→	2(5(4(4(0(1(x1))))))	(22)
3(0(1(5(x1))))	→	3(1(4(0(5(4(x1))))))	(23)
3(0(3(1(x1))))	→	1(3(3(2(0(x1)))))	(24)
3(0(3(5(x1))))	→	3(2(5(0(2(3(x1))))))	(25)
3(3(0(1(x1))))	→	0(1(3(2(2(3(x1))))))	(26)
3(4(5(1(x1))))	→	3(2(5(4(2(1(x1))))))	(27)
4(1(3(5(x1))))	→	1(2(5(3(4(4(x1))))))	(28)
4(1(5(1(x1))))	→	4(4(5(1(2(1(x1))))))	(29)
4(4(1(5(x1))))	→	4(1(2(5(4(x1)))))	(30)
0(1(4(5(5(x1)))))	→	0(5(1(4(2(5(x1))))))	(31)
0(2(1(4(5(x1)))))	→	0(0(1(2(5(4(x1))))))	(32)
0(2(1(5(5(x1)))))	→	0(1(2(2(5(5(x1))))))	(33)
0(4(2(4(1(x1)))))	→	1(3(2(0(4(4(x1))))))	(34)
0(4(5(4(3(x1)))))	→	2(5(0(4(4(3(x1))))))	(35)
0(5(1(5(1(x1)))))	→	0(5(1(1(2(5(x1))))))	(36)
0(5(2(1(5(x1)))))	→	1(2(5(5(0(4(x1))))))	(37)
0(5(2(4(1(x1)))))	→	4(5(2(1(2(0(x1))))))	(38)
3(0(1(4(1(x1)))))	→	0(4(4(1(3(1(x1))))))	(39)
3(0(1(4(1(x1)))))	→	4(3(2(0(1(1(x1))))))	(40)
3(0(3(5(5(x1)))))	→	3(3(2(5(0(5(x1))))))	(41)
3(0(5(3(1(x1)))))	→	1(0(3(3(2(5(x1))))))	(42)
4(0(1(4(1(x1)))))	→	4(4(0(1(3(1(x1))))))	(43)
4(0(1(5(1(x1)))))	→	0(1(2(5(4(1(x1))))))	(44)
4(0(2(4(5(x1)))))	→	4(0(2(5(0(4(x1))))))	(45)
4(1(1(5(1(x1)))))	→	1(1(2(5(4(1(x1))))))	(46)
4(5(1(4(1(x1)))))	→	4(4(1(2(1(5(x1))))))	(47)
4(5(2(3(1(x1)))))	→	4(3(1(2(2(5(x1))))))	(48)
4(5(4(3(1(x1)))))	→	4(1(2(5(3(4(x1))))))	(49)
4(5(5(3(1(x1)))))	→	1(3(2(5(5(4(x1))))))	(50)

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.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

0^#(5(2(1(5(x1)))))	→	0^#(4(x1))	(171)
0^#(3(5(1(x1))))	→	0^#(x1)	(121)
4^#(1(3(5(x1))))	→	3^#(4(4(x1)))	(169)
4^#(0(2(4(5(x1)))))	→	4^#(x1)	(170)
0^#(5(2(4(1(x1)))))	→	0^#(x1)	(120)
0^#(2(4(1(x1))))	→	0^#(4(x1))	(80)
4^#(0(2(4(5(x1)))))	→	0^#(4(x1))	(119)
4^#(5(4(3(1(x1)))))	→	4^#(x1)	(117)
0^#(4(3(5(x1))))	→	4^#(x1)	(116)
0^#(1(1(x1)))	→	0^#(x1)	(114)
4^#(1(3(5(x1))))	→	4^#(x1)	(113)
0^#(4(2(4(1(x1)))))	→	4^#(x1)	(112)
4^#(0(1(5(1(x1)))))	→	4^#(1(x1))	(110)
3^#(0(1(4(1(x1)))))	→	0^#(1(1(x1)))	(109)
0^#(3(1(x1)))	→	0^#(x1)	(51)
3^#(3(0(1(x1))))	→	3^#(x1)	(107)
0^#(2(1(4(5(x1)))))	→	4^#(x1)	(105)
3^#(0(1(5(x1))))	→	0^#(5(4(x1)))	(104)
4^#(1(3(5(x1))))	→	4^#(4(x1))	(101)
0^#(4(1(x1)))	→	4^#(x1)	(159)
0^#(4(1(x1)))	→	0^#(4(x1))	(95)
0^#(3(1(5(x1))))	→	3^#(x1)	(94)
0^#(4(5(1(x1))))	→	0^#(1(x1))	(152)
0^#(4(0(1(x1))))	→	4^#(4(0(1(x1))))	(93)
4^#(1(1(5(1(x1)))))	→	4^#(1(x1))	(92)
0^#(4(5(4(3(x1)))))	→	0^#(4(4(3(x1))))	(91)
0^#(3(5(1(x1))))	→	3^#(0(x1))	(88)
0^#(5(2(1(5(x1)))))	→	4^#(x1)	(146)
3^#(0(3(5(5(x1)))))	→	0^#(5(x1))	(144)
0^#(4(1(5(x1))))	→	4^#(x1)	(85)
0^#(3(1(5(x1))))	→	4^#(x1)	(143)
0^#(3(1(x1)))	→	0^#(x1)	(51)
4^#(4(1(5(x1))))	→	4^#(x1)	(83)
0^#(3(1(5(x1))))	→	0^#(4(x1))	(81)
4^#(5(4(3(1(x1)))))	→	3^#(4(x1))	(79)
0^#(2(4(1(x1))))	→	0^#(4(x1))	(80)
0^#(4(2(4(1(x1)))))	→	0^#(4(4(x1)))	(140)
0^#(4(5(1(x1))))	→	4^#(0(1(x1)))	(139)
0^#(2(4(5(x1))))	→	4^#(x1)	(138)
4^#(5(5(3(1(x1)))))	→	4^#(x1)	(73)
0^#(2(4(1(x1))))	→	4^#(x1)	(70)
0^#(0(4(5(x1))))	→	4^#(x1)	(136)
3^#(0(3(5(x1))))	→	3^#(x1)	(135)
3^#(0(1(5(x1))))	→	4^#(0(5(4(x1))))	(134)
0^#(4(0(1(x1))))	→	0^#(4(4(0(1(x1)))))	(66)
0^#(1(4(5(x1))))	→	4^#(x1)	(64)
3^#(0(3(5(x1))))	→	0^#(2(3(x1)))	(129)
0^#(2(4(5(x1))))	→	0^#(4(x1))	(130)
0^#(3(5(1(x1))))	→	3^#(x1)	(128)
0^#(3(1(5(x1))))	→	3^#(0(4(x1)))	(60)
3^#(0(3(1(x1))))	→	0^#(x1)	(59)
0^#(4(5(4(3(x1)))))	→	4^#(4(3(x1)))	(125)
3^#(0(1(5(x1))))	→	4^#(x1)	(58)
0^#(4(5(1(x1))))	→	4^#(4(0(1(x1))))	(56)
0^#(4(1(5(x1))))	→	0^#(4(x1))	(57)
0^#(2(4(1(x1))))	→	4^#(x1)	(70)
0^#(4(2(4(1(x1)))))	→	4^#(4(x1))	(123)
0^#(1(5(1(x1))))	→	0^#(1(x1))	(55)
0^#(3(1(x1)))	→	0^#(x1)	(51)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 1
[1(x₁)]	=	x₁ + 1
[4(x₁)]	=	x₁ + 0
[5(x₁)]	=	x₁ + 31599
[3(x₁)]	=	x₁ + 0
[4^#(x₁)]	=	x₁ + 0
[0(x₁)]	=	x₁ + 0
[3^#(x₁)]	=	x₁ + 2
[2(x₁)]	=	x₁ + 0

together with the usable rules

0(3(5(5(x1))))	→	0(3(2(5(5(x1)))))	(18)
4(5(5(3(1(x1)))))	→	1(3(2(5(5(4(x1))))))	(50)
0(3(1(x1)))	→	1(3(3(3(2(0(x1))))))	(4)
0(3(1(5(x1))))	→	1(2(5(3(0(4(x1))))))	(15)
0(1(4(5(x1))))	→	4(0(1(2(5(4(x1))))))	(8)
0(1(1(x1)))	→	1(2(1(2(0(x1)))))	(1)
0(3(1(x1)))	→	3(2(1(2(0(x1)))))	(3)
0(3(5(1(x1))))	→	1(2(5(3(0(x1)))))	(16)
0(4(3(5(x1))))	→	0(4(3(2(5(4(x1))))))	(21)
0(5(1(5(1(x1)))))	→	0(5(1(1(2(5(x1))))))	(36)
3(3(0(1(x1))))	→	0(1(3(2(2(3(x1))))))	(26)
0(4(0(1(x1))))	→	2(0(4(4(0(1(x1))))))	(19)
0(2(1(4(5(x1)))))	→	0(0(1(2(5(4(x1))))))	(32)
0(3(5(1(x1))))	→	0(5(2(1(2(3(x1))))))	(17)
3(4(5(1(x1))))	→	3(2(5(4(2(1(x1))))))	(27)
0(4(2(4(1(x1)))))	→	1(3(2(0(4(4(x1))))))	(34)
0(4(5(1(x1))))	→	2(5(4(4(0(1(x1))))))	(22)
4(1(3(5(x1))))	→	1(2(5(3(4(4(x1))))))	(28)
4(0(1(5(1(x1)))))	→	0(1(2(5(4(1(x1))))))	(44)
0(4(1(x1)))	→	2(1(2(0(4(x1)))))	(5)
0(2(1(5(5(x1)))))	→	0(1(2(2(5(5(x1))))))	(33)
0(1(5(3(x1))))	→	0(5(3(2(1(x1)))))	(10)
3(0(1(4(1(x1)))))	→	0(4(4(1(3(1(x1))))))	(39)
0(1(4(1(x1))))	→	0(1(2(2(4(1(x1))))))	(7)
0(4(1(5(x1))))	→	1(2(5(0(4(x1)))))	(20)
3(0(3(5(x1))))	→	3(2(5(0(2(3(x1))))))	(25)
4(5(4(3(1(x1)))))	→	4(1(2(5(3(4(x1))))))	(49)
4(4(1(5(x1))))	→	4(1(2(5(4(x1)))))	(30)
0(3(1(5(x1))))	→	0(1(2(5(3(x1)))))	(14)
0(1(4(5(5(x1)))))	→	0(5(1(4(2(5(x1))))))	(31)
0(2(4(1(x1))))	→	4(2(1(2(0(4(x1))))))	(12)
4(0(2(4(5(x1)))))	→	4(0(2(5(0(4(x1))))))	(45)
3(0(1(5(x1))))	→	3(1(4(0(5(4(x1))))))	(23)
3(0(3(1(x1))))	→	1(3(3(2(0(x1)))))	(24)
0(2(4(1(x1))))	→	1(3(3(2(0(4(x1))))))	(11)
0(1(5(1(x1))))	→	1(2(2(5(0(1(x1))))))	(9)
0(2(4(5(x1))))	→	0(2(2(5(0(4(x1))))))	(13)
3(0(1(4(1(x1)))))	→	4(3(2(0(1(1(x1))))))	(40)
0(0(4(5(x1))))	→	0(0(2(5(4(x1)))))	(6)
0(5(2(4(1(x1)))))	→	4(5(2(1(2(0(x1))))))	(38)
4(5(2(3(1(x1)))))	→	4(3(1(2(2(5(x1))))))	(48)
4(5(1(4(1(x1)))))	→	4(4(1(2(1(5(x1))))))	(47)
0(5(2(1(5(x1)))))	→	1(2(5(5(0(4(x1))))))	(37)
3(0(3(5(5(x1)))))	→	3(3(2(5(0(5(x1))))))	(41)
3(0(5(3(1(x1)))))	→	1(0(3(3(2(5(x1))))))	(42)
4(1(1(5(1(x1)))))	→	1(1(2(5(4(1(x1))))))	(46)
0(4(5(4(3(x1)))))	→	2(5(0(4(4(3(x1))))))	(35)
4(1(5(1(x1))))	→	4(4(5(1(2(1(x1))))))	(29)
4(0(1(4(1(x1)))))	→	4(4(0(1(3(1(x1))))))	(43)
0(3(1(x1)))	→	1(3(2(2(0(x1)))))	(2)

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

0^#(5(2(1(5(x1)))))	→	0^#(4(x1))	(171)
0^#(3(5(1(x1))))	→	0^#(x1)	(121)
4^#(1(3(5(x1))))	→	3^#(4(4(x1)))	(169)
4^#(0(2(4(5(x1)))))	→	4^#(x1)	(170)
0^#(5(2(4(1(x1)))))	→	0^#(x1)	(120)
0^#(2(4(1(x1))))	→	0^#(4(x1))	(80)
4^#(0(2(4(5(x1)))))	→	0^#(4(x1))	(119)
4^#(5(4(3(1(x1)))))	→	4^#(x1)	(117)
0^#(4(3(5(x1))))	→	4^#(x1)	(116)
0^#(1(1(x1)))	→	0^#(x1)	(114)
4^#(1(3(5(x1))))	→	4^#(x1)	(113)
0^#(4(2(4(1(x1)))))	→	4^#(x1)	(112)
4^#(0(1(5(1(x1)))))	→	4^#(1(x1))	(110)
3^#(0(1(4(1(x1)))))	→	0^#(1(1(x1)))	(109)
0^#(3(1(x1)))	→	0^#(x1)	(51)
3^#(3(0(1(x1))))	→	3^#(x1)	(107)
0^#(2(1(4(5(x1)))))	→	4^#(x1)	(105)
3^#(0(1(5(x1))))	→	0^#(5(4(x1)))	(104)
4^#(1(3(5(x1))))	→	4^#(4(x1))	(101)
0^#(4(1(x1)))	→	4^#(x1)	(159)
0^#(4(1(x1)))	→	0^#(4(x1))	(95)
0^#(3(1(5(x1))))	→	3^#(x1)	(94)
0^#(4(5(1(x1))))	→	0^#(1(x1))	(152)
0^#(4(0(1(x1))))	→	4^#(4(0(1(x1))))	(93)
4^#(1(1(5(1(x1)))))	→	4^#(1(x1))	(92)
0^#(4(5(4(3(x1)))))	→	0^#(4(4(3(x1))))	(91)
0^#(3(5(1(x1))))	→	3^#(0(x1))	(88)
0^#(5(2(1(5(x1)))))	→	4^#(x1)	(146)
3^#(0(3(5(5(x1)))))	→	0^#(5(x1))	(144)
0^#(4(1(5(x1))))	→	4^#(x1)	(85)
0^#(3(1(5(x1))))	→	4^#(x1)	(143)
0^#(3(1(x1)))	→	0^#(x1)	(51)
4^#(4(1(5(x1))))	→	4^#(x1)	(83)
0^#(3(1(5(x1))))	→	0^#(4(x1))	(81)
4^#(5(4(3(1(x1)))))	→	3^#(4(x1))	(79)
0^#(2(4(1(x1))))	→	0^#(4(x1))	(80)
0^#(4(2(4(1(x1)))))	→	0^#(4(4(x1)))	(140)
0^#(4(5(1(x1))))	→	4^#(0(1(x1)))	(139)
0^#(2(4(5(x1))))	→	4^#(x1)	(138)
4^#(5(5(3(1(x1)))))	→	4^#(x1)	(73)
0^#(2(4(1(x1))))	→	4^#(x1)	(70)
0^#(0(4(5(x1))))	→	4^#(x1)	(136)
3^#(0(3(5(x1))))	→	3^#(x1)	(135)
3^#(0(1(5(x1))))	→	4^#(0(5(4(x1))))	(134)
0^#(1(4(5(x1))))	→	4^#(x1)	(64)
3^#(0(3(5(x1))))	→	0^#(2(3(x1)))	(129)
0^#(2(4(5(x1))))	→	0^#(4(x1))	(130)
0^#(3(5(1(x1))))	→	3^#(x1)	(128)
0^#(3(1(5(x1))))	→	3^#(0(4(x1)))	(60)
3^#(0(3(1(x1))))	→	0^#(x1)	(59)
0^#(4(5(4(3(x1)))))	→	4^#(4(3(x1)))	(125)
3^#(0(1(5(x1))))	→	4^#(x1)	(58)
0^#(4(5(1(x1))))	→	4^#(4(0(1(x1))))	(56)
0^#(4(1(5(x1))))	→	0^#(4(x1))	(57)
0^#(2(4(1(x1))))	→	4^#(x1)	(70)
0^#(4(2(4(1(x1)))))	→	4^#(4(x1))	(123)
0^#(1(5(1(x1))))	→	0^#(1(x1))	(55)
0^#(3(1(x1)))	→	0^#(x1)	(51)

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

0^#(4(0(1(x1))))

→

0^#(4(4(0(1(x1)))))

(66)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

[0^#(x₁)]

1	0
0	0

· x₁ +

[1(x₁)]

0	1
0	1

· x₁ +

26962

[4(x₁)]

0	1
1	0

· x₁ +

[5(x₁)]

80892

[3(x₁)]

x₁ +

[4^#(x₁)]

[0(x₁)]

1	1
1	1

· x₁ +

26963

26965

[3^#(x₁)]

[2(x₁)]

1	0
0	0

· x₁ +

together with the usable rules

0(3(5(5(x1))))	→	0(3(2(5(5(x1)))))	(18)
4(5(5(3(1(x1)))))	→	1(3(2(5(5(4(x1))))))	(50)
0(3(1(x1)))	→	1(3(3(3(2(0(x1))))))	(4)
0(3(1(5(x1))))	→	1(2(5(3(0(4(x1))))))	(15)
0(1(4(5(x1))))	→	4(0(1(2(5(4(x1))))))	(8)
0(1(1(x1)))	→	1(2(1(2(0(x1)))))	(1)
0(3(1(x1)))	→	3(2(1(2(0(x1)))))	(3)
0(3(5(1(x1))))	→	1(2(5(3(0(x1)))))	(16)
0(4(3(5(x1))))	→	0(4(3(2(5(4(x1))))))	(21)
0(5(1(5(1(x1)))))	→	0(5(1(1(2(5(x1))))))	(36)
3(3(0(1(x1))))	→	0(1(3(2(2(3(x1))))))	(26)
0(4(0(1(x1))))	→	2(0(4(4(0(1(x1))))))	(19)
0(2(1(4(5(x1)))))	→	0(0(1(2(5(4(x1))))))	(32)
0(3(5(1(x1))))	→	0(5(2(1(2(3(x1))))))	(17)
3(4(5(1(x1))))	→	3(2(5(4(2(1(x1))))))	(27)
0(4(2(4(1(x1)))))	→	1(3(2(0(4(4(x1))))))	(34)
0(4(5(1(x1))))	→	2(5(4(4(0(1(x1))))))	(22)
4(1(3(5(x1))))	→	1(2(5(3(4(4(x1))))))	(28)
4(0(1(5(1(x1)))))	→	0(1(2(5(4(1(x1))))))	(44)
0(4(1(x1)))	→	2(1(2(0(4(x1)))))	(5)
0(2(1(5(5(x1)))))	→	0(1(2(2(5(5(x1))))))	(33)
0(1(5(3(x1))))	→	0(5(3(2(1(x1)))))	(10)
3(0(1(4(1(x1)))))	→	0(4(4(1(3(1(x1))))))	(39)
0(1(4(1(x1))))	→	0(1(2(2(4(1(x1))))))	(7)
0(4(1(5(x1))))	→	1(2(5(0(4(x1)))))	(20)
3(0(3(5(x1))))	→	3(2(5(0(2(3(x1))))))	(25)
4(5(4(3(1(x1)))))	→	4(1(2(5(3(4(x1))))))	(49)
4(4(1(5(x1))))	→	4(1(2(5(4(x1)))))	(30)
0(3(1(5(x1))))	→	0(1(2(5(3(x1)))))	(14)
0(1(4(5(5(x1)))))	→	0(5(1(4(2(5(x1))))))	(31)
0(2(4(1(x1))))	→	4(2(1(2(0(4(x1))))))	(12)
4(0(2(4(5(x1)))))	→	4(0(2(5(0(4(x1))))))	(45)
3(0(1(5(x1))))	→	3(1(4(0(5(4(x1))))))	(23)
3(0(3(1(x1))))	→	1(3(3(2(0(x1)))))	(24)
0(2(4(1(x1))))	→	1(3(3(2(0(4(x1))))))	(11)
0(1(5(1(x1))))	→	1(2(2(5(0(1(x1))))))	(9)
0(2(4(5(x1))))	→	0(2(2(5(0(4(x1))))))	(13)
3(0(1(4(1(x1)))))	→	4(3(2(0(1(1(x1))))))	(40)
0(0(4(5(x1))))	→	0(0(2(5(4(x1)))))	(6)
0(5(2(4(1(x1)))))	→	4(5(2(1(2(0(x1))))))	(38)
4(5(2(3(1(x1)))))	→	4(3(1(2(2(5(x1))))))	(48)
4(5(1(4(1(x1)))))	→	4(4(1(2(1(5(x1))))))	(47)
0(5(2(1(5(x1)))))	→	1(2(5(5(0(4(x1))))))	(37)
3(0(3(5(5(x1)))))	→	3(3(2(5(0(5(x1))))))	(41)
3(0(5(3(1(x1)))))	→	1(0(3(3(2(5(x1))))))	(42)
4(1(1(5(1(x1)))))	→	1(1(2(5(4(1(x1))))))	(46)
0(4(5(4(3(x1)))))	→	2(5(0(4(4(3(x1))))))	(35)
4(1(5(1(x1))))	→	4(4(5(1(2(1(x1))))))	(29)
4(0(1(4(1(x1)))))	→	4(4(0(1(3(1(x1))))))	(43)
0(3(1(x1)))	→	1(3(2(2(0(x1)))))	(2)

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

0^#(4(0(1(x1))))

→

0^#(4(4(0(1(x1)))))

(66)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.