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

Let LL := ((pres p53 *o pres mdm2) +o (abs p53 *o abs mdm2)).
Let RR :=
 (((pres p53 *o abs mdm2) +o (abs p53 *o pres mdm2)) *o (dont_care dNAdam)).
Let Gamma := s_system.

Theorem Property4 :
  forall w:world, 
    forall (n:nat) (A B:oo_), s_fireable n A -> s_not_fireable n B ->
       seq_ Gamma mnil_ ((LL ->> ((A &a step RR) +o B)) @ w).
Proof.
intro w; intro n; case n.
intros A B h; inversion h.
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property4_1 of the subgoal:
  LL := pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) : oo world atm tm
  RR := pres p53 *o abs mdm2 +o (abs p53 *o pres mdm2) *o dont_care dNAdam
     : oo world atm tm
  Gamma := s_system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (LL ->>
      pres dNAdam *o pres mdm2 *o dont_care p53 &a step RR +o
      (abs dNAdam *o pres mdm2 +o (pres dNAdam *o abs mdm2) +o
       (abs dNAdam *o abs mdm2) *o dont_care p53) @ w) *)
apply s_ImpR with
(madd (pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres p53 *o pres mdm2)
 (abs p53 *o abs mdm2)
 (w) 
 mnil_
 (madd (pres p53 *o pres mdm2 @ w)
  mnil_)
 (madd (abs p53 *o abs mdm2 @ w)
  mnil_); auto.
apply s_ConjML with
 (pres p53)
 (pres mdm2)
 (w) 
 mnil_
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)); auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres dNAdam +o abs dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd (abs dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_DisjAR1; auto.
apply s_ConjAR; auto.
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_copy with
 (dagger s_rule1)
 (0)
 (madd (dagger s_rule1 @ 0)
  (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); simpl; auto.
unfold s_rule1; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (pres dNAdam *o pres 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 (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd ((pres dNAdam *o pres 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 (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); auto.
apply s_AtL with
 (pres dNAdam *o pres 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 (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd (pres dNAdam *o pres 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 p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); auto.
apply s_ImpL with
 (pres dNAdam *o pres 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 (pres 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 (pres 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_ConjMR with
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
unfold step; auto.
apply s_DownR; auto.
apply s_AtR; 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 (pres 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 (pres 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 (pres 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 (pres 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 (pres 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 (pres p53 @ w)
  mnil_))); simpl; auto.
apply s_ConjAL1 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 (pres p53 @ w)
  mnil_))
 (madd (pres p53 at w ->> pres p53 at (w + 1) @ w)
  (madd (step (pres dNAdam *o abs mdm2) @ w)
  (madd (pres p53 @ w)
  mnil_))); auto.
apply s_ImpL with
 (pres p53 at w)
 (pres p53 at (w + 1))
 (w) 
 (madd (pres p53 @ w)
  mnil_)
 (madd (step (pres dNAdam *o abs mdm2) @ w)
  mnil_)
 (madd (pres 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 (pres p53 at (w + 1) @ w)
  mnil_)
 (madd (pres 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 (pres p53 at (w + 1) @ w)
  mnil_)
 (madd (pres 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_ConjML with
 (pres dNAdam)
 (abs mdm2)
 (w + 1) 
 (madd (pres p53 at (w + 1) @ w)
  mnil_)
 (madd (pres p53 at (w + 1) @ w)
  (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_AtL with
 (pres p53)
 (w + 1)
 (w)
 (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_))
 (madd (pres p53 @ w + 1)
  (madd (pres dNAdam @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_))); auto.
apply s_ConjMR with
 (madd (pres p53 @ w + 1)
  (madd (abs mdm2 @ w + 1)
  mnil_))
 (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_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_ConjMR with
 (madd (pres p53 @ w + 1)
  mnil_)
 (madd (abs mdm2 @ w + 1)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_DisjAR1; auto.
apply s_DisjAR1; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_ConjML with
 (abs p53)
 (abs mdm2)
 (w) 
 mnil_
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs mdm2 @ w)
  mnil_)
 (madd (abs p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  (madd (abs mdm2 @ w)
  mnil_)); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 (madd (abs mdm2 @ w)
  mnil_)
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  (madd (abs mdm2 @ w)
  mnil_)); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 (madd (abs mdm2 @ w)
  mnil_)
 (madd (pres dNAdam +o abs dNAdam @ w)
  (madd (abs mdm2 @ w)
  mnil_)); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 (madd (abs mdm2 @ w)
  mnil_)
 (madd (pres dNAdam @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd (abs dNAdam @ w)
  (madd (abs mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR1; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (abs mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (abs mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property4_2 of the subgoal:
  LL := pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) : oo world atm tm
  RR := pres p53 *o abs mdm2 +o (abs p53 *o pres mdm2) *o dont_care dNAdam
     : oo world atm tm
  Gamma := s_system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (LL ->>
      abs mdm2 *o abs p53 *o dont_care dNAdam &a step RR +o
      (pres mdm2 *o abs p53 +o (abs mdm2 *o pres p53) +o
       (pres mdm2 *o pres p53) *o dont_care dNAdam) @ w) *)
apply s_ImpR with
(madd (pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres p53 *o pres mdm2)
 (abs p53 *o abs mdm2)
 (w) 
 mnil_
 (madd (pres p53 *o pres mdm2 @ w)
  mnil_)
 (madd (abs p53 *o abs mdm2 @ w)
  mnil_); auto.
apply s_ConjML with
 (pres p53)
 (pres mdm2)
 (w) 
 mnil_
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 mnil_; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (pres p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  mnil_); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 mnil_
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  mnil_); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 mnil_
 (madd (pres dNAdam +o abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_ConjML with
 (abs p53)
 (abs mdm2)
 (w) 
 mnil_
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR1; auto.
apply s_ConjAR; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 mnil_; auto.
apply s_ConjMR with
 (madd (abs mdm2 @ w)
  mnil_)
 (madd (abs p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  mnil_); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 mnil_
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  mnil_); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 mnil_
 (madd (pres dNAdam +o abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_copy with
 (dagger s_rule2)
 (0)
 (madd (dagger s_rule2 @ 0)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); simpl; auto.
unfold s_rule2; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (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)
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd ((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 @ 0)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); auto.
apply s_AtL with
 (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)
 (0)
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd (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)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); auto.
apply s_ImpL with
 (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) 
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 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)
  mnil_); auto.
apply s_ConjMR with
 (madd (abs mdm2 @ w)
  mnil_)
 (madd (abs p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
unfold step; auto.
apply s_DownR; auto.
apply s_AtR; 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) 
 mnil_
 (madd (step (abs mdm2 *o pres p53) @ w)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  mnil_)); auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (abs mdm2 *o pres p53) at (W1 + 1))
 (w)
 (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  mnil_)
 (madd ((abs mdm2 *o pres p53) at (w + 1) @ w)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  mnil_)); auto.
apply s_AtL with
 (abs mdm2 *o pres p53)
 (w + 1)
 (w)
 (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  mnil_)
 (madd (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)
  mnil_)); auto.
apply s_ConjML with
 (abs mdm2)
 (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)
  mnil_)
 (madd (abs mdm2 @ w + 1)
  (madd (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)
  mnil_))); auto.
apply s_DownL with
 (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1))))
 (w)
 (madd (abs mdm2 @ w + 1)
  (madd (pres p53 @ w + 1)
  mnil_))
 (madd (abs mdm2 @ w + 1)
  (madd (pres p53 @ w + 1)
  (madd (!! ((pres dNAdam at w ->> pres dNAdam at (w + 1)) &a (abs dNAdam at w ->> abs dNAdam at (w + 1))) @ w)
  mnil_))); auto.
unfold munion,madd; simpl; auto.
apply ms_perm312; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm312; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_BangL with
 ((pres dNAdam at w ->> pres dNAdam at (w + 1)) &a (abs dNAdam at w ->> abs dNAdam at (w + 1)))
 (w)
 (madd (abs mdm2 @ w + 1)
  (madd (pres p53 @ w + 1)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm312; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_ConjMR with
 (madd (abs mdm2 @ w + 1)
  (madd (pres p53 @ w + 1)
  mnil_))
 mnil_; auto.
apply s_DisjAR1; auto.
apply s_ConjMR with
 (madd (pres p53 @ w + 1)
  mnil_)
 (madd (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).
apply s_init; auto.
apply s_init; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  mnil_); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w + 1)
 mnil_
 (madd ((pres dNAdam +o abs dNAdam) at (w + 1) @ 0)
  mnil_); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w + 1)
 (0)
 mnil_
 (madd (pres dNAdam +o abs dNAdam @ w + 1)
  mnil_); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w + 1) 
 mnil_
 (madd (pres dNAdam @ w + 1)
  mnil_)
 (madd (abs dNAdam @ w + 1)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property4_3 of the subgoal:
  LL := pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) : oo world atm tm
  RR := pres p53 *o abs mdm2 +o (abs p53 *o pres mdm2) *o dont_care dNAdam
     : oo world atm tm
  Gamma := s_system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (LL ->>
      pres p53 *o abs mdm2 *o dont_care dNAdam &a step RR +o
      (abs p53 *o abs mdm2 +o (pres p53 *o pres mdm2) +o
       (abs p53 *o pres mdm2) *o dont_care dNAdam) @ w) *)
apply s_ImpR with
(madd (pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres p53 *o pres mdm2)
 (abs p53 *o abs mdm2)
 (w) 
 mnil_
 (madd (pres p53 *o pres mdm2 @ w)
  mnil_)
 (madd (abs p53 *o abs mdm2 @ w)
  mnil_); auto.
apply s_ConjML with
 (pres p53)
 (pres mdm2)
 (w) 
 mnil_
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 mnil_; auto.
apply s_DisjAR1; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres p53 @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  mnil_); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 mnil_
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  mnil_); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 mnil_
 (madd (pres dNAdam +o abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_ConjML with
 (abs p53)
 (abs mdm2)
 (w) 
 mnil_
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 mnil_; auto.
apply s_DisjAR1; auto.
apply s_DisjAR1; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  mnil_)
 (madd (abs mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  mnil_); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 mnil_
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  mnil_); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 mnil_
 (madd (pres dNAdam +o abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property4_4 of the subgoal:
  LL := pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) : oo world atm tm
  RR := pres p53 *o abs mdm2 +o (abs p53 *o pres mdm2) *o dont_care dNAdam
     : oo world atm tm
  Gamma := s_system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (LL ->>
      pres mdm2 *o pres p53 *o dont_care dNAdam &a step RR +o
      (abs mdm2 *o pres p53 +o (pres mdm2 *o abs p53) +o
       (abs mdm2 *o abs p53) *o dont_care dNAdam) @ w) *)
apply s_ImpR with
(madd (pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres p53 *o pres mdm2)
 (abs p53 *o abs mdm2)
 (w) 
 mnil_
 (madd (pres p53 *o pres mdm2 @ w)
  mnil_)
 (madd (abs p53 *o abs mdm2 @ w)
  mnil_); auto.
apply s_ConjML with
 (pres p53)
 (pres mdm2)
 (w) 
 mnil_
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR1; auto.
apply s_ConjAR; auto.
apply s_ConjMR with
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 mnil_; auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (pres p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  mnil_); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 mnil_
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  mnil_); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 mnil_
 (madd (pres dNAdam +o abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_copy with
 (dagger s_rule4)
 (0)
 (madd (dagger s_rule4 @ 0)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); simpl; auto.
unfold s_rule4; auto.
unfold dagger; auto.
apply s_WallL with
 (fun W1 => (pres mdm2 *o pres p53 ->> step (pres mdm2 *o abs p53) *o down (fun W2 => !! ((pres dNAdam at W2 ->> pres dNAdam at (W2 + 1)) &a (abs dNAdam at W2 ->> abs dNAdam at (W2 + 1))))) at W1)
 (0)
 (w)
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd ((pres mdm2 *o pres p53 ->> step (pres mdm2 *o abs p53) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1))))) at w @ 0)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_AtL with
 (pres mdm2 *o pres p53 ->> step (pres mdm2 *o abs p53) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w)
 (0)
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres mdm2 *o pres p53 ->> step (pres mdm2 *o abs p53) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_ImpL with
 (pres mdm2 *o pres p53)
 (step (pres mdm2 *o abs p53) *o down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))))
 (w) 
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  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)
  mnil_); auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (pres p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
unfold step; auto.
apply s_DownR; auto.
apply s_AtR; 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) 
 mnil_
 (madd (step (pres mdm2 *o abs p53) @ w)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  mnil_)); auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (pres mdm2 *o abs p53) at (W1 + 1))
 (w)
 (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  mnil_)
 (madd ((pres mdm2 *o abs p53) at (w + 1) @ w)
  (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  mnil_)); auto.
apply s_AtL with
 (pres mdm2 *o abs p53)
 (w + 1)
 (w)
 (madd (down (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1)))) @ w)
  mnil_)
 (madd (pres mdm2 *o abs 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)
  mnil_)); auto.
