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: a fix: fix(F) lambda: λx.A[x] pair: <a, b> inl: inl x natural_number: $n sqequal: 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