NO Non-Confluence Proof

Non-Confluence Proof

by ACP

Input

The rewrite relation of the following TRS is considered.

The system is not confluent due to the following forking derivations.

t₀ = a

→_ε f(a)

→₁ f(b)

= t₂

t₀ = a

→_ε b

= t₁

The two resulting terms cannot be joined for the following reason:

We take the usable rules of the first term (w.r.t. the TRS for the first term) and the usable rules of the second term (w.r.t. the TRS for the second term). Then the terms are not joinable w.r.t. the resulting TRSs.
The first mentioned term is different (not smaller than) the second one w.r.t. the following interpretation. Moreover, the (reversed) rules are (quasi)-models of the interpretation. The following interpretations form a model of the rules.
As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):

[b] = 1

[f(x₁)] = 1 + 1x₁

ACP

[b]	=	1
[f(x₁)]	=	1 + 1x₁