YES Confluence Proof

Confluence Proof

by csi

Input

The rewrite relation of the following TRS is considered.

b(a(b(b(x)))) b(b(b(a(b(x)))))
b(a(a(b(b(x))))) b(a(b(b(a(a(b(x)))))))
b(a(a(a(b(b(x)))))) b(a(a(b(b(a(a(a(b(x)))))))))

Proof

1 Critical Pair Closing System

Confluence is proven using the following terminating critical-pair-closing-system R:

b(a(b(b(x)))) b(b(b(a(b(x)))))
b(a(a(b(b(x))))) b(a(b(b(a(a(b(x)))))))
b(a(a(a(b(b(x)))))) b(a(a(b(b(a(a(a(b(x)))))))))

1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
b(b(a(b(x)))) b(a(b(b(b(x)))))
b(b(a(a(b(x))))) b(a(a(b(b(a(b(x)))))))
b(b(a(a(a(b(x)))))) b(a(a(a(b(b(a(a(b(x)))))))))

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
b#(b(a(b(x)))) b#(b(x))
b#(b(a(b(x)))) b#(b(b(x)))
b#(b(a(b(x)))) b#(a(b(b(b(x)))))
b#(b(a(a(b(x))))) b#(a(b(x)))
b#(b(a(a(b(x))))) b#(b(a(b(x))))
b#(b(a(a(b(x))))) b#(a(a(b(b(a(b(x)))))))
b#(b(a(a(a(b(x)))))) b#(a(a(b(x))))
b#(b(a(a(a(b(x)))))) b#(b(a(a(b(x)))))
b#(b(a(a(a(b(x)))))) b#(a(a(a(b(b(a(a(b(x)))))))))

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

Tool configuration

csi