proposition: Lemma parent_invariant_inductive_optim1 : forall (c : Config) (t : class_trans c) (s1 s2 : Site) (q : queue Message) (n : s1 <> s2) (e : bm c s1 owner = input Message dec (input Message (inc_dec s2) q)), legal c -> (legal c -> forall s : Site, indirect_son1 c s -> exists s0 : Site, direct_son c s0 /\ ancestor c s0 s) -> legal (transition c (redirect_inc c s1 s2 q n e)) -> forall s : Site, indirect_son1 (transition c (redirect_inc c s1 s2 q n e)) s -> exists s0 : Site, direct_son (transition c (redirect_inc c s1 s2 q n e)) s0 /\ ancestor (transition c (redirect_inc c s1 s2 q n e)) s0 s.
proof: Proof. intro; intro. simpl in |- *. intros s1 s2 q n e H H0 Hnext; intros. elim (decide_rt c s1); intro. elim (H0 H s). intros. decompose [and] H2. split with x. split. elim H3; intros; apply direct_son_intro; auto. simpl in |- *. rewrite post_elsewhere. rewrite other_queue. auto. left; unfold not in |- *; intro. rewrite H8 in H6. rewrite H6 in a. discriminate. left; unfold not in |- *; intro. rewrite H8 in a; rewrite a in H6; discriminate. elim H4. intros. apply short. elim H5; intros. apply parent_intro. simpl in |- *. auto. simpl in |- *. cut (s1 <> s5). intro. rewrite post_elsewhere. rewrite other_queue. auto. left; auto. auto. unfold not in |- *; intro. rewrite H8 in a; rewrite a in H6; discriminate. intros. apply long with (s1 := s3). auto. elim H7. intros. apply parent_intro. auto. simpl in |- *. cut (s1 <> s6). intro. rewrite post_elsewhere. rewrite other_queue. auto. auto. auto. unfold not in |- *; intro. rewrite H10 in a; rewrite a in H8; discriminate. elim H1; intros. apply indirect_son1_intro. auto. generalize H3; simpl in |- *. auto. generalize H4; simpl in |- *. generalize H3; simpl in |- *; intro. cut (s0 <> s1). intro. rewrite post_elsewhere. rewrite other_queue. auto. auto. auto. unfold not in |- *; intro. rewrite H6 in H5; rewrite H5 in a; discriminate. elim (decide_direct_son (redirect_inc_trans c s1 s2 q) s1). intro. elim (H0 H s). intros. decompose [and] H2. elim (decide_ancestor c x s s1). intro. cut (s1 <> s). intro. elim H5. intro; elim H6; auto. intro. split with s1. split. auto. generalize e H6 a. elim H7; intros. apply short. generalize e0. elim H8; simpl in |- *; intros. apply parent_intro; simpl in |- *. auto. apply inc_dec_in_post. rewrite other_queue. auto. left. cut (s4 <> s5). auto. apply not_reflexive with (c := c). auto. apply inc_dec_in. auto. auto. intro; discriminate. apply long with (s1 := s3). apply H9. auto. apply ancestor_not_reflexive with (c := c). auto. auto. auto. generalize H11. elim H10; intros. apply parent_intro; simpl in |- *. auto. apply inc_dec_in_post. rewrite other_queue. auto. auto. intro; discriminate. generalize a. elim H1. intros. inversion a0. unfold not in |- *; intro. elim H8. rewrite <- H13. intro. generalize (H11 s4). auto. intro. split with x. split. decompose [and] H5. generalize H6 H7. elim H3. intros. apply direct_son_intro. auto. simpl in |- *. auto. simpl in |- *. intro. apply inc_dec_not_in_post. case (eq_site_dec s1 s0); intro. rewrite e0 in e. rewrite e in H10. elim (H10 s2). simpl in |- *. case (eq_site_dec s2 s2); intro. auto. elim n0; auto. rewrite other_queue. auto. auto. intro; discriminate. decompose [and] H5. generalize H6 H7. elim H4. intros. apply short. generalize H9 H10. elim H8; intros. apply parent_intro; simpl in |- *. auto. rewrite post_elsewhere. rewrite other_queue. auto. auto. auto. intros. apply long with (s1 := s3). apply H9. unfold not in |- *; intro. elim H12. rewrite H13. apply short. auto. unfold not in |- *; intro. elim H12. apply long with (s1 := s3). auto. auto. generalize H11 H12. elim H10. intros. apply parent_intro; simpl in |- *. auto. rewrite post_elsewhere. rewrite other_queue. auto. auto. auto. auto. auto. apply indirect_son1_intro. unfold not in |- *; intro; generalize e. rewrite H5; rewrite empty_q_to_me; simpl in |- *. intro; discriminate. auto. auto. unfold not in |- *; intro. apply (H5 s2). rewrite e; simpl in |- *. case (eq_site_dec s2 s2); intro; auto. elim H1. intros. apply indirect_son1_intro. auto. generalize H3; simpl in |- *; auto. generalize H4; simpl in |- *. intro. unfold not in |- *; intro. elim H5. intro. apply inc_dec_not_in_post. rewrite other_queue. unfold not in |- *; intro. elim (H6 s3); auto. left; unfold not in |- *; intro. apply (H6 s2). rewrite H7; rewrite e. simpl in |- *. case (eq_site_dec s2 s2); intro; auto. intro; discriminate. intro. cut (s1 <> owner). intro. elim (direct_or_indirect_son1 (redirect_inc_trans c s1 s2 q) s1 H2). intro. elim b0; auto. intro. inversion b1. elim (decide_inc_dec_in_queue (redirect_inc_trans c s1 s2 q) s1); intro. elim a. intros. elim (direct_or_indirect_son1 (redirect_inc_trans c s1 s2 q) x). intro. elim (H0 H s). intros. elim (decide_ancestor c x0 s s1). intro. split with x. split. auto. elim H8; intro. apply short. apply parent_intro; simpl in |- *. rewrite <- H9; auto. generalize p; simpl in |- *. auto. rewrite H9; auto. apply long_inv with (s1 := s1). apply parent_intro; auto. generalize H9. elim H9; intros. apply short. generalize H11; elim H10; intros. cut (s5 <> s6). intro. apply parent_intro; simpl in |- *. auto. apply inc_dec_in_post. rewrite other_queue. auto. auto. intro; discriminate. apply ancestor_not_reflexive with (c := c). auto. auto. apply long with (s1 := s4). apply H11; auto. generalize H13. elim H12; intros. cut (s3 <> s7). intro. apply parent_intro. simpl in |- *; auto. simpl in |- *. apply inc_dec_in_post. rewrite other_queue. auto. auto. intro; discriminate. apply ancestor_not_reflexive with (c := c). auto. auto. intro. split with x0. decompose [and] H7. split. elim H9; intros. apply direct_son_intro; simpl in |- *. auto. auto. intro. apply inc_dec_not_in_post. rewrite other_queue. auto. left; unfold not in |- *; intro. elim (H13 s2); rewrite H14; rewrite e. simpl in |- *. case (eq_site_dec s2 s2); intro; auto. intro; discriminate. generalize H8. elim H10; intros. apply short. generalize H12. elim H11; intros. decompose [and] H15. apply parent_intro; simpl in |- *. auto. apply inc_dec_in_post. rewrite other_queue. auto. auto. intro; discriminate. apply long with (s1 := s4). apply H12. decompose [and] H14. split. unfold not in |- *; intro. elim H16. rewrite H17; apply short; auto. unfold not in |- *; intro. elim H16. apply long with (s1 := s4). auto. auto. generalize H14; elim H13; intros. apply parent_intro; simpl in |- *. auto. apply inc_dec_in_post. rewrite other_queue. auto. left; decompose [and] H17; auto. intro; discriminate. decompose [and] H7; auto. decompose [and] H7; auto. apply indirect_son1_intro; simpl in |- *. auto. auto. unfold not in |- *; intro. apply (H8 s2). rewrite e. simpl in |- *. case (eq_site_dec s2 s2); intro; auto. elim H1; intros. apply indirect_son1_intro. auto. generalize H8; simpl in |- *; auto. unfold not in |- *; intro. elim H9; intro. simpl in |- *. apply inc_dec_not_in_post. case (eq_site_dec s1 s3); intro. unfold not in |- *; intro. apply (H10 s2); rewrite <- e0. rewrite e; simpl in |- *; auto. case (eq_site_dec s2 s2); intro; auto. rewrite other_queue. unfold not in |- *; intro. apply (H10 s4). auto. auto. intro; discriminate. intro. elim (H0 H x). intros. elim (H0 H s). intros. elim (decide_ancestor c x1 s s1). intro. decompose [and] H7. split with x0. split. elim H10; intros. apply direct_son_intro. auto. simpl in |- *; auto. simpl in |- *. intro. apply inc_dec_not_in_post. rewrite other_queue. auto. left. elim b1. simpl in |- *. intros. unfold not in |- *; intro. elim H17. intro. apply inc_dec_not_in_post. case (eq_site_dec s1 s5); intro. elim (H14 s2). rewrite H18; rewrite <- e0. rewrite e. simpl in |- *. case (eq_site_dec s2 s2); intro; auto. rewrite other_queue. rewrite <- H18. auto. left; auto. intro; discriminate. intro; discriminate. generalize (parent_intro (redirect_inc_trans c s1 s2 q) x s1 b p). intro. cut (ancestor (redirect_inc_trans c s1 s2 q) x0 s1). intro. elim H9. intro. rewrite <- H14; auto. intro. apply ancestor_transitive with (s2 := s1). auto. generalize H14. elim H14. intros. apply short. generalize H16. elim H15; simpl in |- *; intros. apply parent_intro; simpl in |- *. auto. apply inc_dec_in_post. rewrite other_queue. auto. left. cut (s5 <> s6). auto. apply ancestor_not_reflexive with (c := c). auto. auto. intro; discriminate. intros. apply long with (s1 := s4). apply H16. auto. generalize H15 H17. elim H17. intros. apply parent_intro; simpl in |- *. auto. apply inc_dec_in_post. rewrite other_queue. auto. left. cut (s3 <> s7). auto. apply ancestor_not_reflexive with (c := c). auto. apply long with (s1 := s6). auto. auto. intro; discriminate. apply long with (s1 := x). cut (ancestor (redirect_inc_trans c s1 s2 q) x s1). intro. generalize H13. elim H11. intros. apply short. generalize H15. elim H14. intros. cut (s6 <> s1). intro. apply parent_intro; simpl in |- *. auto. rewrite post_elsewhere. rewrite other_queue. auto. auto. auto. apply ancestor_not_reflexive with (c := redirect_inc_trans c s1 s2 q). auto. auto. intros. apply long with (s1 := s4). apply H15. apply long_inv with (s1 := s5). generalize H17. elim H16; intros. cut (s7 <> s1). intro. apply parent_intro; simpl in |- *. auto. rewrite post_elsewhere. rewrite other_queue. auto. auto. auto. apply ancestor_not_reflexive with (c := redirect_inc_trans c s1 s2 q). auto. auto. auto. generalize H17. elim H16; intros. cut (s7 <> s1). intro. apply parent_intro; simpl in |- *. auto. rewrite post_elsewhere. rewrite other_queue. auto. auto. auto. apply ancestor_not_reflexive with (c := redirect_inc_trans c s1 s2 q). auto. auto. apply short. auto. auto. intro. split with x1. decompose [and] H8. split. elim H10; intros. apply direct_son_intro. auto. simpl in |- *; auto. simpl in |- *. intro. apply inc_dec_not_in_post. rewrite other_queue. auto. left. elim b1. simpl in |- *. intros. unfold not in |- *; intro. elim H17. intro. apply inc_dec_not_in_post. case (eq_site_dec s1 s5); intro. elim (H14 s2). rewrite H18; rewrite <- e0. rewrite e. simpl in |- *. case (eq_site_dec s2 s2); intro; auto. rewrite other_queue. rewrite <- H18. auto. left; auto. intro; discriminate. intro; discriminate. generalize H9. elim H11. intros. apply short. generalize H13. elim H12; intros. apply parent_intro; simpl in |- *. auto. apply inc_dec_in_post. rewrite other_queue. auto. left; decompose [and] H16; auto. intro; discriminate. intros. apply long with (s1 := s4). apply H13. decompose [and] H15. split. unfold not in |- *; intro. elim H17. rewrite H18; apply short; auto. unfold not in |- *; intro. elim H17. apply long with (s1 := s4). auto. auto. generalize H15. elim H14; intros. apply parent_intro; simpl in |- *. auto. apply inc_dec_in_post. rewrite other_queue. auto. left; decompose [and] H18; auto. intro; discriminate. decompose [and] H8; auto. decompose [and] H8; auto. apply indirect_son1_intro. auto. auto. unfold not in |- *; intro. apply (H9 s2); rewrite e; simpl in |- *. case (eq_site_dec s2 s2); intro; auto. generalize b1; elim H1; simpl in |- *; intros. apply indirect_son1_intro; simpl in |- *. auto. auto. unfold not in |- *; intro. case (eq_site_dec s3 s1); intro. apply (H11 s2). rewrite e0. rewrite e; simpl in |- *. case (eq_site_dec s2 s2); intro; auto. elim H10. intro. apply inc_dec_not_in_post. rewrite other_queue. unfold not in |- *; intro; elim (H11 s4); auto. auto. intro; discriminate. cut (x <> s1). elim b2; simpl in |- *; intros. apply indirect_son1_intro; simpl in |- *. auto. auto. unfold not in |- *; intro. elim H9; intro. apply inc_dec_not_in_post. rewrite other_queue. unfold not in |- *; intro; elim (H11 s4); auto. auto. intro; discriminate. apply not_reflexive with (c := redirect_inc_trans c s1 s2 q). auto. apply inc_dec_in. auto. auto. apply (not_owner_inc3 (redirect_inc_trans c s1 s2 q) s1 owner). auto. apply inc_dec_in. auto. auto. simpl in |- *. apply st_rt. auto. apply (not_owner_inc3 (redirect_inc_trans c s1 s2 q) s1 owner). auto. apply inc_dec_in. auto. auto. cut (st (redirect_inc_trans c s1 s2 q) x > 0)%Z. simpl in |- *. auto. apply positive_st with (s5 := s1). apply not_owner_inc3 with (c := redirect_inc_trans c s1 s2 q) (s1 := s1) (s2 := owner). auto. apply inc_dec_in. auto. auto. auto. apply inc_dec_in. auto. auto. elim H5. auto. simpl in |- *. auto. unfold not in |- *; intro; generalize e. rewrite H2; rewrite empty_q_to_me. intro; discriminate. auto. unfold not in |- *; intro; generalize e. rewrite H2; rewrite empty_q_to_me. intro. discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine4.invariant6