Certification Problem

Input (TPDB TRS_Standard/SK90/4.20)

The rewrite relation of the following TRS is considered.

not(x) → xor(x,true) (1)
or(x,y) → xor(and(x,y),xor(x,y)) (2)
implies(x,y) → xor(and(x,y),xor(x,true)) (3)
and(x,true) → x (4)
and(x,false) → false (5)
and(x,x) → x (6)
xor(x,false) → x (7)
xor(x,x) → false (8)
and(xor(x,y),z) → xor(and(x,z),and(y,z)) (9)

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(false) = 0 status(false) = [] list-extension(false) = Lex
prec(implies) = 4 status(implies) = [2, 1] list-extension(implies) = Lex
prec(and) = 1 status(and) = [2, 1] list-extension(and) = Lex
prec(or) = 0 status(or) = [2, 1] list-extension(or) = Lex
prec(xor) = 0 status(xor) = [2, 1] list-extension(xor) = Lex
prec(true) = 0 status(true) = [] list-extension(true) = Lex
prec(not) = 0 status(not) = [1] list-extension(not) = Lex
and the following Max-polynomial interpretation
[false] = max(0)
[implies(x1, x2)] = max(1, 6 + 1 · x1, 0 + 1 · x2)
[and(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[or(x1, x2)] = max(0, 1 + 1 · x1, 2 + 1 · x2)
[xor(x1, x2)] = max(1, 0 + 1 · x1, 0 + 1 · x2)
[true] = max(6)
[not(x1)] = max(7, 1 + 1 · x1)
all of the following rules can be deleted.
not(x) → xor(x,true) (1)
or(x,y) → xor(and(x,y),xor(x,y)) (2)
implies(x,y) → xor(and(x,y),xor(x,true)) (3)
and(x,true) → x (4)
and(x,false) → false (5)
and(x,x) → x (6)
xor(x,false) → x (7)
xor(x,x) → false (8)
and(xor(x,y),z) → xor(and(x,z),and(y,z)) (9)

1.1 R is empty

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