### 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 <z m1 then L1[a] n`
`                                      if n <z 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: `X || Y` nat: `ℕ` ifthenelse: `if b then t else f fi ` lt_int: `i <z j` uall: `∀[x:A]. B[x]` so_apply: `x[s]` apply: `f a` fix: `fix(F)` lambda: `λx.A[x]` pair: `<a, b>` inl: `inl x` subtract: `n - m` add: `n + m` natural_number: `\$n` base: `Base` sqequal: `s ~ 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)`
\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