Nuprl Lemma : feedback-df-prog2-meaning
[A:
']. [dfp1,dfp2:DataflowProgram(A)]. [B:{B:Type| valueall-type(B)} ]. [G:bag(df-program-type(dfp1))
bag(df-program-type(dfp2))
bag(B)
bag(B)]. [P:bag(B) 
].
[buf:bag(B)].
better-feedback-dataflow(2;
k.[df-program-meaning(dfp1); df-program-meaning(dfp2)][k];g,x.G[g 0;g 1;x];buf;s.P[s])
= df-program-meaning(feedback-df-prog2(B;G;P;buf;dfp1;dfp2))
supposing buf:bag(B). ((G {} {} buf) = {})
Proof not projected
Definitions occuring in Statement :
feedback-df-prog2: feedback-df-prog2(B;G;P;buf;dfp1;dfp2),
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
dataflow: dataflow(A;B),
select: l[i],
bool: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s1;s2;s3],
so_apply: x[s],
all: x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
cons: [car / cdr],
nil: [],
natural_number: $n,
universe: Type,
equal: s = t,
empty-bag: {},
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
uall: [x:A]. B[x],
df-program-type: df-program-type(dfp),
uimplies: b supposing a,
df-program-meaning: df-program-meaning(dfp),
so_apply: x[s1;s2;s3],
so_apply: x[s],
feedback-df-prog2: feedback-df-prog2(B;G;P;buf;dfp1;dfp2),
member: t 
T,
pi1: fst(t),
spreadn: spread4,
squash: 
T,
true: True,
so_lambda: 
x.t[x],
unit: Unit,
all: x:A. B[x],
spreadn: spread3,
so_lambda: x y.t[x; y],
prop: 
,
implies: P 
Q,
and: P 
Q,
top: Top,
subtype: S 
T,
bag: bag(T),
assert: 
b,
isl: isl(x),
pi2: snd(t),
let: let,
ifthenelse: if b then t else f fi ,
band: p 
q,
bnot: 
b,
outl: outl(x),
btrue: tt,
bfalse: ff,
outr: outr(x),
dataflow-program: DataflowProgram(A),
so_apply: x[s1;s2],
sq_stable: SqStable(P),
not: A,
false: False,
guard: {T}
Lemmas :
feedback-2-equiv,
bag_wf,
unit_wf2,
empty-bag_wf,
equal_wf,
squash_wf,
true_wf,
dataflow_wf,
all_wf,
bool_wf,
valueall-type_wf,
df-program-type_wf,
dataflow-program_wf,
rec-dataflow_wf,
evalall-equal,
let_wf,
ifthenelse_wf,
band_wf,
bnot_wf,
isl_wf,
it_wf,
product-valueall-type,
union-valueall-type,
sq_stable__valueall-type,
equal-valueall-type,
bag-valueall-type,
rec-dataflow-equal,
and_wf,
not_wf,
assert_wf,
pi1_wf_top,
pi2_wf,
outl_wf,
permutation_wf,
bag_qinc,
outr_wf,
false_wf
\mforall{}[A:\mBbbU{}']. \mforall{}[dfp1,dfp2:DataflowProgram(A)]. \mforall{}[B:\{B:Type| valueall-type(B)\} ].
\mforall{}[G:bag(df-program-type(dfp1)) {}\mrightarrow{} bag(df-program-type(dfp2)) {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(B)]. \mforall{}[P:bag(B) {}\mrightarrow{} \mBbbB{}].
\mforall{}[buf:bag(B)].
better-feedback-dataflow(2;\mlambda{}k.[df-program-meaning(dfp1); df-program-meaning(dfp2)][k];
\mlambda{}g,x.G[g 0;g 1;x];buf;s.P[s])
= df-program-meaning(feedback-df-prog2(B;G;P;buf;dfp1;dfp2))
supposing \mforall{}buf:bag(B). ((G \{\} \{\} buf) = \{\})
Date html generated:
2012_01_23-PM-12_00_22
Last ObjectModification:
2011_12_28-PM-02_48_16
Home
Index