Nuprl Lemma : bag-member-list-member

[T:Type]. ((∀x,y:T.  Dec(x y ∈ T))  (∀L:T List. ∀b:bag(T). ∀x:T.  ((L b ∈ bag(T))  x ↓∈  (x ∈ L))))


Proof




Definitions occuring in Statement :  bag-member: x ↓∈ bs bag: bag(T) l_member: (x ∈ l) list: List decidable: Dec(P) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T squash: T prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q so_lambda: λ2x.t[x] so_apply: x[s] empty-bag: {} uiff: uiff(P;Q) false: False cons-bag: x.b sq_or: a ↓∨ b or: P ∨ Q rev_implies:  Q sq_stable: SqStable(P)
Lemmas referenced :  bag-member_wf squash_wf true_wf bag_wf iff_weakening_equal list_induction list-subtype-bag l_member_wf list_wf bag-member-empty-iff nil_wf bag-member-cons cons_wf equal_wf all_wf decidable_wf cons_member sq_stable__l_member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache natural_numberEquality sqequalRule imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination functionEquality cumulativity voidElimination voidEquality rename dependent_functionElimination unionElimination inlFormation hyp_replacement Error :applyLambdaEquality,  inrFormation

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}L:T  List.  \mforall{}b:bag(T).  \mforall{}x:T.    ((L  =  b)  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (x  \mmember{}  L))))



Date html generated: 2016_10_25-AM-10_28_10
Last ObjectModification: 2016_07_12-AM-06_44_25

Theory : bags


Home Index