proposition: Lemma termination_measure_decreases : forall (c : Config) (t : class_trans c), legal c -> ~ copy_p c t -> (termination_measure (transition c t) < termination_measure c)%Z.
proof: Proof. simple induction t; simpl in |- *; unfold termination_measure, termination_rt_measure, termination_q_measure in |- *; simpl in |- *; intros. elim H0; auto. rewrite sigma2_sigma2_but_x_y with (s0 := s1) (s1 := s2) (eq_site_dec := eq_site_dec). rewrite collect_here. unfold termination_q_count in |- *. rewrite reduce_first_out with (m := dec). rewrite sigma2_sigma2_but_x_y with (s0 := s1) (s1 := s2) (eq_site_dec := eq_site_dec). apply add_reduce10. apply sigma2_but_simpl2. intros. rewrite collect_elsewhere. auto. case (eq_queue_dec s1 x s2 y); intro. elim H1; auto. decompose [and] a; split; auto. auto. apply finite_site. apply finite_site. unfold termination_count in |- *; simpl in |- *. omega. apply finite_site. apply finite_site. auto. apply finite_site. apply finite_site. apply add_reduce15. rewrite new_sigma2_sigma2_but_x_y with (s0 := owner) (s1 := s3) (eq_site_dec := eq_site_dec). rewrite new_sigma2_sigma2_but_x_y with (s0 := owner) (s1 := s3) (eq_site_dec := eq_site_dec). unfold new_sigma2_but_table in |- *. rewrite post_here. unfold termination_q_count in |- *; simpl in |- *. rewrite collect_elsewhere. rewrite new_sigma2_sigma2_but_x_y with (s0 := s1) (s1 := owner) (eq_site_dec := eq_site_dec). rewrite new_sigma2_sigma2_but_x_y with (s0 := s1) (s1 := owner) (eq_site_dec := eq_site_dec). unfold new_sigma2_but_table in |- *. case (eq_site_dec s1 owner); intro. generalize e; rewrite e0. rewrite empty_q_to_me; simpl in |- *. intro; discriminate. auto. rewrite post_elsewhere. rewrite collect_here. rewrite reduce_first_out with (m := inc_dec s3). apply add_reduce19. unfold sigma2_table in |- *. apply sigma_table_simpl. apply funct_eq. intro. unfold sigma_table in |- *. apply sigma_simpl. intros. case (eq_site_dec e0 s1); intro. case (eq_site_dec x owner); intro. auto. case (eq_site_dec e0 owner); intro. case (eq_site_dec x s3); intro. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. case (eq_site_dec e0 owner); intro. case (eq_site_dec x s3); intro. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. unfold termination_count in |- *; simpl in |- *. omega. auto. auto. apply finite_site. apply finite_site. apply finite_site. apply finite_site. left; unfold not in |- *; intro. generalize e; rewrite H1; rewrite empty_q_to_me. simpl in |- *; intro; discriminate. auto. apply finite_site. apply finite_site. apply finite_site. apply finite_site. apply add_reduce15. rewrite new_sigma2_sigma2_but_x_y with (s0 := s2) (s1 := s1) (eq_site_dec := eq_site_dec). rewrite new_sigma2_sigma2_but_x_y with (s0 := s2) (s1 := s1) (eq_site_dec := eq_site_dec). unfold new_sigma2_but_table in |- *. rewrite post_here. unfold termination_q_count in |- *; simpl in |- *. rewrite collect_elsewhere. rewrite new_sigma2_sigma2_but_x_y with (s0 := s1) (s1 := s2) (eq_site_dec := eq_site_dec). rewrite new_sigma2_sigma2_but_x_y with (s0 := s1) (s1 := s2) (eq_site_dec := eq_site_dec). unfold new_sigma2_but_table in |- *. case (eq_site_dec s1 s2); intro. generalize e0; rewrite e1; rewrite empty_q_to_me; simpl in |- *. intro; discriminate. auto. rewrite post_elsewhere. rewrite collect_here. rewrite reduce_first_out with (m := copy). apply add_reduce19. unfold sigma2_table in |- *. apply sigma_table_simpl. apply funct_eq. intro. unfold sigma_table in |- *. apply sigma_simpl. intros. case (eq_site_dec e1 s1); intro. case (eq_site_dec x s2); intro. auto. case (eq_site_dec e1 s2); intro. case (eq_site_dec x s1); intro. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. case (eq_site_dec e1 s2); intro. case (eq_site_dec x s1); intro. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. unfold termination_count in |- *; simpl in |- *. omega. auto. auto. apply finite_site. apply finite_site. apply finite_site. apply finite_site. left; unfold not in |- *; intro. generalize e0; rewrite H1; rewrite empty_q_to_me; simpl in |- *. intro; discriminate. auto. apply finite_site. apply finite_site. apply finite_site. apply finite_site. rewrite sigma2_sigma2_but_x_y with (s0 := owner) (s1 := s2) (eq_site_dec := eq_site_dec). rewrite collect_here. unfold termination_q_count in |- *. rewrite reduce_first_out with (m := copy). unfold sigma_table in |- *. rewrite (sigma_sigma_but Site s2 eq_site_dec). unfold Z_id in |- *. rewrite sigma2_sigma2_but_x_y with (s0 := owner) (s1 := s2) (eq_site_dec := eq_site_dec). apply add_reduce11. rewrite (sigma_sigma_but Site s2 eq_site_dec). rewrite e; unfold termination_rt_count in |- *. simpl in |- *. apply add_reduce12. apply sigma_but_simpl. intros. unfold Set_rec_table in |- *. cut (change_site bool (rt c) s2 true s = rt c s). intro. rewrite H2. auto. rewrite other_site. auto. auto. apply finite_site. apply sigma2_but_simpl2. intros. case (eq_queue_dec owner x s2 y); intro. elim H1; decompose [and] a. split; auto. rewrite collect_elsewhere. auto. auto. apply finite_site. apply finite_site. unfold termination_rt_count in |- *; unfold Set_rec_table in |- *. unfold termination_count in |- *; simpl in |- *. cut (change_site bool (rt c) s2 true s2 = true). intro. rewrite H1. omega. rewrite that_site; auto. apply finite_site. apply finite_site. apply finite_site. auto. apply finite_site. apply finite_site. unfold sigma_table in |- *. rewrite (sigma_sigma_but Site s2 eq_site_dec). unfold Z_id in |- *. rewrite new_sigma2_sigma2_but_x_y with (s0 := s2) (s1 := owner) (eq_site_dec := eq_site_dec). rewrite new_sigma2_sigma2_but_x_y with (s0 := s2) (s1 := owner) (eq_site_dec := eq_site_dec). unfold new_sigma2_but_table in |- *. rewrite post_here. unfold termination_q_count in |- *; simpl in |- *. rewrite collect_elsewhere. rewrite new_sigma2_sigma2_but_x_y with (s0 := s1) (s1 := s2) (eq_site_dec := eq_site_dec). rewrite new_sigma2_sigma2_but_x_y with (s0 := s1) (s1 := s2) (eq_site_dec := eq_site_dec). unfold new_sigma2_but_table in |- *. case (eq_site_dec s1 s2); intro. generalize e0; rewrite e1; rewrite empty_q_to_me; simpl in |- *. intro; discriminate. auto. rewrite post_elsewhere. rewrite collect_here. rewrite reduce_first_out with (m := copy). rewrite (sigma_sigma_but Site s2 eq_site_dec). apply add_reduce22. unfold sigma2_table in |- *. apply sigma_table_simpl. apply funct_eq. intro. unfold sigma_table in |- *. apply sigma_simpl. intros. case (eq_site_dec e1 s1); intro. case (eq_site_dec x s2); intro. auto. case (eq_site_dec e1 s2); intro. case (eq_site_dec x owner); intro. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. case (eq_site_dec e1 s2); intro. case (eq_site_dec x owner); intro. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. rewrite post_elsewhere. rewrite collect_elsewhere; auto. auto. apply sigma_but_simpl. intros. unfold Set_rec_table in |- *; rewrite other_site. auto. auto. unfold Set_rec_table in |- *; rewrite that_site. rewrite e. unfold termination_rt_count in |- *. cut (termination_count copy > 4)%Z. intro. omega. simpl in |- *. omega. apply finite_site. auto. auto. apply finite_site. apply finite_site. apply finite_site. apply finite_site. left; unfold not in |- *; intro; generalize e0. rewrite H1; rewrite empty_q_to_me. simpl in |- *; intro; discriminate. auto. apply finite_site. apply finite_site. apply finite_site. apply finite_site. apply finite_site. rewrite sigma2_sigma2_but_x_y with (s0 := s) (s1 := owner) (eq_site_dec := eq_site_dec). rewrite post_here. rewrite sigma2_sigma2_but_x_y with (s0 := s) (s1 := owner) (eq_site_dec := eq_site_dec). unfold termination_q_count in |- *. simpl in |- *. unfold sigma_table in |- *. rewrite (sigma_sigma_but Site s eq_site_dec). unfold Z_id in |- *. unfold sigma_table in |- *. rewrite (sigma_sigma_but Site s eq_site_dec). apply add_reduce14. apply sigma_but_simpl. intros. unfold Reset_rec_table in |- *. rewrite other_site. auto. auto. apply sigma2_but_simpl2. intros. case (eq_queue_dec s x owner y); intro. elim H1; decompose [and] a. split; auto. rewrite post_elsewhere; auto. apply finite_site. apply finite_site. unfold Reset_rec_table in |- *; rewrite that_site. rewrite e0. unfold termination_rt_count in |- *; simpl in |- *. omega. apply finite_site. apply finite_site. apply finite_site. apply finite_site. apply finite_site. apply finite_site. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8