---

Step * 1 of Lemma es-hist-is-concat


1. [Info] : Type
2. es : EO+(Info)@i'
⊢ ∀e1,e2:E.
    ∀L:Info List
      (∃f:ℕ||[]|| + 1 ─→ E
        ((((f 0) = e1 ∈ E) ∧ f ||[]|| ≤loc e2 )
        c∧ (∀i:ℕ||[]||. (f i <loc f (i + 1)))
        c∧ ((∀i:ℕ||[]||. (es-hist(es;f i;pred(f (i + 1))) = [][i] ∈ (Info List)))
           ∧ (es-hist(es;f ||[]||;e2) = L ∈ (Info List))))) supposing 
         ((es-hist(es;e1;e2) = (concat([]) @ L) ∈ (Info List)) and 
         (¬(L = [] ∈ (Info List))) and 
         (∀L∈[].¬(L = [] ∈ (Info List)))) 
    supposing loc(e1) = loc(e2) ∈ Id
BY
{ (Reduce 0
   THEN (Using [`i',i] Auto)⋅
   THEN Auto
   THEN (InstConcl [λx.e1])⋅
   THEN Reduce 0
   THEN (Using [`i',i] Auto)⋅
   THEN Auto) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. loc(e1) = loc(e2) ∈ Id
6. L : Info List@i
7. (∀L∈[].¬(L = [] ∈ (Info List)))
8. ¬(L = [] ∈ (Info List))
9. es-hist(es;e1;e2) = L ∈ (Info List)
10. e1 = e1 ∈ E
⊢ e1 ≤loc e2 

---

Latex:



1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
\mvdash{}  \mforall{}e1,e2:E.
        \mforall{}L:Info  List
            (\mexists{}f:\mBbbN{}||[]||  +  1  {}\mrightarrow{}  E
                ((((f  0)  =  e1)  \mwedge{}  f  ||[]||  \mleq{}loc  e2  )
                c\mwedge{}  (\mforall{}i:\mBbbN{}||[]||.  (f  i  <loc  f  (i  +  1)))
                c\mwedge{}  ((\mforall{}i:\mBbbN{}||[]||.  (es-hist(es;f  i;pred(f  (i  +  1)))  =  [][i]))
                      \mwedge{}  (es-hist(es;f  ||[]||;e2)  =  L))))  supposing 
                  ((es-hist(es;e1;e2)  =  (concat([])  @  L))  and 
                  (\mneg{}(L  =  []))  and 
                  (\mforall{}L\mmember{}[].\mneg{}(L  =  []))) 
        supposing  loc(e1)  =  loc(e2)


By

(Reduce  0
  THEN  (Using  [`i',i]  Auto)\mcdot{}
  THEN  Auto
  THEN  (InstConcl  [\mlambda{}x.e1])\mcdot{}
  THEN  Reduce  0
  THEN  (Using  [`i',i]  Auto)\mcdot{}
  THEN  Auto)

---

Home Index