### Nuprl Lemma : bag-remove1_wf

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  (bag-remove1(eq;bs;x) ∈ bag(T)?)`

Proof

Definitions occuring in Statement :  bag-remove1: `bag-remove1(eq;bs;a)` bag: `bag(T)` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` unit: `Unit` member: `t ∈ T` union: `left + right` universe: `Type`
Definitions unfolded in proof :  bag: `bag(T)` member: `t ∈ T` uall: `∀[x:A]. B[x]` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` guard: `{T}` or: `P ∨ Q` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` bag-append: `as + bs` subtype_rel: `A ⊆r B` uimplies: `b supposing a` true: `True` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` squash: `↓T` rev_implies: `P `` Q` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` not: `¬A` false: `False`
Lemmas referenced :  bag_wf unit_wf2 list_wf permutation_wf equal_wf equal-wf-base deq_wf member-permutation bag-remove1-property1 subtype_rel_union list-subtype-bag quotient-member-eq permutation-equiv append_wf squash_wf true_wf bag-append_wf reverse-bag iff_weakening_equal permutation_transitivity permutation_weakening cons_wf nil_wf permutation_functionality_wrt_permutation append_functionality_wrt_permutation permutation-rotate list_ind_cons_lemma list_ind_nil_lemma cons_cancel_wrt_permutation reverse_wf length_wf_nat nat_wf member_append cons_member l_member_wf bag-remove1_wf1
Rules used in proof :  sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity pointwiseFunctionalityForEquality unionEquality cut introduction extract_by_obid isectElimination thin cumulativity hypothesisEquality hypothesis sqequalRule pertypeElimination productElimination equalityTransitivity equalitySymmetry lambdaFormation because_Cache rename dependent_functionElimination independent_functionElimination productEquality universeEquality isect_memberFormation axiomEquality isect_memberEquality unionElimination hyp_replacement applyLambdaEquality applyEquality independent_isectElimination lambdaEquality natural_numberEquality inlEquality imageElimination imageMemberEquality baseClosed voidElimination voidEquality dependent_set_memberEquality inlFormation inrFormation setElimination

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].    (bag-remove1(eq;bs;x)  \mmember{}  bag(T)?)

Date html generated: 2018_05_21-PM-09_48_11
Last ObjectModification: 2017_07_26-PM-06_30_34

Theory : bags_2

Home Index