Nuprl Lemma : bag-member-filter

āˆ€[T:Type]. āˆ€[P:T āŸ¶ š”¹]. āˆ€[x:T]. āˆ€[bs:bag(T)].  uiff(x ā†“āˆˆ [xāˆˆbs|P[x]];x ā†“āˆˆ bs āˆ§ (ā†‘P[x]))


Proof




Definitions occuring in Statement :  bag-member: x ā†“āˆˆ bs bag-filter: [xāˆˆb|p[x]] bag: bag(T) assert: ā†‘b bool: š”¹ uiff: uiff(P;Q) uall: āˆ€[x:A]. B[x] so_apply: x[s] and: P āˆ§ Q function: x:A āŸ¶ B[x] universe: Type
Definitions unfolded in proof :  uall: āˆ€[x:A]. B[x] member: t āˆˆ T uiff: uiff(P;Q) and: P āˆ§ Q uimplies: supposing a squash: ā†“T sq_stable: SqStable(P) implies: ā‡’ Q exists: āˆƒx:A. B[x] prop: ā„™ so_lambda: Ī»2x.t[x] so_apply: x[s] subtype_rel: A āŠ†B bag-filter: [xāˆˆb|p[x]] bag-member: x ā†“āˆˆ bs rev_uimplies: rev_uimplies(P;Q) all: āˆ€x:A. B[x] bag: bag(T) quotient: x,y:A//B[x; y] cand: cāˆ§ B guard: {T} iff: ā‡ā‡’ Q assert: ā†‘b ifthenelse: if then else fi  btrue: tt true: True rev_implies: ā‡ Q label: ...$L... t
Lemmas referenced :  bag_to_squash_list sq_stable__bag-member bag-member_wf bag-filter_wf subtype_rel_bag assert_wf assert_witness bag_wf bool_wf eqtt_to_assert sq_stable_from_decidable decidable__assert member-permutation member_filter_2 l_member_wf equal_wf list-subtype-bag member_wf list_wf filter_wf5 permutation_wf member_filter iff_imp_equal_bool true_wf assert_functionality_wrt_uiff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality imageElimination hypothesis independent_functionElimination productElimination promote_hyp equalitySymmetry hyp_replacement applyLambdaEquality cumulativity sqequalRule lambdaEquality applyEquality functionExtensionality setEquality independent_isectElimination setElimination rename imageMemberEquality baseClosed independent_pairEquality productEquality isect_memberEquality equalityTransitivity functionEquality dependent_functionElimination pertypeElimination dependent_pairFormation lambdaFormation natural_numberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].    uiff(x  \mdownarrow{}\mmember{}  [x\mmember{}bs|P[x]];x  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\muparrow{}P[x]))



Date html generated: 2017_10_01-AM-08_54_12
Last ObjectModification: 2017_07_26-PM-04_35_57

Theory : bags


Home Index