---

Step * 1 1 of Lemma CCC-finite


1. n : ℕ
2. k : ℕ
3. n ≤ 2^k
⊢ CCC(ℕn)
BY
{ (Assert ∀m:ℕ3. CCC(ℕm) BY
         ((D 0 THENA Auto)
          THEN (IntSegCases (-1)
                THENL [(D 0 THEN Auto)
                      ; (D 0
                         THEN Auto
                         THEN (D -1 With ⌜λx.0⌝  THENA Auto)
                         THEN Reduce -1
                         THEN ParallelLast
                         THEN Auto
                         THEN IntSegCases (-1)
                         THEN Auto)
                      ; (InstLemma `CCC-surjection` [⌜𝔹⌝;⌜ℕ2⌝]⋅
                         THEN Auto
                         THEN (Assert 𝔹 ~ ℕ2 BY
                                     Auto)
                         THEN D -1
                         THEN D 0 With ⌜f⌝ 
                         THEN Auto)]
               )
          )) }

1
1. n : ℕ
2. k : ℕ
3. n ≤ 2^k
4. ∀m:ℕ3. CCC(ℕm)
⊢ CCC(ℕn)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  n  \mleq{}  2\^{}k
\mvdash{}  CCC(\mBbbN{}n)


By

---

Latex:
(Assert  \mforall{}m:\mBbbN{}3.  CCC(\mBbbN{}m)  BY
              ((D  0  THENA  Auto)
                THEN  (IntSegCases  (-1)
                            THENL  [(D  0  THEN  Auto)
                                        ;  (D  0
                                              THEN  Auto
                                              THEN  (D  -1  With  \mkleeneopen{}\mlambda{}x.0\mkleeneclose{}    THENA  Auto)
                                              THEN  Reduce  -1
                                              THEN  ParallelLast
                                              THEN  Auto
                                              THEN  IntSegCases  (-1)
                                              THEN  Auto)
                                        ;  (InstLemma  `CCC-surjection`  [\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}\mBbbN{}2\mkleeneclose{}]\mcdot{}
                                              THEN  Auto
                                              THEN  (Assert  \mBbbB{}  \msim{}  \mBbbN{}2  BY
                                                                      Auto)
                                              THEN  D  -1
                                              THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{} 
                                              THEN  Auto)]
                          )
                ))

---

Home Index