---

Step * 1 of Lemma uncurry-gen_wf


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
BY
{ ((InstHyp [⌜d - 1⌝] 3⋅ THENA Auto') THEN BHyp (-1) THEN Auto THEN (GenConclAtAddr [2;1] THENA 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)
10. ∀n,m:ℕ.
      ((m ≤ n)
      ⇒ ((n - m) ≤ (d - 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)))
11. x : k:ℕn ⟶ (A k)
12. v : funtype(n - m;λx.(A (x + m));B)
13. (g x) = v ∈ funtype(n - m;λx.(A (x + m));B)
⊢ v (x m) ∈ funtype(n - m + 1;λx.(A (x + m + 1));B)

---

Latex:

---

Latex:

1.  B  :  Type
2.  d  :  \mBbbN{}
3.  \mforall{}d:\mBbbN{}d.  \mforall{}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)))
4.  n  :  \mBbbN{}
5.  m  :  \mBbbN{}
6.  (m  +  1)  \mleq{}  n
7.  (n  -  m)  \mleq{}  d
8.  A  :  \mBbbN{}n  {}\mrightarrow{}  Type
9.  g  :  (k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)
\mvdash{}  uncurry-gen(n)  (m  +  1)  (\mlambda{}x.(g  x  (x  m)))  \mmember{}  (k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  B


By

---

Latex:
((InstHyp  [\mkleeneopen{}d  -  1\mkleeneclose{}]  3\mcdot{}  THENA  Auto')
  THEN  BHyp  (-1)
  THEN  Auto
  THEN  (GenConclAtAddr  [2;1]  THENA  Auto'))

---

Home Index