---

Step * 2 of Lemma array_subtype


1. Val1 : Type
2. Val2 : Type
3. m : ℕ
4. n : ℕ
5. Val1 ⊆r Val2
6. Val2 ⊆r Val1
7. n ≤ m
8. Arr : Type
9. idx : ℕm ⟶ Arr ⟶ Val1
10. upd : ℕm ⟶ Val1 ⟶ Arr ⟶ Arr
11. newarray : Val1 ⟶ Arr
12. ∀[i:ℕm]. ∀[v:Val1].  ((idx i (newarray v)) = v ∈ Val1)
13. x : ⋂i:ℕm. ∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val1)
14. i : ℕn
⊢ x ∈ ∀[j:ℕn]. ∀[x:Arr]. ∀[v:Val2].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val2)
BY
{ SubsumeC ⌜∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val1)⌝⋅ }

1
1. Val1 : Type
2. Val2 : Type
3. m : ℕ
4. n : ℕ
5. Val1 ⊆r Val2
6. Val2 ⊆r Val1
7. n ≤ m
8. Arr : Type
9. idx : ℕm ⟶ Arr ⟶ Val1
10. upd : ℕm ⟶ Val1 ⟶ Arr ⟶ Arr
11. newarray : Val1 ⟶ Arr
12. ∀[i:ℕm]. ∀[v:Val1].  ((idx i (newarray v)) = v ∈ Val1)
13. x : ⋂i:ℕm. ∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val1)
14. i : ℕn
⊢ x ∈ ∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val1)

2
1. Val1 : Type
2. Val2 : Type
3. m : ℕ
4. n : ℕ
5. Val1 ⊆r Val2
6. Val2 ⊆r Val1
7. n ≤ m
8. Arr : Type
9. idx : ℕm ⟶ Arr ⟶ Val1
10. upd : ℕm ⟶ Val1 ⟶ Arr ⟶ Arr
11. newarray : Val1 ⟶ Arr
12. ∀[i:ℕm]. ∀[v:Val1].  ((idx i (newarray v)) = v ∈ Val1)
13. x : ⋂i:ℕm. ∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val1)
14. i : ℕn
15. x = x ∈ (∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val1))
⊢ (∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val1))
    ⊆r (∀[j:ℕn]. ∀[x:Arr]. ∀[v:Val2].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val2))

---

Latex:

---

Latex:

1.  Val1  :  Type
2.  Val2  :  Type
3.  m  :  \mBbbN{}
4.  n  :  \mBbbN{}
5.  Val1  \msubseteq{}r  Val2
6.  Val2  \msubseteq{}r  Val1
7.  n  \mleq{}  m
8.  Arr  :  Type
9.  idx  :  \mBbbN{}m  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Val1
10.  upd  :  \mBbbN{}m  {}\mrightarrow{}  Val1  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Arr
11.  newarray  :  Val1  {}\mrightarrow{}  Arr
12.  \mforall{}[i:\mBbbN{}m].  \mforall{}[v:Val1].    ((idx  i  (newarray  v))  =  v)
13.  x  :  \mcap{}i:\mBbbN{}m
                    \mforall{}[j:\mBbbN{}m].  \mforall{}[x:Arr].  \mforall{}[v:Val1].    ((idx  i  (upd  j  v  x))  =  if  (i  =\msubz{}  j)  then  v  else  idx  i  x  fi  )
14.  i  :  \mBbbN{}n
\mvdash{}  x  \mmember{}  \mforall{}[j:\mBbbN{}n].  \mforall{}[x:Arr].  \mforall{}[v:Val2].    ((idx  i  (upd  j  v  x))  =  if  (i  =\msubz{}  j)  then  v  else  idx  i  x  fi  )


By

---

Latex:
SubsumeC  \mkleeneopen{}\mforall{}[j:\mBbbN{}m].  \mforall{}[x:Arr].  \mforall{}[v:Val1].
                        ((idx  i  (upd  j  v  x))  =  if  (i  =\msubz{}  j)  then  v  else  idx  i  x  fi  )\mkleeneclose{}\mcdot{}

---

Home Index