---

Step * of Lemma es-init_wf

∀[es:EO]. ∀[e:E].  (es-init(es;e) ∈ E)
BY
{ (Auto
   THEN Unfold `es-init` 0
   THEN Unfold `bfalse` 0
   THEN Auto
   THEN (InstLemma `es-causl-swellfnd` [⌈es⌉]⋅ THENA Auto)
   THEN (((InstLemma `strongwf-monotone` [⌈E⌉; ⌈λ2x.λy.(x < y)⌉])⋅ THENA Auto)
         THEN (BHyp -1 
               THEN Auto
               THEN RepUR ``p-graph so_lambda rel_implies bfalse`` 0⋅
               THEN Auto
               THEN MoveToConcl (-1)
               THEN RepUR ``can-apply do-apply`` 0
               THEN AutoSplit⋅
               THEN Auto
               THEN D (-1)
               THEN Auto)⋅
         )⋅) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    (es-init(es;e)  \mmember{}  E)


By

(Auto
  THEN  Unfold  `es-init`  0
  THEN  Unfold  `bfalse`  0
  THEN  Auto
  THEN  (InstLemma  `es-causl-swellfnd`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (((InstLemma  `strongwf-monotone`  [\mkleeneopen{}E\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}x.\mlambda{}y.(x  <  y)\mkleeneclose{}])\mcdot{}  THENA  Auto)
              THEN  (BHyp  -1 
                          THEN  Auto
                          THEN  RepUR  ``p-graph  so\_lambda  rel\_implies  bfalse``  0\mcdot{}
                          THEN  Auto
                          THEN  MoveToConcl  (-1)
                          THEN  RepUR  ``can-apply  do-apply``  0
                          THEN  AutoSplit\mcdot{}
                          THEN  Auto
                          THEN  D  (-1)
                          THEN  Auto)\mcdot{}
              )\mcdot{})

---

Home Index