Certification Problem

Input (COPS 186)

We consider the TRS containing the following rules:

+(x,0)	→	x	(1)
+(s(x),y)	→	s(+(x,y))	(2)
+(x,y)	→	+(y,x)	(3)

The underlying signature is as follows:

{+/2, 0/0, s/1}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2023)

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

+(x,y)	→	+(y,x)	(3)
+(s(x),y)	→	s(+(x,y))	(2)
+(x,0)	→	x	(1)
+(0,x)	→	x	(4)
+(y,s(x))	→	s(+(x,y))	(5)
+(y,s(x31))	→	s(+(x31,y))	(6)

All redundant rules that were added or removed can be simulated in 2 steps .

1.1 Decreasing Diagrams

1.1.2 Rule Labeling

Confluence is proven, because all critical peaks can be joined decreasingly using the following rule labeling function (rules that are not shown have label 0).

+(x,y) → +(y,x) (3)
↦ 0
+(s(x),y) → s(+(x,y)) (2)
↦ 1
+(x,0) → x (1)
↦ 0
+(0,x) → x (4)
↦ 0
+(y,s(x)) → s(+(x,y)) (5)
↦ 1
+(y,s(x31)) → s(+(x31,y)) (6)
↦ 3

The critical pairs can be joined as follows. Here, ↔ is always chosen as an appropriate rewrite relation which is automatically inferred by the certifier.

The critical peak s = +(y,s(x))←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ t
The critical peak s = +(0,x)←→_ε x = t can be joined as follows.
s ↔ t
The critical peak s = +(x,0)←→_ε x = t can be joined as follows.
s ↔ t
The critical peak s = +(s(x),y)←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ t
The critical peak s = +(s(x31),y)←→_ε s(+(x31,y)) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(x157,y))←→_ε +(y,s(x157)) = t can be joined as follows.
s ↔ s(+(x157,y)) ↔ t
The critical peak s = s(+(x159,0))←→_ε s(x159) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(x161,s(x)))←→_ε s(+(x,s(x161))) = t can be joined as follows.
s ↔ s(s(+(x,x161))) ↔ s(s(+(x161,x))) ↔ t
The critical peak s = s(+(x161,s(x)))←→_ε s(+(x,s(x161))) = t can be joined as follows.
s ↔ s(+(s(x),x161)) ↔ s(s(+(x,x161))) ↔ s(s(+(x161,x))) ↔ t
The critical peak s = s(+(x161,s(x)))←→_ε s(+(x,s(x161))) = t can be joined as follows.
s ↔ s(s(+(x,x161))) ↔ s(s(+(x161,x))) ↔ t
The critical peak s = s(+(x161,s(x)))←→_ε s(+(x,s(x161))) = t can be joined as follows.
s ↔ s(s(+(x,x161))) ↔ s(s(+(x161,x))) ↔ s(+(s(x161),x)) ↔ t
The critical peak s = s(+(x163,s(x31)))←→_ε s(+(x31,s(x163))) = t can be joined as follows.
s ↔ s(s(+(x31,x163))) ↔ s(s(+(x163,x31))) ↔ t
The critical peak s = s(+(x163,s(x31)))←→_ε s(+(x31,s(x163))) = t can be joined as follows.
s ↔ s(+(s(x31),x163)) ↔ s(s(+(x31,x163))) ↔ s(s(+(x163,x31))) ↔ t
The critical peak s = s(+(x163,s(x31)))←→_ε s(+(x31,s(x163))) = t can be joined as follows.
s ↔ s(s(+(x31,x163))) ↔ s(s(+(x163,x31))) ↔ t
The critical peak s = s(+(x163,s(x31)))←→_ε s(+(x31,s(x163))) = t can be joined as follows.
s ↔ s(s(+(x31,x163))) ↔ s(s(+(x163,x31))) ↔ s(+(s(x163),x31)) ↔ t
The critical peak s = x←→_ε +(0,x) = t can be joined as follows.
s ↔ x ↔ t
The critical peak s = s(x)←→_ε s(+(x,0)) = t can be joined as follows.
s ↔ s(x) ↔ t
The critical peak s = 0←→_ε 0 = t can be joined as follows.
s ↔ t
The critical peak s = y←→_ε +(y,0) = t can be joined as follows.
s ↔ y ↔ t
The critical peak s = 0←→_ε 0 = t can be joined as follows.
s ↔ t
The critical peak s = s(x)←→_ε s(+(x,0)) = t can be joined as follows.
s ↔ s(x) ↔ t
The critical peak s = s(x31)←→_ε s(+(x31,0)) = t can be joined as follows.
s ↔ s(x31) ↔ t
The critical peak s = s(+(x173,x))←→_ε +(s(x173),x) = t can be joined as follows.
s ↔ s(+(x173,x)) ↔ t
The critical peak s = s(+(x175,s(x)))←→_ε s(+(x,s(x175))) = t can be joined as follows.
s ↔ s(s(+(x,x175))) ↔ s(s(+(x175,x))) ↔ t
The critical peak s = s(+(x175,s(x)))←→_ε s(+(x,s(x175))) = t can be joined as follows.
s ↔ s(+(s(x),x175)) ↔ s(s(+(x,x175))) ↔ s(s(+(x175,x))) ↔ t
The critical peak s = s(+(x175,s(x)))←→_ε s(+(x,s(x175))) = t can be joined as follows.
s ↔ s(s(+(x,x175))) ↔ s(s(+(x175,x))) ↔ t
The critical peak s = s(+(x175,s(x)))←→_ε s(+(x,s(x175))) = t can be joined as follows.
s ↔ s(s(+(x,x175))) ↔ s(s(+(x175,x))) ↔ s(+(s(x175),x)) ↔ t
The critical peak s = s(+(x177,0))←→_ε s(x177) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(x179,x))←→_ε +(s(x179),x) = t can be joined as follows.
s ↔ s(+(x179,x)) ↔ t
The critical peak s = s(+(x181,s(x)))←→_ε s(+(x,s(x181))) = t can be joined as follows.
s ↔ s(s(+(x,x181))) ↔ s(s(+(x181,x))) ↔ t
The critical peak s = s(+(x181,s(x)))←→_ε s(+(x,s(x181))) = t can be joined as follows.
s ↔ s(+(s(x),x181)) ↔ s(s(+(x,x181))) ↔ s(s(+(x181,x))) ↔ t
The critical peak s = s(+(x181,s(x)))←→_ε s(+(x,s(x181))) = t can be joined as follows.
s ↔ s(s(+(x,x181))) ↔ s(s(+(x181,x))) ↔ t
The critical peak s = s(+(x181,s(x)))←→_ε s(+(x,s(x181))) = t can be joined as follows.
s ↔ s(s(+(x,x181))) ↔ s(s(+(x181,x))) ↔ s(+(s(x181),x)) ↔ t
The critical peak s = s(+(x183,0))←→_ε s(x183) = t can be joined as follows.
s ↔ t