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 ttt2 @ termCOMP 2023)

1 Rule Removal

Using the Weighted Path Order with the following precedence and status
prec(equiv) = 1 status(equiv) = [2, 1] list-extension(equiv) = Lex
prec(or) = 0 status(or) = [2, 1] list-extension(or) = Lex
prec(impl) = 0 status(impl) = [2, 1] list-extension(impl) = Lex
prec(and) = 1 status(and) = [1, 2] list-extension(and) = Lex
prec(T) = 0 status(T) = [] list-extension(T) = Lex
prec(neg) = 0 status(neg) = [1] list-extension(neg) = Lex
prec(xor) = 0 status(xor) = [2, 1] list-extension(xor) = Lex
prec(F) = 0 status(F) = [] list-extension(F) = Lex
and the following Max-polynomial interpretation
[equiv(x1, x2)] = max(4, 1 + 1 · x1, 5 + 1 · x2)
[or(x1, x2)] = 7 + 1 · x1 + 1 · x2
[impl(x1, x2)] = 7 + 1 · x1 + 1 · x2
[and(x1, x2)] = 0 + 1 · x1 + 1 · x2
[T] = max(1)
[neg(x1)] = max(0, 2 + 1 · x1)
[xor(x1, x2)] = max(1, 1 + 1 · x1, 0 + 1 · x2)
[F] = max(0)
all of the following rules can be deleted.
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)

1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.