Nuprl Lemma : callbyvalueall-ifthenelse
∀[C:Base]. ∀[a,A,B:Top].
(let x ⟵ if a then A else B fi
in C[x] ~ if a then let x ⟵ A in C[x] else let x ⟵ B in C[x] fi )
Proof
Definitions occuring in Statement :
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
base: Base,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
top: Top,
so_lambda: λ2x.t[x],
so_apply: x[s],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4],
uimplies: b supposing a
Lemmas referenced :
lifting-strict-ifthenelse,
strict4-callbyvalueall,
base_wf,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
hypothesis,
sqequalAxiom,
lemma_by_obid,
sqequalRule,
sqequalHypSubstitution,
isect_memberEquality,
isectElimination,
thin,
hypothesisEquality,
because_Cache,
baseApply,
closedConclusion,
baseClosed,
voidElimination,
voidEquality,
independent_isectElimination
Latex:
\mforall{}[C:Base]. \mforall{}[a,A,B:Top].
(let x \mleftarrow{}{} if a then A else B fi
in C[x] \msim{} if a then let x \mleftarrow{}{} A in C[x] else let x \mleftarrow{}{} B in C[x] fi )
Date html generated:
2016_05_13-PM-03_41_56
Last ObjectModification:
2016_01_14-PM-07_08_54
Theory : computation
Home
Index