---

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

.....assertion..... 
1. Info : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. L1 : Info List@i
6. L2 : Info List@i
7. ¬(L1 = [] ∈ (Info List))
8. ¬(L2 = [] ∈ (Info List))
9. map(λe.info(e);[e1, e2]) = (L1 @ L2) ∈ (Info List)
10. ||[e1, e2]|| = (||L1|| + ||L2||) ∈ ℤ
11. ||L2|| ≥ 1 
12. ||L1|| ≥ 1 
13. e : E
14. (e1 <loc e)
15. e ≤loc e2 
16. ||[e1, pred(e)]|| = ||L1|| ∈ ℤ
17. (e1 <loc e)
18. e ≤loc e2 
19. [e1, e2] = ([e1, pred(e)] @ [e, e2]) ∈ (E List)
⊢ map(λe.info(e);[e1, pred(e)] @ [e, e2]) = (L1 @ L2) ∈ (Info List)
BY
{ StrongRevHypSubst (-1) 0 }

1
1. Info : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. L1 : Info List@i
6. L2 : Info List@i
7. ¬(L1 = [] ∈ (Info List))
8. ¬(L2 = [] ∈ (Info List))
9. map(λe.info(e);[e1, e2]) = (L1 @ L2) ∈ (Info List)
10. ||[e1, e2]|| = (||L1|| + ||L2||) ∈ ℤ
11. ||L2|| ≥ 1 
12. ||L1|| ≥ 1 
13. e : E
14. (e1 <loc e)
15. e ≤loc e2 
16. ||[e1, pred(e)]|| = ||L1|| ∈ ℤ
17. (e1 <loc e)
18. e ≤loc e2 
19. [e1, e2] = ([e1, pred(e)] @ [e, e2]) ∈ (E List)
⊢ map(λe.info(e);[e1, e2]) = (L1 @ L2) ∈ (Info List)

---

Latex:


.....assertion..... 
1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  e1  :  E@i
4.  e2  :  E@i
5.  L1  :  Info  List@i
6.  L2  :  Info  List@i
7.  \mneg{}(L1  =  [])
8.  \mneg{}(L2  =  [])
9.  map(\mlambda{}e.info(e);[e1,  e2])  =  (L1  @  L2)
10.  ||[e1,  e2]||  =  (||L1||  +  ||L2||)
11.  ||L2||  \mgeq{}  1 
12.  ||L1||  \mgeq{}  1 
13.  e  :  E
14.  (e1  <loc  e)
15.  e  \mleq{}loc  e2 
16.  ||[e1,  pred(e)]||  =  ||L1||
17.  (e1  <loc  e)
18.  e  \mleq{}loc  e2 
19.  [e1,  e2]  =  ([e1,  pred(e)]  @  [e,  e2])
\mvdash{}  map(\mlambda{}e.info(e);[e1,  pred(e)]  @  [e,  e2])  =  (L1  @  L2)


By

StrongRevHypSubst  (-1)  0

---

Home Index