proposition: Lemma rinc_trans_st_rt : forall s0 : Site, s0 <> owner -> ((st c0 s0 > 0)%Z -> rt c0 s0 = true) -> (st (rec_inc_trans c0 s1 s2) s0 > 0)%Z -> rt (rec_inc_trans c0 s1 s2) s0 = true.
proof: Proof. intros s0 H; simpl in |- *. rewrite no_inc_send_table; auto. Qed.
imports: init table_act mess_act