Nuprl 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 (newarray v)) v ∈ Val))
  ∧ (∀i,j:ℕn. ∀x:Arr. ∀v:Val.  ((idx (upd x)) if (i =z j) then else idx fi  ∈ Val))


Proof




Definitions occuring in Statement :  mk_array: mk_array(Arr;idx;upd;newarray) array: array{i:l}(Val;n) int_seg: {i..j-} nat: ifthenelse: if then else fi  eq_int: (i =z j) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] and: P ∧ Q member: t ∈ T apply: a function: x:A ⟶ B[x] natural_number: $n universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q mk_array: mk_array(Arr;idx;upd;newarray) array: array{i:l}(Val;n) squash: T prop: all: x:A. B[x] true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q int_seg: {i..j-} bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff uiff: uiff(P;Q) exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb assert: b false: False nat: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  equal_wf squash_wf true_wf iff_weakening_equal eq_int_wf bool_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int all_wf int_seg_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule dependent_pairEquality cumulativity hypothesisEquality functionExtensionality applyEquality because_Cache independent_pairEquality isect_memberEquality axiomEquality lambdaEquality imageElimination extract_by_obid isectElimination equalityTransitivity hypothesis equalitySymmetry dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed universeEquality independent_isectElimination independent_functionElimination setElimination rename lambdaFormation unionElimination equalityElimination dependent_pairFormation promote_hyp instantiate voidElimination productEquality isectEquality functionEquality

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  ))



Date html generated: 2017_10_01-AM-08_43_52
Last ObjectModification: 2017_07_26-PM-04_29_59

Theory : monads


Home Index