include "ground_2/steps/rtc_isrt.ma".
(* RT-TRANSITION COUNTER ****************************************************)
include "ground_2/steps/rtc_isrt.ma".
(* RT-TRANSITION COUNTER ****************************************************)
lemma plus_rew: ∀ri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2.
〈ri1+ri2,rs1+rs2,ti1+ti2,ts1+ts2〉 =
(〈ri1,rs1,ti1,ts1〉) + (〈ri2,rs2,ti2,ts2〉).
lemma plus_rew: ∀ri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2.
〈ri1+ri2,rs1+rs2,ti1+ti2,ts1+ts2〉 =
(〈ri1,rs1,ti1,ts1〉) + (〈ri2,rs2,ti2,ts2〉).