{ 
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,
assert: b,
all: x:A. B[x],
iff: P Q,
list: type List,
atom: Atom$n
Definitions :
all: x:A. B[x],
iff: P Q,
assert: b,
ses-is-legal: ses-is-legal(prvt; pas),
isl: isl(x),
member: t 
T,
prop: 
,
implies: P Q,
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
true: True,
and: P 
Q,
rev_implies: P Q,
decidable: Dec(P),
or: P 
Q,
not: 
A,
false: False
Lemmas :
protocol-action_wf,
decidable_wf,
ses-legal-sequence_wf,
true_wf,
false_wf
\mforall{}prvt:Atom1. \mforall{}pas:ProtocolAction List. (\muparrow{}ses-is-legal(prvt; pas) \mLeftarrow{}{}\mRightarrow{} Legal(pas) given prvt)
Date html generated:
2010_08_28-AM-02_46_50
Last ObjectModification:
2009_12_17-PM-10_32_50
Home
Index