### Nuprl Lemma : bag-accum_wf

`∀[T,S:Type]. ∀[init:S]. ∀[f:S ⟶ T ⟶ S]. ∀[bs:bag(T)].`
`  bag-accum(v,x.f[v;x];init;bs) ∈ S supposing ∀v:S. ∀x,y:T.  (f[f[v;y];x] = f[f[v;x];y] ∈ S)`

Proof

Definitions occuring in Statement :  bag-accum: `bag-accum(v,x.f[v; x];init;bs)` bag: `bag(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
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-accum: `bag-accum(v,x.f[v; x];init;bs)` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` so_apply: `x[s]` so_lambda: `λ2x y.t[x; y]` squash: `↓T` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` subtype_rel: `A ⊆r B` guard: `{T}`
Lemmas referenced :  list_wf permutation_wf equal_wf equal-wf-base all_wf bag_wf permutation-invariant list_accum_wf squash_wf true_wf cons_wf list_induction append_wf nil_wf list_ind_nil_lemma list_accum_cons_lemma list_accum_nil_lemma list_ind_cons_lemma iff_weakening_equal
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 lambdaEquality applyEquality functionExtensionality isect_memberEquality functionEquality universeEquality addLevel hyp_replacement imageElimination natural_numberEquality imageMemberEquality baseClosed levelHypothesis voidElimination voidEquality independent_isectElimination

Latex:
\mforall{}[T,S:Type].  \mforall{}[init:S].  \mforall{}[f:S  {}\mrightarrow{}  T  {}\mrightarrow{}  S].  \mforall{}[bs:bag(T)].
bag-accum(v,x.f[v;x];init;bs)  \mmember{}  S  supposing  \mforall{}v:S.  \mforall{}x,y:T.    (f[f[v;y];x]  =  f[f[v;x];y])

Date html generated: 2017_10_01-AM-08_48_12
Last ObjectModification: 2017_07_26-PM-04_32_25

Theory : bags

Home Index