(****************************************************************************************************)
(***************************************        Soundness       *************************************)
(****************************************************************************************************)
Require Export syntax.
Require Export configurations.
Require Export auxiliary_functions.
Require Export static_semantics.
Require Export dynamic_semantics.

Section preservation_theorem.

Lemma successors_are_lt : forall x y : nat, 
  x < y -> 
  S x < S y.
Proof.
intros. induction H. 
Focus 1. unfold lt. auto.
Focus 1. unfold lt. auto.
Qed.

Lemma len_store_con : forall A (r : A) H, 
  length(H) < length (H ++ (r :: nil)).
Proof.
intros.
induction H. simpl. auto.
simpl. apply successors_are_lt. assumption.
Qed.

Lemma nth_store_con : forall A (r : A) H default,
  r = nth (length H) (H ++ (r :: nil)) default.
Proof.
intros.
induction H. 
Focus 1. simpl. reflexivity.
simpl. apply IHlist.
Qed.

Lemma val_env_independent : forall v Gamma H T beta omega, 
  val_b v ->
  has_type_b empty H v T beta omega ->
  has_type_b Gamma H v T beta omega.
Proof.
intros. inversion H0.
Focus 1. replace v with (loc_exp_b l) in H1. inversion H1.
  Focus 1. apply has_type_b_loc_act with (S:=S) (beta_list':=beta_list') 
  (C:=C) (ln:=ln) (default:=default). auto. auto. auto. auto.
  Focus 1. apply has_type_b_loc_fut with (v:=v0) (ln:=ln) (default:=default).
  auto. auto. auto.
Focus 1. replace v with (null_exp_b) in H1. inversion H1.
  apply has_type_b_null.
Focus 1. replace v with (unresl_exp_b) in H1. inversion H1.
  apply has_type_b_unresl.
Qed.

Lemma val_typed_in_empty : forall v Gamma H T beta omega,
  val_b v -> 
  has_type_b Gamma H v T beta omega -> 
  has_type_b empty H v T beta omega.
Proof.
intros. inversion H0.
Focus 1. replace v with (loc_exp_b l) in H1. inversion H1.
  Focus 1. apply has_type_b_loc_act with (S:= S) (beta_list':=beta_list')
  (C:=C) (ln:=ln) (default:=default). auto. auto. auto. auto.
  Focus 1. apply has_type_b_loc_fut with (v:=v0) (ln:=ln) (default:=default).
  auto. auto. auto.
Focus 1. replace v with (null_exp_b) in H1. inversion H1.
  apply has_type_b_null.
Focus 1. replace v with (unresl_exp_b) in H1. inversion H1.
  apply has_type_b_unresl.
Qed.

Lemma st_env_independent : forall s Gamma Gamma' H T beta omega, 
  has_type_b Gamma H (st_read_exp_b s) T beta omega -> 
  has_type_b Gamma' H (st_read_exp_b s) T beta omega.
Proof.
intros. inversion H0. apply has_type_b_read with (v:=v) (S:=S) 
  (beta:=beta0) (n:=n) (C:=C) (beta_list':=beta_list') 
  (default_S:=default_S) (default_b:=default_b); auto.
Qed.

Lemma id_env_weakening : 
  forall Gamma, 
  env_weakening Gamma Gamma.
Proof. 
intros. eapply environment_weakening. intros; auto.
Qed.

Inductive beta_equiv : Gamma_env -> beta_ty_var -> beta_ty_var -> Prop :=
  | beta_equivalent : forall Gamma beta1 beta2,
    (forall H x T e' T' beta' omega',
    has_type_b (update Gamma x (T, Gamma_snd_beta beta1)) 
      H e' T' beta' omega' -> 
    has_type_b (update Gamma x (T, Gamma_snd_beta beta2)) 
      H e' T' beta' omega' )-> 
    beta_equiv Gamma beta1 beta2.

Inductive omega_subset : omega_bhvr -> omega_bhvr -> Prop := 
  | omega_subset_eq : forall omega' omega,
    omega' = omega -> 
    omega_subset omega' omega
  | omega_subset_union : forall omega' omega omega1 omega2,
    omega = union_omega_bhvr omega1 omega2 -> 
    (omega_subset omega' omega1) \/ (omega_subset omega' omega2) -> 
    omega_subset omega' omega
  | omega_subset_hpns_bfr1 : forall omega' omega omega1 omega2,
    omega = (hpns_bfr_omega_bhvr omega1 omega2) ->
    (omega_subset omega' omega1) \/ (omega_subset omega' omega2) -> 
    omega_subset omega' omega
  | omega_subset_hpns_bfr2 : forall omega' omega omega1 omega2 omega1' omega2',
    omega = (hpns_bfr_omega_bhvr omega1 omega2) -> 
    omega' = (hpns_bfr_omega_bhvr omega1' omega2') -> 
    omega_subset omega1' omega1 -> 
    omega_subset omega2' omega2 -> 
    omega_subset omega' omega
  | omega_subset_ctxt1 : forall omega' omega omega1 delta,
    omega = (ctxt_omega_bhvr omega1 delta) -> 
    omega_subset omega' omega1 ->
    omega_subset omega' omega
  | omega_subset_ctxt2 : forall omega' omega omega1 omega1' delta,
    omega = (ctxt_omega_bhvr omega1 delta) -> 
    omega' = (ctxt_omega_bhvr omega1' delta) -> 
    omega_subset omega1' omega1 -> 
    omega_subset omega' omega
  | omega_subset_flow : forall omega' omega beta1 beta2 beta1' beta2' Gamma,
    omega' = (theta_bhvr_omega_bhvr (flow_theta_bhvr beta1' beta2')) -> 
    omega = (theta_bhvr_omega_bhvr (flow_theta_bhvr beta1 beta2)) -> 
    (beta1' = beta1) \/ (beta_equiv Gamma beta1 beta1') -> 
    (beta2' = beta2) \/ (beta_equiv Gamma beta2 beta2') -> 
    omega_subset omega' omega
  | omega_subset_empty : forall omega' omega,
    omega' = empty_omega_bhvr -> 
    omega_subset omega' omega.

