Nuprl Lemma : parallel-dataflow

{

[A,C:Type].

[n:

].

[B:

n

Type].

[F:k:

n

B[k]

C].

[ds1,ds2:k:

n

dataflow(A;B[k])].
    parallel-dataflow(
    ds1;
    F)

parallel-dataflow(
         ds2;
         F)
    supposing

k:

n. ds1 k

ds2 k }

{ Proof }

Definitions occuring in Statement : dataflow-equiv: d1

d2, parallel-dataflow: parallel-dataflow, dataflow: dataflow(A;B), int_seg: {i..j

}, nat:

, uimplies: b supposing a, uall:

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

x:A. B[x], apply: f a, function: x:A

B[x], natural_number: $n, universe: Type
Definitions : uall:

[x:A]. B[x], so_apply: x[s], uimplies: b supposing a, all:

x:A. B[x], dataflow-equiv: d1

d2, member: t

T, prop:

, le: A

B, top: Top, subtype: S

T, squash:

T, true: True, and: P

Q, not:

A, implies: P

Q, false: False, nat:

, int_seg: {i..j

}, lelt: i

j < k, guard: {T}
Lemmas : int_seg_wf, dataflow-equiv_wf, dataflow_wf, nat_wf, top_wf, map_wf, squash_wf, true_wf, length_wf1, upto_wf, select_wf, le_wf, length-data-stream, parallel-data-stream

\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C]. \mforall{}[ds1,ds2:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])]. parallel-dataflow(ds1;F) \mequiv{} parallel-dataflow(ds2;F) supposing \mforall{}k:\mBbbN{}n. ds1 k \mequiv{} ds2 k Date html generated: 2011_08_10-AM-08_22_21 Last ObjectModification: 2011_06_18-AM-08_32_39 Home Index