Nuprl Lemma : parallel-2-equiv

[A,B,C,D,S1,S2:Type].

[F1:S1

A

(S1

C)].

[F2:S2

A

(S2

D)].

[G:C

D

B].

[s1:S1].

[s2:S2].
(better-parallel-dataflow(
2;

k.[rec-dataflow(s1;s,a.F1[s;a]); rec-dataflow(s2;s,a.F2[s;a])][k];

g.G[g 0;g 1])
  = rec-dataflow(<s1, s2>;s,a.let s1,s2 = s
                              in let s1',out1 = F1[s1;a]
                                 in let s2',out2 = F2[s2;a]
                                    in <<s1', s2'>, G[out1;out2]>))

Proof not projected

Definitions occuring in Statement : better-parallel-dataflow: better-parallel-dataflow, rec-dataflow: rec-dataflow(s0;s,m.next[s; m]), dataflow: dataflow(A;B), select: l[i], uall:

[x:A]. B[x], so_apply: x[s1;s2], apply: f a, lambda:

x.A[x], function: x:A

B[x], spread: spread def, pair: <a, b>, product: x:A

B[x], cons: [car / cdr], nil: [], natural_number: $n, universe: Type, equal: s = t
Definitions : suptype: suptype(S; T), subtype: S

T, top: Top, so_lambda:

x y.t[x; y], all:

x:A. B[x], member: t

T, so_apply: x[s1;s2], uall:

[x:A]. B[x], btrue: tt, bfalse: ff, lt_int: i <z j, bnot:

b, le_int: i

z j, ifthenelse: if b then t else f fi , ycomb: Y, label: ...$L... t, ge: i

j , and: P

Q, lelt: i

j < k, length: ||as||, so_lambda:

x.t[x], false: False, implies: P

Q, not:

A, le: A

B, int_seg: {i..j

}, nat:

, select: l[i], uimplies: b supposing a, guard: {T}, sq_type: SQType(T), or: P

Q, decidable: Dec(P), prop:

, so_apply: x[s]
Lemmas : data-stream_wf, parallel-2-rec-dataflow, rec-dataflow_wf, dataflow-extensionality, lelt_wf, dataflow_wf, int_subtype_base, subtype_base_sq, decidable__equal_int, int_seg_wf, length_wf_nat, non_neg_length, length_cons, length_wf_nil, length_nil, length_wf, select_wf, le_wf, better-parallel-dataflow_wf

\mforall{}[A,B,C,D,S1,S2:Type]. \mforall{}[F1:S1 {}\mrightarrow{} A {}\mrightarrow{} (S1 \mtimes{} C)]. \mforall{}[F2:S2 {}\mrightarrow{} A {}\mrightarrow{} (S2 \mtimes{} D)]. \mforall{}[G:C {}\mrightarrow{} D {}\mrightarrow{} B]. \mforall{}[s1:S1]. \mforall{}[s2:S2]. (better-parallel-dataflow( 2;\mlambda{}k.[rec-dataflow(s1;s,a.F1[s;a]); rec-dataflow(s2;s,a.F2[s;a])][k]; \mlambda{}g.G[g 0;g 1]) = rec-dataflow(<s1, s2>s,a.let s1,s2 = s in let s1',out1 = F1[s1;a] in let s2',out2 = F2[s2;a] in <<s1', s2'>, G[out1;out2]>)) Date html generated: 2012_01_23-AM-11_57_34 Last ObjectModification: 2011_12_12-PM-06_57_05 Home Index