---

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


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
6. e1 : E@i
7. e2 : E@i
8. loc(e1) = loc(e2) ∈ Id
9. L : Info List@i
10. (∀L∈[LL / L1].¬(L = [] ∈ (Info List)))
11. ¬(L = [] ∈ (Info List))
12. es-hist(es;e1;e2) = (LL @ concat(L1) @ L) ∈ (Info List)
13. e : E
14. (e1 <loc e)
15. e ≤loc e2 
16. es-hist(es;e1;pred(e)) = LL ∈ (Info List)
17. es-hist(es;e;e2) = (concat(L1) @ L) ∈ (Info List)
18. f : ℕ||L1|| + 1 ─→ E
19. (f 0) = e ∈ E
20. f ||L1|| ≤loc e2 
21. ∀i:ℕ||L1||. (f i <loc f (i + 1))
22. ∀i:ℕ||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i] ∈ (Info List))
23. es-hist(es;f ||L1||;e2) = 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))))
BY
{ InstConcl [⌈λx.if (x =z 0) then e1 else f (x - 1) fi ⌉]⋅ }

1
.....wf..... 
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
6. e1 : E@i
7. e2 : E@i
8. loc(e1) = loc(e2) ∈ Id
9. L : Info List@i
10. (∀L∈[LL / L1].¬(L = [] ∈ (Info List)))
11. ¬(L = [] ∈ (Info List))
12. es-hist(es;e1;e2) = (LL @ concat(L1) @ L) ∈ (Info List)
13. e : E
14. (e1 <loc e)
15. e ≤loc e2 
16. es-hist(es;e1;pred(e)) = LL ∈ (Info List)
17. es-hist(es;e;e2) = (concat(L1) @ L) ∈ (Info List)
18. f : ℕ||L1|| + 1 ─→ E
19. (f 0) = e ∈ E
20. f ||L1|| ≤loc e2 
21. ∀i:ℕ||L1||. (f i <loc f (i + 1))
22. ∀i:ℕ||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i] ∈ (Info List))
23. es-hist(es;f ||L1||;e2) = L ∈ (Info List)
⊢ λx.if (x =z 0) then e1 else f (x - 1) fi  ∈ ℕ||[LL / L1]|| + 1 ─→ E

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
6. e1 : E@i
7. e2 : E@i
8. loc(e1) = loc(e2) ∈ Id
9. L : Info List@i
10. (∀L∈[LL / L1].¬(L = [] ∈ (Info List)))
11. ¬(L = [] ∈ (Info List))
12. es-hist(es;e1;e2) = (LL @ concat(L1) @ L) ∈ (Info List)
13. e : E
14. (e1 <loc e)
15. e ≤loc e2 
16. es-hist(es;e1;pred(e)) = LL ∈ (Info List)
17. es-hist(es;e;e2) = (concat(L1) @ L) ∈ (Info List)
18. f : ℕ||L1|| + 1 ─→ E
19. (f 0) = e ∈ E
20. f ||L1|| ≤loc e2 
21. ∀i:ℕ||L1||. (f i <loc f (i + 1))
22. ∀i:ℕ||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i] ∈ (Info List))
23. es-hist(es;f ||L1||;e2) = L ∈ (Info List)
⊢ ((((λx.if (x =z 0) then e1 else f (x - 1) fi ) 0) = e1 ∈ E)
  ∧ (λx.if (x =z 0) then e1 else f (x - 1) fi ) ||[LL / L1]|| ≤loc e2 )
c∧ (∀i:ℕ||[LL / L1]||
      ((λx.if (x =z 0) then e1 else f (x - 1) fi ) i <loc (λx.if (x =z 0) then e1 else f (x - 1) fi ) (i + 1)))
c∧ ((∀i:ℕ||[LL / L1]||
       (es-hist(es;(λx.if (x =z 0) then e1 else f (x - 1) fi ) i;pred((λx.if (x =z 0) then e1 else f (x - 1) fi ) 
                                                                      (i + 1)))
       = [LL / L1][i]
       ∈ (Info List)))
   ∧ (es-hist(es;(λx.if (x =z 0) then e1 else f (x - 1) fi ) ||[LL / L1]||;e2) = L ∈ (Info List)))

