Nuprl Lemma : hdf-parallel-transformation2

[L,G,H,S,init,out:Base]. ∀[m:ℕ].
  (inl a.<inr Ax out>|| fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<case H[g;s]
                                                                             of inl() =>
                                                                             mk-hdf S[g;s]
                                                                             inr() =>
                                                                             inr Ax 
                              init fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z m)
                                                                          then case fst(s)
                                                                                of inl(x) =>
                                                                                mk_lambdas_fun(λg.(out G[g]);m)
                                                                                inr(x) =>
                                                                          else L[snd(s);a] n
                                                                          fi ; λg.<case H[partial_ap(g;m 1;m);snd(s)]
                                                                                    of inl() =>
                                                                                    <inr Ax 
                                                                                    S[partial_ap(g;m 1;m);snd(s)]
                                                                                    inr() =>
                                                                                    inr Ax 
                                     <inl Ax, init>)


Definitions occuring in Statement :  hdf-parallel: || Y nat: ifthenelse: if then else fi  eq_int: (i =z j) uall: [x:A]. B[x] 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> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x add: m natural_number: $n base: Base sqequal: t axiom: Ax bag-append: as bs select_fun_last: select_fun_last(g;m) partial_ap: partial_ap(g;n;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 eq_int: (i =z 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) 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 so_apply: x[s] 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] so_apply: x[s1;s2] empty-bag: {} nil: [] it: pi1: fst(t) pi2: snd(t) select_fun_last: select_fun_last(g;m) int_seg: {i..j-} lelt: i ≤ j < k satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A decidable: Dec(P) subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) nat: ge: i ≥  sq_type: SQType(T)

\mforall{}[L,G,H,S,init,out:Base].  \mforall{}[m:\mBbbN{}].
    (inl  (\mlambda{}a.<inr  Ax  ,  out>)  ||  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<case  H[g;s]
                                                                                                                                                          of  inl()  =>
                                                                                                                                                          mk-hdf  S[g;s]
                                                                                                                                                          |  inr()  =>
                                                                                                                                                          inr  Ax 
                                                                                                                                                      ,  G[g]
                                                                                                                                                      >  m))))) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                                  then  case  fst(s)
                                                                                              of  inl(x)  =>
                                                                                              mk\_lambdas\_fun(\mlambda{}g.(out  +  G[g]);m)
                                                                                              |  inr(x)  =>
                                                                                  else  L[snd(s);a]  n
                                                                                  fi  ;  \mlambda{}g.<case  H[partial\_ap(g;m  +  1;m);snd(s)]
                                                                                                      of  inl()  =>
                                                                                                      mk-hdf  <inr  Ax  ,  S[partial\_ap(g;m  +  1;m);snd(s)]>
                                                                                                      |  inr()  =>
                                                                                                      inr  Ax 
                                                                                                  ,  select\_fun\_last(g;m)
                                                                                                  >  m  +  1))))) 
        <inl  Ax,  init>)

Date html generated: 2016_05_16-AM-10_47_01
Last ObjectModification: 2016_01_17-AM-11_11_10

Theory : halting!dataflow

Home Index