Certification Problem

Input (COPS 8)

We consider the TRS containing the following rules:

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

The underlying signature is as follows:

{+/2, 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)
+(x,s(y))	→	s(+(x,y))	(2)
+(s(x),y)	→	s(+(x,y))	(1)
+(x,y)	→	+(x,y)	(4)
+(x,s(y))	→	s(+(y,x))	(5)
+(s(x),y)	→	s(+(y,x))	(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
+(x,s(y)) → s(+(x,y)) (2)
↦ 0
+(s(x),y) → s(+(x,y)) (1)
↦ 0
+(x,y) → +(x,y) (4)
↦ 0
+(x,s(y)) → s(+(y,x)) (5)
↦ 0
+(s(x),y) → s(+(y,x)) (6)
↦ 0

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 = +(s(y),x)←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ s(+(y,x)) ↔ t
The critical peak s = +(s(y),x)←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ t
The critical peak s = +(y,s(x))←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ s(+(y,x)) ↔ t
The critical peak s = +(y,s(x))←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ t
The critical peak s = +(y,x)←→_ε +(x,y) = t can be joined as follows.
s ↔ +(y,x) ↔ t
The critical peak s = +(y,x)←→_ε +(x,y) = t can be joined as follows.
s ↔ t
The critical peak s = +(s(y),x)←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ t
The critical peak s = +(s(y),x)←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ s(+(x,y)) ↔ t
The critical peak s = +(y,s(x))←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ t
The critical peak s = +(y,s(x))←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ s(+(x,y)) ↔ t
The critical peak s = s(+(x,x175))←→_ε +(s(x175),x) = t can be joined as follows.
s ↔ s(+(x,x175)) ↔ t
The critical peak s = s(+(x,x175))←→_ε +(s(x175),x) = t can be joined as follows.
s ↔ s(+(x175,x)) ↔ t
The critical peak s = s(+(s(x),x177))←→_ε s(+(x,s(x177))) = t can be joined as follows.
s ↔ s(s(+(x,x177))) ↔ t
The critical peak s = s(+(s(x),x177))←→_ε s(+(x,s(x177))) = t can be joined as follows.
s ↔ s(s(+(x177,x))) ↔ t
The critical peak s = s(+(x,x179))←→_ε +(x,s(x179)) = t can be joined as follows.
s ↔ s(+(x,x179)) ↔ t
The critical peak s = s(+(x,x179))←→_ε +(x,s(x179)) = t can be joined as follows.
s ↔ s(+(x179,x)) ↔ t
The critical peak s = s(+(x,y))←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ s(+(x,y)) ↔ t
The critical peak s = s(+(x,y))←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(s(x),x183))←→_ε s(+(s(x183),x)) = t can be joined as follows.
s ↔ s(s(+(x,x183))) ↔ t
The critical peak s = s(+(s(x),x183))←→_ε s(+(s(x183),x)) = t can be joined as follows.
s ↔ s(s(+(x183,x))) ↔ t
The critical peak s = s(+(x184,y))←→_ε +(y,s(x184)) = t can be joined as follows.
s ↔ s(+(x184,y)) ↔ t
The critical peak s = s(+(x184,y))←→_ε +(y,s(x184)) = t can be joined as follows.
s ↔ s(+(y,x184)) ↔ t
The critical peak s = s(+(x186,s(y)))←→_ε s(+(s(x186),y)) = t can be joined as follows.
s ↔ s(s(+(x186,y))) ↔ t
The critical peak s = s(+(x186,s(y)))←→_ε s(+(s(x186),y)) = t can be joined as follows.
s ↔ s(s(+(y,x186))) ↔ t
The critical peak s = s(+(x188,y))←→_ε +(s(x188),y) = t can be joined as follows.
s ↔ s(+(x188,y)) ↔ t
The critical peak s = s(+(x188,y))←→_ε +(s(x188),y) = t can be joined as follows.
s ↔ s(+(y,x188)) ↔ t
The critical peak s = s(+(x190,s(y)))←→_ε s(+(y,s(x190))) = t can be joined as follows.
s ↔ s(s(+(x190,y))) ↔ t
The critical peak s = s(+(x190,s(y)))←→_ε s(+(y,s(x190))) = t can be joined as follows.
s ↔ s(s(+(y,x190))) ↔ t
The critical peak s = s(+(x,y))←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ s(+(x,y)) ↔ t
The critical peak s = s(+(x,y))←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ t
The critical peak s = +(x,y)←→_ε +(y,x) = t can be joined as follows.
s ↔ +(x,y) ↔ t
The critical peak s = +(x,y)←→_ε +(y,x) = t can be joined as follows.
s ↔ t
The critical peak s = +(x,s(y))←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ t
The critical peak s = +(x,s(y))←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ s(+(y,x)) ↔ t
The critical peak s = +(s(x),y)←→_ε s(+(x,y)) = 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 ↔ s(+(y,x)) ↔ t
The critical peak s = +(x,s(y))←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ s(+(x,y)) ↔ t
The critical peak s = +(x,s(y))←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ t
The critical peak s = +(s(x),y)←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ s(+(x,y)) ↔ t
The critical peak s = +(s(x),y)←→_ε s(+(y,x)) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(x205,x))←→_ε +(s(x205),x) = t can be joined as follows.
s ↔ s(+(x205,x)) ↔ t
The critical peak s = s(+(x205,x))←→_ε +(s(x205),x) = t can be joined as follows.
s ↔ s(+(x,x205)) ↔ t
The critical peak s = s(+(y,x))←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ s(+(y,x)) ↔ t
The critical peak s = s(+(y,x))←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(x209,s(x)))←→_ε s(+(x,s(x209))) = t can be joined as follows.
s ↔ s(s(+(x209,x))) ↔ t
The critical peak s = s(+(x209,s(x)))←→_ε s(+(x,s(x209))) = t can be joined as follows.
s ↔ s(s(+(x,x209))) ↔ t
The critical peak s = s(+(x211,x))←→_ε +(x,s(x211)) = t can be joined as follows.
s ↔ s(+(x211,x)) ↔ t
The critical peak s = s(+(x211,x))←→_ε +(x,s(x211)) = t can be joined as follows.
s ↔ s(+(x,x211)) ↔ t
The critical peak s = s(+(x213,s(x)))←→_ε s(+(s(x213),x)) = t can be joined as follows.
s ↔ s(s(+(x213,x))) ↔ t
The critical peak s = s(+(x213,s(x)))←→_ε s(+(s(x213),x)) = t can be joined as follows.
s ↔ s(s(+(x,x213))) ↔ t
The critical peak s = s(+(y,x214))←→_ε +(y,s(x214)) = t can be joined as follows.
s ↔ s(+(y,x214)) ↔ t
The critical peak s = s(+(y,x214))←→_ε +(y,s(x214)) = t can be joined as follows.
s ↔ s(+(x214,y)) ↔ t
The critical peak s = s(+(s(y),x216))←→_ε s(+(s(x216),y)) = t can be joined as follows.
s ↔ s(s(+(y,x216))) ↔ t
The critical peak s = s(+(s(y),x216))←→_ε s(+(s(x216),y)) = t can be joined as follows.
s ↔ s(s(+(x216,y))) ↔ t
The critical peak s = s(+(y,x))←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ s(+(y,x)) ↔ t
The critical peak s = s(+(y,x))←→_ε s(+(x,y)) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(y,x220))←→_ε +(s(x220),y) = t can be joined as follows.
s ↔ s(+(y,x220)) ↔ t
The critical peak s = s(+(y,x220))←→_ε +(s(x220),y) = t can be joined as follows.
s ↔ s(+(x220,y)) ↔ t
The critical peak s = s(+(s(y),x222))←→_ε s(+(y,s(x222))) = t can be joined as follows.
s ↔ s(s(+(y,x222))) ↔ t
The critical peak s = s(+(s(y),x222))←→_ε s(+(y,s(x222))) = t can be joined as follows.
s ↔ s(s(+(x222,y))) ↔ t