Nuprl Lemma : hdf-sqequal6-2
∀[s,F,G:Top].
(fix((λmk-hdf,s0. (inl (λa.let bs' ←─ ∪f∈[λb.[G[a;b]]].∪b∈s0.f b
in <mk-hdf case null(bs') of inl() => s0 | inr() => bs', F[s0;bs']>))))
[s] ~ fix((λmk-hdf,s0. (inl (λa.let bs' ←─ G[a;s0] in <mk-hdf bs', F[[s0];[bs']]>)))) s)
Proof
Definitions occuring in Statement :
null: null(as),
cons: [a / b],
nil: [],
callbyvalueall: callbyvalueall,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s1;s2],
apply: f a,
fix: fix(F),
lambda: λx.A[x],
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x,
sqequal: s ~ t,
bag-combine: ∪x∈bs.f[x]
Lemmas :
nat_properties,
less_than_transitivity1,
less_than_irreflexivity,
ge_wf,
less_than_wf,
base_wf,
strictness-apply,
bottom_diverge,
has-value_wf_base,
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,
bag-combine-unit-left-top,
top_wf,
empty_bag_append_lemma,
bag-append-empty,
cons_wf,
nil_wf,
callbyvalueall-single-sqle2,
int_subtype_base,
callbyvalueall-single-sqle,
bag-append-assoc
\mforall{}[s,F,G:Top].
(fix((\mlambda{}mk-hdf,s0. (inl (\mlambda{}a.let bs' \mleftarrow{}{} \mcup{}f\mmember{}[\mlambda{}b.[G[a;b]]].\mcup{}b\mmember{}s0.f b
in <mk-hdf case null(bs') of inl() => s0 | inr() => bs', F[s0;bs']>))))\000C
[s] \msim{} fix((\mlambda{}mk-hdf,s0. (inl (\mlambda{}a.let bs' \mleftarrow{}{} G[a;s0] in <mk-hdf bs', F[[s0];[bs']]>)))) s)
Date html generated:
2015_07_17-AM-08_17_17
Last ObjectModification:
2015_01_27-AM-11_51_22
Home
Index