---

Step * 1 of Lemma callbyvalueall_seq_wf


1. m : ℕ
2. T : Type
3. U : Type
4. A : ℕm ⟶ {T:Type| valueall-type(T)} 
5. L : i:ℕm ⟶ funtype(i;A;A i)
6. F : (funtype(m;A;T) ⟶ T) ⟶ U
7. k : ℤ
8. ¬(m ≤ (m - k))
9. 0 < k
10. 0 ≤ (m - k)
11. m - k < m + 1
12. G : ∀[T:Type]. (funtype(m - k;A;T) ⟶ T)
13. ∀G:∀[T:Type]. (funtype((m - k) + 1;A;T) ⟶ T). (callbyvalueall_seq(L;G;F;(m - k) + 1;m) ∈ U)
⊢ let v ⟵ G (L (m - k))
  in callbyvalueall_seq(L;λf.(G f v);F;(m - k) + 1;m) ∈ U
BY
{ (GenConclAtAddr [2;1]
   THEN Auto
   THEN BackThruSomeHyp
   THEN (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.  U  :  Type
4.  A  :  \mBbbN{}m  {}\mrightarrow{}  \{T:Type|  valueall-type(T)\} 
5.  L  :  i:\mBbbN{}m  {}\mrightarrow{}  funtype(i;A;A  i)
6.  F  :  (funtype(m;A;T)  {}\mrightarrow{}  T)  {}\mrightarrow{}  U
7.  k  :  \mBbbZ{}
8.  \mneg{}(m  \mleq{}  (m  -  k))
9.  0  <  k
10.  0  \mleq{}  (m  -  k)
11.  m  -  k  <  m  +  1
12.  G  :  \mforall{}[T:Type].  (funtype(m  -  k;A;T)  {}\mrightarrow{}  T)
13.  \mforall{}G:\mforall{}[T:Type].  (funtype((m  -  k)  +  1;A;T)  {}\mrightarrow{}  T).  (callbyvalueall\_seq(L;G;F;(m  -  k)  +  1;m)  \mmember{}  U)
\mvdash{}  let  v  \mleftarrow{}{}  G  (L  (m  -  k))
    in  callbyvalueall\_seq(L;\mlambda{}f.(G  f  v);F;(m  -  k)  +  1;m)  \mmember{}  U


By

---

Latex:
(GenConclAtAddr  [2;1]
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  (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