Hypothesis safe_store_update : forall e' Q Phi l G V H e'' Phi' G' V' H'
    Gamma e T beta omega,
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((e') :: Q) Phi l) G (V, H))
    (add_glbl_cnfg (act_cnfg ((e'') :: Q) Phi' l) G' (V', H'))-> 
    has_type_b Gamma H e T beta omega -> 
    has_type_b Gamma H' e T beta omega.

Hypothesis beta_aliasing : forall e' Q Phi l G V H e'' Phi' G' V' H'
    Gamma T beta omega Gamma' beta' omega',
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((e') :: Q) Phi l) G (V, H))
    (add_glbl_cnfg (act_cnfg ((e'') :: Q) Phi' l) G' (V', H'))-> 
    has_type_b Gamma H e' T beta omega -> 
    has_type_b Gamma' H' e'' T beta' omega' -> 
    beta_equiv Gamma beta beta' /\ beta_equiv Gamma' beta beta'.

Theorem preservation : 
  forall Gamma e T beta omega Q Phi l G H V e' Phi' G' H',
  has_type_b Gamma H e T beta omega ->
  step_dyn
  (add_glbl_cnfg (act_cnfg (e :: Q) Phi l) G (V, H))
  (add_glbl_cnfg (act_cnfg (e' :: Q) Phi' l) G' (V, H')) ->
  wellformed_GVH Gamma V H e ->
  (exists Gamma' beta' omega', has_type_b Gamma' H' e' T beta' omega'
  /\ omega_subset omega' omega
  /\ env_weakening Gamma Gamma')
  \/ val_b e.
Proof with eauto.
intros Gamma e T beta omega Q Phi l G H V e' Phi' G' H' Ht.
generalize dependent e'. induction Ht.

(*case of variable expression*)
Focus 8. intros. inversion H1. Focus 1. left. exists Gamma. exists null_beta_ty_var. 
  exists empty_omega_bhvr. split. apply has_type_b_null. 
  split. apply omega_subset_empty. reflexivity. apply id_env_weakening.

(*case of unresolved expression*)
Focus 13. intros. right. apply unresl_val_b.

(*case of location expression*)
Focus 12. intros. right. apply loc_val_b.
Focus 11. intros. right. apply loc_val_b.

(*case of null expression*)
Focus 8. intros. right. apply null_val_b.

(*case of invocation expression*)
Focus 1. intros. inversion H9. Focus 1. left. exists Gamma.
  exists (fut_beta_ty_var beta''' beta''''). exists empty_omega_bhvr.
  split. eapply has_type_b_loc_fut with (v := unresl_exp_b). apply H36.
  replace H' with (H ++ fut_record beta''' beta'''' T'0 unresl_exp_b :: nil).
  apply len_store_con.
  replace H' with (H ++ fut_record beta''' beta'''' T'0 unresl_exp_b :: nil).
  replace T with T'0. apply nth_store_con.
  inversion H0. destruct H51 with (m_name:=m_name) (C1:=C) (T1:=T) 
  (tv_list1:=tv_list) (e1:=e) (C2:=C0) (T2:=T'0) (tv_list2:=tv_list0)
  (e2:=e0). assumption. inversion H30. assumption. destruct H53.
  symmetry. assumption. split.
  apply omega_subset_empty. reflexivity. apply id_env_weakening.

(*case of new act expression*)
Focus 3. intros. inversion H8. Focus 1. left. 
  exists Gamma. exists (act_beta_ty_var C). exists empty_omega_bhvr.
  split. eapply has_type_b_loc_act with (beta_list' := beta_list') 
  (C := C) (S := S). replace l' with (Id (length(H))).
  eexists. replace H' with 
  (H ++ act_record (act_beta_ty_var C) beta_list' C S :: nil).
  apply len_store_con. replace H' with 
  (H ++ act_record (act_beta_ty_var C) beta_list' C S :: nil).
  apply nth_store_con. reflexivity. split. apply omega_subset_empty.
  reflexivity. apply id_env_weakening.

(*case of new future expression*)
Focus 2. intros. inversion H0. Focus 1. left. exists Gamma. 
  exists (fut_beta_ty_var beta beta'). exists empty_omega_bhvr. split. 
  eapply has_type_b_loc_fut with (v:=v) (ln:=(length H)).
  auto. replace H' with 
  (H ++ fut_record beta beta' (fut_val_ty T) v :: nil).
  apply len_store_con. replace H' with 
  (H ++ fut_record beta beta' (fut_val_ty T) v :: nil). 
  apply nth_store_con. split. apply omega_subset_empty. reflexivity.
  apply id_env_weakening.

(*case of context expression*)
Focus 5. intros. inversion H3. Focus 1. left. exists Gamma.
  exists beta'. exists omega'. split. replace e' with e.
  replace H' with H. auto. split. apply omega_subset_ctxt1 with omega' delta.
  assumption. apply omega_subset_eq. reflexivity. apply id_env_weakening.
  Focus 1. left. assert (Hstp : step_dyn (add_glbl_cnfg (act_cnfg (e :: Q) Phi l) G (V, H))
  (add_glbl_cnfg (act_cnfg (e'' :: Q) Phi' l) G' (V, H'))). auto. 
  apply IHHt2 in Hstp. inversion Hstp as [HstpA | HstpB]. 
  Focus 1. inversion HstpA as [Gamma' Hstp2].
  inversion Hstp2 as [beta'' Hstp3]. inversion Hstp3 as [omega'' Hstp4].
  inversion Hstp4 as [Hstp4' Hstp4'']. inversion Hstp4'' as [Hstp4''' Hstp4''''].
  exists Gamma'. exists beta''. exists (ctxt_omega_bhvr omega'' delta). 
  split. apply has_type_b_ctxt with (omega':=omega'') (delta:=delta) 
  (Delta:=Delta) (Delta':=Delta') (beta:=beta).
  apply safe_store_update with (e':=e) (Q:=Q) (Phi:=Phi) (l:=l) 
  (G:=G) (V:=V) (H:=H) (e'':= e'') (Phi':=Phi') (G':=G') (V':=V) (H':=H')
  (Gamma:=Gamma') (e:=(loc_exp_b l0)) (T:=(act_val_ty C))
  (beta:=beta) (omega:=empty_omega_bhvr). auto. apply val_env_independent. 
  apply loc_val_b. apply val_typed_in_empty with Gamma. apply loc_val_b.
  auto.
  assumption. assumption. assumption. reflexivity.
  split.
  apply omega_subset_ctxt2 with (delta:=delta) (omega1:=omega')
  (omega1':=omega''). assumption. reflexivity.
  assumption. auto.
  Focus 1. contradict HstpB. intros; auto.
  inversion H4; auto.

(*case of resolution expression*)
Focus 5. intros. inversion H0. 
  Focus 1. left. replace e' with e. exists Gamma. exists beta. exists omega.
  split. 
  apply safe_store_update with (e':=resl_exp_b l0 e) (Q:=Q) (Phi:=Phi) (l:=l) 
  (G:=G) (V:=V) (H:=H) (e'':= e') (Phi':=Phi') (G':=G') (V':=V) (H':=H')
  (Gamma:=Gamma) (e:=e) (T:=T)
  (beta:=beta) (omega:=omega).
  auto. auto.
  split. apply omega_subset_eq. reflexivity. apply id_env_weakening.
  Focus 1. 
  assert (Hstp :  step_dyn (add_glbl_cnfg (act_cnfg (e :: Q) Phi l) G (V, H))
  (add_glbl_cnfg (act_cnfg (e'' :: Q) Phi' l) G' (V, H'))).
  auto. apply IHHt in Hstp. inversion Hstp as [HstpA | HstpB]. 
  Focus 1. left.
  inversion HstpA as [Gamma' Hstp2].
  inversion Hstp2 as [beta' Hstp3]. inversion Hstp3 as [omega' Hstp4].
  inversion Hstp4 as [Hstp4' Hstp4'']. 
  exists Gamma'. exists beta'. exists omega'.
  split. apply has_type_b_resl. auto. auto. 
  Focus 1. left. contradict HstpB. intros. auto.
  inversion H1; auto.

(*case of state write expression*)
Focus 2. intros. inversion H0. 
  Focus 1. left. exists Gamma. exists beta'. exists omega. split.
  replace e' with e.
  apply safe_store_update with (e':=st_asgn_exp_b s e) (Q:=Q) (Phi:=Phi) (l:=l) 
  (G:=G) (V:=V) (H:=H) (e'':= e') (Phi':=Phi') (G':=G') (V':=V) (H':=H')
  (Gamma:=Gamma) (e:=e) (T:=T)
  (beta:=beta') (omega:=omega).
  auto. auto.
  split. apply omega_subset_hpns_bfr1 with (omega1:=omega) 
  (omega2:= (theta_bhvr_omega_bhvr (flow_theta_bhvr beta' beta))).
  reflexivity. left. apply omega_subset_eq. reflexivity. apply id_env_weakening.
  Focus 1. 
  assert (Hstp :  step_dyn (add_glbl_cnfg (act_cnfg (e :: Q) Phi l) G (V, H))
  (add_glbl_cnfg (act_cnfg (e'0 :: Q) Phi' l) G' (V, H'))).
  auto. apply IHHt2 in Hstp. inversion Hstp as [HstpA | HstpB].
  Focus 1. left.
  inversion HstpA as [Gamma' Hstp2].
  inversion Hstp2 as [beta'' Hstp3]. inversion Hstp3 as [omega' Hstp4].
  inversion Hstp4 as [Hstp4' Hstp4''].
  exists Gamma'. exists beta. exists (hpns_bfr_omega_bhvr omega'
  (theta_bhvr_omega_bhvr (flow_theta_bhvr beta'' beta))).
  split. apply has_type_b_asgn.
  apply st_env_independent with (Gamma:=Gamma).
  apply safe_store_update with (e':=e) (Q:=Q) (Phi:=Phi) (l:=l) 
  (G:=G) (V:=V) (H:=H) (e'':= e'0) (Phi':=Phi') (G':=G') (V':=V) (H':=H')
  (Gamma:=Gamma) (e:=st_read_exp_b s) (T:=T)
  (beta:=beta) (omega:=empty_omega_bhvr). 
  auto. auto.
  auto. assert (Hbe : beta_equiv Gamma beta' beta'' 
  /\ beta_equiv Gamma' beta' beta''). eapply beta_aliasing.
  apply H15. apply Ht2. apply Hstp4'. split.
  eapply omega_subset_hpns_bfr2. eexists. eexists. 
  inversion Hstp4'' as [Hstp4''' Hstp4'''']. auto.
  eapply omega_subset_flow. eexists. eexists. right.
  inversion Hbe as [Hbe' Hbe'']. apply Hbe'. left. reflexivity.
  apply Hstp4''.
  Focus 1. contradict HstpB. intros; auto.
  inversion H1. auto.

(*case of state read expression*)
Focus 3. intros. inversion H6. inversion H5. assert (He' : 
  (In (act_record B B_list C0 S0) H) /\ 
  (n0 < length S0) /\ ((state_decl T_tmp s, e') = nth n0 S0 default)).
  split. replace H with H'. auto. split. auto. auto.
  apply H9 in He'.
  assert (Hv : 
  In (act_record B B_list C0 S0) H /\
  n0 < length S0 /\
  (state_decl T_tmp s, e') = nth n0 S0 default /\
  In (act_record beta beta_list' C S) H /\
  n < length S /\ 
  (state_decl T s, v) = nth n S default_S ). split; try(repeat split). 
  replace H with H'. auto. auto. auto. auto. auto. auto.
  apply H13 in Hv. inversion He'. inversion Hv. inversion H33. 
  Focus 1. left.
  exists Gamma. exists beta'0. exists empty_omega_bhvr.
  split. replace T with T_tmp. replace H' with H.
  apply val_env_independent. auto. auto. split.
  apply omega_subset_empty. reflexivity. apply id_env_weakening.

(*case of wait expression*)
Focus 1. intros. inversion H0. inversion H1. 
  assert (Hve : lookup_var_loc V x (loc_exp_b l') /\
  lookup_var_loc V x (loc_exp_b l'0) /\
  l' = Id ln' /\
  l'0 = Id ln'0 /\
  fut_record beta0 beta'0 T0 e' = nth ln' H default /\
  fut_record beta1 beta'1 T1 v0 = nth ln'0 H default0).
  split. auto. split. auto. split. auto. split. auto.
  split. replace H with H'. auto. auto. apply H29 in Hve.
  replace e' with v0. apply H33 in Ht.
  Focus 1. left.
  exists Gamma. exists beta''. exists empty_omega_bhvr.
  replace H' with H. split. auto. split. apply omega_subset_empty.
  reflexivity. apply id_env_weakening.

(*case of let expression*)
Focus 1. intros. inversion H0. Focus 1. left.
  exists (update Gamma x (T', Gamma_snd_beta beta')).
  exists beta''. exists omega'. split. replace H' with H.
  replace e'0 with e''. auto. split.
  apply omega_subset_hpns_bfr1 with omega omega'. reflexivity.
  right. apply omega_subset_eq. reflexivity.
  inversion H1. assert (HType_e : has_type_b Gamma H e' T' beta' omega); auto.
  apply H27 in HType_e. auto.
  Focus 1. assert (Hstp : 
  step_dyn (add_glbl_cnfg (act_cnfg (e' :: Q) Phi l) G (V, H))
  (add_glbl_cnfg (act_cnfg (e''0 :: Q) Phi' l) G' (V, H'))).
  auto. apply IHHt1 in Hstp. inversion Hstp as [HstpA | HstpB].
  Focus 1. left.
  inversion HstpA as [Gamma' Hstp1]. inversion Hstp1 as [beta''' Hstp2]. 
  inversion Hstp2 as [omega'' Hstp3]. inversion Hstp3 as [Hstp3' Hstp3''].
  inversion Hstp3'' as [Hstp3''' Hstp3'''']. exists Gamma'. exists beta''. 
  exists (hpns_bfr_omega_bhvr omega'' omega').
  split. apply has_type_b_let with T' beta'''.
  auto.
  inversion H1. assert (Hwk : env_weakening (update Gamma x (T', Gamma_snd_beta beta''')) 
  (update Gamma' x (T', Gamma_snd_beta beta'''))). apply H28; auto. 
  inversion Hwk. apply H29. eapply safe_store_update with (H:=H).
  apply H0. 
  assert (Hbe : beta_equiv Gamma beta' beta''' /\ beta_equiv Gamma' beta' beta'''). 
  eapply beta_aliasing with (e':=e') (e'':=e''0). 
  apply H16. apply Ht1. apply Hstp3'.
  inversion Hbe as [Hbe' Hbe'']. inversion Hbe'. apply H32. auto. auto.
  split.
  apply omega_subset_hpns_bfr2 with (omega1:=omega) 
  (omega2:=omega') (omega1':=omega'') (omega2':=omega').
  reflexivity. reflexivity.
  auto. apply omega_subset_eq. reflexivity. auto.
  Focus 1. contradict HstpB. intros; auto.
  inversion H1. auto.

(*miscellaneous shelved goals*)
Unshelve. auto. 
  apply (act_record (act_beta_ty_var C) beta_list' C S).
  apply ( fut_record beta beta' (fut_val_ty T) v).
Qed.

End preservation_theorem.

Section progress_theorem.

(* This lemma states that if a mapping and store are wellformed as defined by 
wellformed_GVH then they are also wellformed as defined by wellformed_V *)
Lemma wellformedness_implies : 
  forall Gamma V H e, 
  wellformed_GVH Gamma V H e -> 
  wellformed_V V H e.
Proof.
intros. induction e; inversion H0.
Focus 9. apply wellformed_V_null.
Focus 9. apply wellformed_V_loc.
Focus 8. apply wellformed_V_var.
Focus 9. apply wellformed_V_resl; eauto.
Focus 8. apply wellformed_V_ctxt; eauto.
Focus 1. eapply wellformed_V_inv; eauto.
Focus 2. eapply wellformed_V_fut; eauto.
Focus 1. eapply wellformed_V_act; eauto.
Focus 3. apply wellformed_V_asgn; auto.
Focus 2. apply wellformed_V_let; auto.
Focus 2. apply wellformed_V_read.
Focus 1. eapply wellformed_V_wait; eauto.
Qed.

Theorem progress :
  forall Gamma e T beta omega Q Phi l G H V, 
  has_type_b Gamma H e T beta omega ->
  wellformed_V V H e ->
  (val_b e) \/ ~ (val_b e) /\
  (exists e' Phi' G' H' V',
  step_dyn 
  (add_glbl_cnfg (act_cnfg (e :: Q) Phi l) G (V, H))
  (add_glbl_cnfg (act_cnfg (e' :: Q) Phi' l) G' (V', H'))). 
Proof with eauto.
intros. induction H0; subst.

(*case of null expression*)
Focus 9. left. apply null_val_b.

(*case of loc expression*)
Focus 11. left. apply loc_val_b.
Focus 11. left. apply loc_val_b.

(*case of unresolved expression*)
Focus 11. left. apply unresl_val_b.

(*case of variable expression*)
Focus 8. right. split. Focus 1. intro Hval; inversion Hval.
  repeat eexists. apply step_dyn_XCPT_var.

(*case of new future expression*)
Focus 3. right. split. Focus 1. intro Hval; inversion Hval. 
  eexists. exists Phi. exists G. inversion H1.
  exists (H ++ (fut_record beta beta' (fut_val_ty T) v) :: nil). 
  exists V. apply step_dyn_fut with v. apply H7. apply H10. eexists.
  reflexivity. 

(*case of new activity expression*)
Focus 3. right. split. Focus 1. intro Hval; inversion Hval. 
  inversion H1. eexists. eexists. eexists.
  exists (H ++ act_record (act_beta_ty_var C) beta_list' C
  (new_act_st_map st_list v_list0) :: nil). eexists.
  eapply step_dyn_act with (v_list := v_list0). apply H12.
  eexists. apply H0. eexists. eexists. reflexivity.
  eexists. eexists. eexists. eexists.

(*case of invocation expression*)
Focus 1. right. split. Focus 1. intro Hval; inversion Hval. 
  inversion H1. repeat eexists.
  eapply step_dyn_inv with (l' := l') (ln' := ln') (beta' := beta'0)
  (beta_list'' := beta_list''0) (C := C0) (S := S) (default_H := default_H)
  (m_name := m_name) (T' := T0) (tv_list := tv_list0) (e := e0). 
  apply H11. apply H14. apply H15. apply H17. apply H16. 
  eexists. eexists. eexists. eexists. eexists. eexists.
  eexists. eexists. eexists. eexists. eexists. eexists.
  eexists. eexists.

(*case of context expression*)
Focus 5. destruct IHhas_type_b2. Focus 1. inversion H1. auto.
  Focus 1. right. split. Focus 1. intro Hval; inversion Hval.
  repeat eexists. eapply step_dyn_ctxt. apply H0.
  Focus 1. right. split. Focus 1. intro Hval; inversion Hval. 
  inversion H0. inversion H3. inversion H4. 
  inversion H5. inversion H6. inversion H7. 
  exists (ctxt_exp_b x l0 C m_name).
  exists x0. exists x1. exists x2. exists x3. apply step_dyn_ctxt_congr.
  auto. auto.

(*case of resolution expression*)
Focus 5. destruct IHhas_type_b. inversion H1. apply H6.
  Focus 1. right. split. Focus 1. intro Hval; inversion Hval. 
  destruct l0. repeat eexists. eapply step_dyn_resl.
  eexists. auto. eexists. eexists. eexists.
  Focus 1. right. split. Focus 1. intro Hval; inversion Hval. 
  inversion H2. inversion H4. inversion H5. 
  inversion H6. inversion H7. inversion H8. exists (resl_exp_b l0 x).
  exists x0. exists x1. exists x2. exists x3. apply step_dyn_resl_congr.
  auto. auto.

(*case of let expression*)
Focus 3. destruct IHhas_type_b1. inversion H1. auto.
  Focus 1. right. split. Focus 1. intro Hval; inversion Hval. 
  repeat eexists. eapply step_dyn_let.
  apply H0. inversion H1. auto.
  Focus 1. right. split. Focus 1. intro Hval; inversion Hval. 
  inversion H0. inversion H3. inversion H4. inversion H5.
  inversion H6. inversion H7. exists (let_exp_b x x0 e'').
  exists x1. exists x2. exists x3. exists x4. eapply step_dyn_let_congr.
  auto. auto.

(*case of wait expression*)
Focus 1. right. split. Focus 1. intro Hval; inversion Hval. 
  inversion H1. exists v. 
  exists ((sync_theta_bhvr (fut_beta_ty_var beta0 beta'0)) :: Phi).
  exists G. exists H. exists V. eapply step_dyn_wait with (l' := l') 
  (ln' := ln') (beta :=beta0) (beta' := beta'0) (T := T0) 
  (default := default). auto. auto. auto. auto. auto. auto. auto.

(*case of state read expression*)
Focus 2. right. split. Focus 1. intro Hval; inversion Hval. 
  repeat eexists. eapply step_dyn_read. 
  apply H0. apply H2. apply H3. auto.

(*case of state assignment expression*)
Focus 1. destruct l. destruct s. destruct IHhas_type_b2.
  Focus 1. inversion H1. auto.
  Focus 1. right. split. Focus 1. intro Hval; inversion Hval. 
  repeat eexists. eapply step_dyn_asgn.
  eexists. eexists. eexists. apply H0. apply H0_. eexists. eexists.
  Focus 1. right. split. Focus 1. intro Hval; inversion Hval. 
  inversion H0. inversion H3. inversion H4. inversion H5.
  inversion H6. inversion H7. exists (st_asgn_exp_b (Id n0) x).
  exists x0. exists x1. exists x2. exists x3. 
  eapply step_dyn_asgn_congr. auto. auto.

(*miscellaneous shelved goals*)
Unshelve. auto. auto. apply nil. auto. auto. auto. 
Qed.

End progress_theorem.

(************************************************* **************************************************)
(****************************************  Order Graph Syntax ***************************************)
(************************************************* **************************************************)

Fixpoint In_omega_theta (omega : omega_bhvr) (theta : theta_bhvr) : Prop := 
  match omega with 
    | empty_omega_bhvr => False
    | hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta') (theta_bhvr_omega_bhvr theta'') => (theta = theta') \/ (theta = theta'') 
    | hpns_bfr_omega_bhvr omega' omega'' => (In_omega_theta omega' theta) \/ (In_omega_theta omega'' theta)
    | theta_bhvr_omega_bhvr theta' => (theta = theta')
    | union_omega_bhvr omega' omega'' => (In_omega_theta omega' theta) \/ (In_omega_theta omega'' theta)
    | ctxt_omega_bhvr omega' delta => In_omega_theta omega' theta
  end.

Fixpoint In_omega_omega (omega : omega_bhvr) (omega_1 : omega_bhvr) : Prop := 
  match omega with 
    | empty_omega_bhvr => (empty_omega_bhvr = omega_1) 
    | hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta') (theta_bhvr_omega_bhvr theta'') => (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta') (theta_bhvr_omega_bhvr theta'')  = omega_1)
    | hpns_bfr_omega_bhvr omega' omega'' => ((hpns_bfr_omega_bhvr omega' omega'') = omega_1) \/ (In_omega_omega omega' omega_1) \/ (In_omega_omega omega'' omega_1)
    | theta_bhvr_omega_bhvr theta' => ((theta_bhvr_omega_bhvr theta') = omega_1)
    | union_omega_bhvr omega' omega'' => ((union_omega_bhvr omega' omega'') = omega_1) \/ (In_omega_omega omega' omega_1) \/ (In_omega_omega omega'' omega_1)
    | ctxt_omega_bhvr omega' delta => (omega' = omega_1) \/ (In_omega_omega omega' omega_1)
  end.

Definition Omega_grph := omega_bhvr.

Inductive Omega_jdgmt : Omega_grph -> omega_bhvr -> Prop := 
  | Omega_jdgmt_rflx : forall Omega beta, 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta beta))
  | Omega_jdgmt_flow_trans : forall Omega beta_1 beta_2 beta_3, 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_1 beta_2)) -> 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_2 beta_3)) -> 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_1 beta_3))
  | Omega_jdgmt_ctxt : forall Omega beta beta' delta, 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr (ctxt_theta_bhvr (flow_theta_bhvr beta beta') delta)) -> 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta beta'))
  | Omega_jdgmt_hapn_trans : forall Omega theta_1 theta_2 theta_3, 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) (theta_bhvr_omega_bhvr theta_2)) -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_2) (theta_bhvr_omega_bhvr theta_3)) -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) (theta_bhvr_omega_bhvr theta_3))
  | Omega_jdgmt_flow : forall Omega theta, 
    In_omega_theta Omega theta -> 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr theta)
  | Omega_jdgmt_hapn : forall Omega omega', 
    In_omega_omega Omega omega' -> 
    Omega_jdgmt Omega omega'.

Inductive mtype_b :delta_call -> omega_bhvr -> Prop := 
  | meth_type_b : forall omega C m_name T tv_list e alpha_list Delta' Delta
    beta_list e' Gamma T_e' beta_e' beta H,
    m_body C m_name (meth_decl T m_name tv_list e) -> 
    alpha_list = label e ->
    Delta' = d2s Delta H ->
    beta_list = refresh Delta' alpha_list H C 0 m_name ->
    e' = inv_e_replace e beta_list alpha_list ->
    has_type_b Gamma H e' T_e' beta_e' omega ->
    mtype_b (delta_decl beta C m_name) omega.

Inductive Omega_clsr : Omega_grph -> omega_bhvr -> omega_bhvr -> Prop := 
  | Omega_clsr_inv : forall Omega beta''' beta C omega theta beta' beta_list'' delta m_name, 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta''' beta)) -> 
    theta = inv_theta_bhvr beta beta' m_name beta_list'' -> 
    mtype_b (delta_decl beta C m_name) omega ->
    Omega_clsr Omega (theta_bhvr_omega_bhvr theta) (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (ctxt_omega_bhvr omega delta))
  | Omega_clsr_wait : forall Omega beta' beta,
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta' beta)) -> 
    Omega_clsr Omega (theta_bhvr_omega_bhvr (sync_theta_bhvr beta)) (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr (resl_theta_bhvr beta')) (theta_bhvr_omega_bhvr (sync_theta_bhvr beta)))
  | Omega_clsr_ctxt : forall Omega omega' omega'' delta, 
    Omega_clsr Omega omega' omega'' -> 
    Omega_clsr Omega (ctxt_omega_bhvr omega' delta) (ctxt_omega_bhvr omega'' delta).

Inductive Omega_msg_random : Omega_grph -> omega_bhvr -> Prop := 
  | Omega_message_random : forall Omega theta_1 theta_2 beta_1 beta_1' beta_1_list'' beta_2 beta_2' 
    beta_2_list'' omega_1 omega_2 omega m_name_1 m_name_2 omega_12 omega_21, 
    Omega =  omega -> 
    In_omega_theta omega theta_1 -> 
    In_omega_theta omega theta_2 -> 
    theta_1 = inv_theta_bhvr beta_1 beta_1' m_name_1 beta_1_list'' -> 
    theta_2 = inv_theta_bhvr beta_2 beta_2' m_name_2 beta_2_list'' -> 
    (Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_1 beta_2))) \/ (Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_2 beta_1))) -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) (theta_bhvr_omega_bhvr theta_2)) -> 
    Omega_clsr Omega (theta_bhvr_omega_bhvr theta_1) (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) (omega_1)) -> 
    Omega_clsr Omega (theta_bhvr_omega_bhvr theta_2) (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_2) (omega_2)) -> 
    ((omega_12 = omega_1) /\ (omega_21 = omega_2)) \/ ((omega_12 = omega_2) /\ (omega_21 = omega_1)) ->
    Omega_msg_random Omega (hpns_bfr_omega_bhvr (omega_12) (omega_21)).

Inductive Omega_msg_fifo : Omega_grph -> omega_bhvr -> Prop := 
  | Omega_message_fifo : forall Omega theta_1 theta_2 beta_1 beta_1' beta_1_list'' beta_2 beta_2' 
    beta_2_list'' omega_1 omega_2 omega m_name_1 m_name_2, 
    Omega =  omega -> 
    In_omega_theta omega theta_1 -> 
    In_omega_theta omega theta_2 -> 
    theta_1 = inv_theta_bhvr beta_1 beta_1' m_name_1 beta_1_list'' -> 
    theta_2 = inv_theta_bhvr beta_2 beta_2' m_name_2 beta_2_list'' -> 
    (Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_1 beta_2))) \/ (Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_2 beta_1))) -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) (theta_bhvr_omega_bhvr theta_2)) -> 
    Omega_clsr Omega (theta_bhvr_omega_bhvr theta_1) (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) (omega_1)) -> 
    Omega_clsr Omega (theta_bhvr_omega_bhvr theta_2) (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_2) (omega_2)) -> 
    Omega_msg_fifo Omega (hpns_bfr_omega_bhvr omega_1 omega_2).

