---

Step * 1 of Lemma callbyvalueall-seq_wf


1. m : ℕ
2. T : Type
3. A : ℕm ⟶ {T:Type| valueall-type(T)} 
4. L : i:ℕm ⟶ funtype(i;A;A i)
5. F : funtype(m;A;T)
6. k : ℤ
7. ¬(m ≤ (m - k))
8. 0 < k
9. 0 ≤ (m - k)
10. m - k < m + 1
11. G : ∀[T:Type]. (funtype(m - k;A;T) ⟶ T)
12. ∀G:∀[T:Type]. (funtype((m - k) + 1;A;T) ⟶ T). (callbyvalueall-seq(L;G;F;(m - k) + 1;m) ∈ T)
13. v : A (m - k)
14. (G (L (m - k))) = v ∈ (A (m - k))
15. T1 : Type
16. f : funtype((m - k) + 1;A;T1)
⊢ G f v ∈ T1
BY
{ ((Assert ⌜f ∈ funtype((m - k) + 1;A;T1)⌝⋅ THENA Auto)
   THEN (RWO "funtype-unroll-last-eq" (-1) THENA Auto)
   THEN (Subst ⌜((m - k) + 1) - 1 ~ m - k⌝ (-1)⋅ THENA Auto)
   THEN SplitOnHypITE (-1)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  T  :  Type
3.  A  :  \mBbbN{}m  {}\mrightarrow{}  \{T:Type|  valueall-type(T)\} 
4.  L  :  i:\mBbbN{}m  {}\mrightarrow{}  funtype(i;A;A  i)
5.  F  :  funtype(m;A;T)
6.  k  :  \mBbbZ{}
7.  \mneg{}(m  \mleq{}  (m  -  k))
8.  0  <  k
9.  0  \mleq{}  (m  -  k)
10.  m  -  k  <  m  +  1
11.  G  :  \mforall{}[T:Type].  (funtype(m  -  k;A;T)  {}\mrightarrow{}  T)
12.  \mforall{}G:\mforall{}[T:Type].  (funtype((m  -  k)  +  1;A;T)  {}\mrightarrow{}  T).  (callbyvalueall-seq(L;G;F;(m  -  k)  +  1;m)  \mmember{}  T)
13.  v  :  A  (m  -  k)
14.  (G  (L  (m  -  k)))  =  v
15.  T1  :  Type
16.  f  :  funtype((m  -  k)  +  1;A;T1)
\mvdash{}  G  f  v  \mmember{}  T1


By

---

Latex:
((Assert  \mkleeneopen{}f  \mmember{}  funtype((m  -  k)  +  1;A;T1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "funtype-unroll-last-eq"  (-1)  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}((m  -  k)  +  1)  -  1  \msim{}  m  -  k\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  SplitOnHypITE  (-1)
  THEN  Auto)\mcdot{}

---

Home Index