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]))


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: 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: supposing a bag: bag(T) quotient: x,y:A//B[x; y] and: P ∧ Q all: x:A. B[x] implies:  Q bag-reduce: bag-reduce(x,y.f[x; y];zero;bs) prop: so_apply: x[s1;s2] assoc: Assoc(T;op) infix_ap: y comm: Comm(T;op) so_lambda: λ2x.t[x] so_apply: x[s] squash: T true: True top: Top iff: ⇐⇒ Q rev_implies:  Q guard: {T} subtype_rel: A ⊆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

\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