Nuprl Lemma : hdf-sqequal8-3
∀[mk-hdf,a,s,X,x:Top].
(let b ←─ a
in case null(b) of inl(x1) => let s' ←─ s in <mk-hdf <X, s'>, x> | inr(y1) => <mk-hdf <X, b>, x> ~ let b ←─ a
in let s' ←─ if null(b) then s else b fi
in <mk-hdf <X, s'>, x>)
Proof
Definitions occuring in Statement :
null: null(as),
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
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,X,x:Top].
(let b \mleftarrow{}{} a
in case null(b) of inl(x1) => let s' \mleftarrow{}{} s in <mk-hdf <X, s'>, x> | inr(y1) => <mk-hdf <X, b>, x> \000C\msim{} let b \mleftarrow{}{} a
in let s' \mleftarrow{}{} if null(b)
then s
else b
fi
in <mk-hdf <X, s'>, x>)
Date html generated:
2015_07_17-AM-08_08_16
Last ObjectModification:
2015_01_27-PM-00_05_58
Home
Index