---

Step * of Lemma apply_uncurry

∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type]. ∀[lst:k:{q..n-} ⟶ (A k)].
∀[f:(k:{q..n-} ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)].
  ((uncurry-gen(n) m f lst) = (apply_gen(n;lst) m (f lst)) ∈ B)
BY
{ (RepeatFor 3 ((D 0 THENA Auto'))
   THEN (Assert ⌜∃p:ℕ. (m = (n - p) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜n - m⌝]⋅ THEN Auto))
   THEN D (-1)
   THEN HypSubst' (-1) 0
   THEN (D (-3) THENA Auto)
   THEN (HypSubst' (-1) (-3) THENA Auto)
   THEN Thin (-2)⋅
   THEN Thin (-3)⋅
   THEN Unfolds ``uncurry-gen apply_gen funtype`` 0
   THEN NatInd (-2)⋅
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN RepeatFor 2 (OldAutoSplit)
   THEN Auto'
   THEN Subst ⌜(n - p) + 1 ~ n - p - 1⌝ 0⋅
   THEN Auto
   THEN (RWO "5" 0 THENA Auto')
   THEN Reduce 0
   THEN Auto
   THEN Auto'
   THEN (Fold `apply_gen` 0
         THEN BLemma `apply_gen_wf`
         THEN Auto
         THEN Unfold `funtype` 0
         THEN Reduce 0
         THEN Auto
         THEN Auto')⋅) }

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].  \mforall{}[q:\mBbbN{}m  +  1].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[lst:k:\{q..n\msupminus{}\}  {}\mrightarrow{}  (A  k)].
\mforall{}[f:(k:\{q..n\msupminus{}\}  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)].
    ((uncurry-gen(n)  m  f  lst)  =  (apply\_gen(n;lst)  m  (f  lst)))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto'))
  THEN  (Assert  \mkleeneopen{}\mexists{}p:\mBbbN{}.  (m  =  (n  -  p))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}n  -  m\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  D  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  (D  (-3)  THENA  Auto)
  THEN  (HypSubst'  (-1)  (-3)  THENA  Auto)
  THEN  Thin  (-2)\mcdot{}
  THEN  Thin  (-3)\mcdot{}
  THEN  Unfolds  ``uncurry-gen  apply\_gen  funtype``  0
  THEN  NatInd  (-2)\mcdot{}
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  RepeatFor  2  (OldAutoSplit)
  THEN  Auto'
  THEN  Subst  \mkleeneopen{}(n  -  p)  +  1  \msim{}  n  -  p  -  1\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  (RWO  "5"  0  THENA  Auto')
  THEN  Reduce  0
  THEN  Auto
  THEN  Auto'
  THEN  (Fold  `apply\_gen`  0
              THEN  BLemma  `apply\_gen\_wf`
              THEN  Auto
              THEN  Unfold  `funtype`  0
              THEN  Reduce  0
              THEN  Auto
              THEN  Auto')\mcdot{})

---

Home Index