Nuprl Lemma : hdf-sqequal6
∀[s,F,G:Top].
(fix((λmk-hdf,s0. (inl (λa.let bs' ←─ reduce(λl,l'. (l @ l');[];map(λb.[G[a;b]];s0))
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 :
map: map(f;as),
append: as @ bs,
null: null(as),
reduce: reduce(f;k;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
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,
map_cons_lemma,
map_nil_lemma,
reduce_cons_lemma,
list_ind_cons_lemma,
list_ind_nil_lemma,
reduce_nil_lemma,
callbyvalueall-single-sqle2,
int_subtype_base,
callbyvalueall-single-sqle,
top_wf
\mforall{}[s,F,G:Top].
(fix((\mlambda{}mk-hdf,s0. (inl (\mlambda{}a.let bs' \mleftarrow{}{} reduce(\mlambda{}l,l'. (l @ l');[];map(\mlambda{}b.[G[a;b]];s0))
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_11
Last ObjectModification:
2015_01_27-AM-11_51_17
Home
Index