{ 
es:EO
[P:E 
]
([][]P 
[]P
<><>P <>P
<>P (TR 
P)
[]
P <>P
<>P []P) }
{ Proof }
Definitions occuring in Statement :
es-TR: TR,
es-equiv: P Q,
es-not: P,
es-until: (P Q),
es-diamond: <>P,
es-box: []P,
es-E: E,
event_ordering: EO,
uall: [x:A]. B[x],
prop: ,
all: x:A. B[x],
and: P Q,
function: x:A B[x]
Definitions :
all: x:A. B[x],
uall: [x:A]. B[x],
prop: ,
and: P Q,
es-equiv: P Q,
es-box: []P,
es-diamond: <>P,
es-until: (P Q),
es-TR: TR,
es-not: P,
iff: P 
Q,
implies: P Q,
es-le: e 
loc e' ,
exists: 
x:A. B[x],
true: True,
not: A,
rev_implies: P Q,
member: t 
T,
cand: A c B,
or: P 
Q,
guard: {T},
false: False
Lemmas :
es-le_wf,
es-E_wf,
es-le_transitivity,
es-locl_wf,
true_wf,
not_wf,
event_ordering_wf
\mforall{}es:EO. \mforall{}[P:E {}\mrightarrow{} \mBbbP{}]. ([][]P \mequiv{} []P \mwedge{} <><>P \mequiv{} <>P \mwedge{} <>P \mequiv{} (TR \mcup{} P) \mwedge{} []\mneg{}\mneg{}P \mequiv{} \mneg{}<>\mneg{}P \mwedge{} \mneg{}\mneg{}<>P \mequiv{} \mneg{}[]\mneg{}P)
Date html generated:
2011_08_16-AM-10_50_11
Last ObjectModification:
2011_06_18-AM-09_25_25
Home
Index