(****************************************************************
   File: Property3.v                                                 
   Authors: Amy Felty
   Version: Coq V8.4pl2
   Date: January 2014
                                                                 
   Property 3 from "A Logical Framework for Systems Biology",
   Elisabetta de Maria, Joelle Despeyroux, and Amy P. Felty.

  ***************************************************************)

Require Export BoolEq.
Require Export EqNat.
Require Export hyll_temporal.

Section property3.

Let PP := (state0 *o abs dNAdam).
Let Gamma := system.

Theorem Property3 :
  forall w:world, 
    seq_ Gamma (msingl (PP @ 0)) ((PP at 0) @ w) /\
    forall (n:nat) (A B:oo_), fireable n A -> not_fireable n B ->
       seq_ Gamma mnil_ ((PP ->> ((A &a step PP) +o B)) @ w).
Proof.
intro w; split.
(* automatically generated subproof property3_0 of the subgoal:
7 subgoals, subgoal 1 (ID 32)
  
  PP := state0 *o abs dNAdam : oo world atm tm
  Gamma := system : list judg_
  w : world
  ============================
   seq eqw eqatm Gamma (msingl (abs p53 *o pres mdm2 *o abs dNAdam @ 0))
     (abs p53 *o pres mdm2 *o abs dNAdam @ 0) *)
apply s_AtR; auto.
apply s_ConjML with
 (abs p53 *o pres mdm2)
 (abs dNAdam)
 (0) 
 mnil_
 (madd (abs p53 *o pres mdm2 @ 0)
  (madd (abs dNAdam @ 0)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (0) 
 (madd (abs dNAdam @ 0)
  mnil_)
 (madd (abs p53 @ 0)
  (madd (pres mdm2 @ 0)
  (madd (abs dNAdam @ 0)
  mnil_))); auto.
apply s_ConjMR with
 (madd (abs p53 @ 0)
  (madd (pres mdm2 @ 0)
  mnil_))
 (madd (abs dNAdam @ 0)
  mnil_); auto.
apply s_ConjMR with
 (madd (abs p53 @ 0)
  mnil_)
 (madd (pres mdm2 @ 0)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_init; auto.
(* End of subgoal *)
intro n; case n.
intros A B h; inversion h.
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property3_1 of the subgoal:
subgoal 2 (ID 212) is:
 seq_ Gamma mnil_
   (PP ->>
    pres dNAdam +o (pres dNAdam *o pres mdm2) +o
    (pres dNAdam *o abs mdm2) *o dont_care p53 &a 
    step PP +o (abs dNAdam *o dont_cares (mdm2 :: p53 :: nil)) @ w) *)
apply s_ImpR with
(madd (abs p53 *o pres mdm2 *o abs dNAdam @ w)
  mnil_); auto.
apply s_ConjML with
 (abs p53 *o pres mdm2)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (abs p53 *o pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (w) 
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_))); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm312; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (abs p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property3_2 of the subgoal:
  PP := state0 *o abs dNAdam : oo world atm tm
  Gamma := system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (PP ->>
      abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53) *o
      dont_care dNAdam &a step PP +o
      (pres mdm2 *o dont_cares (p53 :: dNAdam :: nil)) @ w) *)
apply s_ImpR with
(madd (abs p53 *o pres mdm2 *o abs dNAdam @ w)
  mnil_); auto.
apply s_ConjML with
 (abs p53 *o pres mdm2)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (abs p53 *o pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (w) 
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_))); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (abs p53 @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property3_3 of the subgoal:
  PP := state0 *o abs dNAdam : oo world atm tm
  Gamma := system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (PP ->>
      pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2) *o
      dont_care dNAdam &a step PP +o
      (abs p53 *o dont_cares (mdm2 :: dNAdam :: nil)) @ w) *)
apply s_ImpR with
(madd (abs p53 *o pres mdm2 *o abs dNAdam @ w)
  mnil_); auto.
