---

Step * 2 1 of Lemma apply_larger_list


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
BY
{ ((BHyp (-2) THENA Auto)
   THEN (Subst ⌜n - (n - p) + 1 ~ p - 1⌝ 0⋅ THENA Auto)
   THEN Unfold `funtype` (-3)
   THEN (RWO  "primrec-unroll" (-3) THENA Auto)
   THEN (SplitOnHypITE -3  THENA Auto)
   THEN Auto'
   THEN All Reduce
   THEN DoSubsume
   THEN Auto'
   THEN BLemma `subtype_rel-equal`
   THEN Try ((Unfold `funtype` 0 THEN Reduce 0 THEN EqCD THEN Auto'))
   THEN Auto')⋅ }

---

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)
7.  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(p;\mlambda{}x.(A  (x  +  (n  -  p)));B)
13.  \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))
14.  \mneg{}((n  -  p)  =  r)
\mvdash{}  (apply\_gen(n;\mlambda{}x.if  (x  =\msubz{}  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))))


By

---

Latex:
((BHyp  (-2)  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}n  -  (n  -  p)  +  1  \msim{}  p  -  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Unfold  `funtype`  (-3)
  THEN  (RWO    "primrec-unroll"  (-3)  THENA  Auto)
  THEN  (SplitOnHypITE  -3    THENA  Auto)
  THEN  Auto'
  THEN  All  Reduce
  THEN  DoSubsume
  THEN  Auto'
  THEN  BLemma  `subtype\_rel-equal`
  THEN  Try  ((Unfold  `funtype`  0  THEN  Reduce  0  THEN  EqCD  THEN  Auto'))
  THEN  Auto')\mcdot{}

---

Home Index