Nuprl Lemma : reduce-fast-mapfilter1

∀[L,z,k,d,f,p:Top].
  (reduce(λx,a. case d[x;a] of inl() => z | inr() => a;k;fast-mapfilter(p;f;L)) ~ reduce(λx,a. if p x
                                                                                          then case d[f x;a]
                                                                                                of inl() =>
                                                                                                z
                                                                                                | inr() =>
                                                                                                a
                                                                                          else a
                                                                                          fi ;k;L))


Proof



Definitions occuring in Statement :  fast-mapfilter: fast-mapfilter(p;f;L),  reduce: reduce(f;k;as),  ifthenelse: if b then t else f fi ,  uall: ∀[x:A]. B[x],  top: Top,  so_apply: x[s1;s2],  apply: f a,  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  sqequal: s ~ t
Definitions unfolded in proof :  so_apply: x[s1;s2],  fast-mapfilter: fast-mapfilter(p;f;L),  so_apply: x[s],  uall: ∀[x:A]. B[x],  member: t ∈ T,  reduce: reduce(f;k;as),  so_lambda: λ2x.t[x],  uimplies: b supposing a,  strict1: strict1(F),  and: P ∧ Q,  all: ∀x:A. B[x],  implies: P ⇒ Q,  list_ind: list_ind,  has-value: (a)↓,  prop: ℙ,  or: P ∨ Q,  squash: ↓T,  so_lambda: so_lambda(x,y,z.t[x; y; z]),  so_apply: x[s1;s2;s3],  top: Top
Lemmas referenced :  sqequal-list_ind,  has-value_wf_base,  istype-base,  is-exception_wf,  istype-universe,  reduce-ifthenelse,  istype-void,  reduce_cons_lemma,  sqle_wf_base,  reduce_nil_lemma,  top_wf
Rules used in proof :  sqequalSubstitution,  sqequalRule,  sqequalReflexivity,  sqequalTransitivity,  computationStep,  isect_memberFormation_alt,  introduction,  cut,  thin,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  baseApply,  closedConclusion,  baseClosed,  hypothesisEquality,  independent_isectElimination,  independent_pairFormation,  lambdaFormation_alt,  callbyvalueCallbyvalue,  hypothesis,  callbyvalueReduce,  universeIsType,  callbyvalueExceptionCases,  inlFormation_alt,  imageMemberEquality,  imageElimination,  exceptionSqequal,  inrFormation_alt,  isect_memberEquality_alt,  voidElimination,  dependent_functionElimination,  divergentSqle,  sqleRule,  sqleReflexivity,  instantiate,  inhabitedIsType,  because_Cache,  axiomSqEquality,  isectIsTypeImplies
Latex:
\mforall{}[L,z,k,d,f,p:Top].
    (reduce(\mlambda{}x,a.  case  d[x;a]  of  inl()  =>  z  |  inr()  =>  a;k;fast-mapfilter(p;f;L)) 
    \msim{}  reduce(\mlambda{}x,a.  if  p  x  then  case  d[f  x;a]  of  inl()  =>  z  |  inr()  =>  a  else  a  fi  ;k;L))


Date html generated: 2019_10_15-AM-11_09_28
Last ObjectModification: 2018_10_16-AM-09_34_23

Theory : general


Home Index