---

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

.....antecedent..... 
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)
20. (es-hist(es;e1;pred(e)) @ es-hist(es;e;e2)) = (L1 @ L2) ∈ (Info List)
⊢ (||es-hist(es;e1;pred(e))|| = ||L1|| ∈ ℤ) ∨ (||es-hist(es;e;e2)|| = ||L2|| ∈ ℤ)
BY
{ ((D (-1)) THEN Unfold `es-hist` 0 THEN RWO "length-map" 0 THEN Auto) }

---

Latex:


.....antecedent..... 
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])
20.  (es-hist(es;e1;pred(e))  @  es-hist(es;e;e2))  =  (L1  @  L2)
\mvdash{}  (||es-hist(es;e1;pred(e))||  =  ||L1||)  \mvee{}  (||es-hist(es;e;e2)||  =  ||L2||)


By

((D  (-1))  THEN  Unfold  `es-hist`  0  THEN  RWO  "length-map"  0  THEN  Auto)

---

Home Index