### Nuprl Lemma : lifting-callbyvalueall-pair

`∀[a,b,B:Top].  (let x ⟵ <a, b> in B[x] ~ let x ⟵ a in let y ⟵ b in B[<x, y>])`

Proof

Definitions occuring in Statement :  callbyvalueall: callbyvalueall uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` pair: `<a, b>` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` callbyvalueall: callbyvalueall evalall: `evalall(t)` top: `Top` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ`
Lemmas referenced :  has-value_wf_base is-exception_wf equal_wf top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule isect_memberEquality voidElimination voidEquality thin because_Cache lambdaFormation sqequalSqle sqleRule divergentSqle callbyvalueCallbyvalue sqequalHypSubstitution hypothesis callbyvalueReduce sqleReflexivity extract_by_obid isectElimination baseApply closedConclusion baseClosed hypothesisEquality callbyvalueExceptionCases axiomSqleEquality exceptionSqequal equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination sqequalAxiom

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

Date html generated: 2017_04_14-AM-07_35_26
Last ObjectModification: 2017_02_27-PM-03_08_18

Theory : fun_1

Home Index