---

Step * of Lemma es-open-interval-ordered-iff

∀es:EO. ∀e1,e2:E. ∀n1,n2:ℕ||(e1, e2)||.  (n1 < n2 ⇐⇒ ((e1, e2)[n1] <loc (e1, e2)[n2]))
BY
{ (Auto
   THEN Try (Complete ((BLemma `es-open-interval-ordered-inst` THEN Auto)))
   THEN (Assert ⌈n1 < n2 ∨ (n1 = n2 ∈ ℤ) ∨ n2 < n1⌉⋅ THENA Auto)
   THEN RepeatFor 2 ((D (-1) THEN Auto))
   THEN (Assert ⌈False⌉⋅ THEN Auto)
   THEN Try (Complete ((HypSubst' (-1) (-2) THEN FLemma `es-locl_irreflexivity` [-2] THEN Auto)))
   THEN (InstLemma `es-open-interval-ordered-inst` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈n2⌉;⌈n1⌉]⋅ THENA Auto)
   THEN (FLemma `es-locl_transitivity` [-3;-1] THENA Auto)
   THEN FLemma `es-locl_irreflexivity` [-1]
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e1,e2:E.  \mforall{}n1,n2:\mBbbN{}||(e1,  e2)||.    (n1  <  n2  \mLeftarrow{}{}\mRightarrow{}  ((e1,  e2)[n1]  <loc  (e1,  e2)[n2]))


By

(Auto
  THEN  Try  (Complete  ((BLemma  `es-open-interval-ordered-inst`  THEN  Auto)))
  THEN  (Assert  \mkleeneopen{}n1  <  n2  \mvee{}  (n1  =  n2)  \mvee{}  n2  <  n1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((D  (-1)  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Try  (Complete  ((HypSubst'  (-1)  (-2)  THEN  FLemma  `es-locl\_irreflexivity`  [-2]  THEN  Auto)))
  THEN  (InstLemma  `es-open-interval-ordered-inst`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}n2\mkleeneclose{};\mkleeneopen{}n1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FLemma  `es-locl\_transitivity`  [-3;-1]  THENA  Auto)
  THEN  FLemma  `es-locl\_irreflexivity`  [-1]
  THEN  Auto)

---

Home Index