---

Step * of Lemma es-hist-is-concat

∀[Info:Type]
  ∀es:EO+(Info). ∀LL:Info List List. ∀e1,e2:E.
    ∀L:Info List
      (∃f:ℕ||LL|| + 1 ─→ E
        ((((f 0) = e1 ∈ E) ∧ f ||LL|| ≤loc e2 )
        c∧ (∀i:ℕ||LL||. (f i <loc f (i + 1)))
        c∧ ((∀i:ℕ||LL||. (es-hist(es;f i;pred(f (i + 1))) = LL[i] ∈ (Info List)))
           ∧ (es-hist(es;f ||LL||;e2) = L ∈ (Info List))))) supposing 
         ((es-hist(es;e1;e2) = (concat(LL) @ L) ∈ (Info List)) and 
         (¬(L = [] ∈ (Info List))) and 
         (∀L∈LL.¬(L = [] ∈ (Info List)))) 
    supposing loc(e1) = loc(e2) ∈ Id
BY
{ (InductionOnListA THENA (Auto THEN InstHyp [⌈i⌉] (-2)⋅ THEN Auto)) }

1
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

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. LL : Info List@i
4. L1 : Info List List@i
5. ∀e1,e2:E.
     ∀L:Info List
       (∃f:ℕ||L1|| + 1 ─→ E
         ((((f 0) = e1 ∈ E) ∧ f ||L1|| ≤loc e2 )
         c∧ (∀i:ℕ||L1||. (f i <loc f (i + 1)))
         c∧ ((∀i:ℕ||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i] ∈ (Info List)))
            ∧ (es-hist(es;f ||L1||;e2) = L ∈ (Info List))))) supposing 
          ((es-hist(es;e1;e2) = (concat(L1) @ L) ∈ (Info List)) and 
          (¬(L = [] ∈ (Info List))) and 
          (∀L∈L1.¬(L = [] ∈ (Info List)))) 
     supposing loc(e1) = loc(e2) ∈ Id@i
⊢ ∀e1,e2:E.
    ∀L:Info List
      (∃f:ℕ||[LL / L1]|| + 1 ─→ E
        ((((f 0) = e1 ∈ E) ∧ f ||[LL / L1]|| ≤loc e2 )
        c∧ (∀i:ℕ||[LL / L1]||. (f i <loc f (i + 1)))
        c∧ ((∀i:ℕ||[LL / L1]||. (es-hist(es;f i;pred(f (i + 1))) = [LL / L1][i] ∈ (Info List)))
           ∧ (es-hist(es;f ||[LL / L1]||;e2) = L ∈ (Info List))))) supposing 
         ((es-hist(es;e1;e2) = (concat([LL / L1]) @ L) ∈ (Info List)) and 
         (¬(L = [] ∈ (Info List))) and 
         (∀L∈[LL / L1].¬(L = [] ∈ (Info List)))) 
    supposing loc(e1) = loc(e2) ∈ Id

---

Latex:


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


By

(InductionOnListA  THENA  (Auto  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto))

---

Home Index