Nuprl Lemma : reliable-env-property1

{

[M:Type

Type]

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

n2m:

pMsg(P.M[P]).

l2m:Id

pMsg(P.M[P]).

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

(

tn:run-msg-commands(r)
let t,n = tn
in

t':

(((t < t')
c

(((fst((env t' r)))

n)

lg-is-source(run-intransit(r;t');fst((env t' r)))
supposing 0 < lg-size(run-intransit(r;t'))))

(

i:

((t < i)
c

(((fst((env i r)))

n)

lg-is-source(run-intransit(r;i);fst((env i r)))
                              supposing 0 < lg-size(run-intransit(r;i))))
                         supposing i < t')))
    supposing Continuous+(P.M[P]) }

{ Proof }

Definitions occuring in Statement : run-msg-commands: run-msg-commands(r), reliable-env: reliable-env(env; r), InitialSystem: InitialSystem(P.M[P]), run-intransit: run-intransit(r;t), pRun: pRun(S0;env;nat2msg;loc2msg), pEnvType: pEnvType(T.M[T]), pMsg: pMsg(P.M[P]), lg-is-source: lg-is-source(g;i), lg-size: lg-size(g), Id: Id, strong-type-continuous: Continuous+(T.F[T]), assert:

b, nat:

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

[x:A]. B[x], cand: A c

B, so_apply: x[s], pi1: fst(t), le: A

B, all:

x:A. B[x], exists:

x:A. B[x], not:

A, implies: P

Q, and: P

Q, less_than: a < b, apply: f a, function: x:A

B[x], spread: spread def, natural_number: $n, universe: Type
Definitions : all:

x:A. B[x], so_lambda:

x.t[x], InitialSystem: InitialSystem(P.M[P]), function: x:A

B[x], member: t

T, pair: <a, b>, product: x:A

B[x], subtype_rel: A

r B, ext-eq: A

B, isect:

x:A. B[x], nat:

, universe: Type, uall:

[x:A]. B[x], strong-type-continuous: Continuous+(T.F[T]), apply: f a, let: let, prop:

, uimplies: b supposing a, pMsg: pMsg(P.M[P]), Id: Id, pEnvType: pEnvType(T.M[T]), equal: s = t, le: A

B, not:

A, implies: P

Q, false: False, spread: spread def, exists:

x:A. B[x], void: Void, cand: A c

B, assert:

b, less_than: a < b, run-msg-commands: run-msg-commands(r), pRun: pRun(S0;env;nat2msg;loc2msg), fulpRunType: fulpRunType(T.M[T]), uiff: uiff(P;Q), ge: i

j , std-initial: std-initial(S), lg-all:

x

G.P[x], set: {x:A| B[x]} , strong-subtype: strong-subtype(A;B), lambda:

x.A[x], System: System(P.M[P]), reliable-env: reliable-env(env; r), pi1: fst(t), natural_number: $n, lg-size: lg-size(g), run-intransit: run-intransit(r;t), lg-is-source: lg-is-source(g;i), axiom: Ax, int:

, hd: hd(l), tl: tl(l), sq_stable: SqStable(P), squash:

T, fpf-sub: f

g, modulus-of-ccontinuity: modulus-of-ccontinuity(omega;I;f), partitions: partitions(I;p), i-member: r

I, rleq: x

y, rnonneg: rnonneg(r), req: x = y, is_accum_splitting: is_accum_splitting(T;A;L;LL;L2;f;g;x), is_list_splitting: is_list_splitting(T;L;LL;L2;f), value-type: value-type(T), no_repeats: no_repeats(T;l), prime_ideal_p: IsPrimeIdeal(R;P), integ_dom_p: IsIntegDom(r), grp_leq: a

b, monoid_hom_p: IsMonHom{M1,M2}(f), group_p: IsGroup(T;op;id;inv), monoid_p: IsMonoid(T;op;id), monot: monot(T;x,y.R[x; y];f), cancel: Cancel(T;S;op), fun_thru_2op: FunThru2op(A;B;opa;opb;f), fun_thru_1op: fun_thru_1op(A;B;opa;opb;f), dist_1op_2op_lr: Dist1op2opLR(A;1op;2op), action_p: IsAction(A;x;e;S;f), bilinear_p: IsBilinear(A;B;C;+a;+b;+c;f), bilinear: BiLinear(T;pl;tm), inverse: Inverse(T;op;id;inv), comm: Comm(T;op), assoc: Assoc(T;op), ident: Ident(T;op;id), coprime: CoPrime(a,b), uconnex: uconnex(T; x,y.R[x; y]), connex: Connex(T;x,y.R[x; y]), uanti_sym: UniformlyAntiSym(T;x,y.R[x; y]), anti_sym: AntiSym(T;x,y.R[x; y]), utrans: UniformlyTrans(T;x,y.E[x; y]), trans: Trans(T;x,y.E[x; y]), usym: UniformlySym(T;x,y.E[x; y]), sym: Sym(T;x,y.E[x; y]), urefl: UniformlyRefl(T;x,y.E[x; y]), refl: Refl(T;x,y.E[x; y]), eqfun_p: IsEqFun(T;eq), inject: Inj(A;B;f), inv_funs: InvFuns(A;B;f;g), uni_sat: a = !x:T. Q[x], iff: P

Q, decidable: Dec(P), infix_ap: x f y, lg-edge: lg-edge(g;a;b), path-goes-thru: x-f*-y thru i, cut-order: a

(X;f) b, collect-event: collect-event(es;X;n;v.num[v];L.P[L];e), same-thread: same-thread(es;p;e;e'), es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), es-fset-loc: i

locs(s), existse-between3:

e

(e1,e2].P[e], existse-between2:

e

[e1,e2].P[e], alle-between2:

e

[e1,e2].P[e], existse-between1:

e

[e1,e2).P[e], alle-between1:

e

[e1,e2).P[e], alle-le:

e

e'.P[e], alle-lt:

e<e'.P[e], existse-le:

e

e'.P[e], existse-before:

e<e'.P[e], es-causle: e c

e', es-le: e

loc e' , es-locl: (e <loc e'), es-causl: (e < e'), cs-precondition: state s may consider v in inning i, cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i, cs-inning-committable: in state s, inning i could commit v , cs-inning-committed: in state s, inning i has committed v, cs-passed: by state s, a passed inning i without archiving a value, cs-archived: by state s, a archived v in inning i, cs-not-completed: in state s, a has not completed inning i, l_disjoint: l_disjoint(T;l1;l2), fset-closed: (s closed under fs), f-subset: xs

ys, fset-member: a

s, p-outcome: Outcome, i-closed: i-closed(I), i-finite: i-finite(I), q-rel: q-rel(r;x), qless: r < s, qle: r

s, fun-connected: y is f*(x), l_all: (

x

L.P[x]), l_exists: (

x

L. P[x]), prime: prime(a), reducible: reducible(a), l_contains: A

B, or: P

Q, union: left + right, runEvents: runEvents(r), es-E-interface: E(X), es-E: E, consensus-rcv: consensus-rcv(V;A), consensus-state3: consensus-state3(T), MaName: MaName, Knd: Knd, IdLnk: IdLnk, string: Error :string, fset: FSet{T}, dstype: dstype(TypeNames; d; a), atom: Atom$n, rationals:

, limited-type: LimitedType, nat_plus:

, list: type List, unit: Unit, rng_car: |r|, grp_lt: a < b, grp_car: |g|, set_lt: a <p b, set_leq: a

b, set_car: |p|, assoced: a ~ b, divides: b | a, quotient: x,y:A//B[x; y], bool:

, int_seg: {i..j

}, true: True, pInTransit: pInTransit(P.M[P]), fpf: a:A fp-> B[a], eclass: EClass(A[eo; e]), pCom: pCom(P.M[P]), Auto: Error :Auto, CollapseTHEN: Error :CollapseTHEN, D: Error :D, RepeatFor: Error :RepeatFor, Try: Error :Try, atom: Atom, nil: [], token: "$token", cons: [car / cdr], run-command: run-command(r;t;n), pi2: snd(t), com-kind: com-kind(c), l_member: (x

l), run-command-node: run-command-node(r;t;n), and: P

Q, AssertBY: Error :AssertBY, Unfold: Error :Unfold, RepUR: Error :RepUR, MaAuto: Error :MaAuto, so_apply: x[s], pRunType: pRunType(T.M[T]), CollapseTHENA: Error :CollapseTHENA, guard: {T}, multiply: n * m, add: n + m, bag: bag(T), deq: EqDecider(T), ma-state: State(ds), class-program: ClassProgram(T), tag-by: z

T, rev_implies: P

Q, labeled-graph: LabeledGraph(T), record+: record+, record: record(x.T[x]), isect2: T1

T2, b-union: A

B, fpf-cap: f(x)?z, intensional-universe: IType, suptype: suptype(S; T), lelt: i

j < k, ldag: LabeledDAG(T), top: Top, real:

, subtype: S

T, decide: case b of inl(x) => s[x] | inr(y) => t[y], ifthenelse: if b then t else f fi , dep-isect: Error :dep-isect, is-dag: is-dag(g), sq_type: SQType(T), mu: mu(f), length: ||as||
Lemmas : mu-property2, mu-wf2, squash_wf, sq_stable__assert, sq_stable__all, int_subtype_base, subtype_base_sq, lg-edge_wf, uall_wf, iff_weakening_uiff, assert-lg-is-source, assert_witness, ifthenelse_wf, true_wf, pi1_wf_top, lg-is-source_wf_dag, run-intransit_wf, lg-size_wf_dag, top_wf, decidable__assert, decidable__lt, decidable__uimplies, decidable__le, decidable__cand, decidable_wf, ldag_wf, unit_wf, int_seg_wf, nat_plus_wf, subtype_rel_wf, lg-size_wf, pi1_wf, nat_properties, false_wf, intensional-universe_wf, subtype_rel_function, int_seg_properties, subtype_rel_self, lg-is-source_wf, uiff_inversion, decidable__and, pInTransit_wf, com-kind_wf, run-command_wf, decidable__atom_equal, decidable__l_member, sq_stable_from_decidable, pRun_wf, pEnvType_wf, Id_wf, pMsg_wf, InitialSystem_wf, strong-type-continuous_wf, pRun_wf2, member_wf, System_wf, pRunType_wf, not_wf, assert_wf, le_wf, run-msg-commands_wf, reliable-env_wf, l_member_wf, nat_wf

\mforall{}[M:Type {}\mrightarrow{} Type] \mforall{}S0: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(S0;env;n2m;l2m) in reliable-env(env; r) {}\mRightarrow{} (\mforall{}tn:run-msg-commands(r) let t,n = tn in \mexists{}t':\mBbbN{} (((t < t') c\mwedge{} (((fst((env t' r))) \mleq{} n) \mwedge{} \muparrow{}lg-is-source(run-intransit(r;t');fst((env t' r))) supposing 0 < lg-size(run-intransit(r;t')))) \mwedge{} (\mforall{}i:\mBbbN{} \mneg{}((t < i) c\mwedge{} (((fst((env i r))) \mleq{} n) \mwedge{} \muparrow{}lg-is-source(run-intransit(r;i);fst((env i r))) supposing 0 < lg-size(run-intransit(r;i)))) supposing i < t'))) supposing Continuous+(P.M[P]) Date html generated: 2011_08_17-PM-03_45_09 Last ObjectModification: 2011_06_18-AM-11_25_50 Home Index