---

Step * 1 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∈(e1,e2].||[e1, pred(e)]|| = ||L1|| ∈ ℤ
⊢ ∃e∈(e1,e2].(es-hist(es;e1;pred(e)) = L1 ∈ (Info List)) ∧ (es-hist(es;e;e2) = L2 ∈ (Info List))
BY
{ ((ParallelLast THEN ParallelLast THEN ExRepD THEN Try (( Complete (Auto))⋅) THEN D 0) THENL [Auto; ExRepD]) }

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 
⊢ (es-hist(es;e1;pred(e)) = L1 ∈ (Info List)) ∧ (es-hist(es;e;e2) = L2 ∈ (Info List))

---

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


By

((ParallelLast  THEN  ParallelLast  THEN  ExRepD  THEN  Try  ((  Complete  (Auto))\mcdot{})  THEN  D  0)
  THENL  [Auto;  ExRepD]
)

---

Home Index