### Nuprl Lemma : callbyvalueall-reduce-repeat

`∀[F,a:Top].  (let x ⟵ a in let y ⟵ x in F[y] ~ let x ⟵ a in F[x])`

Proof

Definitions occuring in Statement :  callbyvalueall: callbyvalueall uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` callbyvalueall: callbyvalueall so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` has-valueall: `has-valueall(a)` implies: `P `` Q` prop: `ℙ` has-value: `(a)↓`
Lemmas referenced :  evalall-sqequal top_wf has-valueall_wf_base cbv_sqequal
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 lambdaFormation hypothesis sqequalAxiom isect_memberEquality because_Cache callbyvalueReduce

Latex:
\mforall{}[F,a:Top].    (let  x  \mleftarrow{}{}  a  in  let  y  \mleftarrow{}{}  x  in  F[y]  \msim{}  let  x  \mleftarrow{}{}  a  in  F[x])

Date html generated: 2016_05_15-PM-02_08_39
Last ObjectModification: 2016_01_15-PM-10_21_50

Theory : untyped!computation

Home Index