Certification Problem

Input (TPDB TRS_Standard/CiME_04/boolean_rings)

The rewrite relation of the following TRS is considered.

xor(x,F)	→	x	(1)
xor(x,neg(x))	→	F	(2)
and(x,T)	→	x	(3)
and(x,F)	→	F	(4)
and(x,x)	→	x	(5)
and(xor(x,y),z)	→	xor(and(x,z),and(y,z))	(6)
xor(x,x)	→	F	(7)
impl(x,y)	→	xor(and(x,y),xor(x,T))	(8)
or(x,y)	→	xor(and(x,y),xor(x,y))	(9)
equiv(x,y)	→	xor(x,xor(y,T))	(10)
neg(x)	→	xor(x,T)	(11)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

and^#(xor(x,y),z)	→	and^#(x,z)	(12)
or^#(x,y)	→	xor^#(x,y)	(13)
equiv^#(x,y)	→	xor^#(y,T)	(14)
impl^#(x,y)	→	and^#(x,y)	(15)
impl^#(x,y)	→	xor^#(x,T)	(16)
neg^#(x)	→	xor^#(x,T)	(17)
impl^#(x,y)	→	xor^#(and(x,y),xor(x,T))	(18)
or^#(x,y)	→	and^#(x,y)	(19)
and^#(xor(x,y),z)	→	and^#(y,z)	(20)
and^#(xor(x,y),z)	→	xor^#(and(x,z),and(y,z))	(21)
equiv^#(x,y)	→	xor^#(x,xor(y,T))	(22)
or^#(x,y)	→	xor^#(and(x,y),xor(x,y))	(23)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

and^#(xor(x,y),z)	→	and^#(y,z)	(20)
and^#(xor(x,y),z)	→	and^#(x,z)	(12)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[T]	=	0
[F]	=	0
[and(x₁, x₂)]	=	0
[impl^#(x₁, x₂)]	=	0
[equiv(x₁, x₂)]	=	0
[or(x₁, x₂)]	=	0
[neg(x₁)]	=	0
[impl(x₁, x₂)]	=	0
[xor^#(x₁, x₂)]	=	0
[equiv^#(x₁, x₂)]	=	0
[or^#(x₁, x₂)]	=	0
[neg^#(x₁)]	=	0
[xor(x₁, x₂)]	=	x₁ + x₂ + 1
[and^#(x₁, x₂)]	=	x₁ + 0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

and^#(xor(x,y),z)	→	and^#(y,z)	(20)
and^#(xor(x,y),z)	→	and^#(x,z)	(12)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.