(****************************************************************
   File: Property1.v                                                 
   Authors: Amy Felty
   Version: Coq V8.4pl2
   Date: January 2014
                                                                 
   Property 1 (Versions 1 and 2) 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 property1.

Let Gamma := system.

Theorem Property1V1 :
  forall (w:world), exists (u v:world), (u < 3 /\ v < 3 /\
     seq_ Gamma (madd (pres dNAdam *o state0 @ w) mnil_)
       (delt_ u ((state1 *o dont_care dNAdam) &a
                 (delt_ v (state0 *o dont_care dNAdam))) @ w)).
Proof.
intro w; exists 2; exists 2; split; auto; split; auto.
unfold state1,state0,dont_care.
(* automatically generated proof starts here *)
apply s_ConjML with
 (pres dNAdam)
 (abs p53 *o pres mdm2)
 (w) 
 mnil_
 (madd (pres dNAdam @ w)
  (madd (abs p53 *o pres mdm2 @ w)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (w) 
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ 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).
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 delt_; auto.
apply s_DownR; auto.
apply s_AtR; auto.
apply s_copy with
 (dagger rule1)
 (0)
 (madd (dagger rule1 @ 0)
  (madd (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); simpl; auto.
unfold rule1; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2) ->> step (pres dNAdam *o abs 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 (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd ((pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2) ->> step (pres dNAdam *o abs 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 (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); auto.
apply s_AtL with
 (pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2) ->> step (pres dNAdam *o abs 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 (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd (pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2) ->> step (pres dNAdam *o abs 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 dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); auto.
apply s_ImpL with
 (pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2))
 (step (pres dNAdam *o abs 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 dNAdam @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (abs p53 @ w)
  mnil_)
 (madd (step (pres dNAdam *o abs 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_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_DisjAR1; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_ConjML with
 (step (pres dNAdam *o abs 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 (pres dNAdam *o abs 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 (pres dNAdam *o abs mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (step (pres dNAdam *o abs 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 (pres dNAdam *o abs 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 (pres dNAdam *o abs 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 (pres dNAdam *o abs mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (abs p53 at w ->> abs p53 at (w + 1) @ w)
  (madd (step (pres dNAdam *o abs 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 (pres dNAdam *o abs mdm2) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd (step (pres dNAdam *o abs 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 => (pres dNAdam *o abs mdm2) at (W1 + 1))
 (w)
 (madd (abs p53 at (w + 1) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd ((pres dNAdam *o abs 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).
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 dNAdam *o abs mdm2)
 (w + 1)
 (w)
 (madd (abs p53 at (w + 1) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd (pres dNAdam *o abs 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 (pres dNAdam *o abs mdm2 @ w + 1)
  mnil_)
 (madd (abs p53 @ w + 1)
  (madd (pres dNAdam *o abs mdm2 @ w + 1)
  mnil_)); auto.
apply s_ConjML with
 (pres dNAdam)
 (abs mdm2)
 (w + 1) 
 (madd (abs p53 @ w + 1)
  mnil_)
 (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs 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).
apply s_copy with
 (dagger rule2)
 (0)
 (madd (dagger rule2 @ 0)
  (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))); simpl; auto.
unfold rule2; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53) ->> step (abs mdm2 *o pres 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 + 1)
 (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))
 (madd ((abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53) ->> step (abs mdm2 *o pres 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 + 1) @ 0)
  (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))); auto.
apply s_AtL with
 (abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53) ->> step (abs mdm2 *o pres 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 + 1)
 (0)
 (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))
 (madd (abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53) ->> step (abs mdm2 *o pres 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 + 1)
  (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))); auto.
apply s_ImpL with
 (abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53))
 (step (abs mdm2 *o pres 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 + 1) 
 (madd (abs p53 @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_))
 (madd (pres dNAdam @ w + 1)
  mnil_)
 (madd (step (abs mdm2 *o pres 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 + 1)
  (madd (pres 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_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_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs mdm2 @ w + 1)
  mnil_)
 (madd (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).
apply s_init; auto.
apply s_init; auto.
apply s_ConjML with
 (step (abs mdm2 *o pres p53))
 (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w + 1) 
 (madd (pres dNAdam @ w + 1)
  mnil_)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  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 + 1)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  mnil_))
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (!! ((pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1)) &a (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1))) @ w + 1)
  (madd (pres dNAdam @ 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).
specialize (H 0); repeat (inversion_clear 0).
apply s_BangL with
 ((pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1)) &a (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1)))
 (w + 1)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ 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_copy with
 ((pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1)) &a (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1)))
 (w + 1) 
 (madd ((pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1)) &a (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1)) @ w + 1)
  (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  mnil_))); simpl; auto.
apply s_ConjAL1 with
 (pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1))
 (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1))
 (w + 1) 
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  mnil_))
 (madd (pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1) @ w + 1)
  (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  mnil_))); auto.
apply s_ImpL with
 (pres dNAdam at (w + 1))
 (pres dNAdam at (w + 1 + 1))
 (w + 1) 
 (madd (pres dNAdam @ w + 1)
  mnil_)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  mnil_)
 (madd (pres dNAdam at (w + 1 + 1) @ w + 1)
  (madd (step (abs mdm2 *o pres p53) @ 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_AtR; auto.
apply s_init; auto.
apply s_AtL with
 (pres dNAdam)
 (w + 1 + 1)
 (w + 1)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  mnil_)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd (step (abs mdm2 *o pres p53) @ w + 1)
  mnil_)); auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (abs mdm2 *o pres p53) at (W1 + 1))
 (w + 1)
 (madd (pres dNAdam @ w + 1 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd ((abs mdm2 *o pres p53) at (w + 1 + 1) @ 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).
apply s_AtL with
 (abs mdm2 *o pres p53)
 (w + 1 + 1)
 (w + 1)
 (madd (pres dNAdam @ w + 1 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 *o pres p53 @ w + 1 + 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).
apply s_ConjML with
 (abs mdm2)
 (pres p53)
 (w + 1 + 1) 
 (madd (pres dNAdam @ w + 1 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 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).
apply s_ConjAR; auto.
apply s_ConjMR with
 (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_))
 (madd (pres dNAdam @ w + 1 + 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 (pres p53 @ w + 1 + 1)
  mnil_)
 (madd (abs mdm2 @ w + 1 + 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).
replace (w+2) with (w+1+1); try omega.
apply s_init; auto.
replace (w+2) with (w+1+1); try omega.
apply s_init; auto.
apply s_DisjAR1; auto.
replace (w+2) with (w+1+1); try omega.
apply s_init; auto.
unfold delt_; auto.
apply s_DownR; auto.
apply s_AtR; auto.
apply s_copy with
 (dagger rule3)
 (0)
 (madd (dagger rule3 @ 0)
  (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_)))); simpl; auto.
right; right; right; right; left.
simpl; auto.
unfold rule3; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2) ->> step (pres p53 *o pres mdm2) *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 + 2)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_)))
 (madd ((pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2) ->> step (pres p53 *o pres mdm2) *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 + 2) @ 0)
  (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_)))); auto.
apply s_AtL with
 (pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2) ->> step (pres p53 *o pres mdm2) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w + 2)
 (0)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_)))
 (madd (pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2) ->> step (pres p53 *o pres mdm2) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w + 2)
  (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_)))); auto.
