Step * 2 2 of Lemma array_subtype


1. Val1 Type
2. Val2 Type
3. : ℕ
4. : ℕ
5. Val1 ⊆Val2
6. Val2 ⊆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 (newarray v)) v ∈ Val1)
13. : ⋂i:ℕm. ∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx (upd x)) if (i =z j) then else idx fi  ∈ Val1)
14. : ℕn
15. x ∈ (∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx (upd x)) if (i =z j) then else idx fi  ∈ Val1))
⊢ (∀[j:ℕm]. ∀[x:Arr]. ∀[v:Val1].  ((idx (upd x)) if (i =z j) then else idx fi  ∈ Val1))
    ⊆(∀[j:ℕn]. ∀[x:Arr]. ∀[v:Val2].  ((idx (upd x)) if (i =z j) then else idx fi  ∈ Val2))
BY
(Unfold `uall` 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.  \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
15.  x  =  x
\mvdash{}  (\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  ))
        \msubseteq{}r  (\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:
(Unfold  `uall`  0  THEN  Auto)




Home Index