Step * 1 1 of Lemma compact-dCCC


1. K : Type
2. k : K
3. compact-type(K)
4. R : ā„• āŸ¶ K āŸ¶ š”¹
5. d : āˆ€n:ā„•. ((āˆƒm:K. (Ā¬ā†‘(R n m))) āˆØ (āˆ€m:K. (ā†‘(R n m))))
6. āˆƒn:ā„•. (ā†‘(R n case d n of inl(p) => fst(p) | inr(_) => k))
āŠ¢ āˆƒn:ā„•. āˆ€m:K. (ā†‘(R n m))
BY
{ (ParallelLast THEN MoveToConcl (-1) THEN (GenConclTerm āŒœd nāŒā‹… THENA Auto) THEN D -2 THEN Reduce 0) }

1
1. K : Type
2. k : K
3. compact-type(K)
4. R : ā„• āŸ¶ K āŸ¶ š”¹
5. d : āˆ€n:ā„•. ((āˆƒm:K. (Ā¬ā†‘(R n m))) āˆØ (āˆ€m:K. (ā†‘(R n m))))
6. n : ā„•
7. x : āˆƒm:K. (Ā¬ā†‘(R n m))
8. (d n) = (inl x) āˆˆ ((āˆƒm:K. (Ā¬ā†‘(R n m))) āˆØ (āˆ€m:K. (ā†‘(R n m))))
āŠ¢ (ā†‘(R n (fst(x)))) ā‡’ (āˆ€m:K. (ā†‘(R n m)))

2
1. K : Type
2. k : K
3. compact-type(K)
4. R : ā„• āŸ¶ K āŸ¶ š”¹
5. d : āˆ€n:ā„•. ((āˆƒm:K. (Ā¬ā†‘(R n m))) āˆØ (āˆ€m:K. (ā†‘(R n m))))
6. n : ā„•
7. y : āˆ€m:K. (ā†‘(R n m))
8. (d n) = (inr y ) āˆˆ ((āˆƒm:K. (Ā¬ā†‘(R n m))) āˆØ (āˆ€m:K. (ā†‘(R n m))))
āŠ¢ (ā†‘(R n k)) ā‡’ (āˆ€m:K. (ā†‘(R n m)))

Latex:

Latex:

1.  K  :  Type
2.  k  :  K
3.  compact-type(K)
4.  R  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbB{}
5.  d  :  \mforall{}n:\mBbbN{}.  ((\mexists{}m:K.  (\mneg{}\muparrow{}(R  n  m)))  \mvee{}  (\mforall{}m:K.  (\muparrow{}(R  n  m))))
6.  \mexists{}n:\mBbbN{}.  (\muparrow{}(R  n  case  d  n  of  inl(p)  =>  fst(p)  |  inr($_{}$)  =>  k))
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}m:K.  (\muparrow{}(R  n  m))


By

Latex:
(ParallelLast  THEN  MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}d  n\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0)



Home Index