Nuprl Lemma : sub-bags-no-repeats

[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  bag-no-repeats(bag(T);sub-bags(eq;bs)) supposing valueall-type(T)


Proof




Definitions occuring in Statement :  sub-bags: sub-bags(eq;bs) bag-no-repeats: bag-no-repeats(T;bs) bag: bag(T) deq: EqDecider(T) valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sub-bags: sub-bags(eq;bs) bag-no-repeats: bag-no-repeats(T;bs) squash: T all: x:A. B[x] prop: implies:  Q subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] top: Top uiff: uiff(P;Q) and: P ∧ Q inject: Inj(A;B;f) pi1: fst(t) rev_uimplies: rev_uimplies(P;Q) true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  valueall-type_wf bag_wf deq_wf bag-subtype bag-partitions_wf bag-member_wf equal_wf bag-map-no-repeats pi1_wf_top subtype_rel_product top_wf set_wf bag-member-partitions and_wf bag-append_wf bag-append-cancel bag-no-repeats_wf subtype_rel_bag no-repeats-bag-partitions bag-no-repeats-settype decidable__equal_product decidable__equal_bag decidable-equal-deq squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution imageElimination hypothesis imageMemberEquality hypothesisEquality thin baseClosed extract_by_obid isectElimination cumulativity isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality productEquality dependent_functionElimination independent_isectElimination setEquality productElimination independent_pairEquality lambdaFormation independent_functionElimination lambdaEquality setElimination rename applyEquality voidElimination voidEquality dependent_set_memberEquality independent_pairFormation applyLambdaEquality hyp_replacement instantiate natural_numberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].
    bag-no-repeats(bag(T);sub-bags(eq;bs))  supposing  valueall-type(T)



Date html generated: 2018_05_21-PM-09_52_37
Last ObjectModification: 2017_07_26-PM-06_31_54

Theory : bags_2


Home Index