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 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: 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: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: 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:  Q subtype_rel: A ⊆B and: P ∧ Q pi1: fst(t) all: x:A. B[x] cand: 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: ⇐⇒ Q top: Top true: True guard: {T} rev_implies:  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