---

Step * 2 of Lemma apply_larger_list


1. B : Type
2. n : ℕ
3. A : ℕn ⟶ Type
4. p : ℤ
5. 0 < p
6. 0 ≤ n - p - 1 < n + 1
⇒ (∀q:ℕ(n - p - 1) + 1. ∀lst:k:{q..n-} ⟶ (A k). ∀r:ℕn - p - 1. ∀a:A r. ∀f:funtype(n - n - p - 1;λx.(A 
                                                                                                      (x
                                                                                                      + (n - p 
                                                                                                        - 1)));B).
      ((apply_gen(n;λx.if (x =z r) then a else lst x fi ) (n - p - 1) f) = (apply_gen(n;lst) (n - p - 1) f) ∈ B))
7. 0 ≤ n - p < n + 1
8. q : ℕ(n - p) + 1
9. lst : k:{q..n-} ⟶ (A k)
10. r : ℕn - p
11. a : A r
12. f : funtype(n - n - p;λx.(A (x + (n - p)));B)
⊢ (apply_gen(n;λx.if (x =z r) then a else lst x fi ) (n - p) f) = (apply_gen(n;lst) (n - p) f) ∈ B
BY
{ ((D (-7) THENA Auto')
   THEN (Subst ⌜n - p - 1 ~ (n - p) + 1⌝ (-1)⋅ THENA Auto)
   THEN (Subst ⌜n - n - p ~ p⌝ (-2)⋅ THENA Auto)
   THEN Unfold `apply_gen` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Fold `apply_gen` 0
   THEN Reduce 0
   THEN OldAutoSplit
   THEN Auto'
   THEN OldAutoSplit
   THEN Thin (-2)) }

1
1. B : Type
2. n : ℕ
3. A : ℕn ⟶ Type
4. p : ℤ
5. 0 < p
6. 0 ≤ (n - p)
7. n - p < n + 1
8. q : ℕ(n - p) + 1
9. lst : k:{q..n-} ⟶ (A k)
10. r : ℕn - p
11. a : A r
12. f : funtype(p;λx.(A (x + (n - p)));B)
13. ∀q:ℕ((n - p) + 1) + 1. ∀lst:k:{q..n-} ⟶ (A k). ∀r:ℕ(n - p) + 1. ∀a:A r. ∀f:funtype(n - (n - p) + 1;λx.(A 
                                                                                                            (x
                                                                                                            + (n - p)
                                                                                                            + 1));B).
      ((apply_gen(n;λx.if (x =z r) then a else lst x fi ) ((n - p) + 1) f) = (apply_gen(n;lst) ((n - p) + 1) f) ∈ B)
14. ¬((n - p) = r ∈ ℤ)
⊢ (apply_gen(n;λx.if (x =z r) then a else lst x fi ) ((n - p) + 1) (f (lst (n - p))))
= (apply_gen(n;lst) ((n - p) + 1) (f (lst (n - p))))
∈ B

---

Latex:

---

Latex:

1.  B  :  Type
2.  n  :  \mBbbN{}
3.  A  :  \mBbbN{}n  {}\mrightarrow{}  Type
4.  p  :  \mBbbZ{}
5.  0  <  p
6.  0  \mleq{}  n  -  p  -  1  <  n  +  1
{}\mRightarrow{}  (\mforall{}q:\mBbbN{}(n  -  p  -  1)  +  1.  \mforall{}lst:k:\{q..n\msupminus{}\}  {}\mrightarrow{}  (A  k).  \mforall{}r:\mBbbN{}n  -  p  -  1.  \mforall{}a:A  r.
        \mforall{}f:funtype(n  -  n  -  p  -  1;\mlambda{}x.(A  (x  +  (n  -  p  -  1)));B).
            ((apply\_gen(n;\mlambda{}x.if  (x  =\msubz{}  r)  then  a  else  lst  x  fi  )  (n  -  p  -  1)  f)
            =  (apply\_gen(n;lst)  (n  -  p  -  1)  f)))
7.  0  \mleq{}  n  -  p  <  n  +  1
8.  q  :  \mBbbN{}(n  -  p)  +  1
9.  lst  :  k:\{q..n\msupminus{}\}  {}\mrightarrow{}  (A  k)
10.  r  :  \mBbbN{}n  -  p
11.  a  :  A  r
12.  f  :  funtype(n  -  n  -  p;\mlambda{}x.(A  (x  +  (n  -  p)));B)
\mvdash{}  (apply\_gen(n;\mlambda{}x.if  (x  =\msubz{}  r)  then  a  else  lst  x  fi  )  (n  -  p)  f)  =  (apply\_gen(n;lst)  (n  -  p)  f)


By

---

Latex:
((D  (-7)  THENA  Auto')
  THEN  (Subst  \mkleeneopen{}n  -  p  -  1  \msim{}  (n  -  p)  +  1\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}n  -  n  -  p  \msim{}  p\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
  THEN  Unfold  `apply\_gen`  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Fold  `apply\_gen`  0
  THEN  Reduce  0
  THEN  OldAutoSplit
  THEN  Auto'
  THEN  OldAutoSplit
  THEN  Thin  (-2))

---

Home Index