---

Step * of Lemma C-comb_wf_funtype

∀[T:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type].
  C-comb() ∈ funtype(n;A;T) ⟶ funtype(n;λk.if (k =z 0) then A 1 if (k =z 1) then A 0 else A k fi ;T) supposing 2 ≤ n
BY
{ (ProveWfLemma
   THEN MoveToConcl (-1)
   THEN Unfold `funtype` 0
   THEN RepeatFor 2 (((RWO "primrec-unroll" 0 THENA Auto) THEN AutoSplit))
   THEN RepeatFor 3 (AutoSplit⋅)
   THEN Auto
   THEN Auto'
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].
    C-comb()  \mmember{}  funtype(n;A;T)  {}\mrightarrow{}  funtype(n;\mlambda{}k.if  (k  =\msubz{}  0)  then  A  1
                                                                                        if  (k  =\msubz{}  1)  then  A  0
                                                                                        else  A  k
                                                                                        fi  ;T) 
    supposing  2  \mleq{}  n


By

---

Latex:
(ProveWfLemma
  THEN  MoveToConcl  (-1)
  THEN  Unfold  `funtype`  0
  THEN  RepeatFor  2  (((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  AutoSplit))
  THEN  RepeatFor  3  (AutoSplit\mcdot{})
  THEN  Auto
  THEN  Auto'
  THEN  DoSubsume
  THEN  Auto)

---

Home Index