### Nuprl Lemma : accum_filter_rel_nil

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

Proof

Definitions occuring in Statement :  accum_filter_rel: `b = accum(z,x.f[z; x],a,{x∈X|P[x]})` nil: `[]` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2]` so_apply: `x[s]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` prop: `ℙ` so_lambda: `λ2x.t[x]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` false: `False` so_apply: `x[s]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` accum_filter_rel: `b = accum(z,x.f[z; x],a,{x∈X|P[x]})` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` cand: `A c∧ B` top: `Top` or: `P ∨ Q` cons: `[a / b]` subtype_rel: `A ⊆r B`
Lemmas referenced :  accum_filter_rel_wf nil_wf l_member_wf null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse sublist_wf all_wf iff_wf list_wf equal_wf top_wf nil-sublist list_accum_nil_lemma list-cases product_subtype_list list_accum_cons_lemma cons_wf sublist_nil and_wf null_wf3 subtype_rel_list null_cons_lemma bfalse_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality because_Cache hypothesis sqequalRule lambdaEquality lambdaFormation setElimination rename independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination voidElimination setEquality dependent_functionElimination axiomEquality productEquality productElimination independent_pairEquality isect_memberEquality universeEquality voidEquality unionElimination promote_hyp hypothesis_subsumption dependent_set_memberEquality applyEquality

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

Date html generated: 2016_05_15-PM-04_33_01
Last ObjectModification: 2015_12_27-PM-02_48_34

Theory : general

Home Index