Nuprl Lemma : filter-as-accum-aux2

[A:Type]. ∀[p:A ⟶ 𝔹]. ∀[L:A List]. ∀[X:Top List].
  (X filter(p;L) accumulate (with value and list item x):
                      if p[x] then [x] else fi 
                     over list:
                     with starting value:


Definitions occuring in Statement :  filter: filter(P;l) append: as bs list_accum: list_accum cons: [a b] nil: [] list: List ifthenelse: if then else fi  bool: 𝔹 uall: [x:A]. B[x] top: Top so_apply: x[s] function: x:A ⟶ B[x] universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T top: Top so_apply: x[s]
Lemmas referenced :  mapfilter-as-accum-aux filter-as-mapfilter list_wf top_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality voidElimination voidEquality sqequalRule hypothesis sqequalAxiom because_Cache functionEquality universeEquality

\mforall{}[A:Type].  \mforall{}[p:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].  \mforall{}[X:Top  List].
    (X  @  filter(p;L)  \msim{}  accumulate  (with  value  a  and  list  item  x):
                                            if  p[x]  then  a  @  [x]  else  a  fi 
                                          over  list:
                                          with  starting  value:

Date html generated: 2016_05_15-PM-03_57_20
Last ObjectModification: 2015_12_27-PM-03_08_10

Theory : general

Home Index