---

Step * 1 of Lemma es-init-eq


∀es:EO. ∀e,e':E.  ((loc(e) = loc(e') ∈ Id) ⇒ (es-init(es;e) = es-init(es;e') ∈ E))
BY
{ (RepeatFor 2 ((LocLessInd THENA Auto))
   THEN Auto
   THEN (UnivCD THENA Auto)
   THEN ((FLemma `es-locl-total` [-1]⋅ THENM SplitOrHyps) THENA Auto)) }

1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e':E. ((loc(k) = loc(e') ∈ Id) ⇒ (es-init(es;k) = es-init(es;e') ∈ E))))@i
5. WellFnd{i}(E;x,y.(x <loc y))
6. j1 : E@i
7. ∀k:E. ((k <loc j1) ⇒ (loc(j) = loc(k) ∈ Id) ⇒ (es-init(es;j) = es-init(es;k) ∈ E))@i
8. loc(j) = loc(j1) ∈ Id@i
9. (j <loc j1)
⊢ es-init(es;j) = es-init(es;j1) ∈ E

2
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e':E. ((loc(k) = loc(e') ∈ Id) ⇒ (es-init(es;k) = es-init(es;e') ∈ E))))@i
5. WellFnd{i}(E;x,y.(x <loc y))
6. j1 : E@i
7. ∀k:E. ((k <loc j1) ⇒ (loc(j) = loc(k) ∈ Id) ⇒ (es-init(es;j) = es-init(es;k) ∈ E))@i
8. loc(j) = loc(j1) ∈ Id@i
9. j = j1 ∈ E
⊢ es-init(es;j) = es-init(es;j1) ∈ E

3
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e':E. ((loc(k) = loc(e') ∈ Id) ⇒ (es-init(es;k) = es-init(es;e') ∈ E))))@i
5. WellFnd{i}(E;x,y.(x <loc y))
6. j1 : E@i
7. ∀k:E. ((k <loc j1) ⇒ (loc(j) = loc(k) ∈ Id) ⇒ (es-init(es;j) = es-init(es;k) ∈ E))@i
8. loc(j) = loc(j1) ∈ Id@i
9. (j1 <loc j)
⊢ es-init(es;j) = es-init(es;j1) ∈ E

---

Latex:



\mforall{}es:EO.  \mforall{}e,e':E.    ((loc(e)  =  loc(e'))  {}\mRightarrow{}  (es-init(es;e)  =  es-init(es;e')))


By

(RepeatFor  2  ((LocLessInd  THENA  Auto))
  THEN  Auto
  THEN  (UnivCD  THENA  Auto)
  THEN  ((FLemma  `es-locl-total`  [-1]\mcdot{}  THENM  SplitOrHyps)  THENA  Auto))

---

Home Index