---

Step * of Lemma A-null-property

∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
  ∀A:Arr(AType). ∀k:ℕn.  (A-post-val(AType;A-null(AType);A;k) = A-pre-val(AType;A;k) ∈ Val)
BY
{ (Auto THEN Unfolds ``A-post-val A-pre-val A-null`` 0) }

1
1. Val : Type
2. n : ℕ
3. AType : array{i:l}(Val;n)
4. A : Arr(AType)@i
5. k : ℕn@i
⊢ (A-eval(array-model(AType)) 
   (A-bind(array-model(AType)) (A-return(array-model(AType)) ⋅) 
    (λx.(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k)))) 
   A)
= (idx(AType) k A)
∈ Val

---

Latex:

---

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].
    \mforall{}A:Arr(AType).  \mforall{}k:\mBbbN{}n.    (A-post-val(AType;A-null(AType);A;k)  =  A-pre-val(AType;A;k))


By

---

Latex:
(Auto  THEN  Unfolds  ``A-post-val  A-pre-val  A-null``  0)

---

Home Index