Nuprl Lemma : better-feedback-dataflow-equal

{

[A,C:Type].

[n:

].

[B:

n

Type].

[P:C

].

[F:k:

n

B[k]

C

C].

[ds:k:

n

dataflow(A;B[k])].

[s:C].
    (better-feedback-dataflow(n;ds;F;s;x.P[x])
    = feedback-dataflow(ds;
                        F;s;x.P[x])) }

{ Proof }

Definitions occuring in Statement : better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]), feedback-dataflow: feedback-dataflow, dataflow: dataflow(A;B), bool:

, int_seg: {i..j

}, nat:

, uall:

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

B[x], natural_number: $n, universe: Type, equal: s = t
Definitions : subtype: S

T, so_lambda:

x.t[x], top: Top, prop:

, member: t

T, all:

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

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

Lemmas : int_seg_wf, feedback-dataflow_wf, dataflow-ap_wf, dataflow_wf, pi1_wf_top, data-stream_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{}[ds:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])]. \mforall{}[s:C]. (better-feedback-dataflow(n;ds;F;s;x.P[x]) = feedback-dataflow(ds;F;s;x.P[x])) Date html generated: 2011_08_10-AM-08_19_35 Last ObjectModification: 2011_06_18-AM-08_32_00 Home Index