---

Step * of Lemma mk_array_wf

∀[Val:Type]. ∀[n:ℕ]. ∀[Arr:Type]. ∀[idx:ℕn ⟶ Arr ⟶ Val]. ∀[upd:ℕn ⟶ Val ⟶ Arr ⟶ Arr]. ∀[newarray:Val ⟶ Arr].
  mk_array(Arr;idx;upd;newarray) ∈ array{i:l}(Val;n) 
  supposing (∀i:ℕn. ∀v:Val.  ((idx i (newarray v)) = v ∈ Val))
  ∧ (∀i,j:ℕn. ∀x:Arr. ∀v:Val.  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val))
BY
{ (Auto THEN Unfolds ``mk_array array`` 0 THEN RepUR ``uall`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[Arr:Type].  \mforall{}[idx:\mBbbN{}n  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Val].  \mforall{}[upd:\mBbbN{}n  {}\mrightarrow{}  Val  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Arr].
\mforall{}[newarray:Val  {}\mrightarrow{}  Arr].
    mk\_array(Arr;idx;upd;newarray)  \mmember{}  array\{i:l\}(Val;n) 
    supposing  (\mforall{}i:\mBbbN{}n.  \mforall{}v:Val.    ((idx  i  (newarray  v))  =  v))
    \mwedge{}  (\mforall{}i,j:\mBbbN{}n.  \mforall{}x:Arr.  \mforall{}v:Val.    ((idx  i  (upd  j  v  x))  =  if  (i  =\msubz{}  j)  then  v  else  idx  i  x  fi  ))


By

---

Latex:
(Auto  THEN  Unfolds  ``mk\_array  array``  0  THEN  RepUR  ``uall``  0  THEN  Auto)

---

Home Index