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