Nuprl Lemma : lifting-strict-callbyvalueall

[F:Base]. ∀[p,q,r:Top].
  ∀[a,B:Top].  (F[let x ⟵ in B[x];p;q;r] let x ⟵ in F[B[x];p;q;r]) supposing strict4(λx,y,z,w. F[x;y;z;w])


Proof




Definitions occuring in Statement :  strict4: strict4(F) callbyvalueall: callbyvalueall uimplies: supposing a uall: [x:A]. B[x] top: Top so_apply: x[s1;s2;s3;s4] so_apply: x[s] lambda: λx.A[x] base: Base sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a callbyvalueall: callbyvalueall top: Top so_lambda: λ2x.t[x] so_apply: x[s] prop:
Lemmas referenced :  base_wf strict4_wf top_wf lifting-strict-callbyvalue
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination isect_memberEquality voidElimination voidEquality sqequalRule sqequalAxiom because_Cache baseApply closedConclusion baseClosed equalityTransitivity equalitySymmetry

Latex:
\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
    \mforall{}[a,B:Top].    (F[let  x  \mleftarrow{}{}  a  in  B[x];p;q;r]  \msim{}  let  x  \mleftarrow{}{}  a  in  F[B[x];p;q;r]) 
    supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])



Date html generated: 2016_05_13-PM-03_41_52
Last ObjectModification: 2016_01_14-PM-07_08_55

Theory : computation


Home Index