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:
Latex:
\mforall{}[es:EO]. \mforall{}[e:E]. (es-init(es;e) \mmember{} E)
By
Latex:
(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