(****************************************************************
   File: Property2.v                                                 
   Authors: Amy Felty
   Version: Coq V8.4pl2
   Date: January 2014
                                                                 
   Property 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 property2.

Let Gamma := system.

Theorem Property2 :
  forall w:world, exists u:world, (u < 5 /\
     seq_ Gamma (madd (state0 *o pres dNAdam @ w) mnil_)
       (state0 *o abs dNAdam @ w+u)).
Proof.
intro w; exists 4; split; auto.
(* apply rule1 *)
assert (h1:In (dagger rule1 @ 0) Gamma).
unfold Gamma,system,system_oo,oo2daggerJudg; simpl; auto.
unfold state0.
(* automatically generated proof starts here *)
apply s_ConjML with
 (abs p53 *o pres mdm2)
 (pres dNAdam)
 (w) 
 mnil_
 (madd (abs p53 *o pres mdm2 @ w)
  (madd (pres dNAdam @ w)
  mnil_)); auto.
apply s_ConjML with
 (abs p53)
 (pres mdm2)
 (w) 
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (pres dNAdam @ w)
  mnil_))); auto.
apply s_copy with
 (dagger rule1)
 (0)
 (madd (dagger rule1 @ 0)
  (madd (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (pres dNAdam @ w)
  mnil_)))); 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 (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (pres dNAdam @ 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 (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (pres dNAdam @ 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 (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (pres dNAdam @ 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 (abs p53 @ w)
  (madd (pres mdm2 @ w)
  (madd (pres dNAdam @ 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 mdm2 @ w)
  (madd (pres dNAdam @ 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_perm231; auto.
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.
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 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 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 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.
unfold munion,madd; simpl; 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.
unfold munion,madd; simpl; 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_copy with
 (dagger rule5)
 (0)
 (madd (dagger rule5 @ 0)
  (madd (pres dNAdam @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_)))); simpl; auto.
unfold rule5,oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres p53 +o (pres p53 *o pres dNAdam) +o (pres p53 *o abs dNAdam) ->> step (abs p53 *o abs dNAdam) *o down (fun W2 => !! ((pres mdm2 at W2 ->> pres mdm2 at (W2 + 1)) &a (abs mdm2 at W2 ->> abs mdm2 at (W2 + 1))))) at W1)
 (0)
 (w + 1 + 1)
 (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 dNAdam) +o (pres p53 *o abs dNAdam) ->> step (abs p53 *o abs dNAdam) *o down (fun W1 => !! ((pres mdm2 at W1 ->> pres mdm2 at (W1 + 1)) &a (abs mdm2 at W1 ->> abs mdm2 at (W1 + 1))))) at (w + 1 + 1) @ 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 dNAdam) +o (pres p53 *o abs dNAdam) ->> step (abs p53 *o abs dNAdam) *o down (fun W1 => !! ((pres mdm2 at W1 ->> pres mdm2 at (W1 + 1)) &a (abs mdm2 at W1 ->> abs mdm2 at (W1 + 1)))))
 (w + 1 + 1)
 (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 dNAdam) +o (pres p53 *o abs dNAdam) ->> step (abs p53 *o abs dNAdam) *o down (fun W1 => !! ((pres mdm2 at W1 ->> pres mdm2 at (W1 + 1)) &a (abs mdm2 at W1 ->> abs mdm2 at (W1 + 1)))) @ w + 1 + 1)
  (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 dNAdam) +o (pres p53 *o abs dNAdam))
 (step (abs p53 *o abs dNAdam) *o down (fun W1 => !! ((pres mdm2 at W1 ->> pres mdm2 at (W1 + 1)) &a (abs mdm2 at W1 ->> abs mdm2 at (W1 + 1)))))
 (w + 1 + 1) 
 (madd (pres dNAdam @ w + 1 + 1)
  (madd (pres p53 @ w + 1 + 1)
  mnil_))
 (madd (abs mdm2 @ w + 1 + 1)
  mnil_)
 (madd (step (abs p53 *o abs dNAdam) *o down (fun W1 => !! ((pres mdm2 at W1 ->> pres mdm2 at (W1 + 1)) &a (abs mdm2 at W1 ->> abs mdm2 at (W1 + 1)))) @ w + 1 + 1)
  (madd (abs mdm2 @ 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_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 p53 @ w + 1 + 1)
  mnil_)
 (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_init; auto.
apply s_init; auto.
apply s_ConjML with
 (step (abs p53 *o abs dNAdam))
 (down (fun W1 => !! ((pres mdm2 at W1 ->> pres mdm2 at (W1 + 1)) &a (abs mdm2 at W1 ->> abs mdm2 at (W1 + 1)))))
 (w + 1 + 1) 
 (madd (abs mdm2 @ w + 1 + 1)
  mnil_)
 (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  (madd (down (fun W1 => !! ((pres mdm2 at W1 ->> pres mdm2 at (W1 + 1)) &a (abs mdm2 at W1 ->> abs mdm2 at (W1 + 1)))) @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  mnil_))); auto.
apply s_DownL with
 (fun W1 => !! ((pres mdm2 at W1 ->> pres mdm2 at (W1 + 1)) &a (abs mdm2 at W1 ->> abs mdm2 at (W1 + 1))))
 (w + 1 + 1)
 (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  mnil_))
 (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  (madd (!! ((pres mdm2 at (w + 1 + 1) ->> pres mdm2 at (w + 1 + 1 + 1)) &a (abs mdm2 at (w + 1 + 1) ->> abs mdm2 at (w + 1 + 1 + 1))) @ w + 1 + 1)
  (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).
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 mdm2 at (w + 1 + 1) ->> pres mdm2 at (w + 1 + 1 + 1)) &a (abs mdm2 at (w + 1 + 1) ->> abs mdm2 at (w + 1 + 1 + 1)))
 (w + 1 + 1)
 (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  (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).
apply s_copy with
 ((pres mdm2 at (w + 1 + 1) ->> pres mdm2 at (w + 1 + 1 + 1)) &a (abs mdm2 at (w + 1 + 1) ->> abs mdm2 at (w + 1 + 1 + 1)))
 (w + 1 + 1) 
 (madd ((pres mdm2 at (w + 1 + 1) ->> pres mdm2 at (w + 1 + 1 + 1)) &a (abs mdm2 at (w + 1 + 1) ->> abs mdm2 at (w + 1 + 1 + 1)) @ w + 1 + 1)
  (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  mnil_))); simpl; auto.
apply s_ConjAL2 with
 (pres mdm2 at (w + 1 + 1) ->> pres mdm2 at (w + 1 + 1 + 1))
 (abs mdm2 at (w + 1 + 1) ->> abs mdm2 at (w + 1 + 1 + 1))
 (w + 1 + 1) 
 (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  mnil_))
 (madd (abs mdm2 at (w + 1 + 1) ->> abs mdm2 at (w + 1 + 1 + 1) @ w + 1 + 1)
  (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1)
  mnil_))); auto.
