---

Step * 1 1 1 1 1 of Lemma A-eval_wf


1. Val : Type
2. n : ℕ
3. AType : Arr:Type
× idx:ℕn ⟶ Arr ⟶ Val
× upd:ℕn ⟶ Val ⟶ Arr ⟶ Arr
× newarray:Val ⟶ Arr
× ∀[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))
4. T : Type
⊢ A-eval(array-model(AType)) ∈ (Arr(AType) ⟶ (T × Arr(AType))) ⟶ Arr(AType) ⟶ T
BY
{ RepUR ``A-eval array-model Arr`` 0 }

1
1. Val : Type
2. n : ℕ
3. AType : Arr:Type
× idx:ℕn ⟶ Arr ⟶ Val
× upd:ℕn ⟶ Val ⟶ Arr ⟶ Arr
× newarray:Val ⟶ Arr
× ∀[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))
4. T : Type
⊢ λm,A. (fst((m A))) ∈ ((fst(AType)) ⟶ (T × (fst(AType)))) ⟶ (fst(AType)) ⟶ T

---

Latex:

---

Latex:

1.  Val  :  Type
2.  n  :  \mBbbN{}
3.  AType  :  Arr:Type
\mtimes{}  idx:\mBbbN{}n  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Val
\mtimes{}  upd:\mBbbN{}n  {}\mrightarrow{}  Val  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Arr
\mtimes{}  newarray:Val  {}\mrightarrow{}  Arr
\mtimes{}  \mforall{}[i:\mBbbN{}n].  \mforall{}[v:Val].    ((idx  i  (newarray  v))  =  v)
\mtimes{}  (\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  ))
4.  T  :  Type
\mvdash{}  A-eval(array-model(AType))  \mmember{}  (Arr(AType)  {}\mrightarrow{}  (T  \mtimes{}  Arr(AType)))  {}\mrightarrow{}  Arr(AType)  {}\mrightarrow{}  T


By

---

Latex:
RepUR  ``A-eval  array-model  Arr``  0

---

Home Index