YES Confluence Proof

Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

f(b) c
c c
f(c) b
a b

Proof

1 Compositional Rule Labeling with Parallel Critical Pairs

Confluence is proven by compositional rule labeling with parallel critical pairs.
The following labeling functions phi and psi are used (if only one is displayed, then phi = psi). The non-0-0 parallel critical pairs are joined as follows. The remaining rules are handled recursively.
f(b) c
c c
f(c) b

1.1 Compositional Rule Labeling with Parallel Critical Pairs

Confluence is proven by compositional rule labeling with parallel critical pairs.
The following labeling functions phi and psi are used (if only one is displayed, then phi = psi). The non-0-0 parallel critical pairs are joined as follows. The remaining rules are handled recursively.
f(b) c
f(c) b

1.1.1 Compositional Rule Labeling with Parallel Critical Pairs

Confluence is proven by compositional rule labeling with parallel critical pairs.
The following labeling functions phi and psi are used (if only one is displayed, then phi = psi). The non-0-0 parallel critical pairs are joined as follows. The remaining rules are handled recursively.

There are no rules.

1.1.1.1 (Weakly) Orthogonal

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

Tool configuration

Hakusan