Nuprl Lemma : reduce-fast-mapfilter1

[L,z,k,d,f,p:Top].
  (reduce(λx,a. case d[x;a] of inl() => inr() => a;k;fast-mapfilter(p;f;L)) reduce(λx,a. if 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 then else fi  uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] apply: a lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: 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: supposing a strict1: strict1(F) and: P ∧ Q all: x:A. B[x] implies:  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