Nuprl Lemma : bag-member-spread

[P:Top × Top]. ∀[C,p,T:Top].  (p ↓∈ let x,y in C[x;y] let x,y in p ↓∈ C[x;y])


Proof




Definitions occuring in Statement :  bag-member: x ↓∈ bs uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] spread: spread def product: x:A × B[x] sqequal: t
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  top_wf
Rules used in proof :  productElimination thin sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut lemma_by_obid hypothesis because_Cache productEquality isect_memberFormation introduction sqequalAxiom sqequalHypSubstitution isect_memberEquality isectElimination hypothesisEquality

Latex:
\mforall{}[P:Top  \mtimes{}  Top].  \mforall{}[C,p,T:Top].    (p  \mdownarrow{}\mmember{}  let  x,y  =  P  in  C[x;y]  \msim{}  let  x,y  =  P  in  p  \mdownarrow{}\mmember{}  C[x;y])



Date html generated: 2016_05_15-PM-02_39_30
Last ObjectModification: 2015_12_27-AM-09_42_30

Theory : bags


Home Index