Nuprl Lemma : bag-drop-commutes

[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x,y:T].
  (bag-drop(eq;bag-drop(eq;bs;x);y) bag-drop(eq;bag-drop(eq;bs;y);x) ∈ bag(T))


Proof




Definitions occuring in Statement :  bag-drop: bag-drop(eq;bs;a) bag: bag(T) deq: EqDecider(T) uall: [x:A]. B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q decidable: Dec(P) or: P ∨ Q prop: bag-drop: bag-drop(eq;bs;a) exists: x:A. B[x] and: P ∧ Q so_lambda: λ2x.t[x] so_apply: x[s] top: Top true: True squash: T subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q uiff: uiff(P;Q) rev_implies:  Q sq_or: a ↓∨ b not: ¬A false: False isl: isl(x) outl: outl(x) assert: b ifthenelse: if then else fi  btrue: tt
Lemmas referenced :  decidable-equal-deq bag-drop_wf equal_wf bag_wf bag-remove1-property bag-remove1_wf unit_wf2 bag-append_wf single-bag_wf all_wf or_wf exists_wf not_wf bag-member_wf equal-wf-T-base bag-append-assoc squash_wf true_wf bag-append-comm subtype_rel_self iff_weakening_equal bag-append-cancel bag-member-append bag-member-single bfalse_wf and_wf outl_wf assert_wf isl_wf deq_wf btrue_wf btrue_neq_bfalse member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache independent_functionElimination hypothesis dependent_functionElimination hypothesisEquality unionElimination hyp_replacement equalitySymmetry applyLambdaEquality productElimination sqequalRule equalityTransitivity unionEquality isect_memberEquality axiomEquality promote_hyp inlEquality lambdaEquality productEquality baseClosed voidElimination voidEquality natural_numberEquality applyEquality imageElimination universeEquality imageMemberEquality instantiate independent_isectElimination inlFormation dependent_set_memberEquality independent_pairFormation setElimination rename inrFormation

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x,y:T].
    (bag-drop(eq;bag-drop(eq;bs;x);y)  =  bag-drop(eq;bag-drop(eq;bs;y);x))



Date html generated: 2019_10_16-AM-11_31_35
Last ObjectModification: 2018_08_21-PM-01_59_37

Theory : bags_2


Home Index