apply s_ConjML with
 (pres mdm2)
 (abs 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)
  mnil_)
 (madd (pres mdm2 @ w + 1)
  (madd (abs 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)
  mnil_))); auto.
apply s_DownL with
 (fun W1 => !! ((pres dNAdam at W1 ->> pres dNAdam at (W1 + 1)) &a (abs dNAdam at W1 ->> abs dNAdam at (W1 + 1))))
 (w)
 (madd (pres mdm2 @ w + 1)
  (madd (abs p53 @ w + 1)
  mnil_))
 (madd (pres mdm2 @ w + 1)
  (madd (abs p53 @ w + 1)
  (madd (!! ((pres dNAdam at w ->> pres dNAdam at (w + 1)) &a (abs dNAdam at w ->> abs dNAdam at (w + 1))) @ w)
  mnil_))); auto.
unfold munion,madd; simpl; auto.
apply ms_perm312; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm312; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_BangL with
 ((pres dNAdam at w ->> pres dNAdam at (w + 1)) &a (abs dNAdam at w ->> abs dNAdam at (w + 1)))
 (w)
 (madd (pres mdm2 @ w + 1)
  (madd (abs p53 @ w + 1)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm312; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_ConjMR with
 (madd (pres mdm2 @ w + 1)
  (madd (abs p53 @ w + 1)
  mnil_))
 mnil_; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs p53 @ w + 1)
  mnil_)
 (madd (pres mdm2 @ w + 1)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  mnil_); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w + 1)
 mnil_
 (madd ((pres dNAdam +o abs dNAdam) at (w + 1) @ 0)
  mnil_); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w + 1)
 (0)
 mnil_
 (madd (pres dNAdam +o abs dNAdam @ w + 1)
  mnil_); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w + 1) 
 mnil_
 (madd (pres dNAdam @ w + 1)
  mnil_)
 (madd (abs dNAdam @ w + 1)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_ConjML with
 (abs p53)
 (abs mdm2)
 (w) 
 mnil_
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 mnil_; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs mdm2 @ w)
  mnil_)
 (madd (abs p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  mnil_); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 mnil_
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  mnil_); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 mnil_
 (madd (pres dNAdam +o abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 mnil_
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property4_5 of the subgoal:
  LL := pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) : oo world atm tm
  RR := pres p53 *o abs mdm2 +o (abs p53 *o pres mdm2) *o dont_care dNAdam
     : oo world atm tm
  Gamma := s_system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (LL ->>
      pres p53 *o pres dNAdam *o dont_care mdm2 &a step RR +o
      (abs p53 *o pres dNAdam +o (pres p53 *o abs dNAdam) +o
       (abs p53 *o abs dNAdam) *o dont_care mdm2) @ w) *)
