proposition: Lemma ancestor_not_reflexive : forall c : Config, legal c -> forall s1 s2 : Site, ancestor c s1 s2 -> s1 <> s2.
proof: Proof. intros c H. generalize H. elim H. simpl in |- *. intros. elim H1. intros. elim H2. simpl in |- *. intuition. simpl in |- *. intros. elim H4. simpl in |- *. intuition. simple induction t. intros. apply H1. auto. elim H3. simpl in |- *. intros. apply short. elim H4. intros. apply parent_intro. generalize H5; simpl in |- *; auto. apply (inc_dec_in_post2 (bm c0) s7 s6 s1 s2 copy). generalize H6; simpl in |- *; auto. discriminate. intros. apply long with (s1 := s5). auto. elim H6. intros. apply parent_intro. generalize H7; simpl in |- *; auto. apply (inc_dec_in_post2 (bm c0) s8 s7 s1 s2 copy). generalize H8; simpl in |- *; auto. discriminate. intros. apply H1. auto. elim H3. simpl in |- *. intros. apply short. elim H4. intros. apply parent_intro. generalize H5; simpl in |- *; auto. apply (inc_dec_in_collect2 (bm c0) dec s7 s1 s2 s6). auto. generalize H6; simpl in |- *; auto. intros. apply long with (s1 := s5). auto. elim H6. intros. apply parent_intro. generalize H7; simpl in |- *; auto. apply (inc_dec_in_collect2 (bm c0) dec s8 s1 s2 s7). auto. generalize H8; simpl in |- *; auto. intros. apply H1. auto. elim H3. simpl in |- *. intros. apply short. elim H4. intros. apply parent_intro. generalize H5; simpl in |- *; auto. apply (inc_dec_in_collect2 (bm c0) (inc_dec s3) s7 s1 owner s6). auto. apply (inc_dec_in_post2 (Collect_message Message (bm c0) s1 owner) s7 s6 owner s3 dec). generalize H6; simpl in |- *; auto. discriminate. intros. apply long with (s1 := s5). auto. elim H6. intros. apply parent_intro. generalize H7; simpl in |- *; auto. apply (inc_dec_in_collect2 (bm c0) (inc_dec s3) s8 s1 owner s7). auto. apply (inc_dec_in_post2 (Collect_message Message (bm c0) s1 owner) s8 s7 owner s3 dec). generalize H8; simpl in |- *; auto. discriminate. intros. apply H1. auto. elim H3. simpl in |- *. intros. apply short. elim H4. intros. apply parent_intro. generalize H5; simpl in |- *; auto. apply (inc_dec_in_collect2 (bm c0) copy s7 s1 s2 s6). auto. apply (inc_dec_in_post2 (Collect_message Message (bm c0) s1 s2) s7 s6 s2 s1 dec). generalize H6; simpl in |- *; auto. discriminate. intros. apply long with (s1 := s5). auto. elim H6. intros. apply parent_intro. generalize H7; simpl in |- *; auto. apply (inc_dec_in_collect2 (bm c0) copy s8 s1 s2 s7). auto. apply (inc_dec_in_post2 (Collect_message Message (bm c0) s1 s2) s8 s7 s2 s1 dec). generalize H8; simpl in |- *; auto. discriminate. simpl in |- *. intros. case (eq_site_dec s0 s2). intro. generalize e e0 e1. elim H3. intro; intro; intro. elim H4. intros. rewrite e4 in H5. rewrite e4 in H6. rewrite e4. generalize (inc_dec_in s5 (bm (rec_copy2_trans c0 s2) s2 owner) H6). intro. apply not_reflexive with (c := rec_copy2_trans c0 s2). auto. auto. intros. apply (ancestor_does_not_join c0 s5 s3 s4). auto. rewrite e4; auto. rewrite e4; auto. rewrite e4; auto. rewrite e4; auto. intro. apply H1. auto. generalize e. generalize n. elim H3. intros. apply short. generalize n0. elim H4. intros. apply parent_intro. generalize H5; simpl in |- *. unfold Set_rec_table in |- *; rewrite other_site; auto. generalize H6; simpl in |- *. intro. apply (inc_dec_in_collect2 (bm c0) copy s6 owner s2 s5). auto. auto. intros. apply long with (s1 := s4). apply H5. apply (parent_does_not_join c0 s2 s4 s5). auto. auto. auto. auto. auto. auto. generalize n0; elim H6. intros. apply parent_intro. generalize H7; simpl in |- *. unfold Set_rec_table in |- *; rewrite other_site; auto. generalize H8; simpl in |- *. intro. apply (inc_dec_in_collect2 (bm c0) copy s7 owner s2 s6). auto. auto. simpl in |- *. intros. case (eq_site_dec s2 s3). intro. generalize e e0 e1. elim H3. intro; intro; intro. elim H4. intros. generalize (inc_dec_in s6 (bm (rec_copy3_trans c0 s1 s2) s7 owner) H6). intro. apply not_reflexive with (c := rec_copy3_trans c0 s1 s2). auto. auto. intros. rewrite <- e4. apply (ancestor_does_not_join2 c0 s1 s2 s4 s5). auto. auto. auto. auto. auto. intro. apply H1. auto. generalize e. generalize n. generalize n0. elim H3. intros. apply short. generalize n1 n2 e1. elim H4. intros. apply parent_intro. generalize H5; simpl in |- *. unfold Set_rec_table in |- *; rewrite other_site; auto. generalize H6; simpl in |- *. rewrite post_elsewhere. intro. apply (inc_dec_in_collect2 (bm c0) copy s7 s1 s2 s6). auto. auto. left; auto. intros. apply long with (s1 := s5). apply H5. generalize (parent_does_not_join2 c0 s1 s2 s5 s6 H0 H2 H6 e1 e0). auto. auto. auto. generalize n1. elim H6. intros. apply parent_intro. generalize H7; simpl in |- *. unfold Set_rec_table in |- *; rewrite other_site; auto. generalize H8; simpl in |- *. rewrite post_elsewhere. intro. apply (inc_dec_in_collect2 (bm c0) copy s8 s1 s2 s7). auto. auto. left; auto. intros. apply H1. auto. elim H3. simpl in |- *. intros. apply short. elim H4. intros. apply parent_intro. generalize H5; simpl in |- *; auto. unfold Reset_rec_table in |- *. case (eq_site_dec s s5). intro; rewrite e1. rewrite that_site; auto. intro; discriminate. intro; rewrite other_site; auto. generalize H6; simpl in |- *. intro. apply (inc_dec_in_post2 (bm c0) s5 s4 s owner dec). auto. discriminate. intros. apply long with (s1 := s3). auto. elim H6. intros. apply parent_intro. generalize H7; simpl in |- *; auto. case (eq_site_dec s s6). intro; rewrite e1; unfold Reset_rec_table in |- *; rewrite that_site. intro; discriminate. intro; unfold Reset_rec_table in |- *; rewrite other_site; auto. generalize H8; simpl in |- *; intro. apply (inc_dec_in_post2 (bm c0) s6 s5 s owner dec). auto. discriminate. Qed.
imports: DistributedReferenceCounting.machine1.invariant0 DistributedReferenceCounting.machine1.invariant1 DistributedReferenceCounting.machine1.invariant2 DistributedReferenceCounting.machine1.invariant3 DistributedReferenceCounting.machine1.invariant4