proposition: Lemma RState_Trans_T : forall (s1 s2 s3 : S) (t1 t2 : Instant), RState_T s1 s2 t1 -> RState_T s2 s3 t2 -> RState_T s1 s3 (plus_Ck t1 t2).
proof: Proof. simple induction 2; unfold plus_Ck in |- *; intros. rewrite (plus_comm t1 time0); unfold time0 in |- *; simpl in |- *; assumption. unfold Inc in |- *; unfold plus_Ck in |- *; rewrite (plus_assoc t1 t tick). apply (rsNextTick_T H2 H3). apply (rsNextDisc_T H2 H3 H4). Qed.
imports: time_clocks