Nuprl Lemma : seq-add-item
∀[T:Type]. ∀[s:sequence(T)]. ∀[x,i:Top].  (seq-add(s;x)[i] ~ if i <z ||s|| then s[i] else x fi )
Proof
Definitions occuring in Statement : 
seq-add: seq-add(s;x)
, 
seq-item: s[i]
, 
seq-len: ||s||
, 
sequence: sequence(T)
, 
ifthenelse: if b then t else f fi 
, 
lt_int: i <z j
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
universe: Type
, 
sqequal: s ~ 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