### Nuprl Lemma : accum_filter_rel_wf

`∀[T,A:Type]. ∀[a,b:A]. ∀[X:T List]. ∀[P:{x:T| (x ∈ X)}  ⟶ ℙ]. ∀[f:A ⟶ {x:T| (x ∈ X)}  ⟶ A].`
`  (b = accum(z,x.f[z;x],a,{x∈X|P[x]}) ∈ ℙ)`

Proof

Definitions occuring in Statement :  accum_filter_rel: `b = accum(z,x.f[z; x],a,{x∈X|P[x]})` l_member: `(x ∈ l)` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  accum_filter_rel: `b = accum(z,x.f[z; x],a,{x∈X|P[x]})` uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` cand: `A c∧ B` prop: `ℙ` implies: `P `` Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q`
Lemmas referenced :  l_member_wf list_wf equal_wf list_accum_wf all_wf list-subtype subtype_rel_list_set
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution axiomEquality equalityTransitivity hypothesis equalitySymmetry functionEquality hypothesisEquality setEquality lemma_by_obid isectElimination thin isect_memberEquality because_Cache cumulativity universeEquality productEquality lambdaEquality applyEquality productElimination independent_isectElimination setElimination rename lambdaFormation dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[T,A:Type].  \mforall{}[a,b:A].  \mforall{}[X:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  X)\}    {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:A  {}\mrightarrow{}  \{x:T|  (x  \mmember{}  X)\}    {}\mrightarrow{}  A].
(b  =  accum(z,x.f[z;x],a,\{x\mmember{}X|P[x]\})  \mmember{}  \mBbbP{})

Date html generated: 2016_05_15-PM-04_32_54
Last ObjectModification: 2015_12_27-PM-02_48_40

Theory : general

Home Index