YES Confluence Proof

Confluence Proof

by csi

Input

The rewrite relation of the following TRS is considered.

f(f(x,y),z) → f(x,f(y,z))
f(1,x) → x

Proof

1 Locally confluent and terminating

Confluence is proven by showing local confluence and termination.

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[1] = 7
[f(x1, x2)] = 1 · x1 + 1 · x2 + 0
the rule
f(f(x,y),z) → f(x,f(y,z))
remains.

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[f(x1, x2)] = 2 · x1 + 1 · x2 + 2
all rules could be removed.

1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.

1.2 Local Confluence Proof

All critical pairs are joinable which can be seen by computing normal forms of all critical pairs.

Tool configuration

csi