### Nuprl Lemma : bag-member-lifting-2

`∀[C,B,A:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[c:C].`
`  uiff(c ↓∈ lifting-2(f) as bs;↓∃a:A. ∃b:B. (a ↓∈ as ∧ b ↓∈ bs ∧ (c = (f a b) ∈ C)))`

Proof

Definitions occuring in Statement :  lifting-2: `lifting-2(f)` bag-member: `x ↓∈ bs` bag: `bag(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` squash: `↓T` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` squash: `↓T` prop: `ℙ` uall: `∀[x:A]. B[x]` bag-member: `x ↓∈ bs` so_lambda: `λ2x.t[x]` so_apply: `x[s]` lifting-2: `lifting-2(f)` lifting2: `lifting2(f;abag;bbag)` lifting-gen-rev: `lifting-gen-rev(n;f;bags)` lifting-gen-list-rev: `lifting-gen-list-rev(n;bags)` eq_int: `(i =z j)` select: `L[n]` cons: `[a / b]` ifthenelse: `if b then t else f fi ` bfalse: `ff` subtract: `n - m` btrue: `tt` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` cand: `A c∧ B` sq_stable: `SqStable(P)` implies: `P `` Q` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  sq_stable__bag-member bag-member-single single-bag_wf bag-combine_wf bag-member-combine bag_wf equal_wf and_wf exists_wf squash_wf lifting-2_wf bag-member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction cut hypothesis sqequalHypSubstitution imageElimination sqequalRule imageMemberEquality hypothesisEquality thin baseClosed lemma_by_obid isectElimination applyEquality lambdaEquality because_Cache functionEquality universeEquality productElimination independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_isectElimination dependent_pairFormation independent_functionElimination

Latex:
\mforall{}[C,B,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[as:bag(A)].  \mforall{}[bs:bag(B)].  \mforall{}[c:C].
uiff(c  \mdownarrow{}\mmember{}  lifting-2(f)  as  bs;\mdownarrow{}\mexists{}a:A.  \mexists{}b:B.  (a  \mdownarrow{}\mmember{}  as  \mwedge{}  b  \mdownarrow{}\mmember{}  bs  \mwedge{}  (c  =  (f  a  b))))

Date html generated: 2016_05_15-PM-03_05_19
Last ObjectModification: 2016_01_16-AM-08_35_14

Theory : bags

Home Index