Nuprl Lemma : hdf-compose2-transformation1-2-2

[L1,L2,G1,G2,init,S:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1)))))
   (fix((λmk-hdf,s. (inl a.cbva_seq(L2[s;a]; λg.<mk-hdf S[g;s], G2[g]>m2))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                         if n <m1 m2 then mk_lambdas(L2[s;a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.⋃f∈G1[g1].⋃b∈G2[g2].f b;m2);m1)
                                         fi ; λg.<mk-hdf S[partial_ap_gen(g;(m1 m2) 1;m1;m2);s]
                                                 select_fun_last(g;m1 m2)
                                                 >(m1 m2) 1))))) 
    init)


Proof




Definitions occuring in Statement :  hdf-compose2: Y nat_plus: + ifthenelse: if then else fi  lt_int: i <j uall: [x:A]. B[x] so_apply: x[s1;s2] 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-combine: x∈bs.f[x] 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 lt_int: i <j ifthenelse: if then else fi  hdf-compose2: Y bfalse: ff btrue: tt hdf-halted: hdf-halted(P) bor: p ∨bq 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] 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: subtract: m nat_plus: + ge: i ≥  eq_int: (i =z j) sq_type: SQType(T)

Latex:
\mforall{}[L1,L2,G1,G2,init,S:Base].  \mforall{}[m1,m2:\mBbbN{}\msupplus{}].
    (fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L1[a];  \mlambda{}g.<mk-hdf,  G1[g]>  m1)))))
      o  (fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L2[s;a];  \mlambda{}g.<mk-hdf  S[g;s],  G2[g]>  m2)))))  init) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n  <z  m1  then  L1[a]  n
                                                                                  if  n  <z  m1  +  m2  then  mk\_lambdas(L2[s;a]  (n  -  m1);m1)
                                                                                  else  mk\_lambdas\_fun(\mlambda{}g1.mk\_lambdas\_fun(\mlambda{}g2.\mcup{}f\mmember{}G1[g1].
                                                                                                                                                                        \mcup{}b\mmember{}G2[g2].
                                                                                                                                                                        f  b;m2);m1)
                                                                                  fi  ;  \mlambda{}g.<mk-hdf  S[partial\_ap\_gen(g;(m1  +  m2)  +  1;m1;m2);s]
                                                                                                  ,  select\_fun\_last(g;m1  +  m2)
                                                                                                  >  (m1  +  m2)  +  1))))) 
        init)



Date html generated: 2016_05_16-AM-10_47_44
Last ObjectModification: 2016_01_17-AM-11_08_53

Theory : halting!dataflow


Home Index