---

Step * 2 of Lemma Cn-comb_wf


1. T : Type
2. n : ℤ
3. 0 < n
4. ∀m:ℕ. ∀A:ℕm ⟶ Type.
     (n - 1 < m
     ⇒ (primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) ∈ funtype(m;A;T) ⟶ funtype(m;λk.if k <z n - 1 then A (k + 1)
                                                                                   if (k =z n - 1) then A 0
                                                                                   else A k
                                                                                   fi ;T)))
5. m : ℕ
6. A : ℕm ⟶ Type
7. n < m
8. 1 ≤ n
⊢ λf,x. (primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) (C-comb() f x)) ∈ funtype(m;A;T) ⟶ funtype(m;λk.if k <z n the\000Cn A (k + 1)
                                                                                               if (k =z n) then A 0
                                                                                               else A k
                                                                                               fi ;T)
BY
{ ((MemCD THENA Auto)
   THEN SubsumeC ⌜(A 1) ⟶ funtype(m - 1;λk.if k <z n - 1 then A (k + 2)
                                            if (k =z n - 1) then A 0
                                            else A (k + 1)
                                            fi ;T)⌝⋅
   ) }

1
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀m:ℕ. ∀A:ℕm ⟶ Type.
     (n - 1 < m
     ⇒ (primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) ∈ funtype(m;A;T) ⟶ funtype(m;λk.if k <z n - 1 then A (k + 1)
                                                                                   if (k =z n - 1) then A 0
                                                                                   else A k
                                                                                   fi ;T)))
5. m : ℕ
6. A : ℕm ⟶ Type
7. n < m
8. 1 ≤ n
9. f : funtype(m;A;T)
⊢ λx.(primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) (C-comb() f x)) ∈ (A 1) ⟶ funtype(m - 1;λk.if k <z n - 1 then A \000C(k + 2)
                                                                                           if (k =z n - 1) then A 0
                                                                                           else A (k + 1)
                                                                                           fi ;T)

2
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀m:ℕ. ∀A:ℕm ⟶ Type.
     (n - 1 < m
     ⇒ (primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) ∈ funtype(m;A;T) ⟶ funtype(m;λk.if k <z n - 1 then A (k + 1)
                                                                                   if (k =z n - 1) then A 0
                                                                                   else A k
                                                                                   fi ;T)))
5. m : ℕ
6. A : ℕm ⟶ Type
7. n < m
8. 1 ≤ n
9. f : funtype(m;A;T)
10. (λx.(primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) (C-comb() f x)))
= (λx.(primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) (C-comb() f x)))
∈ ((A 1) ⟶ funtype(m - 1;λk.if k <z n - 1 then A (k + 2)
                             if (k =z n - 1) then A 0
                             else A (k + 1)
                             fi ;T))
⊢ ((A 1) ⟶ funtype(m - 1;λk.if k <z n - 1 then A (k + 2)
                             if (k =z n - 1) then A 0
                             else A (k + 1)
                             fi ;T)) ⊆r funtype(m;λk.if k <z n then A (k + 1)
                                                     if (k =z n) then A 0
                                                     else A k
                                                     fi ;T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}m:\mBbbN{}.  \mforall{}A:\mBbbN{}m  {}\mrightarrow{}  Type.
          (n  -  1  <  m
          {}\mRightarrow{}  (primrec(n  -  1;\mlambda{}f.f;\mlambda{}i,F,f,x.  (F  (C-comb()  f  x)))  \mmember{}  funtype(m;A;T)  {}\mrightarrow{}  funtype(m;\mlambda{}k.if  k  <z  n\000C  -  1
                                                                                                                                                                          then  A  (k  +  1)
                                                                                                                                                                      if  (k  =\msubz{}  n  -  1)
                                                                                                                                                                          then  A  0
                                                                                                                                                                      else  A  k
                                                                                                                                                                      fi  ;T)))
5.  m  :  \mBbbN{}
6.  A  :  \mBbbN{}m  {}\mrightarrow{}  Type
7.  n  <  m
8.  1  \mleq{}  n
\mvdash{}  \mlambda{}f,x.  (primrec(n  -  1;\mlambda{}f.f;\mlambda{}i,F,f,x.  (F  (C-comb()  f  x)))  (C-comb()  f  x))  \mmember{}  funtype(m;A;T)
    {}\mrightarrow{}  funtype(m;\mlambda{}k.if  k  <z  n  then  A  (k  +  1)
                                    if  (k  =\msubz{}  n)  then  A  0
                                    else  A  k
                                    fi  ;T)


By

---

Latex:
((MemCD  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}(A  1)  {}\mrightarrow{}  funtype(m  -  1;\mlambda{}k.if  k  <z  n  -  1  then  A  (k  +  2)
                                                                                    if  (k  =\msubz{}  n  -  1)  then  A  0
                                                                                    else  A  (k  +  1)
                                                                                    fi  ;T)\mkleeneclose{}\mcdot{}
  )

---

Home Index