---

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


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 
BY
{ ((HypSubst (-1) 0)
   THEN Auto
   THEN BLemma `pos_length`
   THEN Auto
   THEN RWO "es-interval-nil" 0
   THEN Auto
   THEN RWO "es-le-not-locl<" 0
   THEN Auto) }

---

Latex:



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]
9.  hd([a,  b])  =  a
10.  hd([c,  d])  =  c
11.  z  :  E  List
12.  z  =  [c,  d]
\mvdash{}  ||z||  \mgeq{}  1 


By

((HypSubst  (-1)  0)
  THEN  Auto
  THEN  BLemma  `pos\_length`
  THEN  Auto
  THEN  RWO  "es-interval-nil"  0
  THEN  Auto
  THEN  RWO  "es-le-not-locl<"  0
  THEN  Auto)

---

Home Index