Nuprl Lemma : rec_select_update_lemma

y,v,x,r:Top.  (r[x := v].y if =a then else r.y fi )


Proof




Definitions occuring in Statement :  record-update: r[x := v] record-select: r.x ifthenelse: if then else fi  eq_atom: =a y top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T record-update: r[x := v] record-select: r.x
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule

Latex:
\mforall{}y,v,x,r:Top.    (r[x  :=  v].y  \msim{}  if  y  =a  x  then  v  else  r.y  fi  )



Date html generated: 2016_05_15-PM-06_42_40
Last ObjectModification: 2015_12_27-AM-11_50_51

Theory : general


Home Index