Nuprl Lemma : reliable-env-property2

[M:Type

Type]

S:InitialSystem(P.M[P]).

n2m:

pMsg(P.M[P]).

l2m:Id

pMsg(P.M[P]).

env:pEnvType(P.M[P]).
    let r = pRun(S;env;n2m;l2m) in
        reliable-env(env; r)

(

e:runEvents(r).

P:Process(P.M[P]).
((P

run-event-state-when(r;e))

p

snd((P (snd(run-info(r;e))))).let y,c = p
in (com-kind(c)

``msg choose new``)

(

e':runEvents(r)
((run-event-loc(e') = y)

(e run-lt(r) e')

(

n:

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

((run-cause(r) e') = (inl e ))))))
supposing Continuous+(P.M[P])

Proof not projected

Definitions occuring in Statement : command-to-msg: command-to-msg(c;nmsg;lmsg), reliable-env: reliable-env(env; r), InitialSystem: InitialSystem(P.M[P]), run-lt: run-lt(r), run-cause: run-cause(r), run-event-loc: run-event-loc(e), run-event-state-when: run-event-state-when(r;e), runEvents: runEvents(r), run-info: run-info(r;e), pRun: pRun(S0;env;nat2msg;loc2msg), pEnvType: pEnvType(T.M[T]), com-kind: com-kind(c), pMsg: pMsg(P.M[P]), Process: Process(P.M[P]), lg-all:

x

G.P[x], Id: Id, strong-type-continuous: Continuous+(T.F[T]), nat:

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

[x:A]. B[x], infix_ap: x f y, so_apply: x[s], pi2: snd(t), all:

x:A. B[x], exists:

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

Q, and: P

Q, unit: Unit, apply: f a, function: x:A

B[x], spread: spread def, inl: inl x , union: left + right, cons: [car / cdr], nil: [], token: "$token", atom: Atom, universe: Type, equal: s = t, l_member: (x

l)
Definitions : nat_plus:

, so_lambda:

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

B, member: t

T, and: P

Q, implies: P

Q, let: let, 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], Process-apply: Process-apply(P;m), lg-all:

x

G.P[x], pi2: snd(t), top: Top, add-cause: add-cause(ev;ext), ldag: LabeledDAG(T), run-command-node: run-command-node(r;t;n), run-command: run-command(r;t;n), run-msg-commands: run-msg-commands(r), cand: A c

B, pRunType: pRunType(T.M[T]), pi1: fst(t), run-event-step: run-event-step(e), runEvents: runEvents(r), nat:

, InitialSystem: InitialSystem(P.M[P]), pExt: pExt(P.M[P]), run-info: run-info(r;e), lg-contains: g1

g2, exists:

x:A. B[x], prop:

, guard: {T}
Lemmas : strong-type-continuous_wf, InitialSystem_wf, pMsg_wf, Id_wf, pEnvType_wf, reliable-env_wf, runEvents_wf, pRun_wf, run-event-state-when_wf, Process_wf, l_member_wf, run-event-step-positive, pRun_wf2, nat_wf, reliable-env-property, lg-size_wf_dag, int_seg_wf, com-kind_wf, pCom_wf, lg-label_wf_dag, pExt_wf, Process-apply_wf, run-info_wf, subtype_top, subtype_rel-labeled-graph, is-dag_wf, top_wf, labeled-graph_wf, subtype_rel_set, lg-label-map, exists_wf, pInTransit_wf, lg-size_wf, pRunType_wf, unit_wf2, ldag_wf, pi2_wf

\mforall{}[M:Type {}\mrightarrow{} Type] \mforall{}S:InitialSystem(P.M[P]). \mforall{}n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P]). \mforall{}l2m:Id {}\mrightarrow{} pMsg(P.M[P]). \mforall{}env:pEnvType(P.M[P]). let r = pRun(S;env;n2m;l2m) in reliable-env(env; r) {}\mRightarrow{} (\mforall{}e:runEvents(r). \mforall{}P:Process(P.M[P]). ((P \mmember{} run-event-state-when(r;e)) {}\mRightarrow{} \mforall{}p\mmember{}snd((P (snd(run-info(r;e))))).let y,c = p in (com-kind(c) \mmember{} ``msg choose new``) {}\mRightarrow{} (\mexists{}e':runEvents(r) ((run-event-loc(e') = y) \mwedge{} (e run-lt(r) e') \mwedge{} (\mexists{}n:\mBbbN{} \mexists{}nm:Id ((snd(run-info(r;e'))) = command-to-msg(c;n2m n;l2m nm))) \mwedge{} ((run-cause(r) e') = (inl e )))))) supposing Continuous+(P.M[P]) Date html generated: 2012_01_23-PM-12_45_01 Last ObjectModification: 2011_12_14-PM-11_32_40 Home Index