Inductive Omega_msg_trans_fifo : Omega_grph -> omega_bhvr -> Prop := 
  | Omega_message_trans_fifo : forall Omega theta_1 theta_2 theta_3 beta_1 beta_1' beta_1_list'' beta_2 beta_2' 
    beta_2_list'' beta_3 beta_3' beta_3_list'' omega_1 omega_3 omega m_name_1 m_name_2 m_name_3, 
    Omega =  omega -> 
    In_omega_theta omega theta_1 -> 
    In_omega_theta omega theta_2 -> 
    In_omega_theta omega theta_3 ->
    theta_1 = inv_theta_bhvr beta_1 beta_1' m_name_1 beta_1_list'' -> 
    theta_2 = inv_theta_bhvr beta_2 beta_2' m_name_2 beta_2_list'' -> 
    theta_3 = inv_theta_bhvr beta_3 beta_3' m_name_3 beta_3_list'' -> 
    (Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_1 beta_3))) \/ (Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_3 beta_1))) -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) (theta_bhvr_omega_bhvr theta_2)) -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_2) (theta_bhvr_omega_bhvr theta_3)) -> 
    Omega_clsr Omega (theta_bhvr_omega_bhvr theta_1) (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) omega_1) -> 
    Omega_clsr Omega (theta_bhvr_omega_bhvr theta_3) (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_3) omega_3) -> 
    Omega_msg_trans_fifo Omega (hpns_bfr_omega_bhvr omega_1 omega_3).