apply s_ImpR with
(madd (pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres p53 *o pres mdm2)
 (abs p53 *o abs mdm2)
 (w) 
 mnil_
 (madd (pres p53 *o pres mdm2 @ w)
  mnil_)
 (madd (abs p53 *o abs mdm2 @ w)
  mnil_); auto.
apply s_ConjML with
 (pres p53)
 (pres mdm2)
 (w) 
 mnil_
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)); auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres dNAdam +o abs dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd (abs dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_DisjAR1; auto.
apply s_ConjAR; auto.
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  mnil_))
 (madd (pres mdm2 @ w)
  mnil_); auto.
apply s_ConjMR with
 (madd (pres p53 @ w)
  mnil_)
 (madd (pres dNAdam @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_copy with
 (dagger s_rule5)
 (0)
 (madd (dagger s_rule5 @ 0)
  (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); simpl; auto.
unfold s_rule5; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres p53 *o pres 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)
 (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd ((pres p53 *o pres 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 @ 0)
  (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); auto.
apply s_AtL with
 (pres p53 *o pres 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)
 (0)
 (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd (pres p53 *o pres 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)
  (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))); auto.
apply s_ImpL with
 (pres p53 *o pres 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) 
 (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  mnil_))
 (madd (pres mdm2 @ w)
  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)
  (madd (pres mdm2 @ w)
  mnil_)); auto.
apply s_ConjMR with
 (madd (pres p53 @ w)
  mnil_)
 (madd (pres dNAdam @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
unfold step; auto.
apply s_DownR; auto.
apply s_AtR; 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) 
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (step (abs p53 *o abs dNAdam) @ w)
  (madd (down (fun W1 => !! ((pres mdm2 at W1 ->> pres mdm2 at (W1 + 1)) &a (abs mdm2 at W1 ->> abs mdm2 at (W1 + 1)))) @ w)
  (madd (pres mdm2 @ w)
  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)
 (madd (step (abs p53 *o abs dNAdam) @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (step (abs p53 *o abs dNAdam) @ w)
  (madd (!! ((pres mdm2 at w ->> pres mdm2 at (w + 1)) &a (abs mdm2 at w ->> abs mdm2 at (w + 1))) @ w)
  (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).
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 ->> pres mdm2 at (w + 1)) &a (abs mdm2 at w ->> abs mdm2 at (w + 1)))
 (w)
 (madd (step (abs p53 *o abs dNAdam) @ w)
  (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_copy with
 ((pres mdm2 at w ->> pres mdm2 at (w + 1)) &a (abs mdm2 at w ->> abs mdm2 at (w + 1)))
 (w) 
 (madd ((pres mdm2 at w ->> pres mdm2 at (w + 1)) &a (abs mdm2 at w ->> abs mdm2 at (w + 1)) @ w)
  (madd (step (abs p53 *o abs dNAdam) @ w)
  (madd (pres mdm2 @ w)
  mnil_))); simpl; auto.
apply s_ConjAL1 with
 (pres mdm2 at w ->> pres mdm2 at (w + 1))
 (abs mdm2 at w ->> abs mdm2 at (w + 1))
 (w) 
 (madd (step (abs p53 *o abs dNAdam) @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres mdm2 at w ->> pres mdm2 at (w + 1) @ w)
  (madd (step (abs p53 *o abs dNAdam) @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_ImpL with
 (pres mdm2 at w)
 (pres mdm2 at (w + 1))
 (w) 
 (madd (pres mdm2 @ w)
  mnil_)
 (madd (step (abs p53 *o abs dNAdam) @ w)
  mnil_)
 (madd (pres mdm2 at (w + 1) @ w)
  (madd (step (abs p53 *o abs dNAdam) @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_AtR; auto.
apply s_init; auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (abs p53 *o abs dNAdam) at (W1 + 1))
 (w)
 (madd (pres mdm2 at (w + 1) @ w)
  mnil_)
 (madd (pres mdm2 at (w + 1) @ w)
  (madd ((abs p53 *o abs dNAdam) at (w + 1) @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
repeat (inversion_clear H).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_AtL with
 (abs p53 *o abs dNAdam)
 (w + 1)
 (w)
 (madd (pres mdm2 at (w + 1) @ w)
  mnil_)
 (madd (pres mdm2 at (w + 1) @ w)
  (madd (abs p53 *o abs 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).
repeat (inversion_clear H).
apply s_ConjML with
 (abs p53)
 (abs dNAdam)
 (w + 1) 
 (madd (pres mdm2 at (w + 1) @ w)
  mnil_)
 (madd (pres mdm2 at (w + 1) @ w)
  (madd (abs p53 @ w + 1)
  (madd (abs dNAdam @ w + 1)
  mnil_))); auto.
unfold munion,madd; simpl; auto.
apply ms_perm231; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
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)
 (w + 1)
 (w)
 (madd (abs p53 @ w + 1)
  (madd (abs dNAdam @ w + 1)
  mnil_))
 (madd (pres mdm2 @ w + 1)
  (madd (abs p53 @ w + 1)
  (madd (abs dNAdam @ w + 1)
  mnil_))); auto.
apply s_ConjMR with
 (madd (pres mdm2 @ w + 1)
  (madd (abs p53 @ w + 1)
  mnil_))
 (madd (abs dNAdam @ w + 1)
  mnil_); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs p53 @ w + 1)
  mnil_)
 (madd (pres mdm2 @ w + 1)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  (madd (pres p53 @ w)
  mnil_))
 (madd (pres mdm2 @ w)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres p53 @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_ConjML with
 (abs p53)
 (abs mdm2)
 (w) 
 mnil_
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR2; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd (pres dNAdam +o abs dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)))
 (madd (abs dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); auto.
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (abs mdm2 @ w)
  mnil_); auto.
apply s_DisjAR1; auto.
apply s_DisjAR1; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  mnil_)
 (madd (pres dNAdam @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (abs mdm2 @ w)
  mnil_); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs p53 @ w)
  mnil_)
 (madd (abs dNAdam @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
(* End of subgoal *)
clear n; intro n; case n.
intros A B h1 h2; inversion_clear h1; inversion_clear h2.
(* automatically generated subproof property4_6 of the subgoal:
  LL := pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) : oo world atm tm
  RR := pres p53 *o abs mdm2 +o (abs p53 *o pres mdm2) *o dont_care dNAdam
     : oo world atm tm
  Gamma := s_system : list judg_
  w : world
  n : nat
  A : oo_
  B : oo_
  ============================
   seq_ Gamma mnil_
     (LL ->>
      abs dNAdam *o abs mdm2 *o dont_care p53 &a step RR +o
      (pres dNAdam *o abs mdm2 +o (abs dNAdam *o pres mdm2) +o
       (pres dNAdam *o pres mdm2) *o dont_care p53) @ w) *)
apply s_ImpR with
(madd (pres p53 *o pres mdm2 +o (abs p53 *o abs mdm2) @ w)
  mnil_); auto.
apply s_DisjAL with
 (pres p53 *o pres mdm2)
 (abs p53 *o abs mdm2)
 (w) 
 mnil_
 (madd (pres p53 *o pres mdm2 @ w)
  mnil_)
 (madd (abs p53 *o abs mdm2 @ w)
  mnil_); auto.
apply s_ConjML with
 (pres p53)
 (pres mdm2)
 (w) 
 mnil_
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)); auto.
apply s_DisjAR2; auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres dNAdam +o abs dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_)))
 (madd (abs dNAdam @ w)
  (madd (pres p53 @ w)
  (madd (pres mdm2 @ w)
  mnil_))); auto.
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_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_DisjAR1; auto.
apply s_init; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  (madd (pres mdm2 @ w)
  mnil_))
 (madd (pres p53 @ w)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_DisjAR1; auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  mnil_)
 (madd (pres mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR1; auto.
apply s_init; auto.
apply s_ConjML with
 (abs p53)
 (abs mdm2)
 (w) 
 mnil_
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)); auto.
apply s_copy with
 (dagger (pres dNAdam +o abs dNAdam))
 (0) 
 (madd (dagger (pres dNAdam +o abs dNAdam) @ 0)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); simpl; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (pres dNAdam +o abs dNAdam) at W1)
 (0)
 (w)
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd ((pres dNAdam +o abs dNAdam) at w @ 0)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); auto.
apply s_AtL with
 (pres dNAdam +o abs dNAdam)
 (w)
 (0)
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd (pres dNAdam +o abs dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); auto.
apply s_DisjAL with
 (pres dNAdam)
 (abs dNAdam)
 (w) 
 (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd (pres dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)))
 (madd (abs dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_))); auto.
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (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_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_DisjAR1; auto.
apply s_ConjMR with
 (madd (pres dNAdam @ w)
  mnil_)
 (madd (abs mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_DisjAR1; auto.
apply s_ConjAR; auto.
apply s_ConjMR with
 (madd (abs dNAdam @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (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_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 dNAdam @ w)
  mnil_)
 (madd (abs mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
apply s_copy with
 (dagger s_rule6)
 (0)
 (madd (dagger s_rule6 @ 0)
  (madd (abs dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)))); simpl; auto.
unfold s_rule6; auto.
unfold dagger; auto.
unfold oo2daggerJudg; simpl; tauto.
apply s_WallL with
 (fun W1 => (abs dNAdam *o abs mdm2 ->> step (abs dNAdam *o pres mdm2) *o down (fun W2 => !! ((pres p53 at W2 ->> pres p53 at (W2 + 1)) &a (abs p53 at W2 ->> abs p53 at (W2 + 1))))) at W1)
 (0)
 (w)
 (madd (abs dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)))
 (madd ((abs dNAdam *o abs mdm2 ->> step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1))))) at w @ 0)
  (madd (abs dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)))); auto.
