Nuprl Lemma : seq-add-item

[T:Type]. ∀[s:sequence(T)]. ∀[x,i:Top].  (seq-add(s;x)[i] if i <||s|| then s[i] else fi )


Proof




Definitions occuring in Statement :  seq-add: seq-add(s;x) seq-item: s[i] seq-len: ||s|| sequence: sequence(T) ifthenelse: if then else fi  lt_int: i <j uall: [x:A]. B[x] top: Top universe: Type sqequal: t
Definitions unfolded in proof :  pi2: snd(t) pi1: fst(t) seq-add: seq-add(s;x) seq-len: ||s|| seq-item: s[i] sequence: sequence(T) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  sequence_wf top_wf
Rules used in proof :  universeEquality hypothesisEquality isectElimination hypothesis extract_by_obid cut because_Cache sqequalAxiom sqequalRule thin productElimination sqequalHypSubstitution introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  \mforall{}[s:sequence(T)].  \mforall{}[x,i:Top].    (seq-add(s;x)[i]  \msim{}  if  i  <z  ||s||  then  s[i]  else  x  fi  )



Date html generated: 2018_07_25-PM-01_29_47
Last ObjectModification: 2018_06_19-AM-10_16_27

Theory : arithmetic


Home Index