Nuprl Lemma : reduce-fast-mapfilter2

[L,z,k,c,d,f,p:Top].
  (reduce(λx,a. if c[x;a]=d[x;a] then else a;k;fast-mapfilter(p;f;L)) reduce(λx,a. if x
                                                                                  then if c[f x;a]=d[f x;a]
                                                                                       then z
                                                                                       else 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] int_eq: if a=b then else d apply: a lambda: λx.A[x] 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,c,d,f,p:Top].
    (reduce(\mlambda{}x,a.  if  c[x;a]=d[x;a]  then  z  else  a;k;fast-mapfilter(p;f;L)) 
    \msim{}  reduce(\mlambda{}x,a.  if  p  x  then  if  c[f  x;a]=d[f  x;a]  then  z  else  a  else  a  fi  ;k;L))



Date html generated: 2019_10_15-AM-11_09_36
Last ObjectModification: 2018_10_16-AM-09_34_18

Theory : general


Home Index