apply s_AtL with
 (abs dNAdam *o abs mdm2 ->> step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))))
 (w)
 (0)
 (madd (abs dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)))
 (madd (abs dNAdam *o abs mdm2 ->> step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))) @ w)
  (madd (abs dNAdam @ w)
  (madd (abs p53 @ w)
  (madd (abs mdm2 @ w)
  mnil_)))); auto.
apply s_ImpL with
 (abs dNAdam *o abs mdm2)
 (step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))))
 (w) 
 (madd (abs dNAdam @ w)
  (madd (abs mdm2 @ w)
  mnil_))
 (madd (abs p53 @ w)
  mnil_)
 (madd (step (abs dNAdam *o pres mdm2) *o down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))) @ w)
  (madd (abs p53 @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_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 dNAdam @ w)
  mnil_)
 (madd (abs mdm2 @ w)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
unfold step; auto.
apply s_DownR; auto.
apply s_AtR; auto.
apply s_ConjML with
 (step (abs dNAdam *o pres mdm2))
 (down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))))
 (w) 
 (madd (abs p53 @ w)
  mnil_)
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (down (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1)))) @ w)
  (madd (abs p53 @ w)
  mnil_))); auto.
apply s_DownL with
 (fun W1 => !! ((pres p53 at W1 ->> pres p53 at (W1 + 1)) &a (abs p53 at W1 ->> abs p53 at (W1 + 1))))
 (w)
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (!! ((pres p53 at w ->> pres p53 at (w + 1)) &a (abs p53 at w ->> abs p53 at (w + 1))) @ w)
  (madd (abs p53 @ w)
  mnil_))); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
