### Nuprl Lemma : bag-eq_wf

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  (bag-eq(eq;as;bs) ∈ 𝔹)`

Proof

Definitions occuring in Statement :  bag-eq: `bag-eq(eq;as;bs)` bag: `bag(T)` deq: `EqDecider(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bag-eq: `bag-eq(eq;as;bs)` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` nat: `ℕ` so_apply: `x[s]`
Lemmas referenced :  band_wf bag-all_wf eq_int_wf bag-count_wf nat_wf lt_int_wf bag_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality hypothesis applyEquality setElimination rename because_Cache natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:bag(T)].    (bag-eq(eq;as;bs)  \mmember{}  \mBbbB{})

Date html generated: 2016_05_15-PM-08_00_22
Last ObjectModification: 2015_12_27-PM-04_16_00

Theory : bags_2

Home Index