Inductive Omega_race_free : Omega_grph -> Prop := 
  | race_free : forall Omega theta_1 theta_2 beta_1 beta_1' beta_1_list'' beta_2 beta_2' 
    beta_2_list'' omega m_name_1 m_name_2, 
    Omega =  omega -> 
    In_omega_theta omega theta_1 -> 
    In_omega_theta omega theta_2 -> 
    theta_1 = inv_theta_bhvr beta_1 beta_1' m_name_1 beta_1_list'' -> 
    theta_2 = inv_theta_bhvr beta_2 beta_2' m_name_2 beta_2_list'' -> 
    (Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_1 beta_2))) \/ (Omega_jdgmt Omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_2 beta_1))) -> 
    (Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) (theta_bhvr_omega_bhvr theta_2))) \/ (Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_2) (theta_bhvr_omega_bhvr theta_1))) -> 
    Omega_race_free Omega.

Inductive Omega_deadlock_free : Omega_grph -> Prop := 
  | deadlock_free : forall Omega omega theta_1 theta_2 beta_1 beta_2 case_1 case_2, 
    Omega =  omega -> 
    In_omega_theta omega theta_1 -> 
    In_omega_theta omega theta_2 -> 
    theta_1 = resl_theta_bhvr beta_1 -> 
    theta_2 = resl_theta_bhvr beta_2 -> 
    case_1 = Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_1) (theta_bhvr_omega_bhvr theta_2)) -> 
    case_2 = Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta_2) (theta_bhvr_omega_bhvr theta_1)) -> 
    (case_1 /\ (~ case_2)) \/ ((~ case_1) /\ case_2) -> 
    Omega_deadlock_free Omega.

