Nuprl Lemma : assert-ses-is-legal
∀prvt:Atom1. ∀pas:ProtocolAction List. (↑ses-is-legal(prvt; pas) ⇐⇒ Legal(pas) given prvt)
Proof
Definitions occuring in Statement :
ses-is-legal: ses-is-legal(prvt; pas),
ses-legal-sequence: Legal(pas) given prvt,
protocol-action: ProtocolAction,
list: T List,
atom: Atom$n,
assert: ↑b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q
Lemmas :
all_wf,
decidable_wf,
ses-legal-sequence_wf,
true_wf,
false_wf,
equal_wf,
list_wf,
protocol-action_wf
Latex:
\mforall{}prvt:Atom1. \mforall{}pas:ProtocolAction List. (\muparrow{}ses-is-legal(prvt; pas) \mLeftarrow{}{}\mRightarrow{} Legal(pas) given prvt)
Date html generated:
2015_07_23-PM-00_14_20
Last ObjectModification:
2015_01_29-AM-07_52_26
Home
Index