Step * 2 1 1 of Lemma Cn-comb_wf

.....subterm..... T:t
1:n
1. Type
2. : ℤ
3. 0 < n
4. ∀m:ℕ. ∀A:ℕm ⟶ Type.
     (n 1 < m
      (primrec(n 1;λf.f;λi,F,f,x. (F (C-comb() x))) ∈ funtype(m;A;T) ⟶ funtype(m;λk.if k <then (k 1)
                                                                                   if (k =z 1) then 0
                                                                                   else k
                                                                                   fi ;T)))
5. : ℕ
6. : ℕm ⟶ Type
7. n < m
8. 1 ≤ n
9. funtype(m;A;T)
10. 1
⊢ primrec(n 1;λf.f;λi,F,f,x. (F (C-comb() x))) (C-comb() x) ∈ funtype(m 1;λk.if k <then (k 2)
                                                                             if (k =z 1) then 0
                                                                             else (k 1)
                                                                             fi ;T)
BY
((InstLemma `C-comb_wf_funtype` [⌜T⌝;⌜m⌝;⌜A⌝]⋅ THENA Auto) THEN (GenConclTerm ⌜C-comb() f⌝⋅ THENA Auto)) }

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


Latex:


Latex:
.....subterm.....  T:t
1:n
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
9.  f  :  funtype(m;A;T)
10.  x  :  A  1
\mvdash{}  primrec(n  -  1;\mlambda{}f.f;\mlambda{}i,F,f,x.  (F  (C-comb()  f  x)))  (C-comb()  f  x)  \mmember{}  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)


By


Latex:
((InstLemma  `C-comb\_wf\_funtype`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}C-comb()  f\mkleeneclose{}\mcdot{}  THENA  Auto)
  )




Home Index