Nuprl Lemma : hdf-parallel-transformation1-2-0

[L1,L2,G1,G2:Base]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1))))) || fix((λmk-hdf.(inl a.cbva_seq(L2[a]; λg.<mk-hdf
                                                                                                                 G2[g]
                                                                                                                 >;
                                                                                                       m2))))) 
  fix((λmk-hdf.(inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                      if n <m1 m2 then mk_lambdas(L2[a] (n m1);m1)
                                      else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[g1] G2[g2]);m2);m1)
                                      fi ; λg.<mk-hdf, select_fun_last(g;m1 m2)>(m1 m2) 1))))))


Proof




Definitions occuring in Statement :  hdf-parallel: || Y nat: ifthenelse: if then else fi  lt_int: i <j uall: [x:A]. B[x] so_apply: x[s] apply: a fix: fix(F) lambda: λx.A[x] pair: <a, b> inl: inl x subtract: m add: m natural_number: $n base: Base sqequal: t bag-append: as bs select_fun_last: select_fun_last(g;m) mk_lambdas: mk_lambdas(F;m) mk_lambdas_fun: mk_lambdas_fun(F;m) cbva_seq: cbva_seq(L; F; m)
Lemmas :  lifting-strict-spread top_wf has-value_wf_base base_wf base_sq pair-eta lifting-strict-decide decide_bfalse_lemma empty_bag_append_lemma strict4-spread lifting-strict-callbyvalueall 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 lifting-strict-less cbva_seq-spread cbva_seq_extend cbva_seq-combine decidable__le not-le-2 sq_stable__le condition-implies-le minus-add minus-one-mul zero-add add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel lifting-strict-int_eq decidable__lt general_add_assoc cbva_seq-list-case2 cbva_seq-sqequal-n set_subtype_base int_subtype_base less-iff-le minus-zero minus-minus le-add-cancel2 add-mul-special zero-mul le-add-cancel-alt lelt_wf select_fun_last_partial_ap_gen1 subtype_base_sq not-equal-2 nat_wf all_wf sqequal_n_wf int_seg_subtype-nat set_wf less_than_wf primrec-wf2
\mforall{}[L1,L2,G1,G2:Base].  \mforall{}[m1,m2:\mBbbN{}].
    (fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L1[a];  \mlambda{}g.<mk-hdf,  G1[g]>  m1)))))
      ||  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L2[a];  \mlambda{}g.<mk-hdf,  G2[g]>  m2))))) 
    \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n  <z  m1  then  L1[a]  n
                                                                            if  n  <z  m1  +  m2  then  mk\_lambdas(L2[a]  (n  -  m1);m1)
                                                                            else  mk\_lambdas\_fun(\mlambda{}g1.mk\_lambdas\_fun(\mlambda{}g2.(G1[g1]
                                                                                                                                                                  +  G2[g2]);m2);m1)
                                                                            fi  ;  \mlambda{}g.<mk-hdf,  select\_fun\_last(g;m1  +  m2)>  (m1  +  m2)
                                                                      +  1))))))



Date html generated: 2015_07_17-AM-08_09_17
Last ObjectModification: 2015_04_23-PM-10_57_32

Home Index