### Nuprl Lemma : filter-as-accum-aux2

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

Proof

Definitions occuring in Statement :  filter: `filter(P;l)` append: `as @ bs` list_accum: list_accum cons: `[a / b]` nil: `[]` list: `T List` ifthenelse: `if b then t else f fi ` bool: `𝔹` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type` sqequal: `s ~ 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

Latex:
\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:
L
with  starting  value:
X))

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

Theory : general

Home Index