Certification Problem

Input (TPDB TRS_Standard/SK90/2.40)

The rewrite relation of the following TRS is considered.

or(true,y) → true (1)
or(x,true) → true (2)
or(false,false) → false (3)
mem(x,nil) → false (4)
mem(x,set(y)) → =(x,y) (5)
mem(x,union(y,z)) → or(mem(x,y),mem(x,z)) (6)

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

1.1 R is empty

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