Nuprl Lemma : cbva_seq-spread
∀[F,G,H,L:Top]. ∀[m:ℕ]. (let x,y = cbva_seq(L; λg.<F[g], G[g]>; m) in H[x;y] ~ cbva_seq(L; λg.H[F[g];G[g]]; m))
Proof
Definitions occuring in Statement :
cbva_seq: cbva_seq(L; F; m),
nat: ℕ,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s1;s2],
so_apply: x[s],
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
cbva_seq: cbva_seq(L; F; m)
Lemmas referenced :
callbyvalueall_seq-spread0,
nat_wf,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
sqequalAxiom,
sqequalRule,
isect_memberEquality,
because_Cache
Latex:
\mforall{}[F,G,H,L:Top]. \mforall{}[m:\mBbbN{}].
(let x,y = cbva\_seq(L; \mlambda{}g.<F[g], G[g]> m)
in H[x;y] \msim{} cbva\_seq(L; \mlambda{}g.H[F[g];G[g]]; m))
Date html generated:
2016_05_15-PM-02_14_47
Last ObjectModification:
2015_12_27-AM-00_32_14
Theory : untyped!computation
Home
Index