NO Non-Confluence Proof

Non-Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

0(0(0(1(2(1(1(1(0(0(1(0(1(x)))))))))))))	→	0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x)))))))))))))))))
0(0(1(0(0(1(1(1(0(1(2(0(1(x)))))))))))))	→	0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x)))))))))))))))))
0(0(1(0(1(0(1(0(0(1(0(2(0(x)))))))))))))	→	0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x)))))))))))))))))
0(0(1(1(1(1(1(2(1(1(2(1(1(x)))))))))))))	→	0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x)))))))))))))))))
0(1(0(2(0(2(1(0(0(1(0(1(1(x)))))))))))))	→	0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x)))))))))))))))))
0(1(0(2(2(1(1(2(1(2(2(0(1(x)))))))))))))	→	0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x)))))))))))))))))
0(1(1(0(1(1(0(1(0(2(1(0(0(x)))))))))))))	→	0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x)))))))))))))))))
0(1(1(1(2(1(2(0(1(2(1(0(1(x)))))))))))))	→	0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x)))))))))))))))))
0(2(0(0(1(1(2(0(1(0(1(0(2(x)))))))))))))	→	0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x)))))))))))))))))
1(0(2(0(0(2(0(1(2(0(1(0(1(x)))))))))))))	→	1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x)))))))))))))))))
1(0(2(0(2(1(0(2(0(1(1(2(0(x)))))))))))))	→	1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x)))))))))))))))))
1(1(0(0(2(2(2(0(1(2(0(1(1(x)))))))))))))	→	1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x)))))))))))))))))
1(2(0(1(0(2(0(1(0(1(2(1(0(x)))))))))))))	→	1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x)))))))))))))))))
1(2(1(2(0(0(0(1(1(1(0(0(1(x)))))))))))))	→	1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x)))))))))))))))))
2(0(0(0(2(2(0(2(2(0(1(0(1(x)))))))))))))	→	2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x)))))))))))))))))
2(0(2(1(0(0(1(0(0(0(1(1(1(x)))))))))))))	→	0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x)))))))))))))))))
2(0(2(1(1(1(1(0(2(0(1(0(1(x)))))))))))))	→	2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x)))))))))))))))))
2(1(2(2(1(1(2(2(0(1(1(0(1(x)))))))))))))	→	2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x)))))))))))))))))
2(2(1(1(1(1(0(1(1(2(0(1(0(x)))))))))))))	→	0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x)))))))))))))))))

Proof

1 Non-Joinable Fork

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

t₀ = 0(0(0(1(2(1(1(1(0(0(1(0(1(0(1(0(0(1(0(2(0(x1)))))))))))))))))))))

→_{1.1.1.1.1.1.1.1} 0(0(0(1(2(1(1(1(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x1)))))))))))))))))))))))))

= t₁

t₀ = 0(0(0(1(2(1(1(1(0(0(1(0(1(0(1(0(0(1(0(2(0(x1)))))))))))))))))))))

→_ε 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(0(1(0(0(1(0(2(0(x1)))))))))))))))))))))))))

= t₁

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

When applying the cap-function on both terms (where variables may be treated like constants) then the resulting terms do not unify.

Tool configuration

Hakusan

version: 0.10

t₀	=	0(0(0(1(2(1(1(1(0(0(1(0(1(0(1(0(0(1(0(2(0(x1)))))))))))))))))))))
	→_{1.1.1.1.1.1.1.1}	0(0(0(1(2(1(1(1(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x1)))))))))))))))))))))))))
	=	t₁

t₀	=	0(0(0(1(2(1(1(1(0(0(1(0(1(0(1(0(0(1(0(2(0(x1)))))))))))))))))))))
	→_ε	0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(0(1(0(0(1(0(2(0(x1)))))))))))))))))))))))))
	=	t₁