Nuprl Lemma : decidable__bag-member

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


Proof




Definitions occuring in Statement :  bag-member: x ↓∈ bs bag: bag(T) 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 iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q prop: so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B nat:
Lemmas referenced :  deq-exists bag-member-count bag_wf all_wf decidable_wf equal_wf bag-member_wf le_wf bag-count_wf nat_wf decidable__le decidable_functionality iff_weakening_uiff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache productElimination independent_functionElimination hypothesis rename hypothesisEquality sqequalRule lambdaEquality universeEquality natural_numberEquality applyEquality setElimination dependent_functionElimination

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



Date html generated: 2016_05_15-PM-07_58_26
Last ObjectModification: 2015_12_27-PM-04_16_28

Theory : bags_2


Home Index