proposition: Lemma st_rt : forall (c0 : Config) (s0 : Site), legal c0 -> s0 <> owner -> (st c0 s0 > 0)%Z -> rt c0 s0 = true.
proof: Proof. intros c0 s0 H. elim H. simpl in |- *. unfold send_init in |- *. intros. cut (~ (0 > 0)%Z). intro. elim H2; auto. omega. intros c t. elim t. simpl in |- *. intros s1 s2. case (eq_site_dec s0 s1); intro. unfold access in |- *. rewrite e. intros. auto. intros. apply H1. auto. generalize H3; unfold Inc_send_table in |- *. rewrite other_site. auto. auto. simpl in |- *. intros. apply H1. auto. generalize H3; unfold Dec_send_table in |- *. case (eq_site_dec s0 s2). intro. rewrite e0; rewrite that_site. intro. omega. intro; rewrite other_site; auto. simpl in |- *. intros. apply H1. auto. generalize H3; unfold Inc_send_table in |- *; rewrite other_site; auto. simpl in |- *. intros. apply H1; auto. simpl in |- *. intros. case (eq_site_dec s2 s0). intro; unfold Set_rec_table in |- *. rewrite e1; rewrite that_site; auto. intro. unfold Set_rec_table in |- *; rewrite other_site. apply H1; auto. auto. simpl in |- *. intros. case (eq_site_dec s2 s0). intro; unfold Set_rec_table in |- *. rewrite e1; rewrite that_site; auto. intro; unfold Set_rec_table in |- *; rewrite other_site. apply H1; auto. auto. simpl in |- *. intros. case (eq_site_dec s s0). intro. rewrite <- e1 in H3. rewrite e in H3. absurd (0 > 0)%Z. omega. auto. intro; unfold Reset_rec_table in |- *. rewrite other_site. apply H1; auto. auto. auto. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm