Certification Problem

Input (TPDB TRS_Relative/Mixed_relative_TRS/rt-rw4)

The relative rewrite relation R/S is considered where R is the following TRS

RAo(R) → R (1)
RAn(R) → R (2)
WAo(W) → W (3)
WAn(W) → W (4)

and S is the following TRS.

check(RIn(x)) → RIn(check(x)) (5)
WIn(ok(x)) → ok(WIn(x)) (6)
sys_w(ok(x),y) → ok(sys_w(x,y)) (7)
check(WAn(x)) → WAn(check(x)) (8)
check(RIo(x)) → ok(RIo(x)) (9)
top(ok(sys_w(read(r,RIo(x)),write(W,Ww)))) → top(check(sys_w(read(RAo(r),x),write(W,Ww)))) (10)
check(sys_r(x,y)) → sys_r(check(x),y) (11)
check(sys_w(x,y)) → sys_w(x,check(y)) (12)
top(ok(sys_w(read(R,x),write(W,WIn(y))))) → top(check(sys_r(read(R,x),write(WAn(W),y)))) (13)
top(ok(sys_w(read(r,RIn(x)),write(W,Ww)))) → top(check(sys_w(read(RAn(r),x),write(W,Ww)))) (14)
top(ok(sys_r(read(R,Rw),write(W,WIn(y))))) → top(check(sys_r(read(R,Rw),write(WAn(W),y)))) (15)
top(ok(sys_w(read(R,x),write(W,WIo(y))))) → top(check(sys_r(read(R,x),write(WAo(W),y)))) (16)
sys_r(ok(x),y) → ok(sys_r(x,y)) (17)
check(WIn(x)) → WIn(check(x)) (18)
top(ok(sys_w(read(R,Rw),write(W,WIn(y))))) → top(check(sys_w(read(R,Rw),write(WAn(W),y)))) (19)
top(ok(sys_r(read(r,RIo(x)),write(W,y)))) → top(check(sys_w(read(RAo(r),x),write(W,y)))) (20)
WAo(ok(x)) → ok(WAo(x)) (21)
top(ok(sys_r(read(r,RIn(x)),write(W,y)))) → top(check(sys_w(read(RAn(r),x),write(W,y)))) (22)
check(sys_w(x,y)) → sys_w(check(x),y) (23)
top(ok(sys_w(read(R,Rw),write(W,WIo(y))))) → top(check(sys_w(read(R,Rw),write(WAo(W),y)))) (24)
RIn(ok(x)) → ok(RIn(x)) (25)
top(ok(sys_r(read(r,RIn(x)),write(W,Ww)))) → top(check(sys_r(read(RAn(r),x),write(W,Ww)))) (26)
top(ok(sys_r(read(R,Rw),write(W,WIo(y))))) → top(check(sys_r(read(R,Rw),write(WAo(W),y)))) (27)
check(WIo(x)) → WIo(check(x)) (28)
sys_r(x,ok(y)) → ok(sys_r(x,y)) (29)
sys_w(x,ok(y)) → ok(sys_w(x,y)) (30)
check(RAn(x)) → RAn(check(x)) (31)
check(sys_r(x,y)) → sys_r(x,check(y)) (32)
RAn(ok(x)) → ok(RAn(x)) (33)
check(WAo(x)) → WAo(check(x)) (34)
check(RIo(x)) → RIo(check(x)) (35)
WIo(ok(x)) → ok(WIo(x)) (36)
WAn(ok(x)) → ok(WAn(x)) (37)
Rw → RIn(Rw) (38)
Ww → WIn(Ww) (39)
top(ok(sys_r(read(r,RIo(x)),write(W,Ww)))) → top(check(sys_r(read(RAo(r),x),write(W,Ww)))) (40)
check(RAo(x)) → RAo(check(x)) (41)
RAo(ok(x)) → ok(RAo(x)) (42)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[RAo(x1)] = 1 · x1
[R] = 0
[RAn(x1)] = 1 · x1
[WAo(x1)] = 1 · x1
[W] = 0
[WAn(x1)] = 1 · x1
[check(x1)] = 1 · x1
[RIn(x1)] = 1 · x1
[WIn(x1)] = 1 · x1
[ok(x1)] = 1 · x1
[sys_w(x1, x2)] = 1 · x1 + 1 · x2
[RIo(x1)] = 1 + 1 · x1
[top(x1)] = 1 · x1
[read(x1, x2)] = 1 · x1 + 1 · x2
[write(x1, x2)] = 1 · x1 + 1 · x2
[Ww] = 0
[sys_r(x1, x2)] = 1 · x1 + 1 · x2
[Rw] = 0
[WIo(x1)] = 1 + 1 · x1
all of the following rules can be deleted.
top(ok(sys_w(read(r,RIo(x)),write(W,Ww)))) → top(check(sys_w(read(RAo(r),x),write(W,Ww)))) (10)
top(ok(sys_w(read(R,x),write(W,WIo(y))))) → top(check(sys_r(read(R,x),write(WAo(W),y)))) (16)
top(ok(sys_r(read(r,RIo(x)),write(W,y)))) → top(check(sys_w(read(RAo(r),x),write(W,y)))) (20)
top(ok(sys_w(read(R,Rw),write(W,WIo(y))))) → top(check(sys_w(read(R,Rw),write(WAo(W),y)))) (24)
top(ok(sys_r(read(R,Rw),write(W,WIo(y))))) → top(check(sys_r(read(R,Rw),write(WAo(W),y)))) (27)
top(ok(sys_r(read(r,RIo(x)),write(W,Ww)))) → top(check(sys_r(read(RAo(r),x),write(W,Ww)))) (40)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[RAo(x1)] = 1 + 1 · x1
[R] = 0
[RAn(x1)] = 1 · x1
[WAo(x1)] = 1 · x1
[W] = 0
[WAn(x1)] = 1 · x1
[check(x1)] = 1 · x1
[RIn(x1)] = 1 · x1
[WIn(x1)] = 1 · x1
[ok(x1)] = 1 · x1
[sys_w(x1, x2)] = 1 + 1 · x1 + 1 · x2
[RIo(x1)] = 1 · x1
[sys_r(x1, x2)] = 1 + 1 · x1 + 1 · x2
[top(x1)] = 1 · x1
[read(x1, x2)] = 1 · x1 + 1 · x2
[write(x1, x2)] = 1 · x1 + 1 · x2
[Ww] = 0
[Rw] = 0
[WIo(x1)] = 1 · x1
all of the following rules can be deleted.
RAo(R) → R (1)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[RAn(x1)] = 1 · x1
[R] = 0
[WAo(x1)] = 1 + 1 · x1
[W] = 0
[WAn(x1)] = 1 · x1
[check(x1)] = 1 + 1 · x1
[RIn(x1)] = 1 · x1
[WIn(x1)] = 1 · x1
[ok(x1)] = 1 + 1 · x1
[sys_w(x1, x2)] = 1 + 1 · x1 + 1 · x2
[RIo(x1)] = 1 · x1
[sys_r(x1, x2)] = 1 + 1 · x1 + 1 · x2
[top(x1)] = 1 · x1
[read(x1, x2)] = 1 · x1 + 1 · x2
[write(x1, x2)] = 1 · x1 + 1 · x2
[Ww] = 0
[Rw] = 0
[WIo(x1)] = 1 · x1
[RAo(x1)] = 1 · x1
all of the following rules can be deleted.
WAo(W) → W (3)

