---

Step * 1 of Lemma es-interval-one-one

.....assertion..... 
1. es : EO
2. d : E
3. b : E
4. a : E
5. c : E
6. a ≤loc b 
7. c ≤loc d 
8. [a, b] = [c, d] ∈ (E List)
⊢ a = c ∈ E
BY
{ (((((InstLemma `hd-es-interval` [es; a; b])⋅ THENA Auto) THEN (InstLemma `hd-es-interval` [es; c; d])⋅) THENA Auto)
   THEN (StrongHypSubst (-3) (-2))
   THEN Auto) }

1
1. es : EO
2. d : E
3. b : E
4. a : E
5. c : E
6. a ≤loc b 
7. c ≤loc d 
8. [a, b] = [c, d] ∈ (E List)
9. hd([a, b]) = a ∈ E
10. hd([c, d]) = c ∈ E
11. z : E List
12. z = [c, d] ∈ (E List)
⊢ ||z|| ≥ 1 

---

Latex:


.....assertion..... 
1.  es  :  EO
2.  d  :  E
3.  b  :  E
4.  a  :  E
5.  c  :  E
6.  a  \mleq{}loc  b 
7.  c  \mleq{}loc  d 
8.  [a,  b]  =  [c,  d]
\mvdash{}  a  =  c


By

(((((InstLemma  `hd-es-interval`  [es;  a;  b])\mcdot{}  THENA  Auto)
      THEN  (InstLemma  `hd-es-interval`  [es;  c;  d])\mcdot{}
      )
    THENA  Auto
    )
  THEN  (StrongHypSubst  (-3)  (-2))
  THEN  Auto)

---

Home Index