Nuprl Lemma : std-components-property

[M:Type

Type]

n2m:

pMsg(P.M[P]).

l2m:Id

pMsg(P.M[P]).

Cs:component(P.M[P]) List.
assuming(env,r.reliable-env(env; r))
<Cs, lg-nil()> |= es.

cause:E

(E?)
(

C

Cs.

e:E
let G = last(data-stream(snd(C);map(

e.info(e);

loc(e)))) in

p

G.let y,c = p
in (com-kind(c)

``msg choose new``)

(

e':E
((loc(e') = y)

(e < e')

(

n:

.

nm:Id. (info(e') = command-to-msg(c;n2m n;l2m nm)))

((cause e') = (inl e ))))
supposing loc(e) = (fst(C)))
supposing Continuous+(P.M[P])

Proof not projected

Definitions occuring in Statement : system-strongly-realizes: system-strongly-realizes, command-to-msg: command-to-msg(c;nmsg;lmsg), reliable-env: reliable-env(env; r), component: component(P.M[P]), com-kind: com-kind(c), pMsg: pMsg(P.M[P]), lg-all:

x

G.P[x], lg-nil: lg-nil(), es-info: info(e), es-le-before:

loc(e), es-causl: (e < e'), es-loc: loc(e), es-E: E, data-stream: data-stream(P;L), Id: Id, strong-type-continuous: Continuous+(T.F[T]), map: map(f;as), nat:

, let: let, uimplies: b supposing a, uall:

[x:A]. B[x], so_apply: x[s], pi1: fst(t), pi2: snd(t), all:

x:A. B[x], exists:

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

Q, and: P

Q, unit: Unit, apply: f a, lambda:

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

B[x], spread: spread def, pair: <a, b>, inl: inl x , union: left + right, cons: [car / cdr], nil: [], list: type List, token: "$token", atom: Atom, universe: Type, equal: s = t, l_all: (

x

L.P[x]), last: last(L), l_member: (x

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

T, stdEO: stdEO(n2m;l2m;env;S), runEO: runEO(n2m;l2m;env;S), prop:

, cand: A c

B, true: True, bfalse: ff, eq_atom: x =a y, ifthenelse: if b then t else f fi , assert:

b, btrue: tt, mk-eo: mk-eo(E;dom;l;R;a;b;c;d;e;f), run-eo: EO(r), system-realizes: system-realizes, so_lambda:

x.t[x], ext-eq: A

B, member: t

T, System: System(P.M[P]), and: P

Q, implies: P

Q, es-le-before:

loc(e), let: let, es-loc: loc(e), es-E: E, exists:

x:A. B[x], system-strongly-realizes: system-strongly-realizes, all:

x:A. B[x], so_apply: x[s], strong-type-continuous: Continuous+(T.F[T]), uimplies: b supposing a, uall:

[x:A]. B[x], l_all: (

x

L.P[x]), lt_int: i <z j, bnot:

b, le_int: i

z j, length: ||as||, select: l[i], null: null(as), not:

A, ycomb: Y, top: Top, last: last(L), pi2: snd(t), map: map(f;as), es-causl: (e < e'), es-info: info(e), dataflow-ap: df(a), run-event-msg: run-event-msg(r;e), es-before: before(e), squash:

T, InitialSystem: InitialSystem(P.M[P]), component: component(P.M[P]), false: False, uiff: uiff(P;Q), bool:

, unit: Unit, l_contains: A

B, Process-stream: Process-stream(P;msgs), iterate-Process: iterate-Process(P;msgs), it:

Lemmas : strong-type-continuous_wf, pMsg_wf, Id_wf, component_wf, InitialSystem_wf, sub-system_wf, pEnvType_wf, reliable-env_wf, unit_wf2, run-cause_wf, run-event-loc_wf, true_wf, runEvents_wf, reliable-env-property2, pRun_wf2, pInTransit_wf, lg-nil_wf_dag, nat_wf, pRun-invariant2, l_member_wf, pi1_wf_top, es-loc_wf, equal_wf, false_wf, pExt_wf, es-info_wf, Process-stream_wf, last_append, data-stream-cons, es-before_wf, map_wf, data-stream-append, es-locl_wf, es-E_wf, top_wf, event-ordering+_wf, event-ordering+_inc, stdEO_wf, es-before_wf3, map_append_sq, pRun_wf, run-event-state-when_wf, Process_wf, iterate-Process_wf, assert_of_bnot, eqff_to_assert, not_wf, bnot_wf, assert_wf, uiff_transitivity, eqtt_to_assert, bool_wf, es-first_wf, run-event-state_wf, squash_wf, es-le-before_wf, es-pred_wf, es-init-elim2

\mforall{}[M:Type {}\mrightarrow{} Type] \mforall{}n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P]). \mforall{}l2m:Id {}\mrightarrow{} pMsg(P.M[P]). \mforall{}Cs:component(P.M[P]) List. assuming(env,r.reliable-env(env; r)) <Cs, lg-nil()> |= es.\mexists{}cause:E {}\mrightarrow{} (E?) (\mforall{}C\mmember{}Cs.\mforall{}e:E let G = last(data-stream(snd(C);map(\mlambda{}e.info(e);\mleq{}loc(e)))) in \mforall{}p\mmember{}G.let y,c = p in (com-kind(c) \mmember{} ``msg choose new``) {}\mRightarrow{} (\mexists{}e':E ((loc(e') = y) \mwedge{} (e < e') \mwedge{} (\mexists{}n:\mBbbN{} \mexists{}nm:Id (info(e') = command-to-msg(c;n2m n;l2m nm))) \mwedge{} ((cause e') = (inl e )))) supposing loc(e) = (fst(C))) supposing Continuous+(P.M[P]) Date html generated: 2012_01_23-PM-12_45_36 Last ObjectModification: 2011_12_14-PM-11_32_14 Home Index