Nuprl Lemma : hdf-sqequal2

[F,G,H:Top].
  (fix((λmk-hdf,s0. case s0 of inl(y) => inl a.let X',bs in let out ←─ G[bs] in <mk-hdf X', out>inr(z) => H[\000Cz])) 
   fix((λmk-hdf.(inl m.<mk-hdf, F[m]>)))) fix((λmk-hdf.(inl a.let out ←─ G[F[a]]
                                                                    in <mk-hdf, out>)))))


Proof




Definitions occuring in Statement :  callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top so_apply: x[s] apply: a fix: fix(F) lambda: λx.A[x] spread: spread def pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inl: inl x sqequal: t
Lemmas :  less_than_transitivity1 less_than_irreflexivity int_seg_wf decidable__equal_int subtype_rel-int_seg false_wf le_weakening subtract_wf int_seg_properties le_wf decidable__lt decidable__le not-le-2 less-iff-le condition-implies-le add-associates minus-add minus-zero add-zero add-commutes add-swap minus-minus minus-one-mul zero-add add_functionality_wrt_le le-add-cancel-alt le-add-cancel2 add-mul-special zero-mul lelt_wf subtype_base_sq int_subtype_base not-equal-2 le-add-cancel nat_wf set_subtype_base base_wf all_wf sqequal_n_wf int_seg_subtype-nat set_wf less_than_wf primrec-wf2 sq_stable__le top_wf
\mforall{}[F,G,H:Top].
    (fix((\mlambda{}mk-hdf,s0.  case  s0
                                        of  inl(y)  =>
                                        inl  (\mlambda{}a.let  X',bs  =  y  a 
                                                        in  let  out  \mleftarrow{}{}  G[bs]
                                                              in  <mk-hdf  X',  out>)
                                        |  inr(z)  =>
                                        H[z])) 
      fix((\mlambda{}mk-hdf.(inl  (\mlambda{}m.<mk-hdf,  F[m]>))))  \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.let  out  \mleftarrow{}{}  G[F[a]]
                                                                                                                                        in  <mk-hdf,  out>)))))



Date html generated: 2015_07_17-AM-08_08_11
Last ObjectModification: 2015_01_27-PM-00_06_30

Home Index