Nuprl Lemma : rec-comb-locally-programmable

[Info:{Info:Type|

Info} ].

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

[n:

].

[A:

n

Type].

[Xs:k:

n

EClass(A k)].

[F:Id

k:

n

bag(A k)

bag(B)

bag(B)].

[init:Id

bag(B)].

[dfs:k:

n

Id

DataflowProgram(Info)].

[i:Id].

[es:EO+(Info)].

[e:E].
((rec-comb(Xs;F;init) 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 i;init i;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-comb: rec-comb(X;f;init), 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), bag: bag(T), upto: upto(n), valueall-type: valueall-type(T)
Definitions : so_lambda:

x y.t[x; y], ifthenelse: if b then t else f fi , bfalse: ff, false: False, implies: P

Q, and: P

Q, lelt: i

j < k, le: A

B, so_lambda:

x.t[x], so_apply: x[s], subtype: S

T, top: Top, prop:

, true: True, assert:

b, not:

A, member: t

T, all:

x:A. B[x], uimplies: b supposing a, int_seg: {i..j

}, squash:

T, uall:

[x:A]. B[x], ycomb: Y, guard: {T}, rec-comb: rec-comb(X;f;init), nat:

, ge: i

j , es-le-before:

loc(e), map: map(f;as), lt_int: i <z j, le_int: i

z j, btrue: tt, length: ||as||, select: l[i], bnot:

b, null: null(as), last: last(L), reduce: reduce(f;k;as), filter: filter(P;l), append: as @ bs, pi1: fst(t), so_apply: x[s1;s2], sq_type: SQType(T), local-program-at: local-program-at{i:l}(Info;A;X;dfp;x), exists:

x:A. B[x], strongwellfounded: SWellFounded(R[x; y]), eclass: EClass(A[eo; e])
Lemmas : bfalse_wf, valueall-type_wf, eclass_wf, dataflow-program_wf, event-ordering+_wf, local-program-at_wf, all_wf, equal_wf, false_wf, bool_subtype_base, subtype_base_sq, es-le-before-not-null, es-le_wf, es-le-before_wf2, null-map, null-data-stream, bag-subtype-list, bnot_wf, subtype_rel_self, df-program-type_wf, dataflow_subtype, df-program-meaning_wf, select-upto, length_wf, lelt_wf, length_upto, upto_wf, select-map, nat_wf, int_seg_wf, bool_wf, better-feedback-dataflow_wf, es-le-before_wf, es-info_wf, es-loc_wf, Id_wf, event-ordering+_inc, es-E_wf, map_wf, dataflow_wf, true_wf, data-stream_wf, bag_wf, top_wf, null_wf3, assert_wf, not_wf, squash_wf, last_wf, rec-comb_wf2, primed-class-opt_wf, es-causl_wf, less_than_wf, le_wf, es-causl-swellfnd, nat_properties, ge_wf, and_wf, es-before_wf, es-locl_wf, es-before_wf3, map_append_sq, data-stream-cons, data-stream-append, subtype_rel_list, last_append, dataflow-out_wf, ifthenelse_wf, dataflow-ap_wf, pi1_wf_top

\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:Id {}\mrightarrow{} k:\mBbbN{}n {}\mrightarrow{} bag(A k) {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(B)]. \mforall{}[init:Id {}\mrightarrow{} bag(B)]. \mforall{}[dfs:k:\mBbbN{}n {}\mrightarrow{} Id {}\mrightarrow{} DataflowProgram(Info)]. \mforall{}[i:Id]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. ((rec-comb(Xs;F;init) 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 i;init i;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_04 Last ObjectModification: 2012_01_06-AM-10_23_14 Home Index