---

Step * 1 2 1 of Lemma apply_gen_wf2

.....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)
BY
{ (Unfold `funtype` (-1)⋅
   THEN (RWO "primrec-unroll" (-1)⋅ THENA Auto)
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN Auto'
   THEN Reduce (-2)) }

---

Latex:

---

Latex:
.....wf..... 
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)))
9.  0  \mleq{}  m  -  p  <  m  +  1
10.  lst  :  k:\{m  -  p..n\msupminus{}\}  {}\mrightarrow{}  (A  k)
11.  f  :  funtype(n  -  m  -  p;\mlambda{}x.(A  (x  +  (m  -  p)));B)
\mvdash{}  f  (lst  (m  -  p))  \mmember{}  funtype(n  -  (m  -  p)  +  1;\mlambda{}x.(A  (x  +  (m  -  p)  +  1));B)


By

---

Latex:
(Unfold  `funtype`  (-1)\mcdot{}
  THEN  (RWO  "primrec-unroll"  (-1)\mcdot{}  THENA  Auto)
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  Auto'
  THEN  Reduce  (-2))

---

Home Index