apply s_ConjML with
 (abs p53 *o pres mdm2)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (abs p53 *o pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (w) 
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_))); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
apply s_init; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property3_4 of the subgoal:
  PP := state0 *o abs dNAdam : oo world atm tm
  Gamma := system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (PP ->>
      pres mdm2 +o (pres mdm2 *o pres p53) +o (pres mdm2 *o abs p53) *o
      dont_care dNAdam &a step PP +o
      (abs mdm2 *o dont_cares (p53 :: dNAdam :: nil)) @ w) *)
apply s_ImpR with
(madd (abs p53 *o pres mdm2 *o abs dNAdam @ w)
  mnil_); auto.
apply s_ConjML with
 (abs p53 *o pres mdm2)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (abs p53 *o pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (w) 
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_))); auto.
apply s_DisjAR1; auto.
apply s_ConjAR; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (abs p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_copy with
 (dagger rule4)
 (0)
 (madd (dagger rule4 @ 0)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))); simpl; auto.
unfold rule4; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (pres mdm2 +o (pres mdm2 *o pres p53) +o (pres mdm2 *o abs p53) ->> step (pres mdm2 *o abs p53) *o down (fun W2 => !! ((pres dNAdam at W2 ->> pres dNAdam at (W2 + 1)) &a (abs dNAdam at W2 ->> abs dNAdam at (W2 + 1))))) at W1)
 (0)
 (w)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))
 (madd ((pres mdm2 +o (pres mdm2 *o pres p53) +o (pres mdm2 *o abs p53) ->> step (pres mdm2 *o abs p53) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1))))) at w @ 0)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))); auto.
apply s_AtL with
 (pres mdm2 +o (pres mdm2 *o pres p53) +o (pres mdm2 *o abs p53) ->> step (pres mdm2 *o abs p53) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w)
 (0)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))
 (madd (pres mdm2 +o (pres mdm2 *o pres p53) +o (pres mdm2 *o abs p53) ->> step (pres mdm2 *o abs p53) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))); auto.
apply s_ImpL with
 (pres mdm2 +o (pres mdm2 *o pres p53) +o (pres mdm2 *o abs p53))
 (step (pres mdm2 *o abs p53) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w) 
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (step (pres mdm2 *o abs p53) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (abs p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_ConjML with
 (step (pres mdm2 *o abs p53))
 (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w) 
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (step (pres mdm2 *o abs p53) @ w)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  (madd (abs dNAdam @ w)
  mnil_))); auto.
apply s_DownL with
 (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1))))
 (w)
 (madd (step (pres mdm2 *o abs p53) @ w)
  (madd (abs dNAdam @ w)
  mnil_))
 (madd (step (pres mdm2 *o abs p53) @ w)
  (madd (!! ((pres dNAdam at w ->> pres dNAdam at (w + 1)) &a (abs dNAdam at w ->> abs dNAdam at (w + 1))) @ w)
  (madd (abs dNAdam @ w)
  mnil_))); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