1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 1
· x1
[R] =
0
0
[WAn(x1)] =
0
0
+
1 0
0 1
· x1
[W] =
0
0
[check(x1)] =
0
0
+
1 1
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[WIn(x1)] =
0
0
+
1 0
0 1
· x1
[ok(x1)] =
0
0
+
1 0
0 0
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[RIo(x1)] =
0
0
+
1 0
0 1
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2
[Ww] =
0
0
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
0
0
+
1 0
0 1
· x1
[RAo(x1)] =
1
1
+
1 0
0 1
· x1
all of the following rules can be deleted.
check(RAo(x)) → RAo(check(x)) (41)

1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 1
· x1
[R] =
0
0
[WAn(x1)] =
0
0
+
1 0
0 1
· x1
[W] =
0
0
[check(x1)] =
0
0
+
1 0
1 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[WIn(x1)] =
0
0
+
1 0
0 1
· x1
[ok(x1)] =
0
1
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[RIo(x1)] =
1
1
+
1 0
0 0
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2
[Ww] =
0
0
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
0
0
+
1 0
0 1
· x1
[RAo(x1)] =
1
0
+
1 1
1 1
· x1
all of the following rules can be deleted.
RAo(ok(x)) → ok(RAo(x)) (42)

1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 1
· x1
[R] =
0
0
[WAn(x1)] =
0
0
+
1 0
0 1
· x1
[W] =
0
0
[check(x1)] =
0
0
+
1 1
1 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[WIn(x1)] =
0
0
+
1 1
1 1
· x1
[ok(x1)] =
0
1
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[RIo(x1)] =
1
0
+
1 0
0 1
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2
[Ww] =
0
0
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
0
0
+
1 0
0 1
· x1
all of the following rules can be deleted.
WIn(ok(x)) → ok(WIn(x)) (6)

