### Nuprl Lemma : A-fetch2_wf

`∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[i:ℕn].  (A-fetch2(array-model(AType);i) ∈ A-map Val)`

Proof

Definitions occuring in Statement :  A-fetch2: `A-fetch2(AModel;i)` A-map: `A-map` array-model: `array-model(AType)` array: `array{i:l}(Val;n)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` apply: `f a` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` A-fetch2: `A-fetch2(AModel;i)` nat: `ℕ`
Lemmas referenced :  A-fetch_wf int_seg_wf array_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule applyEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry natural_numberEquality setElimination rename isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].  \mforall{}[i:\mBbbN{}n].
(A-fetch2(array-model(AType);i)  \mmember{}  A-map  Val)

Date html generated: 2016_05_15-PM-02_20_40
Last ObjectModification: 2015_12_27-AM-08_57_58