Certification Problem

Input (TPDB TRS_Standard/SK90/2.30)

The rewrite relation of the following TRS is considered.

not(x) → xor(x,true) (1)
implies(x,y) → xor(and(x,y),xor(x,true)) (2)
or(x,y) → xor(and(x,y),xor(x,y)) (3)
=(x,y) → xor(x,xor(y,true)) (4)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[and(x1, x2)] = 1 · x1 + 3 · x2 + 0
[true] = 0
[implies(x1, x2)] = 10 · x1 + 6 · x2 + 0
[or(x1, x2)] = 10 · x1 + 22 · x2 + 0
[not(x1)] = 2 · x1 + 0
[=(x1, x2)] = 2 · x1 + 8 · x2 + 1
[xor(x1, x2)] = 2 · x1 + 4 · x2 + 0
all of the following rules can be deleted.
=(x,y) → xor(x,xor(y,true)) (4)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[and(x1, x2)] = 1 · x1 + 10 · x2 + 0
[true] = 0
[implies(x1, x2)] = 2 · x1 + 10 · x2 + 0
[or(x1, x2)] = 2 · x1 + 11 · x2 + 1
[not(x1)] = 1 · x1 + 0
[xor(x1, x2)] = 1 · x1 + 1 · x2 + 0
all of the following rules can be deleted.
or(x,y) → xor(and(x,y),xor(x,y)) (3)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals
[and(x1, x2)] =
2 1
0 0
· x1 +
1 1
0 1
· x2 +
0 0
2 0
[true] =
0 0
1 0
[implies(x1, x2)] =
7 6
5 4
· x1 +
1 1
2 4
· x2 +
6 0
4 0
[not(x1)] =
4 4
2 2
· x1 +
5 0
0 0
[xor(x1, x2)] =
1 0
2 2
· x1 +
1 2
0 0
· x2 +
2 0
0 0
all of the following rules can be deleted.
not(x) → xor(x,true) (1)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[and(x1, x2)] = 2 · x1 + 8 · x2 + 0
[true] = 0
[implies(x1, x2)] = 12 · x1 + 18 · x2 + 2
[xor(x1, x2)] = 2 · x1 + 4 · x2 + 0
all of the following rules can be deleted.
implies(x,y) → xor(and(x,y),xor(x,true)) (2)

1.1.1.1.1 R is empty

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