Nuprl Lemma : feedback-dataflow-equiv

[A,C:Type]. [n:]. [B:n  Type]. [ds:k:n  dataflow(A;B[k])]. [F:k:n  B[k]  C  C]. [s:C]. [P:C  ].
  feedback-dataflow(ds;
                    F;s;x.P[x])  rec-dataflow(<parallel-dataflow(ds;x.x), s>;s,a.let ds,buf = s 
                                                                                   in let ds',out = ds(a) 
                                                                                      in let x = F out buf in
                                                                                             <<ds'
                                                                                              , if P[x]
                                                                                                then x
                                                                                                else buf
                                                                                                fi 
                                                                                              >
                                                                                             , x
                                                                                             >)


Proof not projected



Definitions occuring in Statement :  dataflow-equiv: d1  d2,  feedback-dataflow: feedback-dataflow,  parallel-dataflow: parallel-dataflow,  dataflow-ap: df(a),  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  dataflow: dataflow(A;B),  ifthenelse: if b then t else f fi ,  bool: ,  int_seg: {i..j},  nat: ,  let: let,  uall: [x:A]. B[x],  so_apply: x[s],  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  spread: spread def,  pair: <a, b>,  natural_number: $n,  universe: Type
Definitions :  uall: [x:A]. B[x],  so_apply: x[s],  dataflow-equiv: d1  d2,  feedback-dataflow: feedback-dataflow,  member: t  T,  prop: ,  all: x:A. B[x],  implies: P  Q,  so_lambda: x y.t[x; y],  so_lambda: x.t[x],  top: Top,  subtype: S  T,  and: P  Q,  cand: A c B,  parallel-dataflow: parallel-dataflow,  pi2: snd(t),  let: let,  dataflow-ap: df(a),  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  ycomb: Y,  pi1: fst(t),  squash: T,  true: True,  nat: ,  uimplies: b supposing a,  so_apply: x[s1;s2]
Lemmas :  rec-dataflow-equiv,  int_seg_wf,  dataflow_wf,  let_wf,  pi1_wf_top,  dataflow-ap_wf,  ifthenelse_wf,  dataflow-out_wf,  parallel-dataflow_wf,  bool_wf,  nat_wf,  equal_wf,  pi2_wf,  and_wf,  squash_wf,  true_wf,  rec-dataflow_wf
\mforall{}[A,C:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[B:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[ds:k:\mBbbN{}n  {}\mrightarrow{}  dataflow(A;B[k])].  \mforall{}[F:k:\mBbbN{}n  {}\mrightarrow{}  B[k]  {}\mrightarrow{}  C  {}\mrightarrow{}  C].
\mforall{}[s:C].  \mforall{}[P:C  {}\mrightarrow{}  \mBbbB{}].
    feedback-dataflow(ds;
                                        F;s;x.P[x])  \mequiv{}  rec-dataflow(<parallel-dataflow(ds;\mlambda{}x.x),  s>
                                                                    s,a.let  ds,buf  =  s 
                                                                            in  let  ds',out  =  ds(a) 
                                                                                  in  let  x  =  F  out  buf  in
                                                                                                <<ds',  if  P[x]  then  x  else  buf  fi  >,  x>)


Date html generated: 2012_01_23-AM-11_57_57
Last ObjectModification: 2011_12_28-PM-12_34_26

Home Index