---

Step * of Lemma list-eo-property

∀[Info:Type]. ∀L:Info List+. ∀i:Id.  ∃e:E. (L = map(λe.info(e);≤loc(e)) ∈ (Info List))
BY
{ (Auto
   THEN (Assert ||L|| - 1 ∈ E BY
               (DVar `L' THEN RWO "list-eo-E-sq" 0⋅ THEN Auto))
   THEN (With ⌜||L|| - 1⌝ (D 0)⋅ THENA Auto)
   THEN RWO "list-eo-info-le-before" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}L:Info  List\msupplus{}.  \mforall{}i:Id.    \mexists{}e:E.  (L  =  map(\mlambda{}e.info(e);\mleq{}loc(e)))


By

---

Latex:
(Auto
  THEN  (Assert  ||L||  -  1  \mmember{}  E  BY
                          (DVar  `L'  THEN  RWO  "list-eo-E-sq"  0\mcdot{}  THEN  Auto))
  THEN  (With  \mkleeneopen{}||L||  -  1\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  RWO  "list-eo-info-le-before"  0
  THEN  Auto)

---

Home Index