---

Step * of Lemma uncurry-gen_wf2

∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type].
∀[g:(k:{q..n-} ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)].
  (uncurry-gen(n) m g ∈ (k:{q..n-} ⟶ (A k)) ⟶ 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 funtype`` 0
   THEN NatInd (-2)⋅
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN Auto'
   THEN Subst ⌜(n - p) + 1 ~ n - p - 1⌝ 0⋅
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto
   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{}[g:(k:\{q..n\msupminus{}\}  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)].
    (uncurry-gen(n)  m  g  \mmember{}  (k:\{q..n\msupminus{}\}  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  B)


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  funtype``  0
  THEN  NatInd  (-2)\mcdot{}
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Auto'
  THEN  Subst  \mkleeneopen{}(n  -  p)  +  1  \msim{}  n  -  p  -  1\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto
  THEN  Auto')

---

Home Index