Certification Problem

Input (COPS 159)

We consider the TRS containing the following rules:

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

The underlying signature is as follows:

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

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2023)

1 Decreasing Diagrams

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,0) → x (1)
↦ 0
+(x,s(y)) → s(+(x,y)) (2)
↦ 1
+(0,y) → y (3)
↦ 0
+(s(x),y) → s(+(x,y)) (4)
↦ 0
inc(x) → s(x) (5)
↦ 0
+(x,y) → +(y,x) (6)
↦ 2
inc(+(x,y)) → +(inc(x),y) (7)
↦ 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 = 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 = x←→_ε +(0,x) = t can be joined as follows.
s ↔ x ↔ t
The critical peak s = inc(x)←→_ε +(inc(x),0) = t can be joined as follows.
s ↔ inc(x) ↔ t
The critical peak s = s(+(0,x139))←→_ε s(x139) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(s(x),x141))←→_ε s(+(x,s(x141))) = t can be joined as follows.
s ↔ s(s(+(x,x141))) ↔ t
The critical peak s = s(+(x,x143))←→_ε +(s(x143),x) = t can be joined as follows.
s ↔ s(+(x143,x)) ↔ t
The critical peak s = inc(s(+(x,x145)))←→_ε +(inc(x),s(x145)) = t can be joined as follows.
s ↔ s(s(+(x,x145))) ↔ s(+(s(x),x145)) ↔ s(+(inc(x),x145)) ↔ t
The critical peak s = inc(s(+(x,x145)))←→_ε +(inc(x),s(x145)) = t can be joined as follows.
s ↔ s(s(+(x,x145))) ↔ s(+(s(x),x145)) ↔ +(s(x),s(x145)) ↔ t
The critical peak s = inc(s(+(x,x145)))←→_ε +(inc(x),s(x145)) = t can be joined as follows.
s ↔ s(s(+(x,x145))) ↔ s(+(x,s(x145))) ↔ +(s(x),s(x145)) ↔ t
The critical peak s = inc(s(+(x,x145)))←→_ε +(inc(x),s(x145)) = t can be joined as follows.
s ↔ s(s(+(x,x145))) ↔ s(s(+(x145,x))) ↔ s(s(+(x,x145))) ↔ s(+(s(x),x145)) ↔ s(+(inc(x),x145)) ↔ t
The critical peak s = inc(s(+(x,x145)))←→_ε +(inc(x),s(x145)) = t can be joined as follows.
s ↔ s(s(+(x,x145))) ↔ s(s(+(x145,x))) ↔ s(s(+(x,x145))) ↔ s(+(s(x),x145)) ↔ +(s(x),s(x145)) ↔ t
The critical peak s = inc(s(+(x,x145)))←→_ε +(inc(x),s(x145)) = t can be joined as follows.
s ↔ s(s(+(x,x145))) ↔ s(s(+(x145,x))) ↔ s(s(+(x,x145))) ↔ s(+(x,s(x145))) ↔ +(s(x),s(x145)) ↔ t
The critical peak s = inc(s(+(x,x145)))←→_ε +(inc(x),s(x145)) = t can be joined as follows.
s ↔ inc(s(+(x145,x))) ↔ s(s(+(x145,x))) ↔ s(s(+(x,x145))) ↔ s(+(s(x),x145)) ↔ s(+(inc(x),x145)) ↔ t
The critical peak s = inc(s(+(x,x145)))←→_ε +(inc(x),s(x145)) = t can be joined as follows.
s ↔ inc(s(+(x145,x))) ↔ s(s(+(x145,x))) ↔ s(s(+(x,x145))) ↔ s(+(s(x),x145)) ↔ +(s(x),s(x145)) ↔ t
The critical peak s = inc(s(+(x,x145)))←→_ε +(inc(x),s(x145)) = t can be joined as follows.
s ↔ inc(s(+(x145,x))) ↔ s(s(+(x145,x))) ↔ s(s(+(x,x145))) ↔ s(+(x,s(x145))) ↔ +(s(x),s(x145)) ↔ t
The critical peak s = 0←→_ε 0 = t can be joined as follows.
s ↔ t
The critical peak s = s(y)←→_ε s(+(0,y)) = t can be joined as follows.
s ↔ s(y) ↔ t
The critical peak s = y←→_ε +(y,0) = t can be joined as follows.
s ↔ y ↔ t
The critical peak s = inc(y)←→_ε +(inc(0),y) = t can be joined as follows.
s ↔ s(y) ↔ s(+(0,y)) ↔ +(s(0),y) ↔ t
The critical peak s = s(+(x150,0))←→_ε s(x150) = t can be joined as follows.
s ↔ t
The critical peak s = s(+(x152,s(y)))←→_ε s(+(s(x152),y)) = t can be joined as follows.
s ↔ s(s(+(x152,y))) ↔ t
The critical peak s = s(+(x154,y))←→_ε +(y,s(x154)) = t can be joined as follows.
s ↔ s(+(y,x154)) ↔ t
The critical peak s = inc(s(+(x156,y)))←→_ε +(inc(s(x156)),y) = t can be joined as follows.
s ↔ s(s(+(x156,y))) ↔ s(+(s(x156),y)) ↔ +(s(s(x156)),y) ↔ t
The critical peak s = inc(s(+(x156,y)))←→_ε +(inc(s(x156)),y) = t can be joined as follows.
s ↔ s(s(+(x156,y))) ↔ s(s(+(y,x156))) ↔ s(s(+(x156,y))) ↔ s(+(s(x156),y)) ↔ +(s(s(x156)),y) ↔ t
The critical peak s = inc(s(+(x156,y)))←→_ε +(inc(s(x156)),y) = t can be joined as follows.
s ↔ inc(s(+(y,x156))) ↔ s(s(+(y,x156))) ↔ s(s(+(x156,y))) ↔ s(+(s(x156),y)) ↔ +(s(s(x156)),y) ↔ t
The critical peak s = s(+(x,y))←→_ε +(inc(x),y) = t can be joined as follows.
s ↔ s(+(x,y)) ↔ +(s(x),y) ↔ t
The critical peak s = +(0,x)←→_ε x = t can be joined as follows.
s ↔ 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 = +(y,0)←→_ε 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 = inc(+(y,x))←→_ε +(inc(x),y) = t can be joined as follows.
s ↔ s(+(y,x)) ↔ s(+(x,y)) ↔ +(s(x),y) ↔ t
The critical peak s = inc(+(y,x))←→_ε +(inc(x),y) = t can be joined as follows.
s ↔ inc(+(x,y)) ↔ s(+(x,y)) ↔ +(s(x),y) ↔ t
The critical peak s = inc(+(y,x))←→_ε +(inc(x),y) = t can be joined as follows.
s ↔ inc(+(x,y)) ↔ t
The critical peak s = +(inc(x169),x170)←→_ε s(+(x169,x170)) = t can be joined as follows.
s ↔ +(s(x169),x170) ↔ t