---

Step * of Lemma pred-member-es-open-interval

∀[es:EO]. ∀[e1,e2:E]. ∀[n:{1..||(e1, e2)||-}].  (pred((e1, e2)[n]) = (e1, e2)[n - 1] ∈ E)
BY
{ (Auto
   THEN (D (-1) THENA Auto)
   THEN (InstLemma `es-open-interval-ordered-inst` [⌜es⌝;⌜e1⌝;⌜e2⌝;⌜n - 1⌝;⌜n⌝]⋅ THENA Auto)
   THEN (Assert ⌜(pred((e1, e2)[n]) <loc (e1, e2)[n])⌝⋅ THENA Auto)) }

1
1. es : EO
2. e1 : E
3. e2 : E
4. n : ℤ
5. 1 ≤ n < ||(e1, e2)||
6. ((e1, e2)[n - 1] <loc (e1, e2)[n])
7. (pred((e1, e2)[n]) <loc (e1, e2)[n])
⊢ pred((e1, e2)[n]) = (e1, e2)[n - 1] ∈ E

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[e1,e2:E].  \mforall{}[n:\{1..||(e1,  e2)||\msupminus{}\}].    (pred((e1,  e2)[n])  =  (e1,  e2)[n  -  1])


By

---

Latex:
(Auto
  THEN  (D  (-1)  THENA  Auto)
  THEN  (InstLemma  `es-open-interval-ordered-inst`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(pred((e1,  e2)[n])  <loc  (e1,  e2)[n])\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index