Step
*
of Lemma
es-interface-or-right-property
∀[Info,A:Type]. ∀[X:EClass(Top)]. ∀[Y:EClass(A)].
es-interface-or-right((X | Y)) = Y ∈ EClass(A) supposing Singlevalued(Y)
BY
{ (Auto
THEN Unfold `eclass` 0
THEN Ext
THEN Auto
THEN RenameVar `es' (-1)
THEN (Try ((Fold `eclass` 0 THEN Auto))
THEN Ext
THEN Auto
THEN RenameVar `e' (-1)
THEN (Try ((Fold `eclass` 0 THEN Auto))
THEN (RepUR ``es-interface-or-right es-interface-or eclass-compose2 `` 0
THEN RepUR ``oob-apply es-filter-image eclass-compose1`` 0
THEN RepeatFor 2 (AutoSplit)
THEN (ElimBagSizeOne'
THEN RepUR ``oob-getright? oob-hasright oob-getright`` 0
THEN Auto
THEN RWO "bag-size-zero" 0
THEN Auto
THEN Try ((Fold `empty-bag` 0⋅ THEN Auto))
THEN ((With ⌈es⌉ (D 5)⋅ THENA Auto) THEN InstHyp [⌈e⌉] (-1)⋅ THEN Auto')⋅)⋅)⋅
)⋅)⋅) }
Latex:
Latex:
\mforall{}[Info,A:Type]. \mforall{}[X:EClass(Top)]. \mforall{}[Y:EClass(A)].
es-interface-or-right((X | Y)) = Y supposing Singlevalued(Y)
By
Latex:
(Auto
THEN Unfold `eclass` 0
THEN Ext
THEN Auto
THEN RenameVar `es' (-1)
THEN (Try ((Fold `eclass` 0 THEN Auto))
THEN Ext
THEN Auto
THEN RenameVar `e' (-1)
THEN (Try ((Fold `eclass` 0 THEN Auto))
THEN (RepUR ``es-interface-or-right es-interface-or eclass-compose2 `` 0
THEN RepUR ``oob-apply es-filter-image eclass-compose1`` 0
THEN RepeatFor 2 (AutoSplit)
THEN (ElimBagSizeOne'
THEN RepUR ``oob-getright? oob-hasright oob-getright`` 0
THEN Auto
THEN RWO "bag-size-zero" 0
THEN Auto
THEN Try ((Fold `empty-bag` 0\mcdot{} THEN Auto))
THEN ((With \mkleeneopen{}es\mkleeneclose{} (D 5)\mcdot{} THENA Auto) THEN InstHyp [\mkleeneopen{}e\mkleeneclose{}] (-1)\mcdot{} THEN Auto')\mcdot{})
\mcdot{})\mcdot{}
)\mcdot{})\mcdot{})
Home
Index