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

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2]` pi1: `fst(t)` pi2: `snd(t)` spread: spread def product: `x:A × B[x]` sqequal: `s ~ t`
Definitions unfolded in proof :  pi1: `fst(t)` pi2: `snd(t)` 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{}  p  \mdownarrow{}\mmember{}  C[fst(P);snd(P)])

Date html generated: 2016_05_15-PM-02_39_35
Last ObjectModification: 2015_12_27-AM-09_42_33

Theory : bags

Home Index