Inductive Omega_well_formed : Omega_grph -> Prop := 
  | well_formed : forall Omega, 
    Omega_race_free Omega ->
    Omega_deadlock_free Omega -> 
    Omega_well_formed Omega.

(************************************************* **************************************************)
(****************************************  Behavior Soundness ***************************************)
(************************************************* **************************************************)

Section behavior_theorem.

Lemma list_add_neq: 
  forall theta (Phi : Phi_trace),
  Phi <> theta :: Phi.
Proof.
intros. induction Phi. 
  Focus 1. discriminate. 
  Focus 1. injection. intros. replace a with theta in H0. contradict H0.
  auto.
Qed.

Variable l0 : id.
Variable x_l0 : id.
Variable C0 : act_id.
Variable beta0 : beta_ty_var.
Variable MAIN_meth : meth_id.
Variable main_exp : exp_b.
Variable H0 : store.
Variable VM : var_val_map.
Variable l_ent : id.
Variable G0 : glbl_cnfg.
Variable Omega0 : Omega_grph.

Hypothesis def_loc_0 : l0 = Id 0.
Hypothesis def_main_exp : main_exp = inv_exp_b x_l0 beta0 MAIN_meth nil.
Hypothesis def_beta0 : beta0 = act_beta_ty_var C0.
Hypothesis def_H0 : H0 = (act_record beta0 nil C0 nil) :: nil.
Hypothesis def_VM : VM x_l0 = Some(loc_exp_b l0).
Hypothesis def_G0 : G0 = (add_glbl_cnfg 
                         (act_cnfg (main_exp :: nil) nil (l_ent))
                         empty_glbl_cnfg (VM, H0)).
