Nuprl Lemma : hdf-base-transformation2
∀[F:Top]. (hdf-base(m.F[m]) ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λx.⊥; λg.<mk-hdf Ax, F[a]> 0))))) Ax)
Proof
Definitions occuring in Statement : 
hdf-base: hdf-base(m.F[m])
, 
bottom: ⊥
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
so_apply: x[s]
, 
apply: f a
, 
fix: fix(F)
, 
lambda: λx.A[x]
, 
pair: <a, b>
, 
inl: inl x
, 
natural_number: $n
, 
sqequal: s ~ t
, 
axiom: Ax
, 
cbva_seq: cbva_seq(L; F; m)
Lemmas : 
nat_properties, 
less_than_transitivity1, 
less_than_irreflexivity, 
ge_wf, 
less_than_wf, 
fun_exp0_lemma, 
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, 
top_wf
\mforall{}[F:Top].  (hdf-base(m.F[m])  \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}x.\mbot{};  \mlambda{}g.<mk-hdf  Ax,  F[a]>  0)))))  A\000Cx)
Date html generated:
2015_07_17-AM-08_08_22
Last ObjectModification:
2015_01_27-PM-00_06_03
Home
Index