Require Export DistributedReferenceCounting.machine1.machine.
Require Export DistributedReferenceCounting.machine1.cardinal.
Require Export DistributedReferenceCounting.machine1.comm.

Section INVARIANT1.

Lemma invariant1_init :
 sigma_send_table send_init =
 (sigma_receive_table rec_init + sigma_weight bag_init)%Z.
Proof.
  unfold send_init, rec_init, bag_init in |- ×.
  unfold sigma_send_table, sigma_receive_table, sigma_weight in |- ×.
  unfold sigma_table in |- ×.
  simpl in |- ×.
  rewrite sigma_null.
  replace
   (sigma2_table Site LS LS (queue Message) (fun _ _ : Site ⇒ cardinal)
      (fun _ _ : Site ⇒ empty Message)) with 0%Z.
  omega.

  unfold sigma2_table in |- ×.
  unfold sigma_table in |- ×.
  symmetry in |- ×.
  simpl in |- ×.
  rewrite sigma_null.
  apply sigma_null.
Qed.

Lemma invariant1_inductive :
 ∀ (c : Config) (t : class_trans c),
 legal c →
 sigma_send_table (st c) =
 (sigma_receive_table (rt c) + sigma_weight (bm c))%Z →
 sigma_send_table (st (transition c t)) =
 (sigma_receive_table (rt (transition c t)) +
  sigma_weight (bm (transition c t)))%Z.

Proof.
  simple induction t.


  intros; simpl in |- ×.
  rewrite sigma_weight_post_message.
  rewrite sigma_inc_send_table.
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- ×.
  rewrite H0; omega.


  intros; simpl in |- ×.
  rewrite (sigma_weight_collect_message dec).
  rewrite sigma_dec_send_table.
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- ×.
  rewrite H0; omega.
  auto.


  intros; simpl in |- ×.
  rewrite sigma_weight_post_message.
  rewrite sigma_inc_send_table.
  rewrite sigma_weight_collect_message with (m := inc_dec s3).
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- ×.
  rewrite H0; omega.
  auto.


  intros; simpl in |- ×.
  rewrite sigma_weight_post_message.
  rewrite sigma_weight_collect_message with (m := copy).
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- ×.
  rewrite H0; omega.
  auto.


  intros; simpl in |- ×.
  rewrite sigma_weight_collect_message with (m := copy).
  rewrite sigma_set_receive_table.
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- ×.
  rewrite H0; omega.
  auto.
  auto.


  intros; simpl in |- ×.
  rewrite sigma_weight_post_message.
  rewrite sigma_weight_collect_message with (m := copy).
  rewrite sigma_set_receive_table.
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- ×.
  rewrite H0; omega.
  auto.
  auto.


  intros; simpl in |- ×.
  rewrite sigma_weight_post_message.
  rewrite sigma_reset_receive_table.
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- ×.
  rewrite H0; omega.
  auto.
Qed.

Lemma invariant1 :
 ∀ c : Config,
 legal c →
 sigma_send_table (st c) =
 (sigma_receive_table (rt c) + sigma_weight (bm c))%Z.
Proof.
  intros.
  elim H.
  apply invariant1_init.
  exact invariant1_inductive.
Qed.

End INVARIANT1.