Nuprl Lemma : reduce-fast-mapfilter2
∀[L,z,k,c,d,f,p:Top].
  (reduce(λx,a. if c[x;a]=d[x;a] then z else a;k;fast-mapfilter(p;f;L)) ~ reduce(λx,a. if p 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 b then t else f fi 
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
so_apply: x[s1;s2]
, 
int_eq: if a=b then c else d
, 
apply: f a
, 
lambda: λx.A[x]
, 
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,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