1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
1
+
1 0
0 1
· x1
[R] =
0
0
[WAn(x1)] =
0
0
+
1 0
0 1
· x1
[W] =
0
0
[check(x1)] =
0
0
+
1 1
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[ok(x1)] =
0
0
+
1 0
0 0
· x1
[RIo(x1)] =
0
0
+
1 0
0 1
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2
[WIn(x1)] =
0
0
+
1 0
0 1
· x1
[Ww] =
0
0
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
0
0
+
1 0
0 1
· x1
all of the following rules can be deleted.
check(RAn(x)) → RAn(check(x)) (31)

1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 1
· x1
[R] =
0
0
[WAn(x1)] =
0
0
+
1 0
0 1
· x1
[W] =
0
0
[check(x1)] =
0
1
+
1 1
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[ok(x1)] =
0
1
+
1 0
0 1
· x1
[RIo(x1)] =
0
0
+
1 0
0 1
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2
[WIn(x1)] =
0
0
+
1 0
0 1
· x1
[Ww] =
0
0
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
1
1
+
1 1
0 1
· x1
all of the following rules can be deleted.
WIo(ok(x)) → ok(WIo(x)) (36)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 1
· x1
[R] =
0
0
[WAn(x1)] =
0
0
+
1 0
0 1
· x1
[W] =
0
0
[check(x1)] =
0
0
+
1 1
1 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[ok(x1)] =
0
1
+
1 0
0 1
· x1
[RIo(x1)] =
1
0
+
1 0
0 1
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 1
1 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 1
1 1
· x1 +
1 1
0 0
· x2
[WIn(x1)] =
0
0
+
1 1
1 1
· x1
[Ww] =
0
0
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
0
0
+
1 1
1 1
· x1
all of the following rules can be deleted.
sys_r(x,ok(y)) → ok(sys_r(x,y)) (29)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 0
· x1
[R] =
0
0
[WAn(x1)] =
0
0
+
1 0
0 0
· x1
[W] =
0
0
[check(x1)] =
0
0
+
1 0
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 0
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[ok(x1)] =
0
0
+
1 1
0 0
· x1
[RIo(x1)] =
0
0
+
1 0
0 0
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 0
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 1
· x2
[write(x1, x2)] =
0
0
+
1 1
1 1
· x1 +
1 1
0 0
· x2
[WIn(x1)] =
0
0
+
1 1
0 1
· x1
[Ww] =
0
0
[Rw] =
0
1
[WAo(x1)] =
0
0
+
1 0
0 0
· x1
[WIo(x1)] =
0
0
+
1 1
1 1
· x1
all of the following rules can be deleted.
top(ok(sys_r(read(R,Rw),write(W,WIn(y))))) → top(check(sys_r(read(R,Rw),write(WAn(W),y)))) (15)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 0
· x1
[R] =
0
0
[WAn(x1)] =
0
1
+
1 0
0 1
· x1
[W] =
0
0
[check(x1)] =
0
0
+
1 1
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[ok(x1)] =
0
0
+
1 0
0 0
· x1
[RIo(x1)] =
0
0
+
1 0
0 1
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2
[WIn(x1)] =
0
0
+
1 0
0 1
· x1
[Ww] =
0
0
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
0
0
+
1 1
0 1
· x1
all of the following rules can be deleted.
check(WAn(x)) → WAn(check(x)) (8)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 1
· x1
[R] =
0
0
[WAn(x1)] =
0
0
+
1 1
0 1
· x1
[W] =
0
0
[check(x1)] =
0
1
+
1 0
1 1
· x1
[RIn(x1)] =
0
0
+
1 0
1 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[ok(x1)] =
0
1
+
1 0
0 1
· x1
[RIo(x1)] =
1
0
+
1 0
0 0
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 0
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 1
0 0
· x2
[write(x1, x2)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2
[WIn(x1)] =
0
0
+
1 0
0 0
· x1
[Ww] =
0
0
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
0
0
+
1 0
1 0
· x1
all of the following rules can be deleted.
WAn(ok(x)) → ok(WAn(x)) (37)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 1
· x1
[R] =
0
1
[WAn(x1)] =
0
0
+
1 1
1 1
· x1
[W] =
0
0
[check(x1)] =
0
0
+
1 0
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 0
· x1
[sys_w(x1, x2)] =
0
0
+
1 1
0 0
· x1 +
1 0
0 0
· x2
[ok(x1)] =
0
0
+
1 1
0 0
· x1
[RIo(x1)] =
0
0
+
1 0
0 0
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 0
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
1 1
· x1 +
1 0
1 0
· x2
[write(x1, x2)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2
[WIn(x1)] =
0
0
+
1 0
0 0
· x1
[Ww] =
0
0
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 0
· x1
[WIo(x1)] =
0
0
+
1 1
1 1
· x1
all of the following rules can be deleted.
top(ok(sys_w(read(R,x),write(W,WIn(y))))) → top(check(sys_r(read(R,x),write(WAn(W),y)))) (13)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[RAn(x1)] = 1 · x1
[R] = 0
[WAn(x1)] = 1 · x1
[W] = 0
[check(x1)] = 1 · x1
[RIn(x1)] = 1 · x1
[sys_w(x1, x2)] = 1 · x1 + 1 · x2
[ok(x1)] = 1 · x1
[RIo(x1)] = 1 · x1
[sys_r(x1, x2)] = 1 + 1 · x1 + 1 · x2
[top(x1)] = 1 · x1
[read(x1, x2)] = 1 · x1 + 1 · x2
[write(x1, x2)] = 1 · x1 + 1 · x2
[Ww] = 0
[WIn(x1)] = 1 · x1
[Rw] = 0
[WAo(x1)] = 1 · x1
[WIo(x1)] = 1 · x1
all of the following rules can be deleted.
top(ok(sys_r(read(r,RIn(x)),write(W,y)))) → top(check(sys_w(read(RAn(r),x),write(W,y)))) (22)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
1
+
1 0
0 0
· x1
[R] =
0
0
[WAn(x1)] =
1
0
+
1 1
1 1
· x1
[W] =
0
0
[check(x1)] =
0
0
+
1 0
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[ok(x1)] =
0
1
+
1 0
0 0
· x1
[RIo(x1)] =
0
1
+
1 0
0 0
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 0
· x2
[top(x1)] =
0
0
+
1 1
0 0
· x1
[read(x1, x2)] =
0
0
+
1 1
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 1
0 1
· x1 +
1 0
0 0
· x2
[Ww] =
0
0
[WIn(x1)] =
0
0
+
1 0
0 0
· x1
[Rw] =
0
0
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
0
0
+
1 1
1 1
· x1
all of the following rules can be deleted.
WAn(W) → W (4)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 0
· x1
[R] =
0
0
[check(x1)] =
0
0
+
1 0
0 0
· x1
[RIn(x1)] =
0
0
+
1 0
0 0
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 1
0 0
· x2
[ok(x1)] =
0
0
+
1 0
0 1
· x1
[RIo(x1)] =
0
0
+
1 0
0 0
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 0
1 1
· x1 +
1 0
0 0
· x2
[W] =
0
1
[Ww] =
0
0
[WIn(x1)] =
0
0
+
1 0
0 0
· x1
[Rw] =
0
0
[WAn(x1)] =
0
0
+
1 0
1 0
· x1
[WAo(x1)] =
0
0
+
1 0
0 0
· x1
[WIo(x1)] =
0
0
+
1 1
0 1
· x1
all of the following rules can be deleted.
top(ok(sys_w(read(R,Rw),write(W,WIn(y))))) → top(check(sys_w(read(R,Rw),write(WAn(W),y)))) (19)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 0
· x1
[R] =
0
0
[check(x1)] =
0
0
+
1 1
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[ok(x1)] =
0
0
+
1 0
0 0
· x1
[RIo(x1)] =
0
0
+
1 0
0 1
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 0
1 0
· x1 +
1 1
1 1
· x2
[W] =
0
1
[Ww] =
0
0
[WIn(x1)] =
0
0
+
1 1
0 1
· x1
[WAo(x1)] =
0
0
+
1 0
0 1
· x1
[WIo(x1)] =
0
1
+
1 1
0 1
· x1
[Rw] =
0
1
all of the following rules can be deleted.
check(WIo(x)) → WIo(check(x)) (28)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 0
· x1
[R] =
0
0
[check(x1)] =
0
0
+
1 1
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[ok(x1)] =
0
0
+
1 0
0 0
· x1
[RIo(x1)] =
0
0
+
1 0
0 1
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 0
1 0
· x1 +
1 1
1 1
· x2
[W] =
0
1
[Ww] =
0
0
[WIn(x1)] =
0
0
+
1 1
0 1
· x1
[WAo(x1)] =
1
1
+
1 0
0 1
· x1
[Rw] =
1
1
all of the following rules can be deleted.
check(WAo(x)) → WAo(check(x)) (34)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[RAn(x1)] =
0
0
+
1 0
0 0
· x1
[R] =
0
0
[check(x1)] =
0
1
+
1 1
0 1
· x1
[RIn(x1)] =
0
0
+
1 0
0 1
· x1
[sys_w(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[ok(x1)] =
0
0
+
1 0
0 0
· x1
[RIo(x1)] =
1
1
+
1 1
0 1
· x1
[sys_r(x1, x2)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 1
· x2
[top(x1)] =
0
0
+
1 0
0 0
· x1
[read(x1, x2)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[write(x1, x2)] =
0
0
+
1 0
1 0
· x1 +
1 0
1 0
· x2
[W] =
0
1
[Ww] =
0
1
[WIn(x1)] =
0
0
+
1 0
0 1
· x1
[WAo(x1)] =
0
0
+
1 0
1 1
· x1
[Rw] =
0
1
all of the following rules can be deleted.
check(RIo(x)) → ok(RIo(x)) (9)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[RAn(x1)] = 1 + 1 · x1
[R] = 0
[check(x1)] = 1 · x1
[RIn(x1)] = 1 · x1
[sys_w(x1, x2)] = 1 · x1 + 1 · x2
[ok(x1)] = 1 + 1 · x1
[sys_r(x1, x2)] = 1 · x1 + 1 · x2
[top(x1)] = 1 · x1
[read(x1, x2)] = 1 · x1 + 1 · x2
[write(x1, x2)] = 1 · x1 + 1 · x2
[W] = 0
[Ww] = 0
[WIn(x1)] = 1 · x1
[WAo(x1)] = 1 · x1
[RIo(x1)] = 1 · x1
[Rw] = 0
all of the following rules can be deleted.
RAn(R) → R (2)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

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