### Nuprl Lemma : bag-null-bag-union

`∀[T:Type]. ∀[bbs:bag(bag(T))].  ↑bag-null(bag-union(bbs)) supposing ∀bs:bag(T). (bs ↓∈ bbs `` (↑bag-null(bs)))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-union: `bag-union(bbs)` bag-null: `bag-null(bs)` bag: `bag(T)` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` squash: `↓T` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` all: `∀x:A. B[x]` so_apply: `x[s]` sq_stable: `SqStable(P)` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` empty-bag: `{}` bag-null: `bag-null(bs)` null: `null(as)` bag-union: `bag-union(bbs)` concat: `concat(ll)` reduce: `reduce(f;k;as)` list_ind: list_ind nil: `[]` it: `⋅` btrue: `tt` assert: `↑b` ifthenelse: `if b then t else f fi ` true: `True` cons-bag: `x.b` top: `Top` guard: `{T}` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)` cand: `A c∧ B` sq_or: `a ↓∨ b` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  bag_to_squash_list bag_wf sq_stable__all all_wf bag-member_wf assert_wf bag-null_wf bag-union_wf sq_stable_from_decidable decidable__assert assert_witness squash_wf list_induction list-subtype-bag subtype_rel_self list_wf empty-bag_wf bag_union_cons_lemma assert_functionality_wrt_uiff bag-append_wf band_wf bag-null-append cons-bag_wf equal-wf-T-base assert-bag-null bag-member-cons iff_transitivity iff_weakening_uiff assert_of_band equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality hypothesis imageElimination sqequalRule lambdaEquality functionEquality dependent_functionElimination independent_functionElimination lambdaFormation because_Cache productElimination promote_hyp rename applyEquality independent_isectElimination natural_numberEquality isect_memberEquality voidElimination voidEquality hyp_replacement equalitySymmetry Error :applyLambdaEquality,  imageMemberEquality baseClosed equalityTransitivity universeEquality productEquality independent_pairFormation inlFormation comment inrFormation

Latex:
\mforall{}[T:Type].  \mforall{}[bbs:bag(bag(T))].
\muparrow{}bag-null(bag-union(bbs))  supposing  \mforall{}bs:bag(T).  (bs  \mdownarrow{}\mmember{}  bbs  {}\mRightarrow{}  (\muparrow{}bag-null(bs)))

Date html generated: 2016_10_25-AM-10_28_50
Last ObjectModification: 2016_07_12-AM-06_45_09

Theory : bags

Home Index