---

Step * of Lemma uncurry-gen_wf

∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[g:(k:ℕn ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)].
  (uncurry-gen(n) m g ∈ (k:ℕn ⟶ (A k)) ⟶ B)
BY
{ TACTIC:(Auto'
          THEN Assert ⌜∀d,n,m:ℕ.
                         ((m ≤ n)
                         ⇒ ((n - m) ≤ d)
                         ⇒ (∀A:ℕn ⟶ Type. ∀g:(k:ℕn ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B).
                               (uncurry-gen(n) m g ∈ (k:ℕn ⟶ (A k)) ⟶ B)))⌝⋅
          THEN Try (((InstHyp [⌜n - m⌝;⌜n⌝;⌜m⌝] (-1)⋅ THENA Auto') THEN BHyp (-1) THEN Auto))
          THEN All Thin
          THEN CompleteInductionOnNat
          THEN Auto'
          THEN Unfold `uncurry-gen` 0
          THEN RW (SweepUpC UnrollRecursionC) 0
          THEN Fold `uncurry-gen` 0
          THEN Reduce 0
          THEN AutoSplit
          THEN Auto') }

1
1. B : Type
2. d : ℕ
3. ∀d:ℕd. ∀n,m:ℕ.
     ((m ≤ n)
     ⇒ ((n - m) ≤ d)
     ⇒ (∀A:ℕn ⟶ Type. ∀g:(k:ℕn ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B).
           (uncurry-gen(n) m g ∈ (k:ℕn ⟶ (A k)) ⟶ B)))
4. n : ℕ
5. m : ℕ
6. (m + 1) ≤ n
7. (n - m) ≤ d
8. A : ℕn ⟶ Type
9. g : (k:ℕn ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)
⊢ uncurry-gen(n) (m + 1) (λx.(g x (x m))) ∈ (k:ℕn ⟶ (A k)) ⟶ B

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].
\mforall{}[g:(k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)].
    (uncurry-gen(n)  m  g  \mmember{}  (k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  B)


By

---

Latex:
TACTIC:(Auto'
                THEN  Assert  \mkleeneopen{}\mforall{}d,n,m:\mBbbN{}.
                                              ((m  \mleq{}  n)
                                              {}\mRightarrow{}  ((n  -  m)  \mleq{}  d)
                                              {}\mRightarrow{}  (\mforall{}A:\mBbbN{}n  {}\mrightarrow{}  Type.  \mforall{}g:(k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B).
                                                          (uncurry-gen(n)  m  g  \mmember{}  (k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  B)))\mkleeneclose{}\mcdot{}
                THEN  Try  (((InstHyp  [\mkleeneopen{}n  -  m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto')  THEN  BHyp  (-1)  THEN  Auto))
                THEN  All  Thin
                THEN  CompleteInductionOnNat
                THEN  Auto'
                THEN  Unfold  `uncurry-gen`  0
                THEN  RW  (SweepUpC  UnrollRecursionC)  0
                THEN  Fold  `uncurry-gen`  0
                THEN  Reduce  0
                THEN  AutoSplit
                THEN  Auto')

---

Home Index