Nuprl Lemma : hdf-sqequal7
∀[F,G,H,K,L,J,init:Top].
(fix((λmk-hdf,s0. (inl (λa.let X,s = s0
in case X
of inl(P) =>
let X',fs = P a
in let b ←─ G[fs;s]
in let s' ←─ J[b;s]
in <mk-hdf <X', K[s;s']>, L[s;s']>
| inr(z) =>
H[mk-hdf;s;z]))))
<fix((λmk-hdf.(inl (λa.let out ←─ F[a] in <mk-hdf, out>)))), init> ~ fix((λmk-hdf,s. (inl (λa.let out ←─ F[a]
in let b ←─ G[out;s]
in let s' ←─ J[b;s]
in <mk-hdf K[s;s'], L[s;s']>))))
init)
Proof
Definitions occuring in Statement :
callbyvalueall: callbyvalueall,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2],
so_apply: x[s],
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x,
sqequal: s ~ t
Lemmas :
nat_properties,
less_than_transitivity1,
less_than_irreflexivity,
ge_wf,
less_than_wf,
base_wf,
fun_exp0_lemma,
strictness-apply,
bottom_diverge,
has-value_wf_base,
exception-not-bottom,
decidable__le,
subtract_wf,
false_wf,
not-ge-2,
less-iff-le,
condition-implies-le,
minus-one-mul,
zero-add,
minus-add,
minus-minus,
add-associates,
add-swap,
add-commutes,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
fun_exp_unroll_1,
lifting-strict-callbyvalueall,
strict4-spread,
top_wf
\mforall{}[F,G,H,K,L,J,init:Top].
(fix((\mlambda{}mk-hdf,s0. (inl (\mlambda{}a.let X,s = s0
in case X
of inl(P) =>
let X',fs = P a
in let b \mleftarrow{}{} G[fs;s]
in let s' \mleftarrow{}{} J[b;s]
in <mk-hdf <X', K[s;s']>, L[s;s']>
| inr(z) =>
H[mk-hdf;s;z]))))
<fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.let out \mleftarrow{}{} F[a] in <mk-hdf, out>)))), init> \msim{} fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.let\000C out \mleftarrow{}{} F[a]
in let b \mleftarrow{}{} G[out;s]
in let s' \mleftarrow{}{} J[b;s]
in <mk-hdf
K[s;s']
, L[s;s']
>))))
init)
Date html generated:
2015_07_17-AM-08_17_19
Last ObjectModification:
2015_04_30-AM-11_01_57
Home
Index