Nuprl Lemma : better-feedback-dataflow-recode

{

[A,C:Type].

[n:

].

[B:

n + 2

Type].

[ds:k:

n + 2

dataflow(A;bag(B[k]))].

[F:k:

n + 2

bag(B[k])

C

C].

[buf:C].

[P:C

].
(better-feedback-dataflow(n + 2;ds;F;buf;x.P[x])
= better-feedback-dataflow(n + 1;

k.if (k =

0)
                                        then better-parallel-dataflow(
                                             2;ds;

s.bag-merge(s 0;s 1))
else ds (k + 1)
fi ;

g.(F
(

k.if (k =

0)
                                                      then fst(bag-separate(g
                                                                            0))
                                                    if (k =

1)
                                                      then snd(bag-separate(g
                                                                            0))
                                                    else g (k - 1)
                                                    fi ));buf;x.P[x])) }

{ Proof }

Definitions occuring in Statement : better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]), better-parallel-dataflow: better-parallel-dataflow, dataflow: dataflow(A;B), eq_int: (i =

j), ifthenelse: if b then t else f fi , bool:

, int_seg: {i..j

}, nat:

, uall:

[x:A]. B[x], so_apply: x[s], pi1: fst(t), pi2: snd(t), apply: f a, lambda:

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

B[x], subtract: n - m, add: n + m, natural_number: $n, universe: Type, equal: s = t
Definitions : limited-type: LimitedType, prop:

, real:

, grp_car: |g|, subtype: S

T, so_lambda:

x.t[x], pair: <a, b>, fpf: a:A fp-> B[a], strong-subtype: strong-subtype(A;B), ge: i

j , less_than: a < b, uimplies: b supposing a, product: x:A

B[x], and: P

Q, uiff: uiff(P;Q), subtype_rel: A

r B, all:

x:A. B[x], implies: P

Q, false: False, not:

A, le: A

B, int:

, set: {x:A| B[x]} , axiom: Ax, better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]), bool:

, nat:

, universe: Type, bag: Error :bag, int_seg: {i..j

}, function: x:A

B[x], isect:

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

T, uall:

[x:A]. B[x], Auto: Error :Auto, CollapseTHEN: Error :CollapseTHEN, so_apply: x[s], natural_number: $n, subtract: n - m, apply: f a, bag-separate: Error :bag-separate, pi2: snd(t), eq_int: (i =

j), ifthenelse: if b then t else f fi , pi1: fst(t), lambda:

x.A[x], add: n + m, bag-merge: Error :bag-merge, better-parallel-dataflow: better-parallel-dataflow, feedback-dataflow: feedback-dataflow, dataflow: dataflow(A;B), equal: s = t, AssertBY: Error :AssertBY, tactic: Error :tactic, void: Void, rationals:

, fpf-dom: x

dom(f), corec: corec(T.F[T]), suptype: suptype(S; T), inr: inr x , inl: inl x , int_eq: if a=b then c else d, decide: case b of inl(x) => s[x] | inr(y) => t[y], intensional-universe: IType, true: True, squash:

T, deq: EqDecider(T), ma-state: State(ds), fpf-cap: f(x)?z, minus: -n, refl: Refl(T;x,y.E[x; y]), sym: Sym(T;x,y.E[x; y]), trans: Trans(T;x,y.E[x; y]), equiv_rel: EquivRel(T;x,y.E[x; y]), so_lambda:

x y.t[x; y], filter: filter(P;l), permutation: permutation(T;L1;L2), quotient: x,y:A//B[x; y], sq_type: SQType(T), IdLnk: IdLnk, Id: Id, append: as @ bs, locl: locl(a), Knd: Knd, list: type List, lt_int: i <z j, le_int: i

z j, bfalse: ff, btrue: tt, eq_atom: x =a y, null: null(as), set_blt: a <

b, grp_blt: a <

b, infix_ap: x f y, dcdr-to-bool: [d]

, bl-all: (

x

L.P[x])_b, bl-exists: (

x

L.P[x])_b, b-exists: (

i<n.P[i])_b, eq_type: eq_type(T;T'), eq_atom: eq_atom$n(x;y), qeq: qeq(r;s), q_less: q_less(r;s), q_le: q_le(r;s), deq-member: deq-member(eq;x;L), deq-disjoint: deq-disjoint(eq;as;bs), deq-all-disjoint: deq-all-disjoint(eq;ass;bs), name_eq: name_eq(x;y), eq_id: a = b, eq_lnk: a = b, bimplies: p

q, band: p

q, bor: p

q, bnot:

b, unit: Unit, sq_stable: SqStable(P), or: P

Q, guard: {T}, l_member: (x

l), assert:

b, top: Top, p-outcome: Outcome, lelt: i

j < k, sqequal: s ~ t, MaAuto: Error :MaAuto, Complete: Error :Complete, Try: Error :Try, union: left + right
Lemmas : Error :bag-separate_wf, pi2_wf, bool_subtype_base, nat_properties, int_seg_properties, eq_int_wf, ifthenelse_wf, pi1_wf_top, top_wf, uiff_transitivity, eqtt_to_assert, assert_of_eq_int, assert_wf, eqff_to_assert, assert_of_bnot, not_functionality_wrt_uiff, bnot_wf, subtype_base_sq, int_subtype_base, permutation_wf, quotient_wf, equiv_rel_wf, trans_wf, sym_wf, refl_wf, subtype_rel_wf, true_wf, squash_wf, intensional-universe_wf, btrue_wf, bfalse_wf, unit_wf, better-parallel-dataflow_wf, Error :bag-merge_wf, eq_int_eq_true, subtype_rel_self, better-feedback-dataflow-equal, not_wf, false_wf, member_wf, le_wf, bool_wf, nat_wf, feedback-dataflow-recode, int_seg_wf, better-feedback-dataflow_wf, Error :bag_wf, feedback-dataflow_wf, dataflow_wf

\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n + 2 {}\mrightarrow{} Type]. \mforall{}[ds:k:\mBbbN{}n + 2 {}\mrightarrow{} dataflow(A;bag(B[k]))]. \mforall{}[F:k:\mBbbN{}n + 2 {}\mrightarrow{} bag(B[k]) {}\mrightarrow{} C {}\mrightarrow{} C]. \mforall{}[buf:C]. \mforall{}[P:C {}\mrightarrow{} \mBbbB{}]. (better-feedback-dataflow(n + 2;ds;F;buf;x.P[x]) = better-feedback-dataflow(n + 1;\mlambda{}k.if (k =\msubz{} 0) then better-parallel-dataflow( 2;ds; \mlambda{}s.bag-merge(s 0;s 1)) else ds (k + 1) fi ;\mlambda{}g.(F (\mlambda{}k.if (k =\msubz{} 0) then fst(bag-separate(g 0)) if (k =\msubz{} 1) then snd(bag-separate(g 0)) else g (k - 1) fi ));buf;x.P[x])) Date html generated: 2011_08_10-AM-08_24_10 Last ObjectModification: 2011_06_18-AM-08_33_02 Home Index