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: accum(z,x.f[z; x],a,{x∈X|P[x]}) l_member: (x ∈ l) list: 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: accum(z,x.f[z; x],a,{x∈X|P[x]}) uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q cand: c∧ B prop: implies:  Q so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B uimplies: supposing a all: x:A. B[x] iff: ⇐⇒ 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