Nuprl Lemma : hdf-parallel-transformation2-2

[L1,L2,G1,G2,S1,S2,init1,init2:Top]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf,s. (inl a.cbva_seq(L1[s;a]; λg.<mk-hdf S1[g;s], G1[g]>m1))))) init1
   || fix((λmk-hdf,s. (inl a.cbva_seq(L2[s;a]; λg.<mk-hdf S2[g;s], G2[g]>m2))))) init2 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[fst(s);a] n
                                         if n <m1 m2 then mk_lambdas(L2[snd(s);a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[g1] G2[g2]);m2);m1)
                                         fi ; λg.<mk-hdf 
                                                  <S1[partial_ap_gen(g;(m1 m2) 1;0;m1);fst(s)]
                                                  S2[partial_ap_gen(g;(m1 m2) 1;m1;m2);snd(s)]
                                                  >
                                                 select_fun_last(g;m1 m2)
                                                 >(m1 m2) 1))))) 
    <init1, init2>)


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[s1;s2] so_apply: x[s] pi1: fst(t) pi2: snd(t) 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) partial_ap_gen: partial_ap_gen(g;n;s;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_apply: x[s1;s2] so_apply: x[s] bag-append: as bs lt_int: i <j ifthenelse: if then else fi  hdf-parallel: || Y bfalse: ff btrue: tt hdf-halted: hdf-halted(P) band: p ∧b q hdf-ap: X(a) mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) empty-bag: {} hdf-run: hdf-run(P) hdf-halt: hdf-halt() isr: isr(x) so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2x.t[x] top: Top uimplies: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: guard: {T} or: P ∨ Q squash: T so_lambda: λ2y.t[x; y] append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] nat: false: False ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A fun_exp: f^n primrec: primrec(n;b;c) cbva_seq: cbva_seq(L; F; m) callbyvalueall_seq: callbyvalueall_seq(L;G;F;n;m) le_int: i ≤j bnot: ¬bb pi1: fst(t) mk_lambdas: mk_lambdas(F;m) pi2: snd(t) subtract: m mk_lambdas_fun: mk_lambdas_fun(F;m) mk_lambdas-fun: mk_lambdas-fun(F;G;n;m) list_ind: list_ind cons: [a b] partial_ap_gen: partial_ap_gen(g;n;s;m) select_fun_last: select_fun_last(g;m) select_fun_ap: select_fun_ap(g;n;m) decidable: Dec(P) exposed-bfalse: exposed-bfalse bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) sq_type: SQType(T) assert: b compose: g nil: [] nequal: a ≠ b ∈  eq_int: (i =z j) subtype_rel: A ⊆B

Latex:
\mforall{}[L1,L2,G1,G2,S1,S2,init1,init2:Top].  \mforall{}[m1,m2:\mBbbN{}].
    (fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L1[s;a];  \mlambda{}g.<mk-hdf  S1[g;s],  G1[g]>  m1)))))  init1
      ||  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L2[s;a];  \mlambda{}g.<mk-hdf  S2[g;s],  G2[g]>  m2)))))  init2 
    \msim{}  fix((\mlambda{}mk-hdf,s.
                                      (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n  <z  m1  then  L1[fst(s);a]  n
                                                                                if  n  <z  m1  +  m2  then  mk\_lambdas(L2[snd(s);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 
                                                                                                  <S1[partial\_ap\_gen(g;(m1  +  m2)  +  1;0;m1);fst(s)]
                                                                                                  ,  S2[partial\_ap\_gen(g;(m1  +  m2)  +  1;m1;m2);snd(s)]
                                                                                                  >
                                                                                                ,  select\_fun\_last(g;m1  +  m2)
                                                                                                >  (m1  +  m2)  +  1))))) 
        <init1,  init2>)



Date html generated: 2016_05_16-AM-10_47_17
Last ObjectModification: 2016_01_17-AM-11_11_28

Theory : halting!dataflow


Home Index