---

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


∀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)))
BY
{ RepeatFor 4 ((D 0 THENA Auto))
THEN CausalInd'
THEN Auto
THEN RWO "prior-val-pred" 0
THEN Auto
THEN SplitOnConclITE
THEN Auto }

1
.....truecase..... 
1. Info : Type@i'
2. T : Type@i'
3. es : EO+(Info)@i'
4. X : EClass(T)@i'
5. e : E@i
6. ∀e1:E
     ((e1 < e)
     ⇒ (∀p:E
           ((p <loc e1)
           ⇒ (∀e'':E. ((e'' <loc e1) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X)))
           ⇒ (((X)' es e1) = ((X)- es p) ∈ bag(T)))))
7. p : E@i
8. (p <loc e)@i
9. ∀e'':E. ((e'' <loc e) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X))@i
10. ↑pred(e) ∈b X
⊢ {X(pred(e))} = ((X)- es p) ∈ bag(T)

2
.....falsecase..... 
1. Info : Type@i'
2. T : Type@i'
3. es : EO+(Info)@i'
4. X : EClass(T)@i'
5. e : E@i
6. ∀e1:E
     ((e1 < e)
     ⇒ (∀p:E
           ((p <loc e1)
           ⇒ (∀e'':E. ((e'' <loc e1) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X)))
           ⇒ (((X)' es e1) = ((X)- es p) ∈ bag(T)))))
7. p : E@i
8. (p <loc e)@i
9. ∀e'':E. ((e'' <loc e) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X))@i
10. ¬↑pred(e) ∈b X
⊢ ((X)' es pred(e)) = ((X)- es p) ∈ bag(T)

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  4  ((D  0  THENA  Auto))
THEN  CausalInd'
THEN  Auto
THEN  RWO  "prior-val-pred"  0
THEN  Auto
THEN  SplitOnConclITE
THEN  Auto

---

Home Index