---

Step * of Lemma ranked-eo-property

∀[Info:Type]
  ∀L:Id ─→ (Info List)
    ∀[rk:(i:Id × ℕ||L i||) ─→ ℕ]
      ∀i:Id. (0 < ||L i|| ⇒ (∃e:E. ((L i) = map(λe.info(e);≤loc(e)) ∈ (Info List)))) 
      supposing ∀i:Id. ∀j:ℕ||L i||. ∀k:ℕj.  rk <i, k> < rk <i, j>
BY
{ (Auto
   THEN (Assert <i, ||L i|| - 1> ∈ E BY
               (BLemma `ranked-eo-E` THEN Auto))
   THEN With ⌈<i, ||L i|| - 1>⌉ (D 0)⋅
   THEN Auto
   THEN (RWO "ranked-eo-info-le-before" 0 THEN Reduce 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}L:Id  {}\mrightarrow{}  (Info  List)
        \mforall{}[rk:(i:Id  \mtimes{}  \mBbbN{}||L  i||)  {}\mrightarrow{}  \mBbbN{}]
            \mforall{}i:Id.  (0  <  ||L  i||  {}\mRightarrow{}  (\mexists{}e:E.  ((L  i)  =  map(\mlambda{}e.info(e);\mleq{}loc(e))))) 
            supposing  \mforall{}i:Id.  \mforall{}j:\mBbbN{}||L  i||.  \mforall{}k:\mBbbN{}j.    rk  <i,  k>  <  rk  <i,  j>


By

---

Latex:
(Auto
  THEN  (Assert  <i,  ||L  i||  -  1>  \mmember{}  E  BY
                          (BLemma  `ranked-eo-E`  THEN  Auto))
  THEN  With  \mkleeneopen{}<i,  ||L  i||  -  1>\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (RWO  "ranked-eo-info-le-before"  0  THEN  Reduce  0)
  THEN  Auto)

---

Home Index