proposition: Lemma invariant2_ind : forall s0 : Site, s0 <> owner -> forall (c : Config) (t : class_trans c), legal c -> st c s0 = sigma_rooted s0 (bm c) -> st (transition c t) s0 = sigma_rooted s0 (bm (transition c t)).
proof: Proof. simple induction t. intros; simpl in |- *. rewrite sigma_rooted_post_message. unfold Inc_send_table in |- *. unfold rooted_fun in |- *. case (eq_site_dec s1 s0). intro; rewrite e. unfold update_table in |- *; rewrite here. omega. intro; unfold update_table in |- *; rewrite elsewhere. omega. auto. auto. intros; simpl in |- *. rewrite sigma_rooted_collect_message with (m := dec). unfold Dec_send_table in |- *. unfold rooted_fun in |- *. case (eq_site_dec s2 s0). intro; rewrite e0. unfold update_table in |- *; rewrite here. omega. intros; unfold update_table in |- *; rewrite elsewhere. omega. auto. auto. auto. intros; simpl in |- *. rewrite sigma_rooted_post_message. rewrite sigma_rooted_collect_message with (m := inc_dec s3). unfold Inc_send_table, rooted_fun in |- *. unfold update_table in |- *; rewrite elsewhere. case (eq_site_dec s3 s0). case (eq_site_dec owner owner). intros; omega. intro; elim n. auto. intros; omega. auto. auto. auto. auto. intros; simpl in |- *. rewrite sigma_rooted_post_message. rewrite sigma_rooted_collect_message with (m := copy). unfold rooted_fun in |- *. case (eq_site_dec s1 s0). intro; omega. intro; omega. auto. auto. auto. intros; simpl in |- *. rewrite sigma_rooted_collect_message with (m := copy). unfold rooted_fun in |- *. rewrite case_ineq. omega. auto. auto. auto. intros; simpl in |- *. rewrite sigma_rooted_post_message. rewrite sigma_rooted_collect_message with (m := copy). unfold rooted_fun in |- *. case (eq_site_dec s1 s0). rewrite case_eq. intro; omega. intro; omega. auto. auto. auto. intros; simpl in |- *. rewrite sigma_rooted_post_message. unfold rooted_fun in |- *. rewrite case_ineq. omega. auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm