### Nuprl Lemma : sub-bag-list-if-bag-no-repeats-sq

`∀[A:Type]. ∀as:bag(A). ∀bs:A List.  (bag-no-repeats(A;as) `` b_all(A;as;x.(x ∈ bs)) `` (↓sub-bag(A;as;bs)))`

Proof

Definitions occuring in Statement :  b_all: `b_all(T;b;x.P[x])` sub-bag: `sub-bag(T;as;bs)` bag-no-repeats: `bag-no-repeats(T;bs)` bag: `bag(T)` l_member: `(x ∈ l)` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` squash: `↓T` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` squash: `↓T` exists: `∃x:A. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` bag-no-repeats: `bag-no-repeats(T;bs)` sq_stable: `SqStable(P)` and: `P ∧ Q` uimplies: `b supposing a` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` b_all: `b_all(T;b;x.P[x])` subtype_rel: `A ⊆r B` empty-bag: `{}` not: `¬A` false: `False` uiff: `uiff(P;Q)` or: `P ∨ Q` guard: `{T}` sub-bag: `sub-bag(T;as;bs)` bag-append: `as + bs` true: `True` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` cons-bag: `x.b`
Lemmas referenced :  bag_to_squash_list b_all_wf l_member_wf bag-no-repeats_wf sq_stable__no_repeats no_repeats-bag l_all_iff list-member-bag-member list_induction all_wf list_wf no_repeats_wf l_all_wf2 squash_wf sub-bag_wf list-subtype-bag empty-sub-bag nil_wf null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse l_all_cons no_repeats_cons l_member_decomp append_wf cons_wf bag_wf member_append member_singleton and_wf equal_wf exists_wf true_wf bag-append-comm-assoc bag-append_wf iff_weakening_equal bag-append-comm list_ind_cons_lemma list_ind_nil_lemma cons-bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality imageElimination productElimination promote_hyp hypothesis equalitySymmetry hyp_replacement applyLambdaEquality cumulativity sqequalRule lambdaEquality rename independent_functionElimination independent_isectElimination imageMemberEquality baseClosed dependent_functionElimination setElimination setEquality because_Cache functionEquality applyEquality voidEquality voidElimination equalityTransitivity universeEquality addLevel allFunctionality impliesFunctionality levelHypothesis unionElimination inlFormation inrFormation allLevelFunctionality impliesLevelFunctionality dependent_set_memberEquality independent_pairFormation natural_numberEquality dependent_pairFormation isect_memberEquality

Latex:
\mforall{}[A:Type]
\mforall{}as:bag(A).  \mforall{}bs:A  List.    (bag-no-repeats(A;as)  {}\mRightarrow{}  b\_all(A;as;x.(x  \mmember{}  bs))  {}\mRightarrow{}  (\mdownarrow{}sub-bag(A;as;bs)))

Date html generated: 2018_05_21-PM-07_39_04
Last ObjectModification: 2017_07_26-PM-05_13_25

Theory : general

Home Index