apply s_ImpL with
 (pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2))
 (step (pres p53 *o pres mdm2) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w + 2) 
 (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_))
 (madd (pres dNAdam @ w + 1 + 1)
  mnil_)
 (madd (step (pres p53 *o pres mdm2) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w + 2)
  (madd (pres dNAdam @ w + 1 + 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_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_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres p53 @ w + 1 + 1)
  mnil_)
 (madd (abs mdm2 @ w + 1 + 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).
replace (w+2) with (w+1+1); try omega.
apply s_init; auto.
replace (w+2) with (w+1+1); try omega.
apply s_init; auto.
apply s_ConjML with
 (step (pres p53 *o pres mdm2))
 (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w + 2) 
 (madd (pres dNAdam @ w + 1 + 1)
  mnil_)
 (madd (step (pres p53 *o pres mdm2) @ w + 2)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w + 2)
  (madd (pres dNAdam @ w + 1 + 1)
  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 + 2)
 (madd (step (pres p53 *o pres mdm2) @ w + 2)
  (madd (pres dNAdam @ w + 1 + 1)
  mnil_))
 (madd (step (pres p53 *o pres mdm2) @ w + 2)
  (madd (!! ((pres dNAdam at (w + 2) ->> pres dNAdam at (w + 2 + 1)) &a (abs dNAdam at (w + 2) ->> abs dNAdam at (w + 2 + 1))) @ w + 2)
  (madd (pres dNAdam @ w + 1 + 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).
specialize (H 0); repeat (inversion_clear 0).
apply s_BangL with
 ((pres dNAdam at (w + 2) ->> pres dNAdam at (w + 2 + 1)) &a (abs dNAdam at (w + 2) ->> abs dNAdam at (w + 2 + 1)))
 (w + 2)
 (madd (step (pres p53 *o pres mdm2) @ w + 2)
  (madd (pres dNAdam @ w + 1 + 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_copy with
 ((pres dNAdam at (w + 2) ->> pres dNAdam at (w + 2 + 1)) &a (abs dNAdam at (w + 2) ->> abs dNAdam at (w + 2 + 1)))
 (w + 2) 
 (madd ((pres dNAdam at (w + 2) ->> pres dNAdam at (w + 2 + 1)) &a (abs dNAdam at (w + 2) ->> abs dNAdam at (w + 2 + 1)) @ w + 2)
  (madd (step (pres p53 *o pres mdm2) @ w + 2)
  (madd (pres dNAdam @ w + 1 + 1)
  mnil_))); simpl; auto.
apply s_ConjAL1 with
 (pres dNAdam at (w + 2) ->> pres dNAdam at (w + 2 + 1))
 (abs dNAdam at (w + 2) ->> abs dNAdam at (w + 2 + 1))
 (w + 2) 
 (madd (step (pres p53 *o pres mdm2) @ w + 2)
  (madd (pres dNAdam @ w + 1 + 1)
  mnil_))
 (madd (pres dNAdam at (w + 2) ->> pres dNAdam at (w + 2 + 1) @ w + 2)
  (madd (step (pres p53 *o pres mdm2) @ w + 2)
  (madd (pres dNAdam @ w + 1 + 1)
  mnil_))); auto.
apply s_ImpL with
 (pres dNAdam at (w + 2))
 (pres dNAdam at (w + 2 + 1))
 (w + 2) 
 (madd (pres dNAdam @ w + 1 + 1)
  mnil_)
 (madd (step (pres p53 *o pres mdm2) @ w + 2)
  mnil_)
 (madd (pres dNAdam at (w + 2 + 1) @ w + 2)
  (madd (step (pres p53 *o pres mdm2) @ w + 2)
  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.
replace (w+2) with (w+1+1); try omega.
apply s_init; auto.
apply s_AtL with
 (pres dNAdam)
 (w + 2 + 1)
 (w + 2)
 (madd (step (pres p53 *o pres mdm2) @ w + 2)
  mnil_)
 (madd (pres dNAdam @ w + 2 + 1)
  (madd (step (pres p53 *o pres mdm2) @ w + 2)
  mnil_)); auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (pres p53 *o pres mdm2) at (W1 + 1))
 (w + 2)
 (madd (pres dNAdam @ w + 2 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 2 + 1)
  (madd ((pres p53 *o pres mdm2) at (w + 2 + 1) @ w + 2)
  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).
apply s_AtL with
 (pres p53 *o pres mdm2)
 (w + 2 + 1)
 (w + 2)
 (madd (pres dNAdam @ w + 2 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 2 + 1)
  (madd (pres p53 *o pres mdm2 @ w + 2 + 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).
apply s_ConjML with
 (pres p53)
 (pres mdm2)
 (w + 2 + 1) 
 (madd (pres dNAdam @ w + 2 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 2 + 1)
  (madd (pres p53 @ w + 2 + 1)
  (madd (pres mdm2 @ w + 2 + 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).
apply s_copy with
 (dagger rule4)
 (0)
 (madd (dagger rule4 @ 0)
  (madd (pres dNAdam @ w + 2 + 1)
  (madd (pres p53 @ w + 2 + 1)
  (madd (pres mdm2 @ w + 2 + 1)
  mnil_)))); simpl; auto.
right; right; right; right; right; right; left.
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 + 3)
 (madd (pres dNAdam @ w + 2 + 1)
  (madd (pres p53 @ w + 2 + 1)
  (madd (pres mdm2 @ w + 2 + 1)
  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 + 3) @ 0)
  (madd (pres dNAdam @ w + 2 + 1)
  (madd (pres p53 @ w + 2 + 1)
  (madd (pres mdm2 @ w + 2 + 1)
  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 + 3)
 (0)
 (madd (pres dNAdam @ w + 2 + 1)
  (madd (pres p53 @ w + 2 + 1)
  (madd (pres mdm2 @ w + 2 + 1)
  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 + 3)
  (madd (pres dNAdam @ w + 2 + 1)
  (madd (pres p53 @ w + 2 + 1)
  (madd (pres mdm2 @ w + 2 + 1)
  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 + 3) 
 (madd (pres p53 @ w + 2 + 1)
  (madd (pres mdm2 @ w + 2 + 1)
  mnil_))
 (madd (pres dNAdam @ w + 2 + 1)
  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 + 3)
  (madd (pres dNAdam @ w + 2 + 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_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 (pres mdm2 @ w + 2 + 1)
  mnil_)
 (madd (pres p53 @ w + 2 + 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).
replace (w+3) with (w+2+1); try omega.
apply s_init; auto.
replace (w+3) with (w+2+1); try omega.
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 + 3) 
 (madd (pres dNAdam @ w + 2 + 1)
  mnil_)
 (madd (step (pres mdm2 *o abs p53) @ w + 3)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w + 3)
  (madd (pres dNAdam @ w + 2 + 1)
  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 + 3)
 (madd (step (pres mdm2 *o abs p53) @ w + 3)
  (madd (pres dNAdam @ w + 2 + 1)
  mnil_))
 (madd (step (pres mdm2 *o abs p53) @ w + 3)
  (madd (!! ((pres dNAdam at (w + 3) ->> pres dNAdam at (w + 3 + 1)) &a (abs dNAdam at (w + 3) ->> abs dNAdam at (w + 3 + 1))) @ w + 3)
  (madd (pres dNAdam @ w + 2 + 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).
specialize (H 0); repeat (inversion_clear 0).
apply s_BangL with
 ((pres dNAdam at (w + 3) ->> pres dNAdam at (w + 3 + 1)) &a (abs dNAdam at (w + 3) ->> abs dNAdam at (w + 3 + 1)))
 (w + 3)
 (madd (step (pres mdm2 *o abs p53) @ w + 3)
  (madd (pres dNAdam @ w + 2 + 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_copy with
 ((pres dNAdam at (w + 3) ->> pres dNAdam at (w + 3 + 1)) &a (abs dNAdam at (w + 3) ->> abs dNAdam at (w + 3 + 1)))
 (w + 3) 
 (madd ((pres dNAdam at (w + 3) ->> pres dNAdam at (w + 3 + 1)) &a (abs dNAdam at (w + 3) ->> abs dNAdam at (w + 3 + 1)) @ w + 3)
  (madd (step (pres mdm2 *o abs p53) @ w + 3)
  (madd (pres dNAdam @ w + 2 + 1)
  mnil_))); simpl; auto.
apply s_ConjAL1 with
 (pres dNAdam at (w + 3) ->> pres dNAdam at (w + 3 + 1))
 (abs dNAdam at (w + 3) ->> abs dNAdam at (w + 3 + 1))
 (w + 3) 
 (madd (step (pres mdm2 *o abs p53) @ w + 3)
  (madd (pres dNAdam @ w + 2 + 1)
  mnil_))
 (madd (pres dNAdam at (w + 3) ->> pres dNAdam at (w + 3 + 1) @ w + 3)
  (madd (step (pres mdm2 *o abs p53) @ w + 3)
  (madd (pres dNAdam @ w + 2 + 1)
  mnil_))); auto.
apply s_ImpL with
 (pres dNAdam at (w + 3))
 (pres dNAdam at (w + 3 + 1))
 (w + 3) 
 (madd (pres dNAdam @ w + 2 + 1)
  mnil_)
 (madd (step (pres mdm2 *o abs p53) @ w + 3)
  mnil_)
 (madd (pres dNAdam at (w + 3 + 1) @ w + 3)
  (madd (step (pres mdm2 *o abs p53) @ w + 3)
  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.
replace (w+3) with (w+2+1); try omega.
apply s_init; auto.
apply s_AtL with
 (pres dNAdam)
 (w + 3 + 1)
 (w + 3)
 (madd (step (pres mdm2 *o abs p53) @ w + 3)
  mnil_)
 (madd (pres dNAdam @ w + 3 + 1)
  (madd (step (pres mdm2 *o abs p53) @ w + 3)
  mnil_)); auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (pres mdm2 *o abs p53) at (W1 + 1))
 (w + 3)
 (madd (pres dNAdam @ w + 3 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 3 + 1)
  (madd ((pres mdm2 *o abs p53) at (w + 3 + 1) @ w + 3)
  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).
apply s_AtL with
 (pres mdm2 *o abs p53)
 (w + 3 + 1)
 (w + 3)
 (madd (pres dNAdam @ w + 3 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 3 + 1)
  (madd (pres mdm2 *o abs p53 @ w + 3 + 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).
apply s_ConjML with
 (pres mdm2)
 (abs p53)
 (w + 3 + 1) 
 (madd (pres dNAdam @ w + 3 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 3 + 1)
  (madd (pres mdm2 @ w + 3 + 1)
  (madd (abs p53 @ w + 3 + 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).
apply s_ConjMR with
 (madd (pres mdm2 @ w + 3 + 1)
  (madd (abs p53 @ w + 3 + 1)
  mnil_))
 (madd (pres dNAdam @ w + 3 + 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 + 3 + 1)
  mnil_)
 (madd (pres mdm2 @ w + 3 + 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).
replace (w+2+2) with (w+3+1); try omega.
apply s_init; auto.
replace (w+2+2) with (w+3+1); try omega.
apply s_init; auto.
apply s_DisjAR1; auto.
replace (w+2+2) with (w+3+1); try omega.
apply s_init; auto.
Qed.

Theorem Property1V2 : 
  forall (w:world), exists (u v:world), (u < 3 /\ v < 3 /\
     seq_ Gamma (madd (pres dNAdam *o state0 @ w) mnil_)
       (state1 *o dont_care dNAdam @ w+u) /\
     seq_ Gamma (madd (state1 @ w+u) mnil_)
       (state0 @ w+u+v)).
Proof.
intro w; exists 2; exists 2; unfold state1,state0,dont_care;
 repeat (split; auto).
(* first automatically generated proof starts here *)
apply s_ConjML with
 (pres dNAdam)
 (abs p53 *o pres mdm2)
 (w) 
 mnil_
 (madd (pres dNAdam @ w)
  (madd (abs p53 *o pres mdm2 @ w)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (w) 
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ 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).
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
 (dagger rule1)
 (0)
 (madd (dagger rule1 @ 0)
  (madd (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); simpl; auto.
unfold rule1; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2) ->> step (pres dNAdam *o abs 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 (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd ((pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2) ->> step (pres dNAdam *o abs 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 (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); auto.
apply s_AtL with
 (pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2) ->> step (pres dNAdam *o abs 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 (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd (pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2) ->> step (pres dNAdam *o abs 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 dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); auto.
apply s_ImpL with
 (pres dNAdam +o (pres dNAdam *o pres mdm2) +o (pres dNAdam *o abs mdm2))
 (step (pres dNAdam *o abs 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 dNAdam @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (abs p53 @ w)
  mnil_)
 (madd (step (pres dNAdam *o abs 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_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_DisjAR1; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_ConjML with
 (step (pres dNAdam *o abs 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 (pres dNAdam *o abs 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 (pres dNAdam *o abs mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (step (pres dNAdam *o abs 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 (pres dNAdam *o abs 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 (pres dNAdam *o abs 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 (pres dNAdam *o abs mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (abs p53 at w ->> abs p53 at (w + 1) @ w)
  (madd (step (pres dNAdam *o abs 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 (pres dNAdam *o abs mdm2) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd (step (pres dNAdam *o abs 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 => (pres dNAdam *o abs mdm2) at (W1 + 1))
 (w)
 (madd (abs p53 at (w + 1) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd ((pres dNAdam *o abs 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
 (pres dNAdam *o abs mdm2)
 (w + 1)
 (w)
 (madd (abs p53 at (w + 1) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd (pres dNAdam *o abs 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).
repeat (inversion_clear H).
apply s_AtL with
 (abs p53)
 (w + 1)
 (w)
 (madd (pres dNAdam *o abs mdm2 @ w + 1)
  mnil_)
 (madd (abs p53 @ w + 1)
  (madd (pres dNAdam *o abs mdm2 @ w + 1)
  mnil_)); auto.
apply s_ConjML with
 (pres dNAdam)
 (abs mdm2)
 (w + 1) 
 (madd (abs p53 @ w + 1)
  mnil_)
 (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs 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).
apply s_copy with
 (dagger rule2)
 (0)
 (madd (dagger rule2 @ 0)
  (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))); simpl; auto.
unfold rule2; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53) ->> step (abs mdm2 *o pres 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 + 1)
 (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))
 (madd ((abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53) ->> step (abs mdm2 *o pres 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 + 1) @ 0)
  (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))); auto.
apply s_AtL with
 (abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53) ->> step (abs mdm2 *o pres 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 + 1)
 (0)
 (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))
 (madd (abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53) ->> step (abs mdm2 *o pres 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 + 1)
  (madd (abs p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_)))); auto.
apply s_ImpL with
 (abs mdm2 +o (abs mdm2 *o pres p53) +o (abs mdm2 *o abs p53))
 (step (abs mdm2 *o pres 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 + 1) 
 (madd (abs p53 @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_))
 (madd (pres dNAdam @ w + 1)
  mnil_)
 (madd (step (abs mdm2 *o pres 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 + 1)
  (madd (pres 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_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_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs mdm2 @ w + 1)
  mnil_)
 (madd (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).
apply s_init; auto.
apply s_init; auto.
apply s_ConjML with
 (step (abs mdm2 *o pres p53))
 (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w + 1) 
 (madd (pres dNAdam @ w + 1)
  mnil_)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  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 + 1)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  mnil_))
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (!! ((pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1)) &a (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1))) @ w + 1)
  (madd (pres dNAdam @ 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).
specialize (H 0); repeat (inversion_clear 0).
apply s_BangL with
 ((pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1)) &a (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1)))
 (w + 1)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ 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_copy with
 ((pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1)) &a (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1)))
 (w + 1) 
 (madd ((pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1)) &a (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1)) @ w + 1)
  (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  mnil_))); simpl; auto.
apply s_ConjAL1 with
 (pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1))
 (abs dNAdam at (w + 1) ->> abs dNAdam at (w + 1 + 1))
 (w + 1) 
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  mnil_))
 (madd (pres dNAdam at (w + 1) ->> pres dNAdam at (w + 1 + 1) @ w + 1)
  (madd (step (abs mdm2 *o pres p53) @ w + 1)
  (madd (pres dNAdam @ w + 1)
  mnil_))); auto.
apply s_ImpL with
 (pres dNAdam at (w + 1))
 (pres dNAdam at (w + 1 + 1))
 (w + 1) 
 (madd (pres dNAdam @ w + 1)
  mnil_)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  mnil_)
 (madd (pres dNAdam at (w + 1 + 1) @ w + 1)
  (madd (step (abs mdm2 *o pres p53) @ 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_AtR; auto.
apply s_init; auto.
apply s_AtL with
 (pres dNAdam)
 (w + 1 + 1)
 (w + 1)
 (madd (step (abs mdm2 *o pres p53) @ w + 1)
  mnil_)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd (step (abs mdm2 *o pres p53) @ w + 1)
  mnil_)); auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (abs mdm2 *o pres p53) at (W1 + 1))
 (w + 1)
 (madd (pres dNAdam @ w + 1 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd ((abs mdm2 *o pres p53) at (w + 1 + 1) @ 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).
apply s_AtL with
 (abs mdm2 *o pres p53)
 (w + 1 + 1)
 (w + 1)
 (madd (pres dNAdam @ w + 1 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 *o pres p53 @ w + 1 + 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).
apply s_ConjML with
 (abs mdm2)
 (pres p53)
 (w + 1 + 1) 
 (madd (pres dNAdam @ w + 1 + 1)
  mnil_)
 (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 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).
apply s_ConjMR with
 (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_))
 (madd (pres dNAdam @ w + 1 + 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 (pres p53 @ w + 1 + 1)
  mnil_)
 (madd (abs mdm2 @ w + 1 + 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).
replace (w+2) with (w+1+1); try omega.
apply s_init; auto.
replace (w+2) with (w+1+1); try omega.
apply s_init; auto.
apply s_DisjAR1; auto.
replace (w+2) with (w+1+1); try omega.
apply s_init; auto.
(* second automatically generated proof starts here *)
apply s_ConjML with
 (pres p53)
 (abs mdm2)
 (w+2) 
 mnil_
 (madd (pres p53 @ (w+2))
  (madd (abs mdm2 @ (w+2))
  mnil_)); auto.
apply s_copy with
 (dagger rule3)
 (0)
 (madd (dagger rule3 @ 0)
  (madd (pres p53 @ (w+2))
  (madd (abs mdm2 @ (w+2))
  mnil_))); simpl; auto.
unfold rule3; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2) ->> step (pres p53 *o pres mdm2) *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+2)
 (madd (pres p53 @ (w+2))
  (madd (abs mdm2 @ (w+2))
  mnil_))
 (madd ((pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2) ->> step (pres p53 *o pres mdm2) *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+2) @ 0)
  (madd (pres p53 @ (w+2))
  (madd (abs mdm2 @ (w+2))
  mnil_))); auto.
apply s_AtL with
 (pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2) ->> step (pres p53 *o pres mdm2) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w+2)
 (0)
 (madd (pres p53 @ (w+2))
  (madd (abs mdm2 @ (w+2))
  mnil_))
 (madd (pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2) ->> step (pres p53 *o pres mdm2) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ (w+2))
  (madd (pres p53 @ (w+2))
  (madd (abs mdm2 @ (w+2))
  mnil_))); auto.
apply s_ImpL with
 (pres p53 +o (pres p53 *o pres mdm2) +o (pres p53 *o abs mdm2))
 (step (pres p53 *o pres mdm2) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w+2) 
 (madd (pres p53 @ (w+2))
  (madd (abs mdm2 @ (w+2))
  mnil_))
 mnil_
 (madd (step (pres p53 *o pres mdm2) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ (w+2))
  mnil_); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres p53 @ (w+2))
  mnil_)
 (madd (abs mdm2 @ (w+2))
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_ConjML with
 (step (pres p53 *o pres mdm2))
 (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w+2) 
 mnil_
 (madd (step (pres p53 *o pres mdm2) @ (w+2))
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ (w+2))
  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+2)
 (madd (step (pres p53 *o pres mdm2) @ (w+2))
  mnil_)
 (madd (step (pres p53 *o pres mdm2) @ (w+2))
  (madd (!! ((pres dNAdam at (w+2) ->> pres dNAdam at ((w+2) + 1)) &a (abs dNAdam at (w+2) ->> abs dNAdam at ((w+2) + 1))) @ (w+2))
  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+2) ->> pres dNAdam at ((w+2) + 1)) &a (abs dNAdam at (w+2) ->> abs dNAdam at ((w+2) + 1)))
 (w+2)
 (madd (step (pres p53 *o pres mdm2) @ (w+2))
  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 step; auto.
apply s_DownL with
 (fun W1 => (pres p53 *o pres mdm2) at (W1 + 1))
 (w+2)
 mnil_
 (madd ((pres p53 *o pres mdm2) at (w+2+1) @ (w+2))
  mnil_); auto.
apply s_AtL with
 (pres p53 *o pres mdm2)
 (w+2+1)
 (w+2)
 mnil_
 (madd (pres p53 *o pres mdm2 @ w+2+1)
  mnil_); auto.
apply s_ConjML with
 (pres p53)
 (pres mdm2)
 (w+2 + 1) 
 mnil_
 (madd (pres p53 @ w+2 + 1)
  (madd (pres mdm2 @ w+2 + 1)
  mnil_)); auto.
apply s_copy with
 (dagger rule4)
 (0)
 (madd (dagger rule4 @ 0)
  (madd (pres p53 @ w+2 + 1)
  (madd (pres mdm2 @ w+2 + 1)
  mnil_))); simpl; auto.
unfold rule4,oo2daggerJudg; simpl; tauto.
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+2 + 1)
 (madd (pres p53 @ w+2 + 1)
  (madd (pres mdm2 @ w+2 + 1)
  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+2 + 1) @ 0)
  (madd (pres p53 @ w+2 + 1)
  (madd (pres mdm2 @ w+2 + 1)
  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+2 + 1)
 (0)
 (madd (pres p53 @ w+2 + 1)
  (madd (pres mdm2 @ w+2 + 1)
  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+2 + 1)
  (madd (pres p53 @ w+2 + 1)
  (madd (pres mdm2 @ w+2 + 1)
  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+2 + 1) 
 (madd (pres p53 @ w+2 + 1)
  (madd (pres mdm2 @ w+2 + 1)
  mnil_))
 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+2 + 1)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w+2 + 1)
  mnil_)
 (madd (pres p53 @ w+2 + 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_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+2 + 1) 
 mnil_
 (madd (step (pres mdm2 *o abs p53) @ w+2 + 1)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w+2 + 1)
  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+2 + 1)
 (madd (step (pres mdm2 *o abs p53) @ w+2 + 1)
  mnil_)
 (madd (step (pres mdm2 *o abs p53) @ w+2 + 1)
  (madd (!! ((pres dNAdam at (w+2 + 1) ->> pres dNAdam at (w+2 + 1 + 1)) &a (abs dNAdam at (w+2 + 1) ->> abs dNAdam at (w+2 + 1 + 1))) @ w+2 + 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).
specialize (H 0); repeat (inversion_clear 0).
apply s_BangL with
 ((pres dNAdam at (w+2 + 1) ->> pres dNAdam at (w+2 + 1 + 1)) &a (abs dNAdam at (w+2 + 1) ->> abs dNAdam at (w+2 + 1 + 1)))
 (w+2 + 1)
 (madd (step (pres mdm2 *o abs p53) @ w+2 + 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 step; auto.
apply s_DownL with
 (fun W1 => (pres mdm2 *o abs p53) at (W1 + 1))
 (w+2 + 1)
 mnil_
 (madd ((pres mdm2 *o abs p53) at (w+2 + 1 + 1) @ w+2 + 1)
  mnil_); auto.
apply s_AtL with
 (pres mdm2 *o abs p53)
 (w+2 + 1 + 1)
 (w+2 + 1)
 mnil_
 (madd (pres mdm2 *o abs p53 @ w+2 + 1 + 1)
  mnil_); auto.
apply s_ConjML with
 (pres mdm2)
 (abs p53)
 (w+2 + 1 + 1) 
 mnil_
 (madd (pres mdm2 @ w+2 + 1 + 1)
  (madd (abs p53 @ w+2 + 1 + 1)
  mnil_)); auto.
apply s_ConjMR with
 (madd (abs p53 @ w+2 + 1 + 1)
  mnil_)
 (madd (pres mdm2 @ w+2 + 1 + 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).
replace (w+2+2) with (w+2+1+1); try omega.
apply s_init; auto.
replace (w+2+2) with (w+2+1+1); try omega.
apply s_init; auto.
Qed.

End property1.