`∀[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