Nuprl Lemma : feedback-2-equiv

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

[F1:S1

A

(S1

C)].

[F2:S2

A

(S2

D)].

[G:C

D

B

B].

[P:B

].

[s1:S1].

[s2:S2].

[buf:B].
(better-feedback-dataflow(2;

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

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

Proof not projected

Definitions occuring in Statement : better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]), rec-dataflow: rec-dataflow(s0;s,m.next[s; m]), dataflow: dataflow(A;B), select: l[i], ifthenelse: if b then t else f fi , bool:

, let: let, spreadn: spread3, uall:

[x:A]. B[x], so_apply: x[s1;s2;s3], so_apply: x[s1;s2], so_apply: x[s], 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 : btrue: tt, bfalse: ff, lt_int: i <z j, bnot:

b, le_int: i

z j, ycomb: Y, label: ...$L... t, ge: i

j , and: P

Q, lelt: i

j < k, length: ||as||, int_seg: {i..j

}, false: False, implies: P

Q, not:

A, le: A

B, nat:

, suptype: suptype(S; T), subtype: S

T, top: Top, so_lambda:

x.t[x], so_lambda:

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

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

T, ifthenelse: if b then t else f fi , spreadn: spread3, so_apply: x[s], so_apply: x[s1;s2;s3], so_apply: x[s1;s2], select: l[i], uall:

[x:A]. B[x], guard: {T}, sq_type: SQType(T), or: P

Q, decidable: Dec(P), prop:

, uimplies: b supposing a
Lemmas : better-feedback-dataflow_wf, 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, bool_wf, data-stream_wf, feedback-2-rec-dataflow, ifthenelse_wf, let_wf, rec-dataflow_wf, dataflow-extensionality

\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 {}\mrightarrow{} B]. \mforall{}[P:B {}\mrightarrow{} \mBbbB{}]. \mforall{}[s1:S1]. \mforall{}[s2:S2]. \mforall{}[buf:B]. (better-feedback-dataflow(2;\mlambda{}k.[rec-dataflow(s1;s,a.F1[s;a]); rec-dataflow(s2;s,a.F2[s;a])][k]; \mlambda{}g,x.G[g 0;g 1;x];buf;s.P[s]) = rec-dataflow(<s1, s2, buf>s,a.let s1,s2,buf = s in let s1',out1 = F1[s1;a] in let s2',out2 = F2[s2;a] in let x = G[out1;out2;buf] in <<s1', s2', if P[x] then x else buf fi >, x>)) Date html generated: 2012_01_23-AM-11_57_28 Last ObjectModification: 2011_12_17-PM-04_36_19 Home Index