Nuprl Lemma : hdf-parallel-transformation2-1

[L1,L2,G1,G2:Top]. ∀[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] top: Top 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 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)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] top: Top so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]

Latex:
\mforall{}[L1,L2,G1,G2:Top].  \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: 2016_05_16-AM-10_47_10
Last ObjectModification: 2015_12_28-PM-07_39_18

Theory : halting!dataflow


Home Index