Nuprl Lemma : normalization-callbyvalueall-spread1

[F,G,H,a:Top].
  (let x ⟵ a
   in F[x] let u,v in H[x;u;v] let y ⟵ in G[x;u;v;y] let x ⟵ a
                                                              in F[x] let u,v in H[x;u;v] G[x;u;v;u])


Proof




Definitions occuring in Statement :  callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top so_apply: x[s1;s2;s3;s4] so_apply: x[s1;s2;s3] so_apply: x[s] apply: a spread: spread def 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)↓ uiff: uiff(P;Q) and: P ∧ Q
Lemmas referenced :  top_wf is-exception_wf has-value_wf_base evalall-sqequal has-valueall-pair pair-eta 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 sqequalSqle divergentSqle callbyvalueSpread equalityTransitivity equalitySymmetry productElimination callbyvalueReduce sqleReflexivity introduction spreadExceptionCases axiomSqleEquality exceptionSqequal isect_memberFormation sqequalAxiom isect_memberEquality

Latex:
\mforall{}[F,G,H,a:Top].
    (let  x  \mleftarrow{}{}  a
      in  F[x]  let  u,v  =  x  in  H[x;u;v]  let  y  \mleftarrow{}{}  u  in  G[x;u;v;y]  \msim{}  let  x  \mleftarrow{}{}  a
                                                                                                                            in  F[x] 
                                                                                                                                  let  u,v  =  x 
                                                                                                                                  in  H[x;u;v]  G[x;u;v;u])



Date html generated: 2016_05_13-PM-04_08_27
Last ObjectModification: 2016_01_14-PM-07_46_05

Theory : fun_1


Home Index