Certification Problem

Input (COPS 131)

We consider the TRS containing the following rules:

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