Nuprl Lemma : decidable_

{

s:SES.

es:EO+(Info).

e:E. Dec(Action(e)) }

{ Proof }

Definitions occuring in Statement : ses-action: Action(e), ses-info: Info, security-event-structure: SES, event-ordering+: EO+(Info), es-E: E, decidable: Dec(P), all:

x:A. B[x]
Definitions : equal: s = t, member: t

T, function: x:A

B[x], all:

x:A. B[x], security-event-structure: SES, ses-info: Info, event-ordering+: EO+(Info), product: x:A

B[x], dep-isect: Error :dep-isect, event_ordering: EO, es-E: E, universe: Type, top: Top, token: "$token", eq_atom: x =a y, ifthenelse: if b then t else f fi , atom: Atom, subtype_rel: A

r B, eq_atom: eq_atom$n(x;y), apply: f a, record-select: r.x, record+: record+, atom: Atom$n, Id: Id, sdata: SecurityData, void: Void, isect:

x:A. B[x], ses-verify: Verify, implies: P

Q, eclass: EClass(A[eo; e]), es-E-interface: E(X), so_lambda:

x y.t[x; y], in-eclass: e

X, decidable: Dec(P), assert:

b, exists:

x:A. B[x], divides: b | a, assoced: a ~ b, set_leq: a

b, set_lt: a <p b, grp_lt: a < b, cand: A c

B, infix_ap: x f y, l_all: (

x

L.P[x]), l_exists: (

x

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

l), l_contains: A

B, inject: Inj(A;B;f), reducible: reducible(a), prime: prime(a), squash:

T, l_disjoint: l_disjoint(T;l1;l2), fun-connected: y is f*(x), qle: r

s, qless: r < s, q-rel: q-rel(r;x), p-outcome: Outcome, fset-member: a

s, f-subset: xs

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

loc e' , es-causle: e c

e', existse-before:

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

e

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

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

e

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

e

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

e

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

e

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

e

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

e

(e1,e2].P[e], es-fset-loc: i

locs(s), collect-event: collect-event(es;X;n;v.num[v];L.P[L];e), cut-order: a

(X;f) b, path-goes-thru: x-f*-y thru i, es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), same-thread: same-thread(es;p;e;e'), fpf: a:A fp-> B[a], strong-subtype: strong-subtype(A;B), ses-sign: Sign, prop:

, union: left + right, or: P

Q, not:

A, and: P

Q, false: False, iff: P

Q, less_than: a < b, le: A

B, encryption-key: Key, ses-decrypt: Decrypt, ses-encrypt: Encrypt, rec: rec(x.A[x]), tree: Tree(E), ses-rcv: Rcv, ses-send: Send, ses-new: New, subtype: S

T, ses-action: Action(e), MaAuto: Error :MaAuto, Unfold: Error :Unfold, CollapseTHEN: Error :CollapseTHEN
Lemmas : event-ordering+_inc, ses-new_wf, ses-send_wf, ses-rcv_wf, ses-encrypt_wf, ses-decrypt_wf, encryption-key_wf, decidable__or, ses-sign_wf, assert_wf, decidable_wf, decidable__assert, in-eclass_wf, eclass_wf, member_wf, es-interface-top, es-interface-subtype_rel, ses-verify_wf, subtype_rel_wf, sdata_wf, Id_wf, top_wf, es-E_wf, subtype_rel_self, event-ordering+_wf, ses-info_wf, security-event-structure_wf

\mforall{}s:SES. \mforall{}es:EO+(Info). \mforall{}e:E. Dec(Action(e)) Date html generated: 2011_08_17-PM-07_18_28 Last ObjectModification: 2010_09_24-PM-03_14_22 Home Index