TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) Rw ->= RIn(Rw)
(2) Ww ->= WIn(Ww)
(3) RAo(R) -> R
(4) RAn(R) -> R
(5) WAo(W) -> W
(6) WAn(W) -> W
(7) top(ok(sys_r(read(r,RIo(x)),write(W,Ww)))) ->= top(check(sys_r(read(RAo(r),x),write(W,Ww))))
(8) top(ok(sys_w(read(r,RIo(x)),write(W,Ww)))) ->= top(check(sys_w(read(RAo(r),x),write(W,Ww))))
(9) top(ok(sys_r(read(r,RIn(x)),write(W,Ww)))) ->= top(check(sys_r(read(RAn(r),x),write(W,Ww))))
(10) top(ok(sys_w(read(r,RIn(x)),write(W,Ww)))) ->= top(check(sys_w(read(RAn(r),x),write(W,Ww))))
(11) top(ok(sys_r(read(R,Rw),write(W,WIn(y))))) ->= top(check(sys_r(read(R,Rw),write(WAn(W),y))))
(12) top(ok(sys_w(read(R,Rw),write(W,WIn(y))))) ->= top(check(sys_w(read(R,Rw),write(WAn(W),y))))
(13) top(ok(sys_r(read(R,Rw),write(W,WIo(y))))) ->= top(check(sys_r(read(R,Rw),write(WAo(W),y))))
(14) top(ok(sys_w(read(R,Rw),write(W,WIo(y))))) ->= top(check(sys_w(read(R,Rw),write(WAo(W),y))))
(15) top(ok(sys_r(read(r,RIo(x)),write(W,y)))) ->= top(check(sys_w(read(RAo(r),x),write(W,y))))
(16) top(ok(sys_r(read(r,RIn(x)),write(W,y)))) ->= top(check(sys_w(read(RAn(r),x),write(W,y))))
(17) top(ok(sys_w(read(R,x),write(W,WIo(y))))) ->= top(check(sys_r(read(R,x),write(WAo(W),y))))
(18) top(ok(sys_w(read(R,x),write(W,WIn(y))))) ->= top(check(sys_r(read(R,x),write(WAn(W),y))))
(19) check(RIo(x)) ->= ok(RIo(x))
(20) check(RAo(x)) ->= RAo(check(x))
(21) check(RAn(x)) ->= RAn(check(x))
(22) check(WAo(x)) ->= WAo(check(x))
(23) check(WAn(x)) ->= WAn(check(x))
(24) check(RIo(x)) ->= RIo(check(x))
(25) check(RIn(x)) ->= RIn(check(x))
(26) check(WIo(x)) ->= WIo(check(x))
(27) check(WIn(x)) ->= WIn(check(x))
(28) check(sys_r(x,y)) ->= sys_r(check(x),y)
(29) check(sys_r(x,y)) ->= sys_r(x,check(y))
(30) check(sys_w(x,y)) ->= sys_w(check(x),y)
(31) check(sys_w(x,y)) ->= sys_w(x,check(y))
(32) RAo(ok(x)) ->= ok(RAo(x))
(33) RAn(ok(x)) ->= ok(RAn(x))
(34) WAo(ok(x)) ->= ok(WAo(x))
(35) WAn(ok(x)) ->= ok(WAn(x))
(36) RIn(ok(x)) ->= ok(RIn(x))
(37) WIo(ok(x)) ->= ok(WIo(x))
(38) WIn(ok(x)) ->= ok(WIn(x))
(39) sys_r(ok(x),y) ->= ok(sys_r(x,y))
(40) sys_r(x,ok(y)) ->= ok(sys_r(x,y))
(41) sys_w(ok(x),y) ->= ok(sys_w(x,y))
(42) sys_w(x,ok(y)) ->= ok(sys_w(x,y))

