Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3746)

The rewrite relation of the following TRS is considered.

0(5(0(x1)))	→	3(4(3(3(2(0(4(4(4(0(x1))))))))))	(1)
0(2(5(0(x1))))	→	0(2(1(1(5(2(1(4(1(3(x1))))))))))	(2)
0(5(0(5(x1))))	→	3(2(0(2(0(4(4(1(5(4(x1))))))))))	(3)
2(5(5(3(x1))))	→	4(3(0(2(1(0(1(3(4(3(x1))))))))))	(4)
5(5(5(0(x1))))	→	4(1(2(1(2(3(5(0(1(3(x1))))))))))	(5)
0(5(1(5(0(x1)))))	→	3(4(0(1(4(5(2(2(3(1(x1))))))))))	(6)
3(0(0(5(3(x1)))))	→	1(3(4(3(5(2(4(1(3(3(x1))))))))))	(7)
3(5(5(0(0(x1)))))	→	1(4(1(0(0(4(4(0(4(1(x1))))))))))	(8)
0(2(5(1(5(0(x1))))))	→	2(1(0(1(5(2(4(0(2(0(x1))))))))))	(9)
0(2(5(5(1(4(x1))))))	→	4(0(1(1(1(1(0(4(1(5(x1))))))))))	(10)
0(5(3(1(2(5(x1))))))	→	0(2(3(1(1(2(4(4(5(5(x1))))))))))	(11)
0(5(5(1(5(1(x1))))))	→	0(5(1(1(3(3(4(2(1(0(x1))))))))))	(12)
4(5(5(4(2(0(x1))))))	→	2(4(0(1(3(4(4(4(1(0(x1))))))))))	(13)
5(0(0(3(5(2(x1))))))	→	4(4(2(3(0(1(2(0(5(2(x1))))))))))	(14)
5(1(5(0(2(5(x1))))))	→	5(0(0(1(4(2(3(2(1(5(x1))))))))))	(15)
5(2(0(2(5(5(x1))))))	→	5(5(4(4(4(5(4(4(1(4(x1))))))))))	(16)
5(5(0(2(5(0(x1))))))	→	2(0(5(0(2(1(0(0(3(0(x1))))))))))	(17)
5(5(0(3(4(5(x1))))))	→	2(0(5(5(2(1(3(2(3(2(x1))))))))))	(18)
5(5(3(5(0(5(x1))))))	→	5(4(4(3(5(1(3(3(4(5(x1))))))))))	(19)
0(4(4(0(0(5(1(x1)))))))	→	1(3(2(0(4(1(5(1(1(2(x1))))))))))	(20)
0(4(4(2(5(5(5(x1)))))))	→	0(2(4(5(5(4(2(0(1(1(x1))))))))))	(21)
1(0(2(5(2(0(0(x1)))))))	→	3(1(4(4(0(3(0(1(2(2(x1))))))))))	(22)
1(2(0(4(2(5(0(x1)))))))	→	4(2(4(0(3(2(2(4(1(0(x1))))))))))	(23)
1(2(5(5(0(3(3(x1)))))))	→	3(4(1(2(0(3(3(1(0(3(x1))))))))))	(24)
1(5(5(3(3(3(4(x1)))))))	→	1(5(1(0(0(2(2(2(3(5(x1))))))))))	(25)
2(5(4(5(2(5(1(x1)))))))	→	4(3(2(1(4(2(2(4(5(2(x1))))))))))	(26)
3(2(3(5(1(5(2(x1)))))))	→	2(0(3(2(3(2(1(5(5(1(x1))))))))))	(27)
3(3(4(2(5(5(2(x1)))))))	→	1(2(3(3(4(4(1(4(0(1(x1))))))))))	(28)
3(5(0(5(5(5(0(x1)))))))	→	0(0(3(0(3(5(0(3(2(0(x1))))))))))	(29)
4(3(1(2(5(2(4(x1)))))))	→	2(3(1(1(4(3(4(4(2(4(x1))))))))))	(30)
4(5(5(3(1(0(5(x1)))))))	→	1(1(5(2(0(3(3(3(2(1(x1))))))))))	(31)
5(0(5(3(1(0(5(x1)))))))	→	5(2(4(4(2(1(3(5(1(5(x1))))))))))	(32)
5(0(5(3(5(1(5(x1)))))))	→	5(1(1(2(4(0(0(3(2(5(x1))))))))))	(33)
5(1(5(3(3(0(5(x1)))))))	→	4(4(3(2(2(2(5(0(1(1(x1))))))))))	(34)
5(2(0(2(5(3(3(x1)))))))	→	5(2(0(5(1(1(3(2(0(3(x1))))))))))	(35)

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

