---

Step * 1 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. x : ⋂i:ℕm. ∀[v:Val1]. ((idx i (newarray v)) = v ∈ Val1)
13. i : ℕn
⊢ x ∈ ∀[v:Val2]. ((idx i (newarray v)) = v ∈ Val2)
BY
{ (With ⌜i⌝ (D (-2))⋅ THEN Auto) }

---

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.  x  :  \mcap{}i:\mBbbN{}m.  \mforall{}[v:Val1].  ((idx  i  (newarray  v))  =  v)
13.  i  :  \mBbbN{}n
\mvdash{}  x  \mmember{}  \mforall{}[v:Val2].  ((idx  i  (newarray  v))  =  v)


By

---

Latex:
(With  \mkleeneopen{}i\mkleeneclose{}  (D  (-2))\mcdot{}  THEN  Auto)

---

Home Index