specialize (H 0); repeat (inversion_clear 0).
apply s_BangL with
 ((pres dNAdam at w ->> pres dNAdam at (w + 1)) &a (abs dNAdam at w ->> abs dNAdam at (w + 1)))
 (w)
 (madd (step (pres mdm2 *o abs p53) @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_copy with
 ((pres dNAdam at w ->> pres dNAdam at (w + 1)) &a (abs dNAdam at w ->> abs dNAdam at (w + 1)))
 (w) 
 (madd ((pres dNAdam at w ->> pres dNAdam at (w + 1)) &a (abs dNAdam at w ->> abs dNAdam at (w + 1)) @ w)
  (madd (step (pres mdm2 *o abs p53) @ w)
  (madd (abs dNAdam @ w)
  mnil_))); simpl; auto.
apply s_ConjAL2 with
 (pres dNAdam at w ->> pres dNAdam at (w + 1))
 (abs dNAdam at w ->> abs dNAdam at (w + 1))
 (w) 
 (madd (step (pres mdm2 *o abs p53) @ w)
  (madd (abs dNAdam @ w)
  mnil_))
 (madd (abs dNAdam at w ->> abs dNAdam at (w + 1) @ w)
  (madd (step (pres mdm2 *o abs p53) @ w)
  (madd (abs dNAdam @ w)
  mnil_))); auto.
apply s_ImpL with
 (abs dNAdam at w)
 (abs dNAdam at (w + 1))
 (w) 
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (step (pres mdm2 *o abs p53) @ w)
  mnil_)
 (madd (abs dNAdam at (w + 1) @ w)
  (madd (step (pres mdm2 *o abs p53) @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_AtR; auto.
apply s_init; auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (pres mdm2 *o abs p53) at (W1 + 1))
 (w)
 (madd (abs dNAdam at (w + 1) @ w)
  mnil_)
 (madd (abs dNAdam at (w + 1) @ w)
  (madd ((pres mdm2 *o abs p53) at (w + 1) @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
inversion_clear H.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_AtL with
 (pres mdm2 *o abs p53)
 (w + 1)
 (w)
 (madd (abs dNAdam at (w + 1) @ w)
  mnil_)
 (madd (abs dNAdam at (w + 1) @ w)
  (madd (pres mdm2 *o abs p53 @ w + 1)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
inversion_clear H.
apply s_AtL with
 (abs dNAdam)
 (w + 1)
 (w)
 (madd (pres mdm2 *o abs p53 @ w + 1)
  mnil_)
 (madd (abs dNAdam @ w + 1)
  (madd (pres mdm2 *o abs p53 @ w + 1)
  mnil_)); auto.
apply s_ConjML with
 (pres mdm2)
 (abs p53)
 (w + 1) 
 (madd (abs dNAdam @ w + 1)
  mnil_)
 (madd (abs dNAdam @ w + 1)
  (madd (pres mdm2 @ w + 1)
  (madd (abs p53 @ w + 1)
  mnil_))); auto.
unfold munion,madd; simpl; auto.
apply ms_perm231; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold step; auto.
apply s_DownR; auto.
apply s_AtR; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w + 1)
  (madd (abs p53 @ w + 1)
  mnil_))
 (madd (abs dNAdam @ w + 1)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm231; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_ConjMR with
 (madd (abs p53 @ w + 1)
  mnil_)
 (madd (pres mdm2 @ w + 1)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property3_5 of the subgoal:
  PP := state0 *o abs dNAdam : oo world atm tm
  Gamma := system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (PP ->>
      pres p53 +o (pres p53 *o pres dNAdam) +o (pres p53 *o abs dNAdam) *o
      dont_care mdm2 &a step PP +o
      (abs p53 *o dont_cares (mdm2 :: dNAdam :: nil)) @ w) *)
apply s_ImpR with
(madd (abs p53 *o pres mdm2 *o abs dNAdam @ w)
  mnil_); auto.
apply s_ConjML with
 (abs p53 *o pres mdm2)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (abs p53 *o pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (w) 
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_))); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
apply s_init; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_DisjAR1; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property3_6 of the subgoal:
  PP := state0 *o abs dNAdam : oo world atm tm
  Gamma := system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (PP ->>
      abs dNAdam +o (abs dNAdam *o pres mdm2) +o (abs dNAdam *o abs mdm2) *o
      dont_care p53 &a step PP +o
      (pres dNAdam *o dont_cares (mdm2 :: p53 :: nil)) @ w) *)
apply s_ImpR with
(madd (abs p53 *o pres mdm2 *o abs dNAdam @ w)
  mnil_); auto.
apply s_ConjML with
 (abs p53 *o pres mdm2)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (abs p53 *o pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (w) 
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_))); auto.
apply s_DisjAR1; auto.
apply s_ConjAR; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_))
 (madd (abs p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm231; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_DisjAR1; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_copy with
 (dagger rule6)
 (0)
 (madd (dagger rule6 @ 0)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))); simpl; auto.
unfold rule6,oo2daggerJudg; simpl; tauto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (abs dNAdam +o (abs dNAdam *o pres mdm2) +o (abs dNAdam *o abs mdm2) ->> step (abs dNAdam *o pres mdm2) *o down (fun W2 => !! ((pres p53 at W2 ->> pres p53 at (W2 + 1)) &a (abs p53 at W2 ->> abs p53 at (W2 + 1))))) at W1)
 (0)
 (w)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))
 (madd ((abs dNAdam +o (abs dNAdam *o pres mdm2) +o (abs dNAdam *o abs mdm2) ->> step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1))))) at w @ 0)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))); auto.
