---

Step * of Lemma array_subtype

∀[Val1,Val2:Type]. ∀[m,n:ℕ].
  (array{i:l}(Val1;m) ⊆r array{i:l}(Val2;n)) supposing ((n ≤ m) and ((Val1 ⊆r Val2) ∧ (Val2 ⊆r Val1)))
BY
{ (Unfold `array` 0 THEN Auto) }

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. x : ⋂i:ℕm. ∀[v:Val1]. ((idx i (newarray v)) = v ∈ Val1)
13. i : ℕn
⊢ x ∈ ∀[v:Val2]. ((idx i (newarray v)) = v ∈ Val2)

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
⊢ 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)

---

Latex:

---

Latex:
\mforall{}[Val1,Val2:Type].  \mforall{}[m,n:\mBbbN{}].
    (array\{i:l\}(Val1;m)  \msubseteq{}r  array\{i:l\}(Val2;n))  supposing 
          ((n  \mleq{}  m)  and 
          ((Val1  \msubseteq{}r  Val2)  \mwedge{}  (Val2  \msubseteq{}r  Val1)))


By

---

Latex:
(Unfold  `array`  0  THEN  Auto)

---

Home Index