---

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


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. map(λe.info(e);[e1, pred(e)] @ [e, e2]) = (L1 @ L2) ∈ (Info List)
⊢ (es-hist(es;e1;pred(e)) = L1 ∈ (Info List)) ∧ (es-hist(es;e;e2) = L2 ∈ (Info List))
BY
{ (((RWO "map_append_sq" (-1)) THENA Auto)
   THEN (Fold `es-hist` (-1))
   THEN (FLemma `general-append-cancellation` [(-1)])
   THEN Auto⋅) }

1
.....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|| ∈ ℤ)

---

Latex:



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.  map(\mlambda{}e.info(e);[e1,  pred(e)]  @  [e,  e2])  =  (L1  @  L2)
\mvdash{}  (es-hist(es;e1;pred(e))  =  L1)  \mwedge{}  (es-hist(es;e;e2)  =  L2)


By

(((RWO  "map\_append\_sq"  (-1))  THENA  Auto)
  THEN  (Fold  `es-hist`  (-1))
  THEN  (FLemma  `general-append-cancellation`  [(-1)])
  THEN  Auto\mcdot{})

---

Home Index