---

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

.....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)
BY
{ RWO "es-locl-iff" (-3)
THEN Auto
THEN D -3 }

1
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. ¬↑first(e)
9. p = pred(e) ∈ E
10. ∀e'':E. ((e'' <loc e) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X))@i
11. ¬↑pred(e) ∈b X
⊢ ((X)' es pred(e)) = ((X)- es p) ∈ bag(T)

2
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. ¬↑first(e)
9. (p <loc pred(e))
10. ∀e'':E. ((e'' <loc e) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X))@i
11. ¬↑pred(e) ∈b X
⊢ ((X)' es pred(e)) = ((X)- es p) ∈ bag(T)

---

Latex:

---

Latex:
.....falsecase..... 
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.  \mneg{}\muparrow{}pred(e)  \mmember{}\msubb{}  X
\mvdash{}  ((X)'  es  pred(e))  =  ((X)\msupminus{}  es  p)


By

---

Latex:
RWO  "es-locl-iff"  (-3)
THEN  Auto
THEN  D  -3

---

Home Index