### Nuprl Lemma : b_all-squash-exists-bag

`∀[A,B:Type]. ∀[as:bag(A)]. ∀[P:A ⟶ B ⟶ ℙ].`
`  ↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = as ∈ bag(A)) ∧ b_all(A × B;bs;x.let a,b = x in ↓P[a;b])) `
`  supposing b_all(A;as;x.↓∃y:B. P[x;y])`

Proof

Definitions occuring in Statement :  b_all: `b_all(T;b;x.P[x])` bag-map: `bag-map(f;bs)` bag: `bag(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` pi1: `fst(t)` exists: `∃x:A. B[x]` squash: `↓T` and: `P ∧ Q` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` spread: spread def product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` squash: `↓T` exists: `∃x:A. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` so_apply: `x[s]` implies: `P `` Q` subtype_rel: `A ⊆r B` and: `P ∧ Q` pi1: `fst(t)` all: `∀x:A. B[x]` cand: `A c∧ B` bag-map: `bag-map(f;bs)` map: `map(f;as)` list_ind: list_ind nil: `[]` it: `⋅` b_all: `b_all(T;b;x.P[x])` empty-bag: `{}` uiff: `uiff(P;Q)` false: `False` cons-bag: `x.b` iff: `P `⇐⇒` Q` top: `Top` true: `True` guard: `{T}` rev_implies: `P `` Q`
Lemmas referenced :  bag_to_squash_list b_all_wf squash_wf exists_wf list_induction list-subtype-bag bag_wf equal_wf bag-map_wf list_wf nil_wf cons_wf bag-member-empty-iff bag-member_wf equal-wf-T-base pi1_wf b_all-cons sq_stable__squash cons-bag_wf bag-map-cons true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality imageElimination productElimination promote_hyp hypothesis equalitySymmetry hyp_replacement applyLambdaEquality cumulativity sqequalRule lambdaEquality applyEquality functionExtensionality rename functionEquality because_Cache independent_isectElimination productEquality independent_functionElimination lambdaFormation voidEquality voidElimination dependent_functionElimination imageMemberEquality baseClosed isect_memberEquality equalityTransitivity universeEquality dependent_pairFormation independent_pairFormation independent_pairEquality spreadEquality equalityUniverse levelHypothesis natural_numberEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[as:bag(A)].  \mforall{}[P:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
\mdownarrow{}\mexists{}bs:bag(A  \mtimes{}  B).  ((bag-map(\mlambda{}x.(fst(x));bs)  =  as)  \mwedge{}  b\_all(A  \mtimes{}  B;bs;x.let  a,b  =  x  in  \mdownarrow{}P[a;b]))
supposing  b\_all(A;as;x.\mdownarrow{}\mexists{}y:B.  P[x;y])

Date html generated: 2017_10_01-AM-08_55_18
Last ObjectModification: 2017_07_26-PM-04_37_18

Theory : bags

Home Index