Nuprl Lemma : map_reduce_spread2_to_reduce

  (map(f;reduce(λx,a. let y,z in let u,v in case d[y;u;v] of inl(x1) => inr(y1) => [c[y;u;v] a];[];L)) 
  reduce(λx,a. let y,z in let u,v in if d[y;u;v] then else [f c[y;u;v] a] fi ;[];L))


Definitions occuring in Statement :  map: map(f;as) reduce: reduce(f;k;as) cons: [a b] nil: [] ifthenelse: if then else fi  uall: [x:A]. B[x] top: Top so_apply: x[s1;s2;s3] apply: a lambda: λx.A[x] spread: spread def decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T reduce: reduce(f;k;as) so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a strict1: strict1(F) and: P ∧ Q all: x:A. B[x] implies:  Q map: map(f;as) list_ind: list_ind has-value: (a)↓ prop: or: P ∨ Q squash: T guard: {T} so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] top: Top strict4: strict4(F) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] ifthenelse: if then else fi  cons: [a b]
Lemmas referenced :  top_wf map_nil_lemma sqle_wf_base lifting-strict-decide lifting-strict-spread is-exception_wf base_wf has-value_wf_base sqequal-list_ind
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule thin lemma_by_obid sqequalHypSubstitution isectElimination baseApply closedConclusion baseClosed hypothesisEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueCallbyvalue hypothesis callbyvalueReduce callbyvalueExceptionCases inlFormation imageMemberEquality imageElimination exceptionSqequal inrFormation isect_memberEquality voidElimination voidEquality sqleRule sqleReflexivity because_Cache dependent_functionElimination sqequalAxiom

    (map(f;reduce(\mlambda{}x,a.  let  y,z  =  x 
                                            in  let  u,v  =  z 
                                                  in  case  d[y;u;v]  of  inl(x1)  =>  a  |  inr(y1)  =>  [c[y;u;v]  /  a];[];L)) 
    \msim{}  reduce(\mlambda{}x,a.  let  y,z  =  x  in  let  u,v  =  z  in  if  d[y;u;v]  then  a  else  [f  c[y;u;v]  /  a]  fi  ;[];L))

Date html generated: 2016_05_15-PM-02_08_24
Last ObjectModification: 2016_01_15-PM-10_23_56

Theory : untyped!computation

Home Index