---

Step * 1 1 of Lemma apply_gen_wf2

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

---

Latex:

---

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


By

---

Latex:
(Auto'
  THEN  (Subst  \mkleeneopen{}m  -  0  \msim{}  m\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}m  -  0  \msim{}  m\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  Unfold  `apply\_gen`  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}(m  =\msubz{}  m)  \msim{}  tt\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index