Step
*
of Lemma
CCC-compact
∀K:Type. (CCCNSet(K)
⇒ compact-type(K))
BY
{ (InstLemma `CCC-omni` []
THEN RepeatFor 2 ((ParallelLast' THENA Auto))
THEN (D 0 THENA Auto)
THEN (InstHyp [⌜λ2x.¬↑(p x)⌝] 3⋅ THENA Auto)
THEN RepeatFor 2 (ParallelLast)
THEN MoveToConcl (-1)
THEN GenConclAtAddr [2;2]
THEN AutoBoolCase ⌜v⌝⋅) }
Latex:
Latex:
\mforall{}K:Type. (CCCNSet(K) {}\mRightarrow{} compact-type(K))
By
Latex:
(InstLemma `CCC-omni` []
THEN RepeatFor 2 ((ParallelLast' THENA Auto))
THEN (D 0 THENA Auto)
THEN (InstHyp [\mkleeneopen{}\mlambda{}\msubtwo{}x.\mneg{}\muparrow{}(p x)\mkleeneclose{}] 3\mcdot{} THENA Auto)
THEN RepeatFor 2 (ParallelLast)
THEN MoveToConcl (-1)
THEN GenConclAtAddr [2;2]
THEN AutoBoolCase \mkleeneopen{}v\mkleeneclose{}\mcdot{})
Home
Index