Nuprl Lemma : hdf-sqequal9
∀[mk-hdf,a,s:Top].
(let b ←─ a
in case null(b) of inl(x1) => let s' ←─ s in <mk-hdf s', s'> | inr(y1) => <mk-hdf b, b> ~ let b ←─ a
in let s' ←─ case null(b)
of inl(x1) =>
s
| inr(y1) =>
b
in <mk-hdf s', s'>)
Proof
Definitions occuring in Statement :
null: null(as),
callbyvalueall: callbyvalueall,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
sqequal: s ~ t
Lemmas :
lifting-strict-ispair,
has-value_wf_base,
base_wf,
lifting-strict-isaxiom,
strictness-decide,
lifting-strict-decide,
has-valueall-if-has-value-callbyvalueall,
has-valueall-has-value,
evalall-sqequal,
top_wf
\mforall{}[mk-hdf,a,s:Top].
(let b \mleftarrow{}{} a
in case null(b) of inl(x1) => let s' \mleftarrow{}{} s in <mk-hdf s', s'> | inr(y1) => <mk-hdf b, b> \msim{} let b \mleftarrow{}\000C{} a
in let s' \mleftarrow{}{}
case null(b)
of inl(x1) =>
s
| inr(y1) =>
b
in <mk-hdf s', s'>)
Date html generated:
2015_07_17-AM-08_17_21
Last ObjectModification:
2015_01_27-AM-11_51_11
Home
Index