NO Non-Confluence Proof

Non-Confluence Proof

by ACP

Input

The rewrite relation of the following TRS is considered.

NUMERAL(0)	→	0
BIT0(0)	→	0
SUC(NUMERAL(n))	→	NUMERAL(SUC(n))
SUC(0)	→	BIT1(0)
SUC(BIT0(n))	→	BIT1(n)
SUC(BIT1(n))	→	BIT0(SUC(n))
PRE(NUMERAL(n))	→	NUMERAL(PRE(n))
PRE(0)	→	0
PRE(BIT0(n))	→	if(eq(n,0),0,BIT1(PRE(n)))
PRE(BIT1(n))	→	BIT0(n)
plus(NUMERAL(m),NUMERAL(n))	→	NUMERAL(plus(m,n))
plus(0,0)	→	0
plus(0,BIT0(n))	→	BIT0(n)
plus(0,BIT1(n))	→	BIT1(n)
plus(BIT0(n),0)	→	BIT0(n)
plus(BIT1(n),0)	→	BIT1(n)
plus(BIT0(m),BIT0(n))	→	BIT0(plus(m,n))
plus(BIT0(m),BIT1(n))	→	BIT1(plus(m,n))
plus(BIT1(m),BIT0(n))	→	BIT1(plus(m,n))
plus(BIT1(m),BIT1(n))	→	BIT0(SUC(plus(m,n)))
mult(NUMERAL(m),NUMERAL(n))	→	NUMERAL(mult(m,n))
mult(0,0)	→	0
mult(0,BIT0(n))	→	0
mult(0,BIT1(n))	→	0
mult(BIT0(n),0)	→	0
mult(BIT1(n),0)	→	0
mult(BIT0(m),BIT0(n))	→	BIT0(BIT0(mult(m,n)))
mult(BIT0(m),BIT1(n))	→	plus(BIT0(m),BIT0(BIT0(mult(m,n))))
mult(BIT1(m),BIT0(n))	→	plus(BIT0(n),BIT0(BIT0(mult(m,n))))
mult(BIT1(m),BIT1(n))	→	plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
exp(NUMERAL(m),NUMERAL(n))	→	NUMERAL(exp(m,n))
exp(0,0)	→	BIT1(0)
exp(BIT0(m),0)	→	BIT1(0)
exp(BIT1(m),0)	→	BIT1(0)
exp(0,BIT0(n))	→	mult(exp(0,n),exp(0,n))
exp(BIT0(m),BIT0(n))	→	mult(exp(BIT0(m),n),exp(BIT0(m),n))
exp(BIT1(m),BIT0(n))	→	mult(exp(BIT1(m),n),exp(BIT1(m),n))
exp(0,BIT1(n))	→	0
exp(BIT0(m),BIT1(n))	→	mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
exp(BIT1(m),BIT1(n))	→	mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
EVEN(NUMERAL(n))	→	EVEN(n)
EVEN(0)	→	T
EVEN(BIT0(n))	→	T
EVEN(BIT1(n))	→	F
ODD(NUMERAL(n))	→	ODD(n)
ODD(0)	→	F
ODD(BIT0(n))	→	F
ODD(BIT1(n))	→	T
eq(NUMERAL(m),NUMERAL(n))	→	eq(m,n)
eq(0,0)	→	T
eq(BIT0(n),0)	→	eq(n,0)
eq(BIT1(n),0)	→	F
eq(0,BIT0(n))	→	eq(0,n)
eq(0,BIT1(n))	→	F
eq(BIT0(m),BIT0(n))	→	eq(m,n)
eq(BIT0(m),BIT1(n))	→	F
eq(BIT1(m),BIT0(n))	→	F
eq(BIT1(m),BIT1(n))	→	eq(m,n)
le(NUMERAL(m),NUMERAL(n))	→	le(m,n)
le(0,0)	→	T
le(BIT0(n),0)	→	le(n,0)
le(BIT1(n),0)	→	F
le(0,BIT0(n))	→	T
le(0,BIT1(n))	→	T
le(BIT0(m),BIT0(n))	→	le(m,n)
le(BIT0(m),BIT1(n))	→	le(m,n)
le(BIT1(m),BIT0(n))	→	lt(m,n)
le(BIT1(m),BIT1(n))	→	le(m,n)
lt(NUMERAL(m),NUMERAL(n))	→	lt(m,n)
lt(0,0)	→	F
lt(BIT0(n),0)	→	F
lt(BIT1(n),0)	→	F
lt(0,BIT0(n))	→	lt(0,n)
lt(0,BIT1(n))	→	T
lt(BIT0(m),BIT0(n))	→	lt(m,n)
lt(BIT0(m),BIT1(n))	→	le(m,n)
lt(BIT1(m),BIT0(n))	→	lt(m,n)
lt(BIT1(m),BIT1(n))	→	lt(m,n)
ge(NUMERAL(n),NUMERAL(m))	→	ge(n,m)
ge(0,0)	→	T
ge(0,BIT0(n))	→	ge(0,n)
ge(0,BIT1(n))	→	F
ge(BIT0(n),0)	→	T
ge(BIT1(n),0)	→	T
ge(BIT0(n),BIT0(m))	→	ge(n,m)
ge(BIT1(n),BIT0(m))	→	ge(n,m)
ge(BIT0(n),BIT1(m))	→	gt(n,m)
ge(BIT1(n),BIT1(m))	→	ge(n,m)
gt(NUMERAL(n),NUMERAL(m))	→	gt(n,m)
gt(0,0)	→	F
gt(0,BIT0(n))	→	F
gt(0,BIT1(n))	→	F
gt(BIT0(n),0)	→	gt(n,0)
gt(BIT1(n),0)	→	T
gt(BIT0(n),BIT0(m))	→	gt(n,m)
gt(BIT1(n),BIT0(m))	→	ge(n,m)
gt(BIT0(n),BIT1(m))	→	gt(n,m)
gt(BIT1(n),BIT1(m))	→	gt(n,m)
minus(NUMERAL(m),NUMERAL(n))	→	NUMERAL(minus(m,n))
minus(0,0)	→	0
minus(0,BIT0(n))	→	0
minus(0,BIT1(n))	→	0
minus(BIT0(n),0)	→	BIT0(n)
minus(BIT1(n),0)	→	BIT1(n)
minus(BIT0(m),BIT0(n))	→	BIT0(minus(m,n))
minus(BIT0(m),BIT1(n))	→	PRE(BIT0(minus(m,n)))
minus(BIT1(m),BIT0(n))	→	if(le(n,m),BIT1(minus(m,n)),0)
minus(BIT1(m),BIT1(n))	→	BIT0(minus(m,n))

Proof

1 Non-Joinable Fork

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

t₀ = gt(BIT1(c_1),BIT0(0))

→_ε ge(c_1,0)

= t₁

t₀ = gt(BIT1(c_1),BIT0(0))

→₂ gt(BIT1(c_1),0)

→_ε T

= 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.
We filter all terms and rules w.r.t. the following argument filter.

π(0) = []

π(T) = []

π(ge) = [2]

π(c_1) = []

Then the resulting terms are not joinable w.r.t. the resulting TRSs.
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 strictly larger than the second one. Here, the following discrimination pair has been used w.r.t. the following interpretation. Moreover, the (reversed) rules are weakly decreasing. The discrimination pair is given by a recursive path order with the following precedence and status

prec(0)	=	4	stat(0)	=	mul
prec(c_1)	=	3	stat(c_1)	=	mul
prec(T)	=	2	stat(T)	=	mul
prec(ge)	=	1	stat(ge)	=	mul

Tool configuration

ACP

version: 0.72

π(0)	=	[]
π(T)	=	[]
π(ge)	=	[2]
π(c_1)	=	[]