apply s_AtL with
 (abs dNAdam +o (abs dNAdam *o pres mdm2) +o (abs dNAdam *o abs mdm2) ->> step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))))
 (w)
 (0)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))
 (madd (abs dNAdam +o (abs dNAdam *o pres mdm2) +o (abs dNAdam *o abs mdm2) ->> step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))) @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_)))); auto.
apply s_ImpL with
 (abs dNAdam +o (abs dNAdam *o pres mdm2) +o (abs dNAdam *o abs mdm2))
 (step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))))
 (w) 
 (madd (pres mdm2 @ w)
  (madd (abs dNAdam @ w)
  mnil_))
 (madd (abs p53 @ w)
  mnil_)
 (madd (step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))) @ w)
  (madd (abs p53 @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm231; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_DisjAR1; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_ConjML with
 (step (abs dNAdam *o pres mdm2))
 (down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))))
 (w) 
 (madd (abs p53 @ w)
  mnil_)
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))) @ w)
  (madd (abs p53 @ w)
  mnil_))); auto.
apply s_DownL with
 (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1))))
 (w)
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (!! ((pres p53 at w ->> pres p53 at (w + 1)) &a (abs p53 at w ->> abs p53 at (w + 1))) @ w)
  (madd (abs p53 @ w)
  mnil_))); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
specialize (H 0); repeat (inversion_clear 0).
apply s_BangL with
 ((pres p53 at w ->> pres p53 at (w + 1)) &a (abs p53 at w ->> abs p53 at (w + 1)))
 (w)
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_copy with
 ((pres p53 at w ->> pres p53 at (w + 1)) &a (abs p53 at w ->> abs p53 at (w + 1)))
 (w) 
 (madd ((pres p53 at w ->> pres p53 at (w + 1)) &a (abs p53 at w ->> abs p53 at (w + 1)) @ w)
  (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))); simpl; auto.
apply s_ConjAL2 with
 (pres p53 at w ->> pres p53 at (w + 1))
 (abs p53 at w ->> abs p53 at (w + 1))
 (w) 
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (abs p53 at w ->> abs p53 at (w + 1) @ w)
  (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))); auto.
apply s_ImpL with
 (abs p53 at w)
 (abs p53 at (w + 1))
 (w) 
 (madd (abs p53 @ w)
  mnil_)
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd (step (abs dNAdam *o pres mdm2) @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_AtR; auto.
apply s_init; auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (abs dNAdam *o pres mdm2) at (W1 + 1))
 (w)
 (madd (abs p53 at (w + 1) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd ((abs dNAdam *o pres mdm2) at (w + 1) @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
repeat (inversion_clear H).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_AtL with
 (abs dNAdam *o pres mdm2)
 (w + 1)
 (w)
 (madd (abs p53 at (w + 1) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd (abs dNAdam *o pres mdm2 @ w + 1)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
inversion_clear H.
apply s_AtL with
 (abs p53)
 (w + 1)
 (w)
 (madd (abs dNAdam *o pres mdm2 @ w + 1)
  mnil_)
 (madd (abs p53 @ w + 1)
  (madd (abs dNAdam *o pres mdm2 @ w + 1)
  mnil_)); auto.
apply s_ConjML with
 (abs dNAdam)
 (pres mdm2)
 (w + 1) 
 (madd (abs p53 @ w + 1)
  mnil_)
 (madd (abs p53 @ w + 1)
  (madd (abs dNAdam @ w + 1)
  (madd (pres mdm2 @ w + 1)
  mnil_))); auto.
unfold munion,madd; simpl; auto.
apply ms_perm231; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold step; auto.
apply s_DownR; auto.
apply s_AtR; auto.
apply s_ConjMR with
 (madd (abs p53 @ w + 1)
  (madd (pres mdm2 @ w + 1)
  mnil_))
 (madd (abs dNAdam @ w + 1)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_ConjMR with
 (madd (abs p53 @ w + 1)
  mnil_)
 (madd (pres mdm2 @ w + 1)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intros n A B h1 h2.
inversion h1.
Qed.

End property3.