Nuprl Lemma : iterate-feedback-dataflow

{

[A,C:Type].

[n:

].

[B:

n

Type].

[P:C

].

[F:k:

n

B[k]

C

C].

[L:A List].

[ds:k:

n

dataflow(A;B[k])].

[s:C].
    (feedback-dataflow(ds;
                       F;s;x.P[x])*(L)
    ~ feedback-dataflow(if null(L) then ds else

k.ds k*(L) fi ;
                        F;
                        let L' = ... in
                            if null(L') then s else last(L') fi ;x.P[x])) }

{ Proof }

Definitions occuring in Statement : feedback-dataflow: feedback-dataflow, data-stream: data-stream(P;L), iterate-dataflow: P*(inputs), dataflow: dataflow(A;B), null: null(as), 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], list: type List, natural_number: $n, universe: Type, sqequal: s ~ t, filter: filter(P;l), last: last(L)
Definitions : member: t

T, uall:

[x:A]. B[x], so_apply: x[s], nat:

Lemmas : dataflow_wf, int_seg_wf

\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[P:C {}\mrightarrow{} \mBbbB{}]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C {}\mrightarrow{} C]. \mforall{}[L:A List]. \mforall{}[ds:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])]. \mforall{}[s:C]. (feedback-dataflow(ds; F;s;x.P[x])*(L) \msim{} feedback-dataflow(if null(L) then ds else \mlambda{}k.ds k*(L) fi ; F;let L' = filter(\mlambda{}x.P[x];data-stream(feedback-dataflow(ds; F;s;x.P[x]);L)) in if null(L') then s else last(L') fi ;x.P[x])) Date html generated: 2011_08_10-AM-08_18_34 Last ObjectModification: 2011_06_18-AM-08_31_42 Home Index