Certification Problem

Input (TPDB TRS_Standard/Various_04/21)

The rewrite relation of the following TRS is considered.

+(p1,p1) p2 (1)
+(p1,+(p2,p2)) p5 (2)
+(p5,p5) p10 (3)
+(+(x,y),z) +(x,+(y,z)) (4)
+(p1,+(p1,x)) +(p2,x) (5)
+(p1,+(p2,+(p2,x))) +(p5,x) (6)
+(p2,p1) +(p1,p2) (7)
+(p2,+(p1,x)) +(p1,+(p2,x)) (8)
+(p2,+(p2,p2)) +(p1,p5) (9)
+(p2,+(p2,+(p2,x))) +(p1,+(p5,x)) (10)
+(p5,p1) +(p1,p5) (11)
+(p5,+(p1,x)) +(p1,+(p5,x)) (12)
+(p5,p2) +(p2,p5) (13)
+(p5,+(p2,x)) +(p2,+(p5,x)) (14)
+(p5,+(p5,x)) +(p10,x) (15)
+(p10,p1) +(p1,p10) (16)
+(p10,+(p1,x)) +(p1,+(p10,x)) (17)
+(p10,p2) +(p2,p10) (18)
+(p10,+(p2,x)) +(p2,+(p10,x)) (19)
+(p10,p5) +(p5,p10) (20)
+(p10,+(p5,x)) +(p5,+(p10,x)) (21)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(p10) = 2 weight(p10) = 7
prec(p5) = 1 weight(p5) = 5
prec(p2) = 5 weight(p2) = 4
prec(+) = 3 weight(+) = 1
prec(p1) = 0 weight(p1) = 2
all of the following rules can be deleted.
+(p1,p1) p2 (1)
+(p1,+(p2,p2)) p5 (2)
+(p5,p5) p10 (3)
+(+(x,y),z) +(x,+(y,z)) (4)
+(p1,+(p1,x)) +(p2,x) (5)
+(p1,+(p2,+(p2,x))) +(p5,x) (6)
+(p2,p1) +(p1,p2) (7)
+(p2,+(p1,x)) +(p1,+(p2,x)) (8)
+(p2,+(p2,p2)) +(p1,p5) (9)
+(p2,+(p2,+(p2,x))) +(p1,+(p5,x)) (10)
+(p5,p1) +(p1,p5) (11)
+(p5,+(p1,x)) +(p1,+(p5,x)) (12)
+(p5,p2) +(p2,p5) (13)
+(p5,+(p2,x)) +(p2,+(p5,x)) (14)
+(p5,+(p5,x)) +(p10,x) (15)
+(p10,p1) +(p1,p10) (16)
+(p10,+(p1,x)) +(p1,+(p10,x)) (17)
+(p10,p2) +(p2,p10) (18)
+(p10,+(p2,x)) +(p2,+(p10,x)) (19)
+(p10,p5) +(p5,p10) (20)
+(p10,+(p5,x)) +(p5,+(p10,x)) (21)

1.1 R is empty

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