### Nuprl Lemma : seq-cons-item

`∀[T:Type]. ∀[a:Top]. ∀[s:sequence(T)]. ∀[i:Top].  (seq-cons(a;s)[i] ~ if (i =z 0) then a else s[i - 1] fi )`

Proof

Definitions occuring in Statement :  seq-cons: `seq-cons(a;s)` seq-item: `s[i]` sequence: `sequence(T)` ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` uall: `∀[x:A]. B[x]` top: `Top` subtract: `n - m` natural_number: `\$n` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` sequence: `sequence(T)` seq-item: `s[i]` seq-cons: `seq-cons(a;s)` pi2: `snd(t)`
Lemmas referenced :  top_wf sequence_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule hypothesis sqequalAxiom extract_by_obid isect_memberEquality isectElimination hypothesisEquality because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[a:Top].  \mforall{}[s:sequence(T)].  \mforall{}[i:Top].
(seq-cons(a;s)[i]  \msim{}  if  (i  =\msubz{}  0)  then  a  else  s[i  -  1]  fi  )

Date html generated: 2018_07_25-PM-01_29_01
Last ObjectModification: 2018_06_12-PM-10_29_47

Theory : arithmetic

Home Index