Termination proof of rt-rw4.trs

Termination of the given RelTRS could be proven:

0 RelTRS

↳1 RelTRSRRRProof (⇔, 102 ms)

↳2 RelTRS

↳3 RelTRSRRRProof (⇔, 11 ms)

↳4 RelTRS

↳5 RelTRSRRRProof (⇔, 189 ms)

↳6 RelTRS

↳7 RelTRSRRRProof (⇔, 302 ms)

↳8 RelTRS

↳9 RelTRSRRRProof (⇔, 131 ms)

↳10 RelTRS

↳11 RelTRSRRRProof (⇔, 115 ms)

↳12 RelTRS

↳13 RelTRSRRRProof (⇔, 523 ms)

↳14 RelTRS

↳15 RelTRSRRRProof (⇔, 0 ms)

↳16 RelTRS

↳17 RelTRSRRRProof (⇔, 70 ms)

↳18 RelTRS

↳19 RelTRSRRRProof (⇔, 0 ms)

↳20 RelTRS

↳21 RIsEmptyProof (⇔, 0 ms)

↳22 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

RAo(R) → R
RAn(R) → R
WAo(W) → W
WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
top(ok(sys_w(read(r, RIo(x)), write(W, Ww)))) → top(check(sys_w(read(RAo(r), x), write(W, Ww))))
check(sys_r(x, y)) → sys_r(check(x), y)
check(sys_w(x, y)) → sys_w(x, check(y))
top(ok(sys_w(read(R, x), write(W, WIn(y))))) → top(check(sys_r(read(R, x), write(WAn(W), y))))
top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_w(read(RAn(r), x), write(W, Ww))))
top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))
top(ok(sys_w(read(R, x), write(W, WIo(y))))) → top(check(sys_r(read(R, x), write(WAo(W), y))))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) → top(check(sys_w(read(R, Rw), write(WAn(W), y))))
top(ok(sys_r(read(r, RIo(x)), write(W, y)))) → top(check(sys_w(read(RAo(r), x), write(W, y))))
WAo(ok(x)) → ok(WAo(x))
top(ok(sys_r(read(r, RIn(x)), write(W, y)))) → top(check(sys_w(read(RAn(r), x), write(W, y))))
check(sys_w(x, y)) → sys_w(check(x), y)
top(ok(sys_w(read(R, Rw), write(W, WIo(y))))) → top(check(sys_w(read(R, Rw), write(WAo(W), y))))
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
top(ok(sys_r(read(R, Rw), write(W, WIo(y))))) → top(check(sys_r(read(R, Rw), write(WAo(W), y))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
check(RAn(x)) → RAn(check(x))
check(sys_r(x, y)) → sys_r(x, check(y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
check(RIo(x)) → RIo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)
top(ok(sys_r(read(r, RIo(x)), write(W, Ww)))) → top(check(sys_r(read(RAo(r), x), write(W, Ww))))
check(RAo(x)) → RAo(check(x))
RAo(ok(x)) → ok(RAo(x))

(1) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(R) = 0
POL(RAn(x₁)) = x₁
POL(RAo(x₁)) = x₁
POL(RIn(x₁)) = x₁
POL(RIo(x₁)) = 1 + x₁
POL(Rw) = 0
POL(W) = 0
POL(WAn(x₁)) = x₁
POL(WAo(x₁)) = x₁
POL(WIn(x₁)) = x₁
POL(WIo(x₁)) = 1 + x₁
POL(Ww) = 0
POL(check(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(read(x₁, x₂)) = x₁ + x₂
POL(sys_r(x₁, x₂)) = x₁ + x₂
POL(sys_w(x₁, x₂)) = x₁ + x₂
POL(top(x₁)) = x₁
POL(write(x₁, x₂)) = x₁ + x₂

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
none
Rules from S:

top(ok(sys_w(read(r, RIo(x)), write(W, Ww)))) → top(check(sys_w(read(RAo(r), x), write(W, Ww))))
top(ok(sys_w(read(R, x), write(W, WIo(y))))) → top(check(sys_r(read(R, x), write(WAo(W), y))))
top(ok(sys_r(read(r, RIo(x)), write(W, y)))) → top(check(sys_w(read(RAo(r), x), write(W, y))))
top(ok(sys_w(read(R, Rw), write(W, WIo(y))))) → top(check(sys_w(read(R, Rw), write(WAo(W), y))))
top(ok(sys_r(read(R, Rw), write(W, WIo(y))))) → top(check(sys_r(read(R, Rw), write(WAo(W), y))))
top(ok(sys_r(read(r, RIo(x)), write(W, Ww)))) → top(check(sys_r(read(RAo(r), x), write(W, Ww))))

(2) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

RAo(R) → R
RAn(R) → R
WAo(W) → W
WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_r(x, y)) → sys_r(check(x), y)
check(sys_w(x, y)) → sys_w(x, check(y))
top(ok(sys_w(read(R, x), write(W, WIn(y))))) → top(check(sys_r(read(R, x), write(WAn(W), y))))
top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_w(read(RAn(r), x), write(W, Ww))))
top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) → top(check(sys_w(read(R, Rw), write(WAn(W), y))))
WAo(ok(x)) → ok(WAo(x))
top(ok(sys_r(read(r, RIn(x)), write(W, y)))) → top(check(sys_w(read(RAn(r), x), write(W, y))))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
check(RAn(x)) → RAn(check(x))
check(sys_r(x, y)) → sys_r(x, check(y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
check(RIo(x)) → RIo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)
check(RAo(x)) → RAo(check(x))
RAo(ok(x)) → ok(RAo(x))

(3) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(R) = 0
POL(RAn(x₁)) = x₁
POL(RAo(x₁)) = 1 + x₁
POL(RIn(x₁)) = x₁
POL(RIo(x₁)) = x₁
POL(Rw) = 0
POL(W) = 0
POL(WAn(x₁)) = x₁
POL(WAo(x₁)) = 1 + x₁
POL(WIn(x₁)) = x₁
POL(WIo(x₁)) = x₁
POL(Ww) = 0
POL(check(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(read(x₁, x₂)) = x₁ + x₂
POL(sys_r(x₁, x₂)) = x₁ + x₂
POL(sys_w(x₁, x₂)) = x₁ + x₂
POL(top(x₁)) = x₁
POL(write(x₁, x₂)) = x₁ + x₂

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

RAo(R) → R
WAo(W) → W

Rules from S:
none

(4) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

RAn(R) → R
WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_r(x, y)) → sys_r(check(x), y)
check(sys_w(x, y)) → sys_w(x, check(y))
top(ok(sys_w(read(R, x), write(W, WIn(y))))) → top(check(sys_r(read(R, x), write(WAn(W), y))))
top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_w(read(RAn(r), x), write(W, Ww))))
top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) → top(check(sys_w(read(R, Rw), write(WAn(W), y))))
WAo(ok(x)) → ok(WAo(x))
top(ok(sys_r(read(r, RIn(x)), write(W, y)))) → top(check(sys_w(read(RAn(r), x), write(W, y))))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
check(RAn(x)) → RAn(check(x))
check(sys_r(x, y)) → sys_r(x, check(y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
check(RIo(x)) → RIo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)
check(RAo(x)) → RAo(check(x))
RAo(ok(x)) → ok(RAo(x))

(5) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(RAn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(R) =
/ 1 \

\ 1 /

POL(WAn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(W) =
/ 0 \

\ 1 /

POL(check(x₁)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 1 /

· x₁

POL(RIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(WIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(ok(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(sys_w(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁ +
/ 1 1 \

\ 0 1 /

· x₂

POL(RIo(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(sys_r(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 1 /

· x₁ +
/ 1 0 \

\ 0 1 /

· x₂

POL(top(x₁)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 1 0 /

· x₁

POL(read(x₁, x₂)) =
/ 0 \

\ 1 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(write(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂

POL(Ww) =
/ 1 \

\ 1 /

POL(Rw) =
/ 1 \

\ 0 /

POL(WAo(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(WIo(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(RAo(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
none
Rules from S:

check(RIo(x)) → RIo(check(x))

(6) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

RAn(R) → R
WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_r(x, y)) → sys_r(check(x), y)
check(sys_w(x, y)) → sys_w(x, check(y))
top(ok(sys_w(read(R, x), write(W, WIn(y))))) → top(check(sys_r(read(R, x), write(WAn(W), y))))
top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_w(read(RAn(r), x), write(W, Ww))))
top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) → top(check(sys_w(read(R, Rw), write(WAn(W), y))))
WAo(ok(x)) → ok(WAo(x))
top(ok(sys_r(read(r, RIn(x)), write(W, y)))) → top(check(sys_w(read(RAn(r), x), write(W, y))))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
check(RAn(x)) → RAn(check(x))
check(sys_r(x, y)) → sys_r(x, check(y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)
check(RAo(x)) → RAo(check(x))
RAo(ok(x)) → ok(RAo(x))

(7) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(RAn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(R) =
/ 1 \

\ 0 /

POL(WAn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(W) =
/ 1 \

\ 1 /

POL(check(x₁)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 1 /

· x₁

POL(RIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 1 /

· x₁

POL(WIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(ok(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(sys_w(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 1 /

· x₁ +
/ 1 1 \

\ 0 1 /

· x₂

POL(RIo(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(sys_r(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁ +
/ 1 0 \

\ 0 1 /

· x₂

POL(top(x₁)) =
/ 1 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁

POL(read(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂

POL(write(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 1 \

\ 1 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(Ww) =
/ 1 \

\ 1 /

POL(Rw) =
/ 1 \

\ 0 /

POL(WAo(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(WIo(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(RAo(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 0 1 /

· x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
none
Rules from S:

check(RAo(x)) → RAo(check(x))

(8) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

RAn(R) → R
WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_r(x, y)) → sys_r(check(x), y)
check(sys_w(x, y)) → sys_w(x, check(y))
top(ok(sys_w(read(R, x), write(W, WIn(y))))) → top(check(sys_r(read(R, x), write(WAn(W), y))))
top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_w(read(RAn(r), x), write(W, Ww))))
top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) → top(check(sys_w(read(R, Rw), write(WAn(W), y))))
WAo(ok(x)) → ok(WAo(x))
top(ok(sys_r(read(r, RIn(x)), write(W, y)))) → top(check(sys_w(read(RAn(r), x), write(W, y))))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
check(RAn(x)) → RAn(check(x))
check(sys_r(x, y)) → sys_r(x, check(y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)
RAo(ok(x)) → ok(RAo(x))

(9) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(RAn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(R) =
/ 1 \

\ 1 /

POL(WAn(x₁)) =
/ 0 \

\ 1 /

+
/ 1 0 \

\ 1 0 /

· x₁

POL(W) =
/ 1 \

\ 0 /

POL(check(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 1 1 /

· x₁

POL(RIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 1 0 /

· x₁

POL(WIn(x₁)) =
/ 0 \

\ 1 /

+
/ 1 0 \

\ 1 0 /

· x₁

POL(ok(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(sys_w(x₁, x₂)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 1 1 /

· x₁ +
/ 1 0 \

\ 1 1 /

· x₂

POL(RIo(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(sys_r(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 1 1 /

· x₁ +
/ 1 0 \

\ 1 1 /

· x₂

POL(top(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(read(x₁, x₂)) =
/ 1 \

\ 1 /

+
/ 1 1 \

\ 1 1 /

· x₁ +
/ 1 0 \

\ 1 1 /

· x₂

POL(write(x₁, x₂)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 1 1 /

· x₁ +
/ 1 0 \

\ 1 0 /

· x₂

POL(Ww) =
/ 0 \

\ 1 /

POL(Rw) =
/ 1 \

\ 1 /

POL(WAo(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 1 0 /

· x₁

POL(WIo(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(RAo(x₁)) =
/ 1 \

\ 0 /

+
/ 1 1 \

\ 1 0 /

· x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
none
Rules from S:

RAo(ok(x)) → ok(RAo(x))

(10) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

RAn(R) → R
WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_r(x, y)) → sys_r(check(x), y)
check(sys_w(x, y)) → sys_w(x, check(y))
top(ok(sys_w(read(R, x), write(W, WIn(y))))) → top(check(sys_r(read(R, x), write(WAn(W), y))))
top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_w(read(RAn(r), x), write(W, Ww))))
top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) → top(check(sys_w(read(R, Rw), write(WAn(W), y))))
WAo(ok(x)) → ok(WAo(x))
top(ok(sys_r(read(r, RIn(x)), write(W, y)))) → top(check(sys_w(read(RAn(r), x), write(W, y))))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
check(RAn(x)) → RAn(check(x))
check(sys_r(x, y)) → sys_r(x, check(y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)

(11) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(RAn(x₁)) =
/ 0 \

\ 1 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(R) =
/ 1 \

\ 1 /

POL(WAn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(W) =
/ 0 \

\ 1 /

POL(check(x₁)) =
/ 0 \

\ 1 /

+
/ 1 1 \

\ 0 1 /

· x₁

POL(RIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(WIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(ok(x₁)) =
/ 0 \

\ 1 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(sys_w(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁ +
/ 1 0 \

\ 0 1 /

· x₂

POL(RIo(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(sys_r(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁ +
/ 1 0 \

\ 0 1 /

· x₂

POL(top(x₁)) =
/ 1 \

\ 1 /

+
/ 1 1 \

\ 0 1 /

· x₁

POL(read(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(write(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(Ww) =
/ 0 \

\ 0 /

POL(Rw) =
/ 0 \

\ 1 /

POL(WAo(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(WIo(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
none
Rules from S:

check(RAn(x)) → RAn(check(x))

(12) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

RAn(R) → R
WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_r(x, y)) → sys_r(check(x), y)
check(sys_w(x, y)) → sys_w(x, check(y))
top(ok(sys_w(read(R, x), write(W, WIn(y))))) → top(check(sys_r(read(R, x), write(WAn(W), y))))
top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_w(read(RAn(r), x), write(W, Ww))))
top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) → top(check(sys_w(read(R, Rw), write(WAn(W), y))))
WAo(ok(x)) → ok(WAo(x))
top(ok(sys_r(read(r, RIn(x)), write(W, y)))) → top(check(sys_w(read(RAn(r), x), write(W, y))))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
check(sys_r(x, y)) → sys_r(x, check(y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)

(13) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(RAn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 1 1 /

· x₁

POL(R) =
/ 1 \

\ 1 /

POL(WAn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(W) =
/ 1 \

\ 1 /

POL(check(x₁)) =
/ 0 \

\ 1 /

+
/ 1 1 \

\ 0 1 /

· x₁

POL(RIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(WIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(ok(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(sys_w(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁ +
/ 1 0 \

\ 0 1 /

· x₂

POL(RIo(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(sys_r(x₁, x₂)) =
/ 0 \

\ 1 /

+
/ 1 0 \

\ 0 1 /

· x₁ +
/ 1 0 \

\ 0 1 /

· x₂

POL(top(x₁)) =
/ 1 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁

POL(read(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂

POL(write(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂

POL(Ww) =
/ 1 \

\ 1 /

POL(Rw) =
/ 0 \

\ 1 /

POL(WAo(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(WIo(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
none
Rules from S:

check(sys_r(x, y)) → sys_r(check(x), y)
top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_w(read(RAn(r), x), write(W, Ww))))
top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) → top(check(sys_w(read(R, Rw), write(WAn(W), y))))
top(ok(sys_r(read(r, RIn(x)), write(W, y)))) → top(check(sys_w(read(RAn(r), x), write(W, y))))
check(sys_r(x, y)) → sys_r(x, check(y))

(14) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

RAn(R) → R
WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_w(x, y)) → sys_w(x, check(y))
top(ok(sys_w(read(R, x), write(W, WIn(y))))) → top(check(sys_r(read(R, x), write(WAn(W), y))))
top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
WAo(ok(x)) → ok(WAo(x))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)

(15) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(R) = 0
POL(RAn(x₁)) = x₁
POL(RIn(x₁)) = x₁
POL(RIo(x₁)) = x₁
POL(Rw) = 0
POL(W) = 0
POL(WAn(x₁)) = x₁
POL(WAo(x₁)) = x₁
POL(WIn(x₁)) = x₁
POL(WIo(x₁)) = x₁
POL(Ww) = 0
POL(check(x₁)) = 1 + x₁
POL(ok(x₁)) = 1 + x₁
POL(read(x₁, x₂)) = x₁ + x₂
POL(sys_r(x₁, x₂)) = x₁ + x₂
POL(sys_w(x₁, x₂)) = 1 + x₁ + x₂
POL(top(x₁)) = x₁
POL(write(x₁, x₂)) = x₁ + x₂

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
none
Rules from S:

top(ok(sys_w(read(R, x), write(W, WIn(y))))) → top(check(sys_r(read(R, x), write(WAn(W), y))))

(16) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

RAn(R) → R
WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_w(x, y)) → sys_w(x, check(y))
top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
WAo(ok(x)) → ok(WAo(x))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)

(17) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(RAn(x₁)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(R) =
/ 0 \

\ 0 /

POL(WAn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(W) =
/ 1 \

\ 1 /

POL(check(x₁)) =
/ 0 \

\ 1 /

+
/ 1 0 \

\ 1 0 /

· x₁

POL(RIn(x₁)) =
/ 0 \

\ 1 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(WIn(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(ok(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(sys_w(x₁, x₂)) =
/ 1 \

\ 1 /

+
/ 1 0 \

\ 1 0 /

· x₁ +
/ 1 0 \

\ 1 0 /

· x₂

POL(RIo(x₁)) =
/ 0 \

\ 1 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(top(x₁)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 1 1 /

· x₁

POL(sys_r(x₁, x₂)) =
/ 0 \

\ 1 /

+
/ 1 0 \

\ 1 1 /

· x₁ +
/ 1 0 \

\ 1 1 /

· x₂

POL(read(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 1 0 /

· x₂

POL(Rw) =
/ 0 \

\ 1 /

POL(write(x₁, x₂)) =
/ 1 \

\ 1 /

+
/ 1 1 \

\ 1 1 /

· x₁ +
/ 1 1 \

\ 1 0 /

· x₂

POL(WAo(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(Ww) =
/ 1 \

\ 1 /

POL(WIo(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

RAn(R) → R

Rules from S:

top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) → top(check(sys_r(read(R, Rw), write(WAn(W), y))))

(18) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

WAn(W) → W

The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_w(x, y)) → sys_w(x, check(y))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
WAo(ok(x)) → ok(WAo(x))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)

(19) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(RAn(x₁)) = x₁
POL(RIn(x₁)) = x₁
POL(RIo(x₁)) = x₁
POL(Rw) = 0
POL(W) = 0
POL(WAn(x₁)) = 1 + x₁
POL(WAo(x₁)) = x₁
POL(WIn(x₁)) = x₁
POL(WIo(x₁)) = x₁
POL(Ww) = 0
POL(check(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(read(x₁, x₂)) = x₁ + x₂
POL(sys_r(x₁, x₂)) = x₁ + x₂
POL(sys_w(x₁, x₂)) = x₁ + x₂
POL(top(x₁)) = x₁
POL(write(x₁, x₂)) = x₁ + x₂

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

WAn(W) → W

Rules from S:
none

(20) Obligation:

Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:

check(RIn(x)) → RIn(check(x))
WIn(ok(x)) → ok(WIn(x))
sys_w(ok(x), y) → ok(sys_w(x, y))
check(WAn(x)) → WAn(check(x))
check(RIo(x)) → ok(RIo(x))
check(sys_w(x, y)) → sys_w(x, check(y))
sys_r(ok(x), y) → ok(sys_r(x, y))
check(WIn(x)) → WIn(check(x))
WAo(ok(x)) → ok(WAo(x))
check(sys_w(x, y)) → sys_w(check(x), y)
RIn(ok(x)) → ok(RIn(x))
top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) → top(check(sys_r(read(RAn(r), x), write(W, Ww))))
check(WIo(x)) → WIo(check(x))
sys_r(x, ok(y)) → ok(sys_r(x, y))
sys_w(x, ok(y)) → ok(sys_w(x, y))
RAn(ok(x)) → ok(RAn(x))
check(WAo(x)) → WAo(check(x))
WIo(ok(x)) → ok(WIo(x))
WAn(ok(x)) → ok(WAn(x))
Rw → RIn(Rw)
Ww → WIn(Ww)

(21) RIsEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(0) Obligation:

(1) RelTRSRRRProof (EQUIVALENT transformation)

(2) Obligation:

(3) RelTRSRRRProof (EQUIVALENT transformation)

(4) Obligation:

(5) RelTRSRRRProof (EQUIVALENT transformation)

(6) Obligation:

(7) RelTRSRRRProof (EQUIVALENT transformation)

(8) Obligation:

(9) RelTRSRRRProof (EQUIVALENT transformation)

(10) Obligation:

(11) RelTRSRRRProof (EQUIVALENT transformation)

(12) Obligation:

(13) RelTRSRRRProof (EQUIVALENT transformation)

(14) Obligation:

(15) RelTRSRRRProof (EQUIVALENT transformation)

(16) Obligation:

(17) RelTRSRRRProof (EQUIVALENT transformation)

(18) Obligation:

(19) RelTRSRRRProof (EQUIVALENT transformation)

(20) Obligation:

(21) RIsEmptyProof (EQUIVALENT transformation)

(22) YES