YES Confluence Proof

Confluence Proof

by ACP

Input

The rewrite relation of the following TRS is considered.

+(+(x,y),z) +(x,+(y,z))
+(x,+(y,z)) +(+(x,y),z)
+(x,y) +(y,x)

Proof

1 Strongly closed

Confluence is proven since the TRS is strongly closed. The joins can be performed within 12 step(s).

Tool configuration

ACP