### Nuprl Lemma : A-fetch'_wf

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

Proof

Definitions occuring in Statement :  A-fetch': `A-fetch'(AModel)` A-map': `A-map'(AModel)` 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` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` array-model: `array-model(AType)` A-fetch': `A-fetch'(AModel)` A-map': `A-map'(AModel)` pi2: `snd(t)` pi1: `fst(t)` array-monad': `array-monad'(AType)` M-map: `M-map(mnd)` mk_monad: `mk_monad(M;return;bind)` nat: `ℕ`
Lemmas referenced :  array_wf nat_wf idx_wf Arr_wf int_seg_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination thin hypothesisEquality isect_memberEquality because_Cache universeEquality lambdaEquality applyEquality natural_numberEquality setElimination rename

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

Date html generated: 2016_05_15-PM-02_18_49
Last ObjectModification: 2015_12_27-AM-08_58_39