3
.....wf..... 
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
6. e1 : E@i
7. e2 : E@i
8. loc(e1) = loc(e2) ∈ Id
9. L : Info List@i
10. (∀L∈[LL / L1].¬(L = [] ∈ (Info List)))
11. ¬(L = [] ∈ (Info List))
12. es-hist(es;e1;e2) = (LL @ concat(L1) @ L) ∈ (Info List)
13. e : E
14. (e1 <loc e)
15. e ≤loc e2 
16. es-hist(es;e1;pred(e)) = LL ∈ (Info List)
17. es-hist(es;e;e2) = (concat(L1) @ L) ∈ (Info List)
18. f : ℕ||L1|| + 1 ─→ E
19. (f 0) = e ∈ E
20. f ||L1|| ≤loc e2 
21. ∀i:ℕ||L1||. (f i <loc f (i + 1))
22. ∀i:ℕ||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i] ∈ (Info List))
23. es-hist(es;f ||L1||;e2) = L ∈ (Info List)
24. f1 : ℕ||[LL / L1]|| + 1 ─→ E
⊢ (((f1 0) = e1 ∈ E) ∧ f1 ||[LL / L1]|| ≤loc e2 )
  c∧ (∀i:ℕ||[LL / L1]||. (f1 i <loc f1 (i + 1)))
  c∧ ((∀i:ℕ||[LL / L1]||. (es-hist(es;f1 i;pred(f1 (i + 1))) = [LL / L1][i] ∈ (Info List)))
     ∧ (es-hist(es;f1 ||[LL / L1]||;e2) = L ∈ (Info List))) ∈ ℙ

---

Latex:



1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  LL  :  Info  List@i
4.  L1  :  Info  List  List@i
5.  \mforall{}e1,e2:E.
          \mforall{}L:Info  List
              (\mexists{}f:\mBbbN{}||L1||  +  1  {}\mrightarrow{}  E
                  ((((f  0)  =  e1)  \mwedge{}  f  ||L1||  \mleq{}loc  e2  )
                  c\mwedge{}  (\mforall{}i:\mBbbN{}||L1||.  (f  i  <loc  f  (i  +  1)))
                  c\mwedge{}  ((\mforall{}i:\mBbbN{}||L1||.  (es-hist(es;f  i;pred(f  (i  +  1)))  =  L1[i]))
                        \mwedge{}  (es-hist(es;f  ||L1||;e2)  =  L))))  supposing 
                    ((es-hist(es;e1;e2)  =  (concat(L1)  @  L))  and 
                    (\mneg{}(L  =  []))  and 
                    (\mforall{}L\mmember{}L1.\mneg{}(L  =  []))) 
          supposing  loc(e1)  =  loc(e2)@i
6.  e1  :  E@i
7.  e2  :  E@i
8.  loc(e1)  =  loc(e2)
9.  L  :  Info  List@i
10.  (\mforall{}L\mmember{}[LL  /  L1].\mneg{}(L  =  []))
11.  \mneg{}(L  =  [])
12.  es-hist(es;e1;e2)  =  (LL  @  concat(L1)  @  L)
13.  e  :  E
14.  (e1  <loc  e)
15.  e  \mleq{}loc  e2 
16.  es-hist(es;e1;pred(e))  =  LL
17.  es-hist(es;e;e2)  =  (concat(L1)  @  L)
18.  f  :  \mBbbN{}||L1||  +  1  {}\mrightarrow{}  E
19.  (f  0)  =  e
20.  f  ||L1||  \mleq{}loc  e2 
21.  \mforall{}i:\mBbbN{}||L1||.  (f  i  <loc  f  (i  +  1))
22.  \mforall{}i:\mBbbN{}||L1||.  (es-hist(es;f  i;pred(f  (i  +  1)))  =  L1[i])
23.  es-hist(es;f  ||L1||;e2)  =  L
\mvdash{}  \mexists{}f:\mBbbN{}||[LL  /  L1]||  +  1  {}\mrightarrow{}  E
      ((((f  0)  =  e1)  \mwedge{}  f  ||[LL  /  L1]||  \mleq{}loc  e2  )
      c\mwedge{}  (\mforall{}i:\mBbbN{}||[LL  /  L1]||.  (f  i  <loc  f  (i  +  1)))
      c\mwedge{}  ((\mforall{}i:\mBbbN{}||[LL  /  L1]||.  (es-hist(es;f  i;pred(f  (i  +  1)))  =  [LL  /  L1][i]))
            \mwedge{}  (es-hist(es;f  ||[LL  /  L1]||;e2)  =  L)))


By

InstConcl  [\mkleeneopen{}\mlambda{}x.if  (x  =\msubz{}  0)  then  e1  else  f  (x  -  1)  fi  \mkleeneclose{}]\mcdot{}

---

Home Index