0(5(0(x1)))	→	0(4(4(4(0(2(3(3(4(3(x1))))))))))	(36)
0(5(2(0(x1))))	→	3(1(4(1(2(5(1(1(2(0(x1))))))))))	(37)
5(0(5(0(x1))))	→	4(5(1(4(4(0(2(0(2(3(x1))))))))))	(38)
3(5(5(2(x1))))	→	3(4(3(1(0(1(2(0(3(4(x1))))))))))	(39)
0(5(5(5(x1))))	→	3(1(0(5(3(2(1(2(1(4(x1))))))))))	(40)
0(5(1(5(0(x1)))))	→	1(3(2(2(5(4(1(0(4(3(x1))))))))))	(41)
3(5(0(0(3(x1)))))	→	3(3(1(4(2(5(3(4(3(1(x1))))))))))	(42)
0(0(5(5(3(x1)))))	→	1(4(0(4(4(0(0(1(4(1(x1))))))))))	(43)
0(5(1(5(2(0(x1))))))	→	0(2(0(4(2(5(1(0(1(2(x1))))))))))	(44)
4(1(5(5(2(0(x1))))))	→	5(1(4(0(1(1(1(1(0(4(x1))))))))))	(45)
5(2(1(3(5(0(x1))))))	→	5(5(4(4(2(1(1(3(2(0(x1))))))))))	(46)
1(5(1(5(5(0(x1))))))	→	0(1(2(4(3(3(1(1(5(0(x1))))))))))	(47)
0(2(4(5(5(4(x1))))))	→	0(1(4(4(4(3(1(0(4(2(x1))))))))))	(48)
2(5(3(0(0(5(x1))))))	→	2(5(0(2(1(0(3(2(4(4(x1))))))))))	(49)
5(2(0(5(1(5(x1))))))	→	5(1(2(3(2(4(1(0(0(5(x1))))))))))	(50)
5(5(2(0(2(5(x1))))))	→	4(1(4(4(5(4(4(4(5(5(x1))))))))))	(51)
0(5(2(0(5(5(x1))))))	→	0(3(0(0(1(2(0(5(0(2(x1))))))))))	(52)
5(4(3(0(5(5(x1))))))	→	2(3(2(3(1(2(5(5(0(2(x1))))))))))	(53)
5(0(5(3(5(5(x1))))))	→	5(4(3(3(1(5(3(4(4(5(x1))))))))))	(54)
1(5(0(0(4(4(0(x1)))))))	→	2(1(1(5(1(4(0(2(3(1(x1))))))))))	(55)
5(5(5(2(4(4(0(x1)))))))	→	1(1(0(2(4(5(5(4(2(0(x1))))))))))	(56)
0(0(2(5(2(0(1(x1)))))))	→	2(2(1(0(3(0(4(4(1(3(x1))))))))))	(57)
0(5(2(4(0(2(1(x1)))))))	→	0(1(4(2(2(3(0(4(2(4(x1))))))))))	(58)
3(3(0(5(5(2(1(x1)))))))	→	3(0(1(3(3(0(2(1(4(3(x1))))))))))	(59)
4(3(3(3(5(5(1(x1)))))))	→	5(3(2(2(2(0(0(1(5(1(x1))))))))))	(60)
1(5(2(5(4(5(2(x1)))))))	→	2(5(4(2(2(4(1(2(3(4(x1))))))))))	(61)
2(5(1(5(3(2(3(x1)))))))	→	1(5(5(1(2(3(2(3(0(2(x1))))))))))	(62)
2(5(5(2(4(3(3(x1)))))))	→	1(0(4(1(4(4(3(3(2(1(x1))))))))))	(63)
0(5(5(5(0(5(3(x1)))))))	→	0(2(3(0(5(3(0(3(0(0(x1))))))))))	(64)
4(2(5(2(1(3(4(x1)))))))	→	4(2(4(4(3(4(1(1(3(2(x1))))))))))	(65)
5(0(1(3(5(5(4(x1)))))))	→	1(2(3(3(3(0(2(5(1(1(x1))))))))))	(66)
5(0(1(3(5(0(5(x1)))))))	→	5(1(5(3(1(2(4(4(2(5(x1))))))))))	(67)
5(1(5(3(5(0(5(x1)))))))	→	5(2(3(0(0(4(2(1(1(5(x1))))))))))	(68)
5(0(3(3(5(1(5(x1)))))))	→	1(1(0(5(2(2(2(3(4(4(x1))))))))))	(69)
3(3(5(2(0(2(5(x1)))))))	→	3(0(2(3(1(1(5(0(2(5(x1))))))))))	(70)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[0(x₁)]	=	1 · x₁
[5(x₁)]	=	1 · x₁ + 1
[4(x₁)]	=	1 · x₁
[2(x₁)]	=	1 · x₁
[3(x₁)]	=	1 · x₁
[1(x₁)]	=	1 · x₁

