{ 
f:SecurityData 
(?Atom1). A:Id. pas:ProtocolAction List.
(
ses-is-fresh(f;A;pas) 
ses-fresh-sequence(f;A;pas)) }
{ Proof }
Definitions occuring in Statement :
ses-is-fresh: ses-is-fresh(f;A;pas),
ses-fresh-sequence: ses-fresh-sequence(f;A;pas),
protocol-action: ProtocolAction,
sdata: SecurityData,
Id: Id,
assert: b,
all: x:A. B[x],
iff: P Q,
unit: Unit,
function: x:A B[x],
union: left + right,
list: type List,
atom: Atom$n
Definitions :
RepeatFor: Error :RepeatFor,
CollapseTHENA: Error :CollapseTHENA,
Unfold: Error :Unfold,
D: Error :D,
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
ses-is-fresh: ses-is-fresh(f;A;pas),
limited-type: LimitedType,
sdata: SecurityData,
atom: Atom$n,
unit: Unit,
protocol-action: ProtocolAction,
all: x:A. B[x],
or: P 
Q,
union: left + right,
inl: inl x ,
true: True,
assert: b,
iff: P Q,
and: P 
Q,
product: x:A 
B[x],
rev_implies: P Q,
prop: 
,
universe: Type,
decidable: Dec(P),
ses-fresh-sequence: ses-fresh-sequence(f;A;pas),
apply: f a,
decidable-ses-fresh-sequence,
inr: inr x ,
list: type List,
Id: Id,
function: x:A B[x],
member: t 
T,
equal: s = t,
not: 
A,
implies: P Q,
false: False
Lemmas :
false_wf,
ses-fresh-sequence_wf,
true_wf,
decidable_wf,
protocol-action_wf,
Id_wf,
unit_wf,
sdata_wf,
decidable-ses-fresh-sequence,
iff_wf,
assert_wf
\mforall{}f:SecurityData {}\mrightarrow{} (?Atom1). \mforall{}A:Id. \mforall{}pas:ProtocolAction List.
(\muparrow{}ses-is-fresh(f;A;pas) \mLeftarrow{}{}\mRightarrow{} ses-fresh-sequence(f;A;pas))
Date html generated:
2010_08_28-AM-03_11_47
Last ObjectModification:
2010_03_16-PM-02_38_22
Home
Index