---

Step * of Lemma prior-val-as-latest-val

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)]. ∀[e,p:E].
  (((X)' es e) = ((X)- es p) ∈ bag(T)) supposing 
     ((∀e'':E. ((e'' <loc e) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X))) and 
     (p <loc e))
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀Info,T:Type. ∀es:EO+(Info). ∀X:EClass(T). ∀e,p:E.
  ((p <loc e) ⇒ (∀e'':E. ((e'' <loc e) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X))) ⇒ (((X)' es e) = ((X)- es p) ∈ bag(T)))

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T)].  \mforall{}[e,p:E].
    (((X)'  es  e)  =  ((X)\msupminus{}  es  p))  supposing 
          ((\mforall{}e'':E.  ((e''  <loc  e)  {}\mRightarrow{}  (p  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  X)))  and 
          (p  <loc  e))


By

---

Latex:
(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index