Hypothesis def_Omega0 : Omega0 = 
                        (hpns_bfr_omega_bhvr 
                        (theta_bhvr_omega_bhvr (flow_theta_bhvr beta0 beta0))
                        (theta_bhvr_omega_bhvr 
                        (inv_theta_bhvr beta0 beta0 MAIN_meth nil))).

Inductive config_mstep : glbl_cnfg -> glbl_cnfg -> Prop :=
  | cmstep_refl : forall G, config_mstep G G
  | cmstep_trans1 : forall G G' G'', 
    step_dyn G G' -> 
    config_mstep G' G'' -> 
    config_mstep G G''
  | cmstep_trans2 : forall G G' G'' Psi VH,
    step_dyn G (add_glbl_cnfg Psi G' VH) -> 
    config_mstep G' G'' ->
    config_mstep G G''.

Inductive Omega_mclsr : Omega_grph -> Omega_grph -> Prop :=
  | Omclsr_refl : forall Omega, Omega_mclsr Omega Omega
  | Omclsr_trans : forall Omega Omega' Omega'',
    (forall omega1 omega2, 
    Omega_clsr Omega omega1 omega2 -> 
    Omega_jdgmt Omega' omega1 -> 
    Omega_jdgmt Omega' omega2) -> 
    Omega_mclsr Omega' Omega'' -> 
    Omega_mclsr Omega Omega''.

Inductive terminal_order_grph : Gamma_env -> glbl_cnfg -> Omega_grph -> Prop := 
  | terminal_order_grph_wait : forall x Q theta Phi l G V H Gamma Omega,
    (Omega_mclsr Omega0 Omega /\
    config_mstep 
    G0
    (add_glbl_cnfg (act_cnfg ((wait_exp_b x) :: Q) (theta :: Phi) l) G (V, H))
    )
    ->
    (forall T beta beta' beta'' beta''' m_name beta_list'' e' theta' G' V' H',
    has_type_b Gamma H (wait_exp_b x) T beta' (theta_bhvr_omega_bhvr (sync_theta_bhvr (fut_beta_ty_var beta beta'))) ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((wait_exp_b x) :: Q) (theta :: Phi) l) G (V, H))
    (add_glbl_cnfg (act_cnfg (e' :: Q) (theta' :: theta :: Phi) l) G' (V', H'))
    -> 
    theta' = (sync_theta_bhvr (fut_beta_ty_var beta beta')) /\
    theta = (inv_theta_bhvr beta'' beta''' m_name beta_list'') /\ 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr theta') /\    
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr theta') /\
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (theta_bhvr_omega_bhvr theta'))
    )
    ->
    (forall T beta beta' e' theta' G' V' H',
    has_type_b Gamma H (wait_exp_b x) T beta' (theta_bhvr_omega_bhvr (sync_theta_bhvr (fut_beta_ty_var beta beta'))) ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((wait_exp_b x) :: Q) (theta :: Phi) l) G (V, H))
    (add_glbl_cnfg (act_cnfg (e' :: Q) (theta' :: theta :: Phi) l) G' (V', H'))
    -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (theta_bhvr_omega_bhvr theta'))
    )
    ->
    terminal_order_grph
    Gamma
    (add_glbl_cnfg (act_cnfg ((wait_exp_b x) :: Q) (theta :: Phi) l) G (V, H))
    Omega

  | terminal_order_grph_asgn : forall s e Q theta Phi l G V H Gamma Omega,
    (Omega_mclsr Omega0 Omega /\
    config_mstep 
    G0
    (add_glbl_cnfg (act_cnfg ((st_asgn_exp_b s e) :: Q) (theta :: Phi) l) G (V, H))
    )
    ->
    (forall T beta omega beta' e' theta' G' V' H' beta'' beta''' m_name beta_list'',
    has_type_b Gamma H (st_asgn_exp_b s e) T beta (hpns_bfr_omega_bhvr omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta' beta))) ->
    step_dyn
    (add_glbl_cnfg (act_cnfg ((st_asgn_exp_b s e) :: Q) (theta :: Phi) l) G (V, H))
    (add_glbl_cnfg (act_cnfg (e' :: Q) (theta' :: theta :: Phi) l) G' (V', H'))
    -> 
    theta' = (flow_theta_bhvr beta' beta) /\
    theta = (inv_theta_bhvr beta'' beta''' m_name beta_list'') /\ 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr theta') /\    
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr theta') /\
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (theta_bhvr_omega_bhvr theta'))
    )
    ->
    (forall T beta omega beta' e' theta' G' V' H',
    has_type_b Gamma H (st_asgn_exp_b s e) T beta (hpns_bfr_omega_bhvr omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta' beta))) ->
    step_dyn
    (add_glbl_cnfg (act_cnfg ((st_asgn_exp_b s e) :: Q) (theta :: Phi) l) G (V, H))
    (add_glbl_cnfg (act_cnfg (e' :: Q) (theta' :: theta :: Phi) l) G' (V', H'))
    -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (theta_bhvr_omega_bhvr theta'))
    )
    ->
    terminal_order_grph
    Gamma
    (add_glbl_cnfg (act_cnfg ((st_asgn_exp_b s e) :: Q) (theta :: Phi) l) G (V, H))
    Omega

  | terminal_order_grph_new_act : forall beta beta_list' C v_list Q theta Phi l G V H Gamma Omega,
    (Omega_mclsr Omega0 Omega /\
    config_mstep 
    G0
    (add_glbl_cnfg (act_cnfg ((new_act_exp_b beta beta_list' C v_list) :: Q) (theta :: Phi) l) G (V, H))
    )
    ->
    (forall omega_bfr e' theta' G' V' H' beta'' beta''' m_name beta_list'',
    has_type_b Gamma H (new_act_exp_b beta beta_list' C v_list) (act_val_ty C) beta (hpns_bfr_omega_bhvr omega_bfr (theta_bhvr_omega_bhvr (new_act_theta_bhvr beta beta_list' C beta)))
    -> 
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((new_act_exp_b beta beta_list' C v_list) :: Q) (theta :: Phi) l) G (V, H))
    (add_glbl_cnfg (act_cnfg (e' :: Q) (theta' :: theta :: Phi) l) G' (V', H'))
    -> 
    theta' = (new_act_theta_bhvr beta beta_list' C beta) /\
    theta = (inv_theta_bhvr beta'' beta''' m_name beta_list'') /\ 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr theta') /\    
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr theta') /\
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (theta_bhvr_omega_bhvr theta'))
    )
    ->
    (forall omega_bfr e' theta' G' V' H',
    has_type_b Gamma H (new_act_exp_b beta beta_list' C v_list) (act_val_ty C) beta (hpns_bfr_omega_bhvr omega_bfr (theta_bhvr_omega_bhvr (new_act_theta_bhvr beta beta_list' C beta)))
    -> 
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((new_act_exp_b beta beta_list' C v_list) :: Q) (theta :: Phi) l) G (V, H))
    (add_glbl_cnfg (act_cnfg (e' :: Q) (theta' :: theta :: Phi) l) G' (V', H'))
    -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (theta_bhvr_omega_bhvr theta'))
    )
    ->
    terminal_order_grph
    Gamma
    (add_glbl_cnfg (act_cnfg ((new_act_exp_b beta beta_list' C v_list) :: Q) (theta :: Phi) l) G (V, H))
    Omega

  | terminal_order_grph_inv : forall x beta' m_name v_list Q theta Phi l G V H Gamma Omega,
    (Omega_mclsr Omega0 Omega /\
    config_mstep 
    G0
    (add_glbl_cnfg (act_cnfg ((inv_exp_b x beta' m_name v_list) :: Q) (theta :: Phi) l) G (V, H))
    )
    ->
    (forall T beta'' beta beta' m_name beta_list'' e' theta' G' V' H' beta''' beta'''' m_name' beta_list''',
    has_type_b Gamma H (inv_exp_b x beta' m_name v_list) T beta'' (theta_bhvr_omega_bhvr (inv_theta_bhvr beta beta' m_name beta_list''))
    -> 
    step_dyn
    (add_glbl_cnfg (act_cnfg ((inv_exp_b x beta' m_name v_list) :: Q) (theta :: Phi) l) G (V, H)) 
    (add_glbl_cnfg (act_cnfg (e' :: Q) (theta' :: theta :: Phi) l) G' (V', H'))
    -> 
    theta' = (inv_theta_bhvr beta beta' m_name beta_list'') /\
    theta = (inv_theta_bhvr beta''' beta'''' m_name' beta_list''') /\ 
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr theta') /\    
    Omega_jdgmt Omega (theta_bhvr_omega_bhvr theta') /\
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (theta_bhvr_omega_bhvr theta'))
    )
    ->
    (forall T beta'' beta beta' m_name beta_list'' e' theta' G' V' H',
    has_type_b Gamma H (inv_exp_b x beta' m_name v_list) T beta'' (theta_bhvr_omega_bhvr (inv_theta_bhvr beta beta' m_name beta_list''))
    -> 
    step_dyn
    (add_glbl_cnfg (act_cnfg ((inv_exp_b x beta' m_name v_list) :: Q) (theta :: Phi) l) G (V, H)) 
    (add_glbl_cnfg (act_cnfg (e' :: Q) (theta' :: theta :: Phi) l) G' (V', H'))
    -> 
    Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (theta_bhvr_omega_bhvr theta'))
    )
    ->
    terminal_order_grph
    Gamma
    (add_glbl_cnfg (act_cnfg ((inv_exp_b x beta' m_name v_list) :: Q) (theta :: Phi) l) G (V, H)) 
    Omega
.

Theorem behavior_soundness: 
  forall Gamma T beta omega e e' Q theta theta' Phi l G G' V V' H H' Omega, 
  has_type_b Gamma H e T beta omega ->
  step_dyn 
  (add_glbl_cnfg (act_cnfg (e :: Q) (theta :: Phi) l) G (V, H))
  (add_glbl_cnfg (act_cnfg (e' :: Q) (theta' :: theta :: Phi) l) G' (V', H'))
  -> 
  terminal_order_grph 
  Gamma
  (add_glbl_cnfg (act_cnfg (e :: Q) (theta :: Phi) l) G (V, H))
  Omega 
  ->
  Omega_jdgmt Omega (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr theta) (theta_bhvr_omega_bhvr theta')). 
Proof with eauto.
intros Gamma T beta omega e e' Q theta theta' Phi l G G' V V' H H' Omega
  Ht. generalize dependent e'. induction (Ht).

(*case of invocation expression*)
Focus 1. intros. inversion H11. apply H28 with (T:=T) (beta'':=beta'') 
  (beta:=beta) (beta':=beta') (m_name:=m_name) (beta_list'':=beta_list'') 
  (e':=e') (G':=G') (V':=V') (H':=H'). apply Ht. apply H10.

(*case of wait expression*)
Focus 1. intros. inversion H2. apply H16 with (T:=T) (beta:=beta) (beta':=beta') 
  (e':=e') (G':=G') (V':=V') (H':=H'). apply Ht. apply H1.

(*case of new future expression*)
Focus 1. intros. inversion H1. contradict H17. apply list_add_neq.

(*case of new act expression*)
Focus 1. intros. inversion H10. apply H27 with (omega_bfr:=omega_bfr) (e':=e') 
  (G':=G') (V':=V') (H':= H'). apply Ht. apply H9.

(*case of state assignment expression*)
Focus 1. intros. inversion H2. apply H17 with (T:=T) (beta:=beta) (omega:=omega) 
  (beta':=beta') (e':=e') (G':=G') (V':=V') (H':=H'). apply Ht. apply H1.

(*case of let expression*)
Focus 1. intros. inversion H1. Focus 1. contradict H16. apply list_add_neq.
  Focus 1. inversion H2. 

(*case of state read expression*)
Focus 1. intros. inversion H6. contradict H19. apply list_add_neq.

(*case of variable expression*)
Focus 1. intros. inversion H2. contradict H13. apply list_add_neq.

(*case of null expression*)
Focus 1. intros. inversion H1. contradict H11. apply list_add_neq.

(*case of context expression*)
Focus 1. intros. inversion H4. Focus 1. contradict H19. apply list_add_neq.
  Focus 1. inversion H5.

(*case of resolution expression*)
Focus 1. intros. inversion H1. Focus 1. inversion H2. Focus 1. inversion H2. 

(*case of loc expression*)
Focus 1. intros. inversion H5. contradict H16. apply list_add_neq.
Focus 1. intros. inversion H4. contradict H15. apply list_add_neq.

(*case of unresolved expression*)
Focus 1. intros. inversion H1. contradict H11. apply list_add_neq.

Qed.

End behavior_theorem.