Nuprl Lemma : feedback-dataflow-equal

[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 : 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, equal: s = t
Definitions : uall:

[x:A]. B[x], so_apply: x[s], 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-equal, 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]) = 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_21 Last ObjectModification: 2011_12_28-PM-12_21_27 Home Index