Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/86745)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[0(x1)] = 1 · x1 + 61
[1(x1)] = 1 · x1 + 70
[2(x1)] = 1 · x1 + 76
[3(x1)] = 1 · x1 + 77
[4(x1)] = 1 · x1 + 64
[5(x1)] = 1 · x1 + 60
all of the following rules can be deleted.
0(1(2(1(x1)))) → 3(3(2(x1))) (1)
1(2(3(2(x1)))) → 3(4(4(2(x1)))) (2)
0(5(1(4(1(x1))))) → 4(1(4(3(x1)))) (3)
4(3(0(2(2(x1))))) → 4(1(1(4(5(x1))))) (4)
5(5(1(5(2(x1))))) → 4(3(5(2(x1)))) (5)
2(0(4(1(2(2(1(3(x1)))))))) → 2(3(0(4(5(5(1(1(x1)))))))) (7)
1(2(2(1(5(2(1(2(1(x1))))))))) → 1(2(2(2(0(2(4(4(3(x1))))))))) (8)
4(5(1(4(3(4(3(5(4(3(x1)))))))))) → 4(3(2(0(2(4(3(2(3(x1))))))))) (9)
1(4(1(2(5(3(4(3(3(2(2(x1))))))))))) → 0(0(1(4(0(4(5(2(3(0(4(x1))))))))))) (10)
4(5(1(3(2(2(5(4(3(5(4(x1))))))))))) → 4(0(1(1(5(3(5(4(2(2(4(x1))))))))))) (11)
5(1(4(0(1(5(5(3(3(0(3(2(x1)))))))))))) → 3(0(5(3(2(0(1(0(4(1(2(x1))))))))))) (12)
0(4(1(1(3(3(2(5(4(2(2(1(3(x1))))))))))))) → 1(0(1(4(3(4(4(2(3(4(2(2(1(x1))))))))))))) (13)
5(1(3(3(5(3(1(3(2(1(2(0(4(x1))))))))))))) → 2(2(3(2(3(2(3(5(2(5(1(4(x1)))))))))))) (14)
0(5(3(5(3(3(3(3(4(5(5(5(4(4(x1)))))))))))))) → 0(1(0(3(2(3(4(0(5(5(2(4(0(x1))))))))))))) (15)
1(5(0(1(0(4(4(2(2(3(4(1(4(1(x1)))))))))))))) → 3(4(5(0(0(4(0(3(5(0(4(1(5(4(x1)))))))))))))) (16)
5(1(2(2(4(0(2(4(2(5(2(1(4(0(5(x1))))))))))))))) → 0(1(4(3(0(5(3(4(3(3(1(4(1(5(x1)))))))))))))) (18)
0(4(0(3(2(0(2(1(2(0(0(2(4(2(3(4(x1)))))))))))))))) → 3(2(1(3(3(4(5(5(4(0(3(2(1(2(3(x1))))))))))))))) (19)
1(5(1(3(3(3(0(4(0(2(3(1(5(1(4(2(x1)))))))))))))))) → 3(4(0(5(0(4(4(0(2(1(3(1(4(0(4(2(x1)))))))))))))))) (20)
5(1(1(0(0(3(2(5(0(3(4(2(1(2(5(1(x1)))))))))))))))) → 5(1(3(2(1(0(1(0(5(5(3(1(1(4(1(0(x1)))))))))))))))) (21)
4(1(0(3(0(4(3(2(2(1(3(2(2(4(0(2(4(x1))))))))))))))))) → 4(2(5(3(3(3(1(2(4(5(3(5(3(5(1(3(4(x1))))))))))))))))) (23)
3(0(0(2(1(1(3(5(1(2(2(2(5(1(0(0(0(1(x1)))))))))))))))))) → 3(5(1(0(4(0(1(2(2(5(0(3(4(3(5(5(4(3(x1)))))))))))))))))) (24)
4(5(5(1(5(3(5(3(2(0(4(4(2(1(0(3(5(3(x1)))))))))))))))))) → 4(4(0(5(1(3(5(5(3(4(4(0(0(4(3(0(0(0(x1)))))))))))))))))) (25)
4(5(5(2(5(1(0(2(1(0(1(4(4(4(2(1(5(1(x1)))))))))))))))))) → 4(3(2(3(0(2(5(3(4(1(4(4(5(1(1(4(0(x1))))))))))))))))) (26)
0(2(0(2(2(0(1(1(2(4(1(1(0(3(3(2(1(4(1(4(x1)))))))))))))))))))) → 2(2(3(3(0(2(1(3(5(3(4(4(1(2(4(4(4(4(4(0(x1)))))))))))))))))))) (27)
3(4(1(1(0(3(4(0(5(5(5(5(3(5(2(3(2(3(1(3(x1)))))))))))))))))))) → 3(4(3(4(3(1(0(1(1(4(5(5(2(3(2(3(0(2(3(x1))))))))))))))))))) (28)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
0#(4(3(3(4(4(1(x1))))))) → 4#(4(2(5(0(2(2(x1))))))) (31)
0#(4(3(3(4(4(1(x1))))))) → 4#(2(5(0(2(2(x1)))))) (32)
0#(4(3(3(4(4(1(x1))))))) → 5#(0(2(2(x1)))) (33)
0#(4(3(3(4(4(1(x1))))))) → 0#(2(2(x1))) (34)
5#(1(0(5(2(2(2(3(3(2(5(1(5(1(x1)))))))))))))) → 5#(4(0(1(4(3(2(2(3(3(3(5(5(1(x1)))))))))))))) (35)
5#(1(0(5(2(2(2(3(3(2(5(1(5(1(x1)))))))))))))) → 4#(0(1(4(3(2(2(3(3(3(5(5(1(x1))))))))))))) (36)
5#(1(0(5(2(2(2(3(3(2(5(1(5(1(x1)))))))))))))) → 0#(1(4(3(2(2(3(3(3(5(5(1(x1)))))))))))) (37)
5#(1(0(5(2(2(2(3(3(2(5(1(5(1(x1)))))))))))))) → 4#(3(2(2(3(3(3(5(5(1(x1)))))))))) (38)
5#(1(0(5(2(2(2(3(3(2(5(1(5(1(x1)))))))))))))) → 3#(2(2(3(3(3(5(5(1(x1))))))))) (39)
5#(1(0(5(2(2(2(3(3(2(5(1(5(1(x1)))))))))))))) → 3#(3(3(5(5(1(x1)))))) (40)
5#(1(0(5(2(2(2(3(3(2(5(1(5(1(x1)))))))))))))) → 3#(3(5(5(1(x1))))) (41)
5#(1(0(5(2(2(2(3(3(2(5(1(5(1(x1)))))))))))))) → 3#(5(5(1(x1)))) (42)
5#(1(0(5(2(2(2(3(3(2(5(1(5(1(x1)))))))))))))) → 5#(5(1(x1))) (43)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 3#(2(3(1(0(2(0(2(4(5(5(4(1(0(0(2(5(0(x1)))))))))))))))))) (44)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 3#(1(0(2(0(2(4(5(5(4(1(0(0(2(5(0(x1)))))))))))))))) (45)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 0#(2(0(2(4(5(5(4(1(0(0(2(5(0(x1)))))))))))))) (46)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 0#(2(4(5(5(4(1(0(0(2(5(0(x1)))))))))))) (47)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 4#(5(5(4(1(0(0(2(5(0(x1)))))))))) (48)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 5#(5(4(1(0(0(2(5(0(x1))))))))) (49)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 5#(4(1(0(0(2(5(0(x1)))))))) (50)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 4#(1(0(0(2(5(0(x1))))))) (51)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 0#(0(2(5(0(x1))))) (52)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 0#(2(5(0(x1)))) (53)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 5#(0(x1)) (54)
3#(2(1(2(4(2(1(1(3(3(3(5(2(2(0(4(4(x1))))))))))))))))) → 0#(x1) (55)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 4#(4(3(1(4(4(0(5(3(5(2(1(4(2(4(1(0(2(4(5(0(x1))))))))))))))))))))) (56)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 4#(3(1(4(4(0(5(3(5(2(1(4(2(4(1(0(2(4(5(0(x1)))))))))))))))))))) (57)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 3#(1(4(4(0(5(3(5(2(1(4(2(4(1(0(2(4(5(0(x1))))))))))))))))))) (58)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 4#(4(0(5(3(5(2(1(4(2(4(1(0(2(4(5(0(x1))))))))))))))))) (59)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 4#(0(5(3(5(2(1(4(2(4(1(0(2(4(5(0(x1)))))))))))))))) (60)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 0#(5(3(5(2(1(4(2(4(1(0(2(4(5(0(x1))))))))))))))) (61)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 5#(3(5(2(1(4(2(4(1(0(2(4(5(0(x1)))))))))))))) (62)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 3#(5(2(1(4(2(4(1(0(2(4(5(0(x1))))))))))))) (63)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 5#(2(1(4(2(4(1(0(2(4(5(0(x1)))))))))))) (64)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 4#(2(4(1(0(2(4(5(0(x1))))))))) (65)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 4#(1(0(2(4(5(0(x1))))))) (66)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 0#(2(4(5(0(x1))))) (67)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 4#(5(0(x1))) (68)
4#(5(2(3(5(4(5(0(5(1(2(3(0(1(1(0(3(5(0(3(0(x1))))))))))))))))))))) → 5#(0(x1)) (69)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 5#(0(3(2(2(0(4(1(1(5(3(0(1(5(0(1(3(2(2(3(x1)))))))))))))))))))) (70)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 0#(3(2(2(0(4(1(1(5(3(0(1(5(0(1(3(2(2(3(x1))))))))))))))))))) (71)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 3#(2(2(0(4(1(1(5(3(0(1(5(0(1(3(2(2(3(x1)))))))))))))))))) (72)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 0#(4(1(1(5(3(0(1(5(0(1(3(2(2(3(x1))))))))))))))) (73)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 4#(1(1(5(3(0(1(5(0(1(3(2(2(3(x1)))))))))))))) (74)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 5#(3(0(1(5(0(1(3(2(2(3(x1))))))))))) (75)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 3#(0(1(5(0(1(3(2(2(3(x1)))))))))) (76)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 0#(1(5(0(1(3(2(2(3(x1))))))))) (77)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 5#(0(1(3(2(2(3(x1))))))) (78)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 0#(1(3(2(2(3(x1)))))) (79)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 3#(2(2(3(x1)))) (80)
5#(1(4(0(0(3(4(2(3(0(3(5(4(0(4(2(4(0(0(5(0(x1))))))))))))))))))))) → 3#(x1) (81)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.