all of the following rules can be deleted.

0(5(0(x1)))	→	0(4(4(4(0(2(3(3(4(3(x1))))))))))	(36)
5(0(5(0(x1))))	→	4(5(1(4(4(0(2(0(2(3(x1))))))))))	(38)
3(5(5(2(x1))))	→	3(4(3(1(0(1(2(0(3(4(x1))))))))))	(39)
0(5(5(5(x1))))	→	3(1(0(5(3(2(1(2(1(4(x1))))))))))	(40)
0(5(1(5(0(x1)))))	→	1(3(2(2(5(4(1(0(4(3(x1))))))))))	(41)
0(0(5(5(3(x1)))))	→	1(4(0(4(4(0(0(1(4(1(x1))))))))))	(43)
0(5(1(5(2(0(x1))))))	→	0(2(0(4(2(5(1(0(1(2(x1))))))))))	(44)
4(1(5(5(2(0(x1))))))	→	5(1(4(0(1(1(1(1(0(4(x1))))))))))	(45)
1(5(1(5(5(0(x1))))))	→	0(1(2(4(3(3(1(1(5(0(x1))))))))))	(47)
0(2(4(5(5(4(x1))))))	→	0(1(4(4(4(3(1(0(4(2(x1))))))))))	(48)
2(5(3(0(0(5(x1))))))	→	2(5(0(2(1(0(3(2(4(4(x1))))))))))	(49)
5(2(0(5(1(5(x1))))))	→	5(1(2(3(2(4(1(0(0(5(x1))))))))))	(50)
0(5(2(0(5(5(x1))))))	→	0(3(0(0(1(2(0(5(0(2(x1))))))))))	(52)
5(4(3(0(5(5(x1))))))	→	2(3(2(3(1(2(5(5(0(2(x1))))))))))	(53)
5(0(5(3(5(5(x1))))))	→	5(4(3(3(1(5(3(4(4(5(x1))))))))))	(54)
5(5(5(2(4(4(0(x1)))))))	→	1(1(0(2(4(5(5(4(2(0(x1))))))))))	(56)
0(0(2(5(2(0(1(x1)))))))	→	2(2(1(0(3(0(4(4(1(3(x1))))))))))	(57)
0(5(2(4(0(2(1(x1)))))))	→	0(1(4(2(2(3(0(4(2(4(x1))))))))))	(58)
3(3(0(5(5(2(1(x1)))))))	→	3(0(1(3(3(0(2(1(4(3(x1))))))))))	(59)
1(5(2(5(4(5(2(x1)))))))	→	2(5(4(2(2(4(1(2(3(4(x1))))))))))	(61)
2(5(5(2(4(3(3(x1)))))))	→	1(0(4(1(4(4(3(3(2(1(x1))))))))))	(63)
0(5(5(5(0(5(3(x1)))))))	→	0(2(3(0(5(3(0(3(0(0(x1))))))))))	(64)
4(2(5(2(1(3(4(x1)))))))	→	4(2(4(4(3(4(1(1(3(2(x1))))))))))	(65)
5(0(1(3(5(5(4(x1)))))))	→	1(2(3(3(3(0(2(5(1(1(x1))))))))))	(66)
5(1(5(3(5(0(5(x1)))))))	→	5(2(3(0(0(4(2(1(1(5(x1))))))))))	(68)
5(0(3(3(5(1(5(x1)))))))	→	1(1(0(5(2(2(2(3(4(4(x1))))))))))	(69)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

