Certification Problem

Input (COPS 583)

We consider the TRS containing the following rules:

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

The underlying signature is as follows:

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

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2022)

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(+(y,x))	(2)
+(0,y)	→	y	(1)

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

1.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(+(y,x))	(2)
+(0,y)	→	y	(1)
+(y,0)	→	y	(5)
+(y,s(x))	→	s(+(y,x))	(6)
+(y,s(x31))	→	s(+(y,x31))	(7)

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

1.1.1 Decreasing Diagrams

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

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(+(y,x)) = t can be joined as follows.
s ↔ t
The critical peak s = +(y,0)←→_ε y = t can be joined as follows.
s ↔ t
The critical peak s = +(0,y)←→_ε y = 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 ↔ t
The critical peak s = +(s(x31),y)←→_ε s(+(y,x31)) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(y,x154))←→_ε +(y,s(x154)) = t can be joined as follows.
s ↔ s(+(y,x154)) ↔ t
The critical peak s = s(+(0,x156))←→_ε s(x156) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(s(x),x158))←→_ε s(+(s(x158),x)) = t can be joined as follows.
s ↔ s(s(+(x158,x))) ↔ s(s(+(x,x158))) ↔ t
The critical peak s = s(+(s(x),x158))←→_ε s(+(s(x158),x)) = t can be joined as follows.
s ↔ s(+(x158,s(x))) ↔ s(s(+(x158,x))) ↔ s(s(+(x,x158))) ↔ t
The critical peak s = s(+(s(x),x158))←→_ε s(+(s(x158),x)) = t can be joined as follows.
s ↔ s(s(+(x158,x))) ↔ s(s(+(x,x158))) ↔ t
The critical peak s = s(+(s(x),x158))←→_ε s(+(s(x158),x)) = t can be joined as follows.
s ↔ s(s(+(x158,x))) ↔ s(s(+(x,x158))) ↔ s(+(x,s(x158))) ↔ t
The critical peak s = s(+(s(x31),x160))←→_ε s(+(s(x160),x31)) = t can be joined as follows.
s ↔ s(s(+(x160,x31))) ↔ s(s(+(x31,x160))) ↔ t
The critical peak s = s(+(s(x31),x160))←→_ε s(+(s(x160),x31)) = t can be joined as follows.
s ↔ s(+(x160,s(x31))) ↔ s(s(+(x160,x31))) ↔ s(s(+(x31,x160))) ↔ t
The critical peak s = s(+(s(x31),x160))←→_ε s(+(s(x160),x31)) = t can be joined as follows.
s ↔ s(s(+(x160,x31))) ↔ s(s(+(x31,x160))) ↔ t
The critical peak s = s(+(s(x31),x160))←→_ε s(+(s(x160),x31)) = t can be joined as follows.
s ↔ s(s(+(x160,x31))) ↔ s(s(+(x31,x160))) ↔ s(+(x31,s(x160))) ↔ 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(+(0,x)) = t can be joined as follows.
s ↔ s(x) ↔ t
The critical peak s = s(x31)←→_ε s(+(0,x31)) = t can be joined as follows.
s ↔ s(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(+(0,x)) = 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 = s(+(x,x170))←→_ε +(s(x170),x) = t can be joined as follows.
s ↔ s(+(x,x170)) ↔ t
The critical peak s = s(+(s(x),x172))←→_ε s(+(s(x172),x)) = t can be joined as follows.
s ↔ s(s(+(x172,x))) ↔ s(s(+(x,x172))) ↔ t
The critical peak s = s(+(s(x),x172))←→_ε s(+(s(x172),x)) = t can be joined as follows.
s ↔ s(+(x172,s(x))) ↔ s(s(+(x172,x))) ↔ s(s(+(x,x172))) ↔ t
The critical peak s = s(+(s(x),x172))←→_ε s(+(s(x172),x)) = t can be joined as follows.
s ↔ s(s(+(x172,x))) ↔ s(s(+(x,x172))) ↔ t
The critical peak s = s(+(s(x),x172))←→_ε s(+(s(x172),x)) = t can be joined as follows.
s ↔ s(s(+(x172,x))) ↔ s(s(+(x,x172))) ↔ s(+(x,s(x172))) ↔ t
The critical peak s = s(+(0,x174))←→_ε s(x174) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(x,x176))←→_ε +(s(x176),x) = t can be joined as follows.
s ↔ s(+(x,x176)) ↔ t
The critical peak s = s(+(s(x),x178))←→_ε s(+(s(x178),x)) = t can be joined as follows.
s ↔ s(s(+(x178,x))) ↔ s(s(+(x,x178))) ↔ t
The critical peak s = s(+(s(x),x178))←→_ε s(+(s(x178),x)) = t can be joined as follows.
s ↔ s(+(x178,s(x))) ↔ s(s(+(x178,x))) ↔ s(s(+(x,x178))) ↔ t
The critical peak s = s(+(s(x),x178))←→_ε s(+(s(x178),x)) = t can be joined as follows.
s ↔ s(s(+(x178,x))) ↔ s(s(+(x,x178))) ↔ t
The critical peak s = s(+(s(x),x178))←→_ε s(+(s(x178),x)) = t can be joined as follows.
s ↔ s(s(+(x178,x))) ↔ s(s(+(x,x178))) ↔ s(+(x,s(x178))) ↔ t
The critical peak s = s(+(0,x180))←→_ε s(x180) = t can be joined as follows.
s ↔ t