---

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

.....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
11. p = pred(e) ∈ E
12. ↑p ∈b X
⊢ {X(pred(e))} = {X(p)} ∈ bag(T)
BY
{ EqCD
THEN Auto }

---

Latex:

---

Latex:
.....truecase..... 
1.  Info  :  Type@i'
2.  T  :  Type@i'
3.  es  :  EO+(Info)@i'
4.  X  :  EClass(T)@i'
5.  e  :  E@i
6.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  (\mforall{}p:E
                      ((p  <loc  e1)
                      {}\mRightarrow{}  (\mforall{}e'':E.  ((e''  <loc  e1)  {}\mRightarrow{}  (p  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  X)))
                      {}\mRightarrow{}  (((X)'  es  e1)  =  ((X)\msupminus{}  es  p)))))
7.  p  :  E@i
8.  (p  <loc  e)@i
9.  \mforall{}e'':E.  ((e''  <loc  e)  {}\mRightarrow{}  (p  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  X))@i
10.  \muparrow{}pred(e)  \mmember{}\msubb{}  X
11.  p  =  pred(e)
12.  \muparrow{}p  \mmember{}\msubb{}  X
\mvdash{}  \{X(pred(e))\}  =  \{X(p)\}


By

---

Latex:
EqCD
THEN  Auto

---

Home Index