---

Step * 1 2 of Lemma apply_gen_wf2

.....upcase..... 
1. B : Type
2. n : ℕ
3. m : ℤ
4. 0 ≤ m < n + 1
5. A : ℕn ⟶ Type
6. p : ℤ
7. 0 < p
8. 0 ≤ m - p - 1 < m + 1
⇒ (∀lst:k:{m - p - 1..n-} ⟶ (A k). ∀f:funtype(n - m - p - 1;λx.(A (x + (m - p - 1)));B).
      (apply_gen(m;lst) (m - p - 1) f ∈ funtype(n - m;λx.(A (x + m));B)))
⊢ 0 ≤ m - p < m + 1
⇒ (∀lst:k:{m - p..n-} ⟶ (A k). ∀f:funtype(n - m - p;λx.(A (x + (m - p)));B).
      (apply_gen(m;lst) (m - p) f ∈ funtype(n - m;λx.(A (x + m));B)))
BY
{ ((UnivCD THENA Auto')
   THEN Unfold `apply_gen` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN Try (Fold `apply_gen` 0)
   THEN (Subst ⌜(m - p =z m) ~ ff⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN (Subst ⌜m - p - 1 ~ (m - p) + 1⌝ (-4)⋅ THENA Auto)
   THEN BHyp (-4)
   THEN Try (Complete (Auto'))) }

1
.....wf..... 
1. B : Type
2. n : ℕ
3. m : ℤ
4. 0 ≤ m < n + 1
5. A : ℕn ⟶ Type
6. p : ℤ
7. 0 < p
8. 0 ≤ (m - p) + 1 < m + 1
⇒ (∀lst:k:{(m - p) + 1..n-} ⟶ (A k). ∀f:funtype(n - (m - p) + 1;λx.(A (x + (m - p) + 1));B).
      (apply_gen(m;lst) ((m - p) + 1) f ∈ funtype(n - m;λx.(A (x + m));B)))
9. 0 ≤ m - p < m + 1
10. lst : k:{m - p..n-} ⟶ (A k)
11. f : funtype(n - m - p;λx.(A (x + (m - p)));B)
⊢ f (lst (m - p)) ∈ funtype(n - (m - p) + 1;λx.(A (x + (m - p) + 1));B)

---

Latex:

---

Latex:
.....upcase..... 
1.  B  :  Type
2.  n  :  \mBbbN{}
3.  m  :  \mBbbZ{}
4.  0  \mleq{}  m  <  n  +  1
5.  A  :  \mBbbN{}n  {}\mrightarrow{}  Type
6.  p  :  \mBbbZ{}
7.  0  <  p
8.  0  \mleq{}  m  -  p  -  1  <  m  +  1
{}\mRightarrow{}  (\mforall{}lst:k:\{m  -  p  -  1..n\msupminus{}\}  {}\mrightarrow{}  (A  k).  \mforall{}f:funtype(n  -  m  -  p  -  1;\mlambda{}x.(A  (x  +  (m  -  p  -  1)));B).
            (apply\_gen(m;lst)  (m  -  p  -  1)  f  \mmember{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)))
\mvdash{}  0  \mleq{}  m  -  p  <  m  +  1
{}\mRightarrow{}  (\mforall{}lst:k:\{m  -  p..n\msupminus{}\}  {}\mrightarrow{}  (A  k).  \mforall{}f:funtype(n  -  m  -  p;\mlambda{}x.(A  (x  +  (m  -  p)));B).
            (apply\_gen(m;lst)  (m  -  p)  f  \mmember{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)))


By

---

Latex:
((UnivCD  THENA  Auto')
  THEN  Unfold  `apply\_gen`  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  Try  (Fold  `apply\_gen`  0)
  THEN  (Subst  \mkleeneopen{}(m  -  p  =\msubz{}  m)  \msim{}  ff\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}m  -  p  -  1  \msim{}  (m  -  p)  +  1\mkleeneclose{}  (-4)\mcdot{}  THENA  Auto)
  THEN  BHyp  (-4)
  THEN  Try  (Complete  (Auto')))

---

Home Index