Nuprl Lemma : ses-is-protocol-actions-legal
∀s:SES
(ActionsDisjoint
⇒ (∀pas:ProtocolAction List. ∀es:EO+(Info). ∀thr:Thread. ∀A:Id.
(pas(thr) ⇒ Legal(pas) given Private(A) ⇒ Legal(thr)@A)))
Proof
Definitions occuring in Statement :
ses-is-protocol-actions: pas(thr),
ses-legal-sequence: Legal(pas) given prvt,
protocol-action: ProtocolAction,
ses-legal-thread: Legal(thr)@A,
ses-thread: Thread,
ses-disjoint: ActionsDisjoint,
ses-private: Private(A),
ses-info: Info,
security-event-structure: SES,
event-ordering+: EO+(Info),
Id: Id,
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas :
less_than_transitivity1,
length_wf,
ses-act_wf,
protocol-action_wf,
le_weakening,
lelt_wf,
l_contains_wf,
squash_wf,
true_wf,
list_wf,
ses-is-protocol-action-used,
select_wf,
sq_stable__le,
cons_wf,
ses-private_wf,
concat_wf,
map_wf,
set_wf,
le_wf,
less_than_wf,
from-upto_wf,
int_seg_wf,
ses-legal-sequence_wf,
ses-is-protocol-actions_wf,
Id_wf,
ses-thread_wf,
event-ordering+_wf,
ses-info_wf,
ses-disjoint_wf,
security-event-structure_wf,
ses-is-protocol-action-useable,
less_than_transitivity2,
le_weakening2
Latex:
\mforall{}s:SES
(ActionsDisjoint
{}\mRightarrow{} (\mforall{}pas:ProtocolAction List. \mforall{}es:EO+(Info). \mforall{}thr:Thread. \mforall{}A:Id.
(pas(thr) {}\mRightarrow{} Legal(pas) given Private(A) {}\mRightarrow{} Legal(thr)@A)))
Date html generated:
2015_07_23-PM-00_15_22
Last ObjectModification:
2015_01_29-AM-01_33_07
Home
Index