specialize (H 0); repeat (inversion_clear 0).
apply s_BangL with
 ((pres p53 at w ->> pres p53 at (w + 1)) &a (abs p53 at w ->> abs p53 at (w + 1)))
 (w)
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_copy with
 ((pres p53 at w ->> pres p53 at (w + 1)) &a (abs p53 at w ->> abs p53 at (w + 1)))
 (w) 
 (madd ((pres p53 at w ->> pres p53 at (w + 1)) &a (abs p53 at w ->> abs p53 at (w + 1)) @ w)
  (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))); simpl; auto.
apply s_ConjAL2 with
 (pres p53 at w ->> pres p53 at (w + 1))
 (abs p53 at w ->> abs p53 at (w + 1))
 (w) 
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))
 (madd (abs p53 at w ->> abs p53 at (w + 1) @ w)
  (madd (step (abs dNAdam *o pres mdm2) @ w)
  (madd (abs p53 @ w)
  mnil_))); auto.
apply s_ImpL with
 (abs p53 at w)
 (abs p53 at (w + 1))
 (w) 
 (madd (abs p53 @ w)
  mnil_)
 (madd (step (abs dNAdam *o pres mdm2) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd (step (abs dNAdam *o pres mdm2) @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_AtR; auto.
apply s_init; auto.
unfold step; auto.
apply s_DownL with
 (fun W1 => (abs dNAdam *o pres mdm2) at (W1 + 1))
 (w)
 (madd (abs p53 at (w + 1) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd ((abs dNAdam *o pres mdm2) at (w + 1) @ w)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
repeat (inversion_clear H).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_AtL with
 (abs dNAdam *o pres mdm2)
 (w + 1)
 (w)
 (madd (abs p53 at (w + 1) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd (abs dNAdam *o pres mdm2 @ w + 1)
  mnil_)); auto.
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
repeat (inversion_clear H).
apply s_ConjML with
 (abs dNAdam)
 (pres mdm2)
 (w + 1) 
 (madd (abs p53 at (w + 1) @ w)
  mnil_)
 (madd (abs p53 at (w + 1) @ w)
  (madd (abs dNAdam @ w + 1)
  (madd (pres mdm2 @ w + 1)
  mnil_))); auto.
unfold munion,madd; simpl; auto.
apply ms_perm231; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
unfold munion,madd; simpl; auto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_AtL with
 (abs p53)
 (w + 1)
 (w)
 (madd (abs dNAdam @ w + 1)
  (madd (pres mdm2 @ w + 1)
  mnil_))
 (madd (abs p53 @ w + 1)
  (madd (abs dNAdam @ w + 1)
  (madd (pres mdm2 @ w + 1)
  mnil_))); auto.
apply s_ConjMR with
 (madd (abs p53 @ w + 1)
  (madd (pres mdm2 @ w + 1)
  mnil_))
 (madd (abs dNAdam @ w + 1)
  mnil_); auto.
unfold munion,madd; simpl; auto.
apply ms_eq_cons; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
apply ms_perm21; try (apply eqj_refl);
  try (apply eq_nat_refl); try (apply eqatm_refl); eauto.
repeat split; right; auto; intros [hh _];  repeat (inversion_clear 0).
apply s_DisjAR2; auto.
apply s_ConjMR with
 (madd (abs p53 @ w + 1)
  mnil_)
 (madd (pres mdm2 @ w + 1)
  mnil_); auto.
apply s_init; auto.
apply s_init; auto.
apply s_DisjAR2; auto.
apply s_init; auto.
clear n; intros n A B h1 h2.
inversion h1.
Qed.

End property4.