---

Step * of Lemma es-local-relation_wf

∀[Info:Type]. ∀[R:Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ]. ∀[es:EO+(Info)]. ∀[e1,e2:E].
  (es-local-relation(i,j,L1,L2.R[i;j;L1;L2];es;e1;e2) ∈ ℙ)
BY
{ (ProveWfLemma THEN MemTypeCD THEN Auto THEN Unfold `es-le-before` 0 THEN Auto') }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2:E].
    (es-local-relation(i,j,L1,L2.R[i;j;L1;L2];es;e1;e2)  \mmember{}  \mBbbP{})


By

(ProveWfLemma  THEN  MemTypeCD  THEN  Auto  THEN  Unfold  `es-le-before`  0  THEN  Auto')

---

Home Index