Nuprl Lemma : bag-restrict-append

[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b,c:bag(T)].  ((b c|x) (b|x) (c|x))


Proof




Definitions occuring in Statement :  bag-restrict: (b|x) bag-append: as bs bag: bag(T) deq: EqDecider(T) uall: [x:A]. B[x] universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag-restrict: (b|x) so_lambda: λ2x.t[x] top: Top so_apply: x[s]
Lemmas referenced :  bag-filter-append bag_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesis sqequalAxiom hypothesisEquality because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[b,c:bag(T)].    ((b  +  c|x)  \msim{}  (b|x)  +  (c|x))



Date html generated: 2016_05_15-PM-08_10_17
Last ObjectModification: 2015_12_27-PM-04_12_10

Theory : bags_2


Home Index