### Nuprl Lemma : bag-reduce_wf

`∀[T:Type]. ∀[zero:T]. ∀[f:T ⟶ T ⟶ T].`
`  (∀[bs:bag(T)]. (bag-reduce(x,y.f[x;y];zero;bs) ∈ T)) supposing (Assoc(T;λx,y. f[x;y]) and Comm(T;λx,y. f[x;y]))`

Proof

Definitions occuring in Statement :  bag-reduce: `bag-reduce(x,y.f[x; y];zero;bs)` bag: `bag(T)` comm: `Comm(T;op)` assoc: `Assoc(T;op)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` bag: `bag(T)` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` bag-reduce: `bag-reduce(x,y.f[x; y];zero;bs)` prop: `ℙ` so_apply: `x[s1;s2]` assoc: `Assoc(T;op)` infix_ap: `x f y` comm: `Comm(T;op)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` squash: `↓T` true: `True` top: `Top` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` guard: `{T}` subtype_rel: `A ⊆r B` label: `...\$L... t` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]`
Lemmas referenced :  list_wf permutation_wf equal_wf equal-wf-base bag_wf assoc_wf comm_wf permutation-invariant reduce_wf squash_wf true_wf cons_wf reduce_cons_lemma iff_weakening_equal list_induction all_wf append_wf nil_wf list_ind_nil_lemma reduce_nil_lemma list_ind_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality because_Cache sqequalRule pertypeElimination productElimination thin equalityTransitivity hypothesis equalitySymmetry extract_by_obid isectElimination cumulativity hypothesisEquality lambdaFormation rename dependent_functionElimination independent_functionElimination productEquality axiomEquality isect_memberEquality lambdaEquality applyEquality functionExtensionality functionEquality universeEquality addLevel hyp_replacement imageElimination natural_numberEquality imageMemberEquality baseClosed levelHypothesis voidElimination voidEquality independent_isectElimination

Latex:
\mforall{}[T:Type].  \mforall{}[zero:T].  \mforall{}[f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].
(\mforall{}[bs:bag(T)].  (bag-reduce(x,y.f[x;y];zero;bs)  \mmember{}  T))  supposing
(Assoc(T;\mlambda{}x,y.  f[x;y])  and
Comm(T;\mlambda{}x,y.  f[x;y]))

Date html generated: 2017_10_01-AM-08_48_08
Last ObjectModification: 2017_07_26-PM-04_32_22

Theory : bags

Home Index