[2]  Use following polynomial interpretation:
[WIo(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(13)-(14), (17)

[3]  Use following polynomial interpretation:
[RIo(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(7)-(8), (15)

[4]  Use following polynomial interpretation:
[WAo(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(5)

[5]  Use following polynomial interpretation:
[RAo(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(3)

[6]  Label this TRS using following interpretation that is a model:
[top(x)] = 0
[RIo(x)] = 1
rest default

  thus obtaining new TRS:
(1a) Rw ->= RIn$0(Rw)
(2a) Ww ->= WIn$0(Ww)
(4a) RAn$0(R) -> R
(6a) WAn$0(W) -> W
(9a) top$1(ok$1(sys_r$10(read$11(r,RIn$1(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_r$10(read$11(RAn$1(r),x),write$00(W,Ww))))
(9b) top$1(ok$1(sys_r$10(read$10(r,RIn$0(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_r$10(read$10(RAn$1(r),x),write$00(W,Ww))))
(9c) top$1(ok$1(sys_r$10(read$01(r,RIn$1(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_r$10(read$01(RAn$0(r),x),write$00(W,Ww))))
(9d) top$0(ok$0(sys_r$00(read$00(r,RIn$0(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_r$00(read$00(RAn$0(r),x),write$00(W,Ww))))
(10a) top$1(ok$1(sys_w$10(read$11(r,RIn$1(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_w$10(read$11(RAn$1(r),x),write$00(W,Ww))))
(10b) top$1(ok$1(sys_w$10(read$10(r,RIn$0(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_w$10(read$10(RAn$1(r),x),write$00(W,Ww))))
(10c) top$1(ok$1(sys_w$10(read$01(r,RIn$1(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_w$10(read$01(RAn$0(r),x),write$00(W,Ww))))
(10d) top$0(ok$0(sys_w$00(read$00(r,RIn$0(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_w$00(read$00(RAn$0(r),x),write$00(W,Ww))))
(11a) top$1(ok$1(sys_r$01(read$00(R,Rw),write$01(W,WIn$1(y))))) ->= top$1(check$1(sys_r$01(read$00(R,Rw),write$01(WAn$0(W),y))))
(11b) top$0(ok$0(sys_r$00(read$00(R,Rw),write$00(W,WIn$0(y))))) ->= top$0(check$0(sys_r$00(read$00(R,Rw),write$00(WAn$0(W),y))))
(12a) top$1(ok$1(sys_w$01(read$00(R,Rw),write$01(W,WIn$1(y))))) ->= top$1(check$1(sys_w$01(read$00(R,Rw),write$01(WAn$0(W),y))))
(12b) top$0(ok$0(sys_w$00(read$00(R,Rw),write$00(W,WIn$0(y))))) ->= top$0(check$0(sys_w$00(read$00(R,Rw),write$00(WAn$0(W),y))))
(16a) top$1(ok$1(sys_r$11(read$11(r,RIn$1(x)),write$01(W,y)))) ->= top$1(check$1(sys_w$11(read$11(RAn$1(r),x),write$01(W,y))))
(16b) top$1(ok$1(sys_r$10(read$11(r,RIn$1(x)),write$00(W,y)))) ->= top$1(check$1(sys_w$10(read$11(RAn$1(r),x),write$00(W,y))))
(16c) top$1(ok$1(sys_r$11(read$10(r,RIn$0(x)),write$01(W,y)))) ->= top$1(check$1(sys_w$11(read$10(RAn$1(r),x),write$01(W,y))))
(16d) top$1(ok$1(sys_r$10(read$10(r,RIn$0(x)),write$00(W,y)))) ->= top$1(check$1(sys_w$10(read$10(RAn$1(r),x),write$00(W,y))))
(16e) top$1(ok$1(sys_r$11(read$01(r,RIn$1(x)),write$01(W,y)))) ->= top$1(check$1(sys_w$11(read$01(RAn$0(r),x),write$01(W,y))))
(16f) top$1(ok$1(sys_r$10(read$01(r,RIn$1(x)),write$00(W,y)))) ->= top$1(check$1(sys_w$10(read$01(RAn$0(r),x),write$00(W,y))))
(16g) top$1(ok$1(sys_r$01(read$00(r,RIn$0(x)),write$01(W,y)))) ->= top$1(check$1(sys_w$01(read$00(RAn$0(r),x),write$01(W,y))))
(16h) top$0(ok$0(sys_r$00(read$00(r,RIn$0(x)),write$00(W,y)))) ->= top$0(check$0(sys_w$00(read$00(RAn$0(r),x),write$00(W,y))))
(18a) top$1(ok$1(sys_w$11(read$01(R,x),write$01(W,WIn$1(y))))) ->= top$1(check$1(sys_r$11(read$01(R,x),write$01(WAn$0(W),y))))
(18b) top$1(ok$1(sys_w$10(read$01(R,x),write$00(W,WIn$0(y))))) ->= top$1(check$1(sys_r$10(read$01(R,x),write$00(WAn$0(W),y))))
(18c) top$1(ok$1(sys_w$01(read$00(R,x),write$01(W,WIn$1(y))))) ->= top$1(check$1(sys_r$01(read$00(R,x),write$01(WAn$0(W),y))))
(18d) top$0(ok$0(sys_w$00(read$00(R,x),write$00(W,WIn$0(y))))) ->= top$0(check$0(sys_r$00(read$00(R,x),write$00(WAn$0(W),y))))
(19a) check$1(RIo$1(x)) ->= ok$1(RIo$1(x))
(19b) check$1(RIo$0(x)) ->= ok$1(RIo$0(x))
(20a) check$1(RAo$1(x)) ->= RAo$1(check$1(x))
(20b) check$0(RAo$0(x)) ->= RAo$0(check$0(x))
(21a) check$1(RAn$1(x)) ->= RAn$1(check$1(x))
(21b) check$0(RAn$0(x)) ->= RAn$0(check$0(x))
(22a) check$1(WAo$1(x)) ->= WAo$1(check$1(x))
(22b) check$0(WAo$0(x)) ->= WAo$0(check$0(x))
(23a) check$1(WAn$1(x)) ->= WAn$1(check$1(x))
(23b) check$0(WAn$0(x)) ->= WAn$0(check$0(x))
(24a) check$1(RIo$1(x)) ->= RIo$1(check$1(x))
(24b) check$1(RIo$0(x)) ->= RIo$0(check$0(x))
(25a) check$1(RIn$1(x)) ->= RIn$1(check$1(x))
(25b) check$0(RIn$0(x)) ->= RIn$0(check$0(x))
(26a) check$1(WIo$1(x)) ->= WIo$1(check$1(x))
(26b) check$0(WIo$0(x)) ->= WIo$0(check$0(x))
(27a) check$1(WIn$1(x)) ->= WIn$1(check$1(x))
(27b) check$0(WIn$0(x)) ->= WIn$0(check$0(x))
(28a) check$1(sys_r$11(x,y)) ->= sys_r$11(check$1(x),y)
(28b) check$1(sys_r$10(x,y)) ->= sys_r$10(check$1(x),y)
(28c) check$1(sys_r$01(x,y)) ->= sys_r$01(check$0(x),y)
(28d) check$0(sys_r$00(x,y)) ->= sys_r$00(check$0(x),y)
(29a) check$1(sys_r$11(x,y)) ->= sys_r$11(x,check$1(y))
(29b) check$1(sys_r$10(x,y)) ->= sys_r$10(x,check$0(y))
(29c) check$1(sys_r$01(x,y)) ->= sys_r$01(x,check$1(y))
(29d) check$0(sys_r$00(x,y)) ->= sys_r$00(x,check$0(y))
(30a) check$1(sys_w$11(x,y)) ->= sys_w$11(check$1(x),y)
(30b) check$1(sys_w$10(x,y)) ->= sys_w$10(check$1(x),y)
(30c) check$1(sys_w$01(x,y)) ->= sys_w$01(check$0(x),y)
(30d) check$0(sys_w$00(x,y)) ->= sys_w$00(check$0(x),y)
(31a) check$1(sys_w$11(x,y)) ->= sys_w$11(x,check$1(y))
(31b) check$1(sys_w$10(x,y)) ->= sys_w$10(x,check$0(y))
(31c) check$1(sys_w$01(x,y)) ->= sys_w$01(x,check$1(y))
(31d) check$0(sys_w$00(x,y)) ->= sys_w$00(x,check$0(y))
(32a) RAo$1(ok$1(x)) ->= ok$1(RAo$1(x))
(32b) RAo$0(ok$0(x)) ->= ok$0(RAo$0(x))
(33a) RAn$1(ok$1(x)) ->= ok$1(RAn$1(x))
(33b) RAn$0(ok$0(x)) ->= ok$0(RAn$0(x))
(34a) WAo$1(ok$1(x)) ->= ok$1(WAo$1(x))
(34b) WAo$0(ok$0(x)) ->= ok$0(WAo$0(x))
(35a) WAn$1(ok$1(x)) ->= ok$1(WAn$1(x))
(35b) WAn$0(ok$0(x)) ->= ok$0(WAn$0(x))
(36a) RIn$1(ok$1(x)) ->= ok$1(RIn$1(x))
(36b) RIn$0(ok$0(x)) ->= ok$0(RIn$0(x))
(37a) WIo$1(ok$1(x)) ->= ok$1(WIo$1(x))
(37b) WIo$0(ok$0(x)) ->= ok$0(WIo$0(x))
(38a) WIn$1(ok$1(x)) ->= ok$1(WIn$1(x))
(38b) WIn$0(ok$0(x)) ->= ok$0(WIn$0(x))
(39a) sys_r$11(ok$1(x),y) ->= ok$1(sys_r$11(x,y))
(39b) sys_r$10(ok$1(x),y) ->= ok$1(sys_r$10(x,y))
(39c) sys_r$01(ok$0(x),y) ->= ok$1(sys_r$01(x,y))
(39d) sys_r$00(ok$0(x),y) ->= ok$0(sys_r$00(x,y))
(40a) sys_r$11(x,ok$1(y)) ->= ok$1(sys_r$11(x,y))
(40b) sys_r$10(x,ok$0(y)) ->= ok$1(sys_r$10(x,y))
(40c) sys_r$01(x,ok$1(y)) ->= ok$1(sys_r$01(x,y))
(40d) sys_r$00(x,ok$0(y)) ->= ok$0(sys_r$00(x,y))
(41a) sys_w$11(ok$1(x),y) ->= ok$1(sys_w$11(x,y))
(41b) sys_w$10(ok$1(x),y) ->= ok$1(sys_w$10(x,y))
(41c) sys_w$01(ok$0(x),y) ->= ok$1(sys_w$01(x,y))
(41d) sys_w$00(ok$0(x),y) ->= ok$0(sys_w$00(x,y))
(42a) sys_w$11(x,ok$1(y)) ->= ok$1(sys_w$11(x,y))
(42b) sys_w$10(x,ok$0(y)) ->= ok$1(sys_w$10(x,y))
(42c) sys_w$01(x,ok$1(y)) ->= ok$1(sys_w$01(x,y))
(42d) sys_w$00(x,ok$0(y)) ->= ok$0(sys_w$00(x,y))

[7]  Use following polynomial interpretation:
[WIn$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(11a), (12a), (18a), (18c)

[8]  Use following polynomial interpretation:
[sys_r$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(16g)

[9]  Use following polynomial interpretation:
[sys_r$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(16a), (16c), (16e)

[10]  Use following polynomial interpretation:
[ok$0(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(9d), (10d), (11b), (12b), (16h), (18d), (39c), (40b), (41c), (42b)

[11]  Unlabel this TRS to obtain the one consisting of the rules:
(1)-(2), (4), (6), (9)-(10), (16), (18)-(42)

[12]  Label this TRS using following interpretation that is a model:
[top(x)] = 0
[RIo(x)] = 1
rest default

  thus obtaining new TRS:
(1a) Rw ->= RIn$0(Rw)
(2a) Ww ->= WIn$0(Ww)
(4a) RAn$0(R) -> R
(6a) WAn$0(W) -> W
(9a) top$1(ok$1(sys_r$10(read$11(r,RIn$1(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_r$10(read$11(RAn$1(r),x),write$00(W,Ww))))
(9b) top$1(ok$1(sys_r$10(read$10(r,RIn$0(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_r$10(read$10(RAn$1(r),x),write$00(W,Ww))))
(9c) top$1(ok$1(sys_r$10(read$01(r,RIn$1(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_r$10(read$01(RAn$0(r),x),write$00(W,Ww))))
(9d) top$0(ok$0(sys_r$00(read$00(r,RIn$0(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_r$00(read$00(RAn$0(r),x),write$00(W,Ww))))
(10a) top$1(ok$1(sys_w$10(read$11(r,RIn$1(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_w$10(read$11(RAn$1(r),x),write$00(W,Ww))))
(10b) top$1(ok$1(sys_w$10(read$10(r,RIn$0(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_w$10(read$10(RAn$1(r),x),write$00(W,Ww))))
(10c) top$1(ok$1(sys_w$10(read$01(r,RIn$1(x)),write$00(W,Ww)))) ->= top$1(check$1(sys_w$10(read$01(RAn$0(r),x),write$00(W,Ww))))
(10d) top$0(ok$0(sys_w$00(read$00(r,RIn$0(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_w$00(read$00(RAn$0(r),x),write$00(W,Ww))))
(16a) top$1(ok$1(sys_r$11(read$11(r,RIn$1(x)),write$01(W,y)))) ->= top$1(check$1(sys_w$11(read$11(RAn$1(r),x),write$01(W,y))))
(16b) top$1(ok$1(sys_r$10(read$11(r,RIn$1(x)),write$00(W,y)))) ->= top$1(check$1(sys_w$10(read$11(RAn$1(r),x),write$00(W,y))))
(16c) top$1(ok$1(sys_r$11(read$10(r,RIn$0(x)),write$01(W,y)))) ->= top$1(check$1(sys_w$11(read$10(RAn$1(r),x),write$01(W,y))))
(16d) top$1(ok$1(sys_r$10(read$10(r,RIn$0(x)),write$00(W,y)))) ->= top$1(check$1(sys_w$10(read$10(RAn$1(r),x),write$00(W,y))))
(16e) top$1(ok$1(sys_r$11(read$01(r,RIn$1(x)),write$01(W,y)))) ->= top$1(check$1(sys_w$11(read$01(RAn$0(r),x),write$01(W,y))))
(16f) top$1(ok$1(sys_r$10(read$01(r,RIn$1(x)),write$00(W,y)))) ->= top$1(check$1(sys_w$10(read$01(RAn$0(r),x),write$00(W,y))))
(16g) top$1(ok$1(sys_r$01(read$00(r,RIn$0(x)),write$01(W,y)))) ->= top$1(check$1(sys_w$01(read$00(RAn$0(r),x),write$01(W,y))))
(16h) top$0(ok$0(sys_r$00(read$00(r,RIn$0(x)),write$00(W,y)))) ->= top$0(check$0(sys_w$00(read$00(RAn$0(r),x),write$00(W,y))))
(18a) top$1(ok$1(sys_w$11(read$01(R,x),write$01(W,WIn$1(y))))) ->= top$1(check$1(sys_r$11(read$01(R,x),write$01(WAn$0(W),y))))
(18b) top$1(ok$1(sys_w$10(read$01(R,x),write$00(W,WIn$0(y))))) ->= top$1(check$1(sys_r$10(read$01(R,x),write$00(WAn$0(W),y))))
(18c) top$1(ok$1(sys_w$01(read$00(R,x),write$01(W,WIn$1(y))))) ->= top$1(check$1(sys_r$01(read$00(R,x),write$01(WAn$0(W),y))))
(18d) top$0(ok$0(sys_w$00(read$00(R,x),write$00(W,WIn$0(y))))) ->= top$0(check$0(sys_r$00(read$00(R,x),write$00(WAn$0(W),y))))
(19a) check$1(RIo$1(x)) ->= ok$1(RIo$1(x))
(19b) check$1(RIo$0(x)) ->= ok$1(RIo$0(x))
(20a) check$1(RAo$1(x)) ->= RAo$1(check$1(x))
(20b) check$0(RAo$0(x)) ->= RAo$0(check$0(x))
(21a) check$1(RAn$1(x)) ->= RAn$1(check$1(x))
(21b) check$0(RAn$0(x)) ->= RAn$0(check$0(x))
(22a) check$1(WAo$1(x)) ->= WAo$1(check$1(x))
(22b) check$0(WAo$0(x)) ->= WAo$0(check$0(x))
(23a) check$1(WAn$1(x)) ->= WAn$1(check$1(x))
(23b) check$0(WAn$0(x)) ->= WAn$0(check$0(x))
(24a) check$1(RIo$1(x)) ->= RIo$1(check$1(x))
(24b) check$1(RIo$0(x)) ->= RIo$0(check$0(x))
(25a) check$1(RIn$1(x)) ->= RIn$1(check$1(x))
(25b) check$0(RIn$0(x)) ->= RIn$0(check$0(x))
(26a) check$1(WIo$1(x)) ->= WIo$1(check$1(x))
(26b) check$0(WIo$0(x)) ->= WIo$0(check$0(x))
(27a) check$1(WIn$1(x)) ->= WIn$1(check$1(x))
(27b) check$0(WIn$0(x)) ->= WIn$0(check$0(x))
(28a) check$1(sys_r$11(x,y)) ->= sys_r$11(check$1(x),y)
(28b) check$1(sys_r$10(x,y)) ->= sys_r$10(check$1(x),y)
(28c) check$1(sys_r$01(x,y)) ->= sys_r$01(check$0(x),y)
(28d) check$0(sys_r$00(x,y)) ->= sys_r$00(check$0(x),y)
(29a) check$1(sys_r$11(x,y)) ->= sys_r$11(x,check$1(y))
(29b) check$1(sys_r$10(x,y)) ->= sys_r$10(x,check$0(y))
(29c) check$1(sys_r$01(x,y)) ->= sys_r$01(x,check$1(y))
(29d) check$0(sys_r$00(x,y)) ->= sys_r$00(x,check$0(y))
(30a) check$1(sys_w$11(x,y)) ->= sys_w$11(check$1(x),y)
(30b) check$1(sys_w$10(x,y)) ->= sys_w$10(check$1(x),y)
(30c) check$1(sys_w$01(x,y)) ->= sys_w$01(check$0(x),y)
(30d) check$0(sys_w$00(x,y)) ->= sys_w$00(check$0(x),y)
(31a) check$1(sys_w$11(x,y)) ->= sys_w$11(x,check$1(y))
(31b) check$1(sys_w$10(x,y)) ->= sys_w$10(x,check$0(y))
(31c) check$1(sys_w$01(x,y)) ->= sys_w$01(x,check$1(y))
(31d) check$0(sys_w$00(x,y)) ->= sys_w$00(x,check$0(y))
(32a) RAo$1(ok$1(x)) ->= ok$1(RAo$1(x))
(32b) RAo$0(ok$0(x)) ->= ok$0(RAo$0(x))
(33a) RAn$1(ok$1(x)) ->= ok$1(RAn$1(x))
(33b) RAn$0(ok$0(x)) ->= ok$0(RAn$0(x))
(34a) WAo$1(ok$1(x)) ->= ok$1(WAo$1(x))
(34b) WAo$0(ok$0(x)) ->= ok$0(WAo$0(x))
(35a) WAn$1(ok$1(x)) ->= ok$1(WAn$1(x))
(35b) WAn$0(ok$0(x)) ->= ok$0(WAn$0(x))
(36a) RIn$1(ok$1(x)) ->= ok$1(RIn$1(x))
(36b) RIn$0(ok$0(x)) ->= ok$0(RIn$0(x))
(37a) WIo$1(ok$1(x)) ->= ok$1(WIo$1(x))
(37b) WIo$0(ok$0(x)) ->= ok$0(WIo$0(x))
(38a) WIn$1(ok$1(x)) ->= ok$1(WIn$1(x))
(38b) WIn$0(ok$0(x)) ->= ok$0(WIn$0(x))
(39a) sys_r$11(ok$1(x),y) ->= ok$1(sys_r$11(x,y))
(39b) sys_r$10(ok$1(x),y) ->= ok$1(sys_r$10(x,y))
(39c) sys_r$01(ok$0(x),y) ->= ok$1(sys_r$01(x,y))
(39d) sys_r$00(ok$0(x),y) ->= ok$0(sys_r$00(x,y))
(40a) sys_r$11(x,ok$1(y)) ->= ok$1(sys_r$11(x,y))
(40b) sys_r$10(x,ok$0(y)) ->= ok$1(sys_r$10(x,y))
(40c) sys_r$01(x,ok$1(y)) ->= ok$1(sys_r$01(x,y))
(40d) sys_r$00(x,ok$0(y)) ->= ok$0(sys_r$00(x,y))
(41a) sys_w$11(ok$1(x),y) ->= ok$1(sys_w$11(x,y))
(41b) sys_w$10(ok$1(x),y) ->= ok$1(sys_w$10(x,y))
(41c) sys_w$01(ok$0(x),y) ->= ok$1(sys_w$01(x,y))
(41d) sys_w$00(ok$0(x),y) ->= ok$0(sys_w$00(x,y))
(42a) sys_w$11(x,ok$1(y)) ->= ok$1(sys_w$11(x,y))
(42b) sys_w$10(x,ok$0(y)) ->= ok$1(sys_w$10(x,y))
(42c) sys_w$01(x,ok$1(y)) ->= ok$1(sys_w$01(x,y))
(42d) sys_w$00(x,ok$0(y)) ->= ok$0(sys_w$00(x,y))

[13]  Use following polynomial interpretation:
[WIn$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(18a), (18c)

[14]  Use following polynomial interpretation:
[sys_r$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(16g)

[15]  Use following polynomial interpretation:
[sys_r$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(16a), (16c), (16e)

[16]  Use following polynomial interpretation:
[ok$0(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(9d), (10d), (16h), (18d), (39c), (40b), (41c), (42b)

[17]  Use following polynomial interpretation:
[RIn$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(9a), (9c), (10a), (10c), (16b), (16f)

[18]  Use following polynomial interpretation:
[RAn$0(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(4a)

[19]  Unlabel this TRS to obtain the one consisting of the rules:
(1)-(2), (6), (9)-(10), (16), (18)-(42)

[20]  Label this TRS using following interpretation that is a model:
[RIn(x)] = 0
[WIn(x)] = 0
[RAo(x)] = 0
[R] = 1
[RAn(x)] = 0
[WAo(x)] = 0
[WAn(x)] = 0
[top(x)] = 0
[ok(x)] = 0
[sys_r(x,y)] = 0
[RIo(x)] = 0
[write(x,y)] = 0
[check(x)] = 0
[sys_w(x,y)] = 0
[WIo(x)] = 0
rest default

  thus obtaining new TRS:
(1a) Rw ->= RIn$0(Rw)
(2a) Ww ->= WIn$0(Ww)
(6a) WAn$0(W) -> W
(9a) top$0(ok$0(sys_r$10(read$10(r,RIn$1(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_r$10(read$01(RAn$1(r),x),write$00(W,Ww))))
(9b) top$0(ok$0(sys_r$10(read$10(r,RIn$0(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_r$00(read$00(RAn$1(r),x),write$00(W,Ww))))
(9c) top$0(ok$0(sys_r$00(read$00(r,RIn$1(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_r$10(read$01(RAn$0(r),x),write$00(W,Ww))))
(9d) top$0(ok$0(sys_r$00(read$00(r,RIn$0(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_r$00(read$00(RAn$0(r),x),write$00(W,Ww))))
(10a) top$0(ok$0(sys_w$10(read$10(r,RIn$1(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_w$10(read$01(RAn$1(r),x),write$00(W,Ww))))
(10b) top$0(ok$0(sys_w$10(read$10(r,RIn$0(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_w$00(read$00(RAn$1(r),x),write$00(W,Ww))))
(10c) top$0(ok$0(sys_w$00(read$00(r,RIn$1(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_w$10(read$01(RAn$0(r),x),write$00(W,Ww))))
(10d) top$0(ok$0(sys_w$00(read$00(r,RIn$0(x)),write$00(W,Ww)))) ->= top$0(check$0(sys_w$00(read$00(RAn$0(r),x),write$00(W,Ww))))
(16a) top$0(ok$0(sys_r$10(read$10(r,RIn$1(x)),write$01(W,y)))) ->= top$0(check$0(sys_w$10(read$01(RAn$1(r),x),write$01(W,y))))
(16b) top$0(ok$0(sys_r$10(read$10(r,RIn$1(x)),write$00(W,y)))) ->= top$0(check$0(sys_w$10(read$01(RAn$1(r),x),write$00(W,y))))
(16c) top$0(ok$0(sys_r$10(read$10(r,RIn$0(x)),write$01(W,y)))) ->= top$0(check$0(sys_w$00(read$00(RAn$1(r),x),write$01(W,y))))
(16d) top$0(ok$0(sys_r$10(read$10(r,RIn$0(x)),write$00(W,y)))) ->= top$0(check$0(sys_w$00(read$00(RAn$1(r),x),write$00(W,y))))
(16e) top$0(ok$0(sys_r$00(read$00(r,RIn$1(x)),write$01(W,y)))) ->= top$0(check$0(sys_w$10(read$01(RAn$0(r),x),write$01(W,y))))
(16f) top$0(ok$0(sys_r$00(read$00(r,RIn$1(x)),write$00(W,y)))) ->= top$0(check$0(sys_w$10(read$01(RAn$0(r),x),write$00(W,y))))
(16g) top$0(ok$0(sys_r$00(read$00(r,RIn$0(x)),write$01(W,y)))) ->= top$0(check$0(sys_w$00(read$00(RAn$0(r),x),write$01(W,y))))
(16h) top$0(ok$0(sys_r$00(read$00(r,RIn$0(x)),write$00(W,y)))) ->= top$0(check$0(sys_w$00(read$00(RAn$0(r),x),write$00(W,y))))
(18a) top$0(ok$0(sys_w$10(read$11(R,x),write$00(W,WIn$1(y))))) ->= top$0(check$0(sys_r$10(read$11(R,x),write$01(WAn$0(W),y))))
(18b) top$0(ok$0(sys_w$10(read$11(R,x),write$00(W,WIn$0(y))))) ->= top$0(check$0(sys_r$10(read$11(R,x),write$00(WAn$0(W),y))))
(18c) top$0(ok$0(sys_w$10(read$10(R,x),write$00(W,WIn$1(y))))) ->= top$0(check$0(sys_r$10(read$10(R,x),write$01(WAn$0(W),y))))
(18d) top$0(ok$0(sys_w$10(read$10(R,x),write$00(W,WIn$0(y))))) ->= top$0(check$0(sys_r$10(read$10(R,x),write$00(WAn$0(W),y))))
(19a) check$0(RIo$1(x)) ->= ok$0(RIo$1(x))
(19b) check$0(RIo$0(x)) ->= ok$0(RIo$0(x))
(20a) check$0(RAo$1(x)) ->= RAo$0(check$1(x))
(20b) check$0(RAo$0(x)) ->= RAo$0(check$0(x))
(21a) check$0(RAn$1(x)) ->= RAn$0(check$1(x))
(21b) check$0(RAn$0(x)) ->= RAn$0(check$0(x))
(22a) check$0(WAo$1(x)) ->= WAo$0(check$1(x))
(22b) check$0(WAo$0(x)) ->= WAo$0(check$0(x))
(23a) check$0(WAn$1(x)) ->= WAn$0(check$1(x))
(23b) check$0(WAn$0(x)) ->= WAn$0(check$0(x))
(24a) check$0(RIo$1(x)) ->= RIo$0(check$1(x))
(24b) check$0(RIo$0(x)) ->= RIo$0(check$0(x))
(25a) check$0(RIn$1(x)) ->= RIn$0(check$1(x))
(25b) check$0(RIn$0(x)) ->= RIn$0(check$0(x))
(26a) check$0(WIo$1(x)) ->= WIo$0(check$1(x))
(26b) check$0(WIo$0(x)) ->= WIo$0(check$0(x))
(27a) check$0(WIn$1(x)) ->= WIn$0(check$1(x))
(27b) check$0(WIn$0(x)) ->= WIn$0(check$0(x))
(28a) check$0(sys_r$11(x,y)) ->= sys_r$01(check$1(x),y)
(28b) check$0(sys_r$10(x,y)) ->= sys_r$00(check$1(x),y)
(28c) check$0(sys_r$01(x,y)) ->= sys_r$01(check$0(x),y)
(28d) check$0(sys_r$00(x,y)) ->= sys_r$00(check$0(x),y)
(29a) check$0(sys_r$11(x,y)) ->= sys_r$10(x,check$1(y))
(29b) check$0(sys_r$10(x,y)) ->= sys_r$10(x,check$0(y))
(29c) check$0(sys_r$01(x,y)) ->= sys_r$00(x,check$1(y))
(29d) check$0(sys_r$00(x,y)) ->= sys_r$00(x,check$0(y))
(30a) check$0(sys_w$11(x,y)) ->= sys_w$01(check$1(x),y)
(30b) check$0(sys_w$10(x,y)) ->= sys_w$00(check$1(x),y)
(30c) check$0(sys_w$01(x,y)) ->= sys_w$01(check$0(x),y)
(30d) check$0(sys_w$00(x,y)) ->= sys_w$00(check$0(x),y)
(31a) check$0(sys_w$11(x,y)) ->= sys_w$10(x,check$1(y))
(31b) check$0(sys_w$10(x,y)) ->= sys_w$10(x,check$0(y))
(31c) check$0(sys_w$01(x,y)) ->= sys_w$00(x,check$1(y))
(31d) check$0(sys_w$00(x,y)) ->= sys_w$00(x,check$0(y))
(32a) RAo$0(ok$1(x)) ->= ok$0(RAo$1(x))
(32b) RAo$0(ok$0(x)) ->= ok$0(RAo$0(x))
(33a) RAn$0(ok$1(x)) ->= ok$0(RAn$1(x))
(33b) RAn$0(ok$0(x)) ->= ok$0(RAn$0(x))
(34a) WAo$0(ok$1(x)) ->= ok$0(WAo$1(x))
(34b) WAo$0(ok$0(x)) ->= ok$0(WAo$0(x))
(35a) WAn$0(ok$1(x)) ->= ok$0(WAn$1(x))
(35b) WAn$0(ok$0(x)) ->= ok$0(WAn$0(x))
(36a) RIn$0(ok$1(x)) ->= ok$0(RIn$1(x))
(36b) RIn$0(ok$0(x)) ->= ok$0(RIn$0(x))
(37a) WIo$0(ok$1(x)) ->= ok$0(WIo$1(x))
(37b) WIo$0(ok$0(x)) ->= ok$0(WIo$0(x))
(38a) WIn$0(ok$1(x)) ->= ok$0(WIn$1(x))
(38b) WIn$0(ok$0(x)) ->= ok$0(WIn$0(x))
(39a) sys_r$01(ok$1(x),y) ->= ok$0(sys_r$11(x,y))
(39b) sys_r$00(ok$1(x),y) ->= ok$0(sys_r$10(x,y))
(39c) sys_r$01(ok$0(x),y) ->= ok$0(sys_r$01(x,y))
(39d) sys_r$00(ok$0(x),y) ->= ok$0(sys_r$00(x,y))
(40a) sys_r$10(x,ok$1(y)) ->= ok$0(sys_r$11(x,y))
(40b) sys_r$10(x,ok$0(y)) ->= ok$0(sys_r$10(x,y))
(40c) sys_r$00(x,ok$1(y)) ->= ok$0(sys_r$01(x,y))
(40d) sys_r$00(x,ok$0(y)) ->= ok$0(sys_r$00(x,y))
(41a) sys_w$01(ok$1(x),y) ->= ok$0(sys_w$11(x,y))
(41b) sys_w$00(ok$1(x),y) ->= ok$0(sys_w$10(x,y))
(41c) sys_w$01(ok$0(x),y) ->= ok$0(sys_w$01(x,y))
(41d) sys_w$00(ok$0(x),y) ->= ok$0(sys_w$00(x,y))
(42a) sys_w$10(x,ok$1(y)) ->= ok$0(sys_w$11(x,y))
(42b) sys_w$10(x,ok$0(y)) ->= ok$0(sys_w$10(x,y))
(42c) sys_w$00(x,ok$1(y)) ->= ok$0(sys_w$01(x,y))
(42d) sys_w$00(x,ok$0(y)) ->= ok$0(sys_w$00(x,y))

[21]  Use following polynomial interpretation:
[ok$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(32a), (33a), (34a), (35a), (36a), (37a), (38a), (39a)-(39b), (40a), (40c), (41a)-(41b), (42a), (42c)

[22]  Use following polynomial interpretation:
[sys_w$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(30a), (31a)

[23]  Use following polynomial interpretation:
[sys_w$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(31c)

[24]  Use following polynomial interpretation:
[sys_r$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(28a), (29a)

[25]  Use following polynomial interpretation:
[sys_r$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(29c)

[26]  Use following polynomial interpretation:
[WIo$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(26a)

[27]  Use following polynomial interpretation:
[WAn$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(23a)

[28]  Use following polynomial interpretation:
[WAo$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(22a)

[29]  Use following polynomial interpretation:
[RAo$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(20a)

[30]  Use following polynomial interpretation:
[RIo$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(24a)

[31]  Use following polynomial interpretation:
[WIn$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(18a), (18c), (27a)

[32]  Use following polynomial interpretation:
[read$10(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(9a)-(9b), (10a)-(10b), (16a)-(16d)

[33]  Use following polynomial interpretation:
[RAn$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(21a)

[34]  Use following polynomial interpretation:
[read$00(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(9c), (10c), (16e)-(16f)

[35]  Use following polynomial interpretation:
[RIn$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(25a)

[36]  Use following polynomial interpretation:
[sys_w$10(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(18b), (18d), (30b)

[37]  Unlabel this TRS to obtain the one consisting of the rules:
(1)-(2), (6), (9)-(10), (16), (19)-(42)

[38]  Use following polynomial interpretation:
[sys_r(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(16)

[39]  Use following polynomial interpretation:
[WAn(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(6)

[40]  Since there are no remaining strict rules, relative termination is proved!

readers-writers.trs, 2174.18, Y