NO Non-Confluence Proof

Non-Confluence Proof

by csi

Input

The rewrite relation of the following TRS is considered.

not(true) → false
not(false) → true
or(true,y) → true
or(x,true) → true
or(false,false) → false
and(true,true) → true
and(x,true) → x
and(true,y) → y
and(false,false) → false
not(and(x,y)) → or(not(x),not(y))
not(or(x,y)) → and(not(x),not(y))

Proof

1 Non-Joinable Fork

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

t0 = not(or(true,y))
→1 not(true)
→ε false
= t2

t0 = not(or(true,y))
→ε and(not(true),not(y))
→1 and(false,not(y))
= t2

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

Tool configuration

csi