Nuprl Lemma : lifting-spread-callbyvalueall

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


Proof




Definitions occuring in Statement :  callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] so_apply: x[s] spread: spread def sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2] uimplies: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: guard: {T} or: P ∨ Q squash: T so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  lifting-strict-callbyvalueall top_wf equal_wf has-value_wf_base base_wf is-exception_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueSpread hypothesis equalityTransitivity equalitySymmetry productEquality productElimination sqleReflexivity hypothesisEquality dependent_functionElimination independent_functionElimination baseApply closedConclusion spreadExceptionCases inrFormation because_Cache imageMemberEquality imageElimination exceptionSqequal inlFormation sqequalAxiom

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



Date html generated: 2017_04_14-AM-07_20_59
Last ObjectModification: 2017_02_27-PM-02_54_30

Theory : computation


Home Index