Nuprl Lemma : callbyvalueall-reduce-repeat-right-branch

  (let x ⟵ a
   in case d[x] of inl(u) => F[x;u] inr(v) => let y ⟵ in G[y;v] let x ⟵ a
                                                                       in case d[x]
                                                                        of inl(u) =>
                                                                        inr(v) =>


Definitions occuring in Statement :  callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] so_apply: x[s] decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: t
Definitions unfolded in proof :  callbyvalueall: callbyvalueall uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a has-valueall: has-valueall(a) implies:  Q prop: has-value: (a)↓
Lemmas referenced :  top_wf evalall-sqequal has-valueall_wf_base cbv_sqequal
Rules used in proof :  cut sqequalRule thin sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lemma_by_obid sqequalHypSubstitution isectElimination baseApply closedConclusion baseClosed hypothesisEquality independent_isectElimination lambdaFormation hypothesis because_Cache callbyvalueReduce isect_memberFormation introduction sqequalAxiom isect_memberEquality

    (let  x  \mleftarrow{}{}  a
      in  case  d[x]  of  inl(u)  =>  F[x;u]  |  inr(v)  =>  let  y  \mleftarrow{}{}  x  in  G[y;v]  \msim{}  let  x  \mleftarrow{}{}  a
                                                                                                                                              in  case  d[x]
                                                                                                                                                of  inl(u)  =>
                                                                                                                                                |  inr(v)  =>

Date html generated: 2016_05_15-PM-02_08_41
Last ObjectModification: 2016_01_15-PM-10_21_48

Theory : untyped!computation

Home Index