0^#(5(2(0(x1))))	→	3^#(1(4(1(2(5(1(1(2(0(x1))))))))))	(71)
0^#(5(2(0(x1))))	→	1^#(4(1(2(5(1(1(2(0(x1)))))))))	(72)
0^#(5(2(0(x1))))	→	4^#(1(2(5(1(1(2(0(x1))))))))	(73)
0^#(5(2(0(x1))))	→	1^#(2(5(1(1(2(0(x1)))))))	(74)
0^#(5(2(0(x1))))	→	2^#(5(1(1(2(0(x1))))))	(75)
0^#(5(2(0(x1))))	→	5^#(1(1(2(0(x1)))))	(76)
0^#(5(2(0(x1))))	→	1^#(1(2(0(x1))))	(77)
0^#(5(2(0(x1))))	→	1^#(2(0(x1)))	(78)
3^#(5(0(0(3(x1)))))	→	3^#(3(1(4(2(5(3(4(3(1(x1))))))))))	(79)
3^#(5(0(0(3(x1)))))	→	3^#(1(4(2(5(3(4(3(1(x1)))))))))	(80)
3^#(5(0(0(3(x1)))))	→	1^#(4(2(5(3(4(3(1(x1))))))))	(81)
3^#(5(0(0(3(x1)))))	→	4^#(2(5(3(4(3(1(x1)))))))	(82)
3^#(5(0(0(3(x1)))))	→	2^#(5(3(4(3(1(x1))))))	(83)
3^#(5(0(0(3(x1)))))	→	5^#(3(4(3(1(x1)))))	(84)
3^#(5(0(0(3(x1)))))	→	3^#(4(3(1(x1))))	(85)
3^#(5(0(0(3(x1)))))	→	4^#(3(1(x1)))	(86)
3^#(5(0(0(3(x1)))))	→	3^#(1(x1))	(87)
3^#(5(0(0(3(x1)))))	→	1^#(x1)	(88)
5^#(2(1(3(5(0(x1))))))	→	5^#(5(4(4(2(1(1(3(2(0(x1))))))))))	(89)
5^#(2(1(3(5(0(x1))))))	→	5^#(4(4(2(1(1(3(2(0(x1)))))))))	(90)
5^#(2(1(3(5(0(x1))))))	→	4^#(4(2(1(1(3(2(0(x1))))))))	(91)
5^#(2(1(3(5(0(x1))))))	→	4^#(2(1(1(3(2(0(x1)))))))	(92)
5^#(2(1(3(5(0(x1))))))	→	2^#(1(1(3(2(0(x1))))))	(93)
5^#(2(1(3(5(0(x1))))))	→	1^#(1(3(2(0(x1)))))	(94)
5^#(2(1(3(5(0(x1))))))	→	1^#(3(2(0(x1))))	(95)
5^#(2(1(3(5(0(x1))))))	→	3^#(2(0(x1)))	(96)
5^#(2(1(3(5(0(x1))))))	→	2^#(0(x1))	(97)
5^#(5(2(0(2(5(x1))))))	→	4^#(1(4(4(5(4(4(4(5(5(x1))))))))))	(98)
5^#(5(2(0(2(5(x1))))))	→	1^#(4(4(5(4(4(4(5(5(x1)))))))))	(99)
5^#(5(2(0(2(5(x1))))))	→	4^#(4(5(4(4(4(5(5(x1))))))))	(100)
5^#(5(2(0(2(5(x1))))))	→	4^#(5(4(4(4(5(5(x1)))))))	(101)
5^#(5(2(0(2(5(x1))))))	→	5^#(4(4(4(5(5(x1))))))	(102)
5^#(5(2(0(2(5(x1))))))	→	4^#(4(4(5(5(x1)))))	(103)
5^#(5(2(0(2(5(x1))))))	→	4^#(4(5(5(x1))))	(104)
5^#(5(2(0(2(5(x1))))))	→	4^#(5(5(x1)))	(105)
5^#(5(2(0(2(5(x1))))))	→	5^#(5(x1))	(106)
1^#(5(0(0(4(4(0(x1)))))))	→	2^#(1(1(5(1(4(0(2(3(1(x1))))))))))	(107)
1^#(5(0(0(4(4(0(x1)))))))	→	1^#(1(5(1(4(0(2(3(1(x1)))))))))	(108)
1^#(5(0(0(4(4(0(x1)))))))	→	1^#(5(1(4(0(2(3(1(x1))))))))	(109)
1^#(5(0(0(4(4(0(x1)))))))	→	5^#(1(4(0(2(3(1(x1)))))))	(110)
1^#(5(0(0(4(4(0(x1)))))))	→	1^#(4(0(2(3(1(x1))))))	(111)
1^#(5(0(0(4(4(0(x1)))))))	→	4^#(0(2(3(1(x1)))))	(112)
1^#(5(0(0(4(4(0(x1)))))))	→	0^#(2(3(1(x1))))	(113)
1^#(5(0(0(4(4(0(x1)))))))	→	2^#(3(1(x1)))	(114)
1^#(5(0(0(4(4(0(x1)))))))	→	3^#(1(x1))	(115)
1^#(5(0(0(4(4(0(x1)))))))	→	1^#(x1)	(116)
4^#(3(3(3(5(5(1(x1)))))))	→	5^#(3(2(2(2(0(0(1(5(1(x1))))))))))	(117)
4^#(3(3(3(5(5(1(x1)))))))	→	3^#(2(2(2(0(0(1(5(1(x1)))))))))	(118)
4^#(3(3(3(5(5(1(x1)))))))	→	2^#(2(2(0(0(1(5(1(x1))))))))	(119)
4^#(3(3(3(5(5(1(x1)))))))	→	2^#(2(0(0(1(5(1(x1)))))))	(120)
4^#(3(3(3(5(5(1(x1)))))))	→	2^#(0(0(1(5(1(x1))))))	(121)
4^#(3(3(3(5(5(1(x1)))))))	→	0^#(0(1(5(1(x1)))))	(122)
4^#(3(3(3(5(5(1(x1)))))))	→	0^#(1(5(1(x1))))	(123)
4^#(3(3(3(5(5(1(x1)))))))	→	1^#(5(1(x1)))	(124)
2^#(5(1(5(3(2(3(x1)))))))	→	1^#(5(5(1(2(3(2(3(0(2(x1))))))))))	(125)
2^#(5(1(5(3(2(3(x1)))))))	→	5^#(5(1(2(3(2(3(0(2(x1)))))))))	(126)
2^#(5(1(5(3(2(3(x1)))))))	→	5^#(1(2(3(2(3(0(2(x1))))))))	(127)
2^#(5(1(5(3(2(3(x1)))))))	→	1^#(2(3(2(3(0(2(x1)))))))	(128)
2^#(5(1(5(3(2(3(x1)))))))	→	2^#(3(2(3(0(2(x1))))))	(129)
2^#(5(1(5(3(2(3(x1)))))))	→	3^#(2(3(0(2(x1)))))	(130)
2^#(5(1(5(3(2(3(x1)))))))	→	2^#(3(0(2(x1))))	(131)
2^#(5(1(5(3(2(3(x1)))))))	→	3^#(0(2(x1)))	(132)
2^#(5(1(5(3(2(3(x1)))))))	→	0^#(2(x1))	(133)
2^#(5(1(5(3(2(3(x1)))))))	→	2^#(x1)	(134)
5^#(0(1(3(5(0(5(x1)))))))	→	5^#(1(5(3(1(2(4(4(2(5(x1))))))))))	(135)
5^#(0(1(3(5(0(5(x1)))))))	→	1^#(5(3(1(2(4(4(2(5(x1)))))))))	(136)
5^#(0(1(3(5(0(5(x1)))))))	→	5^#(3(1(2(4(4(2(5(x1))))))))	(137)
5^#(0(1(3(5(0(5(x1)))))))	→	3^#(1(2(4(4(2(5(x1)))))))	(138)
5^#(0(1(3(5(0(5(x1)))))))	→	1^#(2(4(4(2(5(x1))))))	(139)
5^#(0(1(3(5(0(5(x1)))))))	→	2^#(4(4(2(5(x1)))))	(140)
5^#(0(1(3(5(0(5(x1)))))))	→	4^#(4(2(5(x1))))	(141)
5^#(0(1(3(5(0(5(x1)))))))	→	4^#(2(5(x1)))	(142)
5^#(0(1(3(5(0(5(x1)))))))	→	2^#(5(x1))	(143)
3^#(3(5(2(0(2(5(x1)))))))	→	3^#(0(2(3(1(1(5(0(2(5(x1))))))))))	(144)
3^#(3(5(2(0(2(5(x1)))))))	→	0^#(2(3(1(1(5(0(2(5(x1)))))))))	(145)
3^#(3(5(2(0(2(5(x1)))))))	→	2^#(3(1(1(5(0(2(5(x1))))))))	(146)
3^#(3(5(2(0(2(5(x1)))))))	→	3^#(1(1(5(0(2(5(x1)))))))	(147)
3^#(3(5(2(0(2(5(x1)))))))	→	1^#(1(5(0(2(5(x1))))))	(148)
3^#(3(5(2(0(2(5(x1)))))))	→	1^#(5(0(2(5(x1)))))	(149)
3^#(3(5(2(0(2(5(x1)))))))	→	5^#(0(2(5(x1))))	(150)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair
5^#(5(2(0(2(5(x1)))))) → 5^#(5(x1)) (106)

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.

