Nuprl Lemma : rec-combined-class-locally-programmable

[Info:{Info:Type|

Info} ].

[B:{B:Type| valueall-type(B)} ].

[n:

].

[A:

n

Type].

[Xs:k:

n

EClass(A k)].

[F:k:

n

bag(A k)

bag(B)

bag(B)].

[dfs:k:

n

Id

DataflowProgram(Info)].

[i:Id].

[es:EO+(Info)].

[e:E].
((F|Xs,(self)'| es e)
= last(data-stream(better-feedback-dataflow(||map(

k.(dfs k i);upto(n))||;

k.map(

dfp.df-program-meaning(dfp);map(

k.(dfs k i);upto(n)))[k];
F;{};b.

null(b));map(

e.info(e);

loc(e))))) supposing
((loc(e) = i) and
(

k:

n.

i:Id. local-program-at{i:l}(Info;A k;Xs k;dfs k i;i)))

Proof not projected

Definitions occuring in Statement : local-program-at: local-program-at{i:l}(Info;A;X;dfp;x), rec-combined-class: f|X,(self)'|, eclass: EClass(A[eo; e]), es-info: info(e), event-ordering+: EO+(Info), es-le-before:

loc(e), es-loc: loc(e), es-E: E, df-program-meaning: df-program-meaning(dfp), dataflow-program: DataflowProgram(A), better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]), data-stream: data-stream(P;L), Id: Id, select: l[i], map: map(f;as), length: ||as||, null: null(as), bnot:

b, int_seg: {i..j

}, nat:

, uimplies: b supposing a, uall:

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

x:A. B[x], squash:

T, set: {x:A| B[x]} , apply: f a, lambda:

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

B[x], natural_number: $n, universe: Type, equal: s = t, last: last(L), empty-bag: {}, bag: bag(T), upto: upto(n), valueall-type: valueall-type(T)
Definitions : so_lambda:

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

x.t[x], true: True, prop:

, member: t

T, uimplies: b supposing a, squash:

T, uall:

[x:A]. B[x], primed-class: Prior(X), primed-class-opt: Prior(X)?b, rec-combined-class: f|X,(self)'|, rec-comb: rec-comb(X;f;init), so_apply: x[s1;s2], so_apply: x[s], all:

x:A. B[x], nat:

, subtype: S

T, eclass: EClass(A[eo; e])
Lemmas : valueall-type_wf, nat_wf, eclass_wf, dataflow-program_wf, event-ordering+_wf, es-E_wf, local-program-at_wf, int_seg_wf, all_wf, event-ordering+_inc, es-loc_wf, Id_wf, bag_wf, true_wf, squash_wf, equal_wf, empty-bag_wf, rec-comb-locally-programmable, rec-combined-class_wf

\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]. \mforall{}[B:\{B:Type| valueall-type(B)\} ]. \mforall{}[n:\mBbbN{}]. \mforall{}[A:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[Xs:k:\mBbbN{}n {}\mrightarrow{} EClass(A k)]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} bag(A k) {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(B)]. \mforall{}[dfs:k:\mBbbN{}n {}\mrightarrow{} Id {}\mrightarrow{} DataflowProgram(Info)]. \mforall{}[i:Id]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. ((F|Xs,(self)'| es e) = last(data-stream(better-feedback-dataflow(||map(\mlambda{}k.(dfs k i);upto(n))||; \mlambda{}k.map(\mlambda{}dfp.df-program-meaning(dfp);map(\mlambda{}k.(dfs k i);upto(n)))[k]; F;\{\};b.\mneg{}\msubb{}null(b));map(\mlambda{}e.info(e);\mleq{}loc(e))))) supposing ((loc(e) = i) and (\mforall{}k:\mBbbN{}n. \mforall{}i:Id. local-program-at\{i:l\}(Info;A k;Xs k;dfs k i;i))) Date html generated: 2012_01_23-PM-12_31_17 Last ObjectModification: 2011_12_14-PM-10_27_09 Home Index