Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/5076)

The rewrite relation of the following TRS is considered.

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

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
5(4(3(x1))) → 2(2(5(3(5(1(2(3(2(3(x1)))))))))) (34)
3(5(4(0(x1)))) → 5(0(5(1(1(3(2(3(0(4(x1)))))))))) (35)
1(4(5(0(x1)))) → 1(0(2(2(1(5(1(4(1(0(x1)))))))))) (36)
3(5(4(3(x1)))) → 2(3(0(1(4(1(2(3(2(3(x1)))))))))) (37)
5(0(5(3(x1)))) → 5(1(0(2(3(3(4(1(2(3(x1)))))))))) (38)
5(5(0(4(x1)))) → 5(3(5(3(0(2(2(2(3(3(x1)))))))))) (39)
4(3(5(5(x1)))) → 2(2(4(3(4(1(4(4(1(1(x1)))))))))) (40)
0(1(5(5(0(x1))))) → 0(4(1(5(1(3(5(4(2(0(x1)))))))))) (41)
0(1(5(3(2(x1))))) → 0(2(4(5(1(1(5(2(1(2(x1)))))))))) (42)
0(0(5(4(3(x1))))) → 0(3(4(0(5(2(1(3(3(4(x1)))))))))) (43)
2(5(3(2(5(x1))))) → 2(2(2(5(0(2(1(2(2(5(x1)))))))))) (44)
1(4(5(4(5(x1))))) → 1(0(2(4(0(1(4(3(5(1(x1)))))))))) (45)
5(5(0(5(0(0(x1)))))) → 2(5(4(2(0(3(4(3(1(1(x1)))))))))) (46)
5(4(3(4(5(0(x1)))))) → 5(2(3(4(3(2(2(0(5(1(x1)))))))))) (47)
0(2(5(4(5(0(x1)))))) → 0(2(2(2(3(3(5(2(2(0(x1)))))))))) (48)
5(0(1(5(5(0(x1)))))) → 5(1(1(3(4(5(2(0(2(1(x1)))))))))) (49)
3(1(1(5(5(0(x1)))))) → 2(4(1(4(1(2(3(0(5(0(x1)))))))))) (50)
4(4(5(3(2(1(x1)))))) → 4(2(2(3(0(4(0(2(0(4(x1)))))))))) (51)
3(3(5(4(0(3(x1)))))) → 3(0(0(1(2(4(5(0(2(4(x1)))))))))) (52)
1(0(5(0(4(3(x1)))))) → 1(0(4(0(0(1(3(1(2(3(x1)))))))))) (53)
1(4(5(4(0(4(x1)))))) → 1(1(0(4(1(1(1(3(4(4(x1)))))))))) (54)
5(5(0(5(3(4(x1)))))) → 5(3(1(2(5(2(5(2(3(4(x1)))))))))) (55)
0(0(1(0(5(5(x1)))))) → 0(4(2(2(4(4(2(4(0(5(x1)))))))))) (56)
1(0(4(0(5(0(0(x1))))))) → 1(4(3(3(0(2(4(4(1(5(x1)))))))))) (57)
0(3(5(3(5(0(0(x1))))))) → 0(0(1(3(4(2(0(5(2(0(x1)))))))))) (58)
5(3(2(5(2(1(0(x1))))))) → 5(5(1(5(0(4(1(3(4(4(x1)))))))))) (59)
3(3(2(5(5(5(0(x1))))))) → 2(4(2(4(5(0(3(1(0(1(x1)))))))))) (60)
4(3(2(5(0(0(1(x1))))))) → 4(0(1(2(3(5(4(1(4(2(x1)))))))))) (61)
5(5(2(2(5(5(1(x1))))))) → 5(1(5(1(3(5(2(4(0(1(x1)))))))))) (62)
3(5(4(3(4(3(2(x1))))))) → 2(2(1(0(5(3(2(5(1(0(x1)))))))))) (63)
5(4(5(0(5(0(4(x1))))))) → 5(5(3(5(2(2(3(1(2(1(x1)))))))))) (64)
1(4(5(5(5(3(5(x1))))))) → 1(4(5(2(3(4(0(2(1(0(x1)))))))))) (65)
4(3(3(5(5(4(5(x1))))))) → 0(0(3(1(4(3(2(0(5(1(x1)))))))))) (66)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1.1 Semantic Labeling Processor

The following interpretations form a model of the rules.

As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):