5^#(5(2(0(2(5(x1)))))) → 5^#(5(x1)) (106)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair
1^#(5(0(0(4(4(0(x1))))))) → 1^#(x1) (116)

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

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

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

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

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.2.1 Size-Change Termination

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

1^#(5(0(0(4(4(0(x1))))))) → 1^#(x1) (116)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair

2^#(5(1(5(3(2(3(x1))))))) → 2^#(3(0(2(x1)))) (131)

2^#(5(1(5(3(2(3(x1))))))) → 2^#(3(2(3(0(2(x1)))))) (129)

2^#(5(1(5(3(2(3(x1))))))) → 2^#(x1) (134)

1.1.1.1.3 Reduction Pair Processor
Using the linear polynomial interpretation over the naturals

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

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

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

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

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

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

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

the pairs

2^#(5(1(5(3(2(3(x1))))))) → 2^#(3(0(2(x1)))) (131)

2^#(5(1(5(3(2(3(x1))))))) → 2^#(3(2(3(0(2(x1)))))) (129)

2^#(5(1(5(3(2(3(x1))))))) → 2^#(x1) (134)

could be deleted.
1.1.1.1.3.1 P is empty

There are no pairs anymore.

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

Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3746)

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

1.1 Rule Removal

1.1.1 Dependency Pair Transformation

1.1.1.1 Dependency Graph Processor

1.1.1.1.1 Size-Change Termination

1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.2.1 Size-Change Termination

1.1.1.1.3 Reduction Pair Processor

1.1.1.1.3.1 P is empty