YES Confluence Proof

Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

+(0,y) y
+(s(x),y) s(+(x,y))
+(x,0) x
+(x,s(y)) s(+(x,y))

Proof

1 Compositional Parallel Critical Pair Systems

All parallel critical pairs of the TRS R are joinable by R. This can be seen as follows: The parallel critical pairs can be joined as follows. Here, ↔ is always chosen as an appropriate rewrite relation which is automatically inferred by the certifier.
The TRS C is chosen as:

There are no rules.

Consequently, PCPS(R,C) is included in the following TRS P where steps are used to show that certain pairs are C-convertible.
+(0,s(x0_2)) s(+(0,x0_2))
+(0,s(x0_2)) s(x0_2)
+(s(y1),0) s(y1)
+(s(y1),0) s(+(y1,0))
+(s(y1),s(x0_2)) s(+(s(y1),x0_2))
+(s(y1),s(x0_2)) s(+(y1,s(x0_2)))
+(s(x0_1),0) s(+(x0_1,0))
+(s(x0_1),0) s(x0_1)
+(0,s(y2)) s(y2)
+(0,s(y2)) s(+(0,y2))
+(s(x0_1),s(y2)) s(+(x0_1,s(y2)))
+(s(x0_1),s(y2)) s(+(s(x0_1),y2))

Relative termination of P / R is proven as follows.

1.1 Rule Removal

Using the recursive path order with the following precedence and status
prec(+) = 1 stat(+) = lex
prec(s) = 0 stat(s) = lex
prec(0) = 0 stat(0) = lex
all rules of R could be removed. Moreover, all rules of S could be removed.

1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S is relative terminating.


Confluence of C is proven as follows.

1.2 (Weakly) Orthogonal

Confluence is proven since the TRS is (weakly) orthogonal.

Tool configuration

Hakusan