Nuprl Lemma : the-member-bag-rep

[T:Type]. ∀[n:ℕ]. ∀[a:T].  a ↓∈ bag-rep(n;a) supposing 0 < n


Proof




Definitions occuring in Statement :  nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] natural_number: $n universe: Type bag-member: x ↓∈ bs bag-rep: bag-rep(n;x)
Lemmas :  primrec-unroll less_than_wf nat_wf equal-wf-T-base assert_wf less_than_transitivity1 le_weakening less_than_irreflexivity bnot_wf not_wf uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot primrec_wf bag_wf decidable__le subtract_wf false_wf not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel le_wf empty-bag_wf cons-bag_wf int_seg_wf bag-member_wf bag-member-cons

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[a:T].    a  \mdownarrow{}\mmember{}  bag-rep(n;a)  supposing  0  <  n



Date html generated: 2015_07_23-AM-11_25_29
Last ObjectModification: 2015_01_28-PM-11_16_10

Home Index