proposition: Lemma mul_ancestor_not_reflexive : forall c : Config, legal c -> forall s1 s2 : Site, mul_ancestor c s1 s2 -> s1 <> s2.
proof: Proof. intros c H. generalize H. elim H. intros. elim H1; intros. elim H2; intros. generalize H4; simpl in |- *. intuition. elim H4; simpl in |- *; intros. contradiction. simple induction t; simpl in |- *; intros. apply H1. auto. elim H3. intros. apply mul_short. elim H4. simpl in |- *. intros. apply mul_parent_intro. auto. apply in_queue_post with (m2 := copy) (s3 := s1) (s4 := s2). discriminate. auto. intros. apply mul_long with (s1 := s5). auto. elim H6; simpl in |- *; intros. apply mul_parent_intro. auto. apply in_queue_post with (m2 := copy) (s3 := s1) (s4 := s2). discriminate. auto. apply H1. auto. elim H3. intros. apply mul_short. elim H4. simpl in |- *. intros. apply mul_parent_intro. auto. apply in_queue_collect with (s3 := s1) (s4 := s2). auto. intros. apply mul_long with (s1 := s5). auto. elim H6; simpl in |- *; intros. apply mul_parent_intro. auto. apply in_queue_collect with (s3 := s1) (s4 := s2). auto. apply H1. auto. elim H3. intros. apply mul_short. elim H4. simpl in |- *. intros. apply mul_parent_intro. auto. cut (inc_dec s6 <> dec). intro. generalize (in_queue_post (Collect_message Message (bm c0) s1 owner) s7 owner owner s3 (inc_dec s6) dec H7 H6). intro. apply in_queue_collect with (s3 := s1) (s4 := owner). auto. discriminate. intros. apply mul_long with (s1 := s5). auto. elim H6; simpl in |- *; intros. apply mul_parent_intro. auto. cut (inc_dec s7 <> dec). intro. generalize (in_queue_post (Collect_message Message (bm c0) s1 owner) s8 owner owner s3 (inc_dec s7) dec H9 H8). intro. apply in_queue_collect with (s3 := s1) (s4 := owner). auto. discriminate. apply H1. auto. elim H3. intros. apply mul_short. elim H4. simpl in |- *. intros. apply mul_parent_intro. auto. cut (inc_dec s6 <> dec). intro. generalize (in_queue_post (Collect_message Message (bm c0) s1 s2) s7 owner s2 s1 (inc_dec s6) dec H7 H6). intro. apply in_queue_collect with (s3 := s1) (s4 := s2). auto. discriminate. intros. apply mul_long with (s1 := s5). auto. elim H6; simpl in |- *; intros. apply mul_parent_intro. auto. cut (inc_dec s7 <> dec). intro. generalize (in_queue_post (Collect_message Message (bm c0) s1 s2) s8 owner s2 s1 (inc_dec s7) dec H9 H8). intro. apply in_queue_collect with (s3 := s1) (s4 := s2). auto. discriminate. case (eq_site_dec s0 s2). intro. generalize e e0 e1. elim H3. intro; intro; intro. elim H4. intros. apply not_reflexive with (c := rec_copy2_trans c0 s2). auto. auto. intros. rewrite e4. apply mul_ancestor_does_not_join with (c0 := c0) (s4 := s4). auto. auto. auto. auto. auto. intro. apply H1. auto. generalize e. generalize n. elim H3. intros. apply mul_short. generalize n0. elim H4. intros. apply mul_parent_intro. generalize H5; simpl in |- *. unfold Set_rec_table in |- *; rewrite other_site; auto. generalize H6; simpl in |- *. intro. apply in_queue_collect with (s3 := owner) (s4 := s2). auto. intros. apply mul_long with (s1 := s4). apply H5. apply (mul_parent_does_not_join c0 s2 s4 s5). auto. auto. auto. auto. auto. auto. generalize n0; elim H6. intros. apply mul_parent_intro. generalize H7; simpl in |- *. unfold Set_rec_table in |- *; rewrite other_site; auto. generalize H8; simpl in |- *. intro. apply in_queue_collect with (s3 := owner) (s4 := s2). auto. simpl in |- *. intros. case (eq_site_dec s2 s3). intro. generalize e e0 e1. elim H3. intro; intro; intro. elim H4. intros. apply not_reflexive with (c := rec_copy3_trans c0 s1 s2). auto. auto. intros. rewrite <- e4. apply (mul_ancestor_does_not_join2 c0 s1 s2 s4 s5). auto. auto. auto. auto. auto. intro. apply H1. auto. generalize e. generalize n. generalize n1. elim H3. intros. apply mul_short. generalize n2 n3 e1. elim H4. intros. apply mul_parent_intro. generalize H5; simpl in |- *. unfold Set_rec_table in |- *; rewrite other_site; auto. generalize H6; simpl in |- *. rewrite post_elsewhere. intro. apply in_queue_collect with (s3 := s1) (s4 := s2). auto. auto. intros. apply mul_long with (s1 := s5). apply H5. generalize (mul_parent_does_not_join2 c0 s1 s2 s5 s6 H0 H2 H6 e1 e0). auto. auto. auto. generalize n2. elim H6. intros. apply mul_parent_intro. generalize H7; simpl in |- *. unfold Set_rec_table in |- *; rewrite other_site; auto. generalize H8; simpl in |- *. rewrite post_elsewhere. intro. apply in_queue_collect with (s3 := s1) (s4 := s2). auto. auto. intros. apply H1. auto. elim H3. simpl in |- *. intros. apply mul_short. elim H4. intros. apply mul_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 in_queue_post with (s3 := s) (s4 := owner) (m2 := dec). discriminate. auto. intros. apply mul_long with (s1 := s3). auto. elim H6. intros. apply mul_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 in_queue_post with (s3 := s) (s4 := owner) (m2 := dec). discriminate. auto. apply H1. auto. elim H3. intros. apply mul_short. elim H4. simpl in |- *. intros. apply mul_parent_intro. auto. cut (inc_dec s6 <> dec). intro. generalize (in_queue_post (change_queue (queue Message) (bm c0) s1 owner q) s7 owner s1 s2 (inc_dec s6) dec H7 H6). case (eq_site_dec s1 s7); intro. rewrite e0. rewrite that_queue. intro. rewrite <- e0. rewrite e. simpl in |- *. auto. rewrite other_queue. auto. left; auto. discriminate. intros. apply mul_long with (s1 := s5). auto. elim H6; simpl in |- *; intros. apply mul_parent_intro. auto. cut (inc_dec s7 <> dec). intro. generalize (in_queue_post (change_queue (queue Message) (bm c0) s1 owner q) s8 owner s1 s2 (inc_dec s7) dec H9 H8). case (eq_site_dec s1 s8); intro. rewrite e0. rewrite that_queue. rewrite <- e0. rewrite e. intro. simpl in |- *. auto. rewrite other_queue. auto. auto. discriminate. apply H1. auto. elim H3. intros. apply mul_short. elim H4. simpl in |- *. intros. apply mul_parent_intro. auto. generalize H6. case (eq_queue_dec s1 s7 s2 owner); intro. decompose [and] a. rewrite H7; rewrite H8. rewrite that_queue. rewrite H7 in e; rewrite H8 in e. rewrite e. intro. apply in_q_shuffle with (q3 := q3) (q4 := q4). auto. auto. rewrite other_queue; auto. elim o; auto. intros. apply mul_long with (s1 := s5). auto. elim H6. simpl in |- *. intros. apply mul_parent_intro. auto. generalize H8. case (eq_queue_dec s1 s8 s2 owner); intro. decompose [and] a. rewrite H9; rewrite H10. rewrite that_queue. rewrite H9 in e; rewrite H10 in e. rewrite e. intro. apply in_q_shuffle with (q3 := q3) (q4 := q4). auto. auto. rewrite other_queue; auto. elim o; auto. Qed.
imports: DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4