apply s_ImpL with
 (abs mdm2 at (w + 1 + 1))
 (abs mdm2 at (w + 1 + 1 + 1))
 (w + 1 + 1) 
 (madd (abs mdm2 @ w + 1 + 1)
  mnil_)
 (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  mnil_)
 (madd (abs mdm2 at (w + 1 + 1 + 1) @ w + 1 + 1)
  (madd (step (abs p53 *o abs 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_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
 (abs mdm2)
 (w + 1 + 1 + 1)
 (w + 1 + 1)
 (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  mnil_)
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd (step (abs p53 *o abs dNAdam) @ w + 1 + 1)
  mnil_)); auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (abs p53 *o abs dNAdam) at (W1 + 1))
 (w + 1 + 1)
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  mnil_)
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd ((abs p53 *o abs dNAdam) at (w + 1 + 1 + 1) @ 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_AtL with
 (abs p53 *o abs dNAdam)
 (w + 1 + 1 + 1)
 (w + 1 + 1)
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  mnil_)
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd (abs p53 *o abs dNAdam @ w + 1 + 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 p53)
 (abs dNAdam)
 (w + 1 + 1 + 1) 
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  mnil_)
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  (madd (abs dNAdam @ w + 1 + 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_copy with
 (dagger rule6)
 (0)
 (madd (dagger rule6 @ 0)
  (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  (madd (abs dNAdam @ w + 1 + 1 + 1)
  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 + 1 + 1 + 1)
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  (madd (abs dNAdam @ w + 1 + 1 + 1)
  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 + 1 + 1 + 1) @ 0)
  (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  (madd (abs dNAdam @ w + 1 + 1 + 1)
  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 + 1 + 1 + 1)
 (0)
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  (madd (abs dNAdam @ w + 1 + 1 + 1)
  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 + 1 + 1 + 1)
  (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  (madd (abs dNAdam @ w + 1 + 1 + 1)
  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 + 1 + 1 + 1) 
 (madd (abs mdm2 @ w + 1 + 1 + 1)
  (madd (abs dNAdam @ w + 1 + 1 + 1)
  mnil_))
 (madd (abs p53 @ w + 1 + 1 + 1)
  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 + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 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_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 dNAdam @ w + 1 + 1 + 1)
  mnil_)
 (madd (abs mdm2 @ w + 1 + 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_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 + 1 + 1 + 1) 
 (madd (abs p53 @ w + 1 + 1 + 1)
  mnil_)
 (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  (madd (down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))) @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  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 + 1 + 1 + 1)
 (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  mnil_))
 (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  (madd (!! ((pres p53 at (w + 1 + 1 + 1) ->> pres p53 at (w + 1 + 1 + 1 + 1)) &a (abs p53 at (w + 1 + 1 + 1) ->> abs p53 at (w + 1 + 1 + 1 + 1))) @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 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 p53 at (w + 1 + 1 + 1) ->> pres p53 at (w + 1 + 1 + 1 + 1)) &a (abs p53 at (w + 1 + 1 + 1) ->> abs p53 at (w + 1 + 1 + 1 + 1)))
 (w + 1 + 1 + 1)
 (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 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 p53 at (w + 1 + 1 + 1) ->> pres p53 at (w + 1 + 1 + 1 + 1)) &a (abs p53 at (w + 1 + 1 + 1) ->> abs p53 at (w + 1 + 1 + 1 + 1)))
 (w + 1 + 1 + 1) 
 (madd ((pres p53 at (w + 1 + 1 + 1) ->> pres p53 at (w + 1 + 1 + 1 + 1)) &a (abs p53 at (w + 1 + 1 + 1) ->> abs p53 at (w + 1 + 1 + 1 + 1)) @ w + 1 + 1 + 1)
  (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  mnil_))); simpl; auto.
apply s_ConjAL2 with
 (pres p53 at (w + 1 + 1 + 1) ->> pres p53 at (w + 1 + 1 + 1 + 1))
 (abs p53 at (w + 1 + 1 + 1) ->> abs p53 at (w + 1 + 1 + 1 + 1))
 (w + 1 + 1 + 1) 
 (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  mnil_))
 (madd (abs p53 at (w + 1 + 1 + 1) ->> abs p53 at (w + 1 + 1 + 1 + 1) @ w + 1 + 1 + 1)
  (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  (madd (abs p53 @ w + 1 + 1 + 1)
  mnil_))); auto.
apply s_ImpL with
 (abs p53 at (w + 1 + 1 + 1))
 (abs p53 at (w + 1 + 1 + 1 + 1))
 (w + 1 + 1 + 1) 
 (madd (abs p53 @ w + 1 + 1 + 1)
  mnil_)
 (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  mnil_)
 (madd (abs p53 at (w + 1 + 1 + 1 + 1) @ w + 1 + 1 + 1)
  (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 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_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
 (abs p53)
 (w + 1 + 1 + 1 + 1)
 (w + 1 + 1 + 1)
 (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  mnil_)
 (madd (abs p53 @ w + 1 + 1 + 1 + 1)
  (madd (step (abs dNAdam *o pres mdm2) @ w + 1 + 1 + 1)
  mnil_)); auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (abs dNAdam *o pres mdm2) at (W1 + 1))
 (w + 1 + 1 + 1)
 (madd (abs p53 @ w + 1 + 1 + 1 + 1)
  mnil_)
 (madd (abs p53 @ w + 1 + 1 + 1 + 1)
  (madd ((abs dNAdam *o pres mdm2) at (w + 1 + 1 + 1 + 1) @ w + 1 + 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_AtL with
 (abs dNAdam *o pres mdm2)
 (w + 1 + 1 + 1 + 1)
 (w + 1 + 1 + 1)
 (madd (abs p53 @ w + 1 + 1 + 1 + 1)
  mnil_)
 (madd (abs p53 @ w + 1 + 1 + 1 + 1)
  (madd (abs dNAdam *o pres mdm2 @ w + 1 + 1 + 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 dNAdam)
 (pres mdm2)
 (w + 1 + 1 + 1 + 1) 
 (madd (abs p53 @ w + 1 + 1 + 1 + 1)
  mnil_)
 (madd (abs p53 @ w + 1 + 1 + 1 + 1)
  (madd (abs dNAdam @ w + 1 + 1 + 1 + 1)
  (madd (pres mdm2 @ w + 1 + 1 + 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 p53 @ w + 1 + 1 + 1 + 1)
  (madd (pres mdm2 @ w + 1 + 1 + 1 + 1)
  mnil_))
 (madd (abs dNAdam @ w + 1 + 1 + 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_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 + 1 + 1 + 1)
  mnil_)
 (madd (pres mdm2 @ w + 1 + 1 + 1 + 1)
  mnil_); auto.
replace (w+4) with (w+1+1+1+1); try omega.
apply s_init; auto.
replace (w+4) with (w+1+1+1+1); try omega.
apply s_init; auto.
replace (w+4) with (w+1+1+1+1); try omega.
apply s_init; auto.
Qed.

End property2.