[5(x1)] = 0
[2#(x1)] = 0
[5#(x1)] = 0
[3#(x1)] = 0
[1#(x1)] = 0
[0#(x1)] = 0
[4#(x1)] = 0
[0(x1)] = 0
[1(x1)] = 1
[2(x1)] = 0
[3(x1)] = 0
[4(x1)] = 0

We obtain the set of labeled pairs

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

and the set of labeled rules:
50(40(30(x1))) → 20(20(50(30(51(10(20(30(20(30(x1)))))))))) (1003)
50(40(31(x1))) → 20(20(50(30(51(10(20(30(20(31(x1)))))))))) (1004)
30(50(40(00(x1)))) → 50(00(51(11(10(30(20(30(00(40(x1)))))))))) (1005)
30(50(40(01(x1)))) → 50(00(51(11(10(30(20(30(00(41(x1)))))))))) (1006)
10(40(50(00(x1)))) → 10(00(20(21(10(51(10(41(10(00(x1)))))))))) (1007)
10(40(50(01(x1)))) → 10(00(20(21(10(51(10(41(10(01(x1)))))))))) (1008)
30(50(40(30(x1)))) → 20(30(01(10(41(10(20(30(20(30(x1)))))))))) (1009)
30(50(40(31(x1)))) → 20(30(01(10(41(10(20(30(20(31(x1)))))))))) (1010)
50(00(50(30(x1)))) → 51(10(00(20(30(30(41(10(20(30(x1)))))))))) (1011)
50(00(50(31(x1)))) → 51(10(00(20(30(30(41(10(20(31(x1)))))))))) (1012)
50(50(00(40(x1)))) → 50(30(50(30(00(20(20(20(30(30(x1)))))))))) (1013)
50(50(00(41(x1)))) → 50(30(50(30(00(20(20(20(30(31(x1)))))))))) (1014)
40(30(50(50(x1)))) → 20(20(40(30(41(10(40(41(11(10(x1)))))))))) (1015)
40(30(50(51(x1)))) → 20(20(40(30(41(10(40(41(11(11(x1)))))))))) (1016)
01(10(50(50(00(x1))))) → 00(41(10(51(10(30(50(40(20(00(x1)))))))))) (1017)
01(10(50(50(01(x1))))) → 00(41(10(51(10(30(50(40(20(01(x1)))))))))) (1018)
01(10(50(30(20(x1))))) → 00(20(40(51(11(10(50(21(10(20(x1)))))))))) (1019)
01(10(50(30(21(x1))))) → 00(20(40(51(11(10(50(21(10(21(x1)))))))))) (1020)
00(00(50(40(30(x1))))) → 00(30(40(00(50(21(10(30(30(40(x1)))))))))) (1021)
00(00(50(40(31(x1))))) → 00(30(40(00(50(21(10(30(30(41(x1)))))))))) (1022)
20(50(30(20(50(x1))))) → 20(20(20(50(00(21(10(20(20(50(x1)))))))))) (1023)
20(50(30(20(51(x1))))) → 20(20(20(50(00(21(10(20(20(51(x1)))))))))) (1024)
10(40(50(40(50(x1))))) → 10(00(20(40(01(10(40(30(51(10(x1)))))))))) (1025)
10(40(50(40(51(x1))))) → 10(00(20(40(01(10(40(30(51(11(x1)))))))))) (1026)
50(50(00(50(00(00(x1)))))) → 20(50(40(20(00(30(40(31(11(10(x1)))))))))) (1027)
50(50(00(50(00(01(x1)))))) → 20(50(40(20(00(30(40(31(11(11(x1)))))))))) (1028)
50(40(30(40(50(00(x1)))))) → 50(20(30(40(30(20(20(00(51(10(x1)))))))))) (1029)
50(40(30(40(50(01(x1)))))) → 50(20(30(40(30(20(20(00(51(11(x1)))))))))) (1030)
00(20(50(40(50(00(x1)))))) → 00(20(20(20(30(30(50(20(20(00(x1)))))))))) (1031)
00(20(50(40(50(01(x1)))))) → 00(20(20(20(30(30(50(20(20(01(x1)))))))))) (1032)
50(01(10(50(50(00(x1)))))) → 51(11(10(30(40(50(20(00(21(10(x1)))))))))) (1033)
50(01(10(50(50(01(x1)))))) → 51(11(10(30(40(50(20(00(21(11(x1)))))))))) (1034)
31(11(10(50(50(00(x1)))))) → 20(41(10(41(10(20(30(00(50(00(x1)))))))))) (1035)
31(11(10(50(50(01(x1)))))) → 20(41(10(41(10(20(30(00(50(01(x1)))))))))) (1036)
40(40(50(30(21(10(x1)))))) → 40(20(20(30(00(40(00(20(00(40(x1)))))))))) (1037)
40(40(50(30(21(11(x1)))))) → 40(20(20(30(00(40(00(20(00(41(x1)))))))))) (1038)
30(30(50(40(00(30(x1)))))) → 30(00(01(10(20(40(50(00(20(40(x1)))))))))) (1039)
30(30(50(40(00(31(x1)))))) → 30(00(01(10(20(40(50(00(20(41(x1)))))))))) (1040)
10(00(50(00(40(30(x1)))))) → 10(00(40(00(01(10(31(10(20(30(x1)))))))))) (1041)
10(00(50(00(40(31(x1)))))) → 10(00(40(00(01(10(31(10(20(31(x1)))))))))) (1042)
10(40(50(40(00(40(x1)))))) → 11(10(00(41(11(11(10(30(40(40(x1)))))))))) (1043)
10(40(50(40(00(41(x1)))))) → 11(10(00(41(11(11(10(30(40(41(x1)))))))))) (1044)
50(50(00(50(30(40(x1)))))) → 50(31(10(20(50(20(50(20(30(40(x1)))))))))) (1045)
50(50(00(50(30(41(x1)))))) → 50(31(10(20(50(20(50(20(30(41(x1)))))))))) (1046)
00(01(10(00(50(50(x1)))))) → 00(40(20(20(40(40(20(40(00(50(x1)))))))))) (1047)
00(01(10(00(50(51(x1)))))) → 00(40(20(20(40(40(20(40(00(51(x1)))))))))) (1048)
10(00(40(00(50(00(00(x1))))))) → 10(40(30(30(00(20(40(41(10(50(x1)))))))))) (1049)
10(00(40(00(50(00(01(x1))))))) → 10(40(30(30(00(20(40(41(10(51(x1)))))))))) (1050)
00(30(50(30(50(00(00(x1))))))) → 00(01(10(30(40(20(00(50(20(00(x1)))))))))) (1051)
00(30(50(30(50(00(01(x1))))))) → 00(01(10(30(40(20(00(50(20(01(x1)))))))))) (1052)
50(30(20(50(21(10(00(x1))))))) → 50(51(10(50(00(41(10(30(40(40(x1)))))))))) (1053)
50(30(20(50(21(10(01(x1))))))) → 50(51(10(50(00(41(10(30(40(41(x1)))))))))) (1054)
30(30(20(50(50(50(00(x1))))))) → 20(40(20(40(50(00(31(10(01(10(x1)))))))))) (1055)
30(30(20(50(50(50(01(x1))))))) → 20(40(20(40(50(00(31(10(01(11(x1)))))))))) (1056)
40(30(20(50(00(01(10(x1))))))) → 40(01(10(20(30(50(41(10(40(20(x1)))))))))) (1057)
40(30(20(50(00(01(11(x1))))))) → 40(01(10(20(30(50(41(10(40(21(x1)))))))))) (1058)
50(50(20(20(50(51(10(x1))))))) → 51(10(51(10(30(50(20(40(01(10(x1)))))))))) (1059)
50(50(20(20(50(51(11(x1))))))) → 51(10(51(10(30(50(20(40(01(11(x1)))))))))) (1060)
30(50(40(30(40(30(20(x1))))))) → 20(21(10(00(50(30(20(51(10(00(x1)))))))))) (1061)
30(50(40(30(40(30(21(x1))))))) → 20(21(10(00(50(30(20(51(10(01(x1)))))))))) (1062)
50(40(50(00(50(00(40(x1))))))) → 50(50(30(50(20(20(31(10(21(10(x1)))))))))) (1063)
50(40(50(00(50(00(41(x1))))))) → 50(50(30(50(20(20(31(10(21(11(x1)))))))))) (1064)
10(40(50(50(50(30(50(x1))))))) → 10(40(50(20(30(40(00(21(10(00(x1)))))))))) (1065)
10(40(50(50(50(30(51(x1))))))) → 10(40(50(20(30(40(00(21(10(01(x1)))))))))) (1066)
40(30(30(50(50(40(50(x1))))))) → 00(00(31(10(40(30(20(00(51(10(x1)))))))))) (1067)
40(30(30(50(50(40(51(x1))))))) → 00(00(31(10(40(30(20(00(51(11(x1)))))))))) (1068)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.