{ 
[prvt:Atom1]. [pas:ProtocolAction List]. (Legal(pas) given prvt 
) }
{ Proof }
Definitions occuring in Statement :
ses-legal-sequence: Legal(pas) given prvt,
protocol-action: ProtocolAction,
uall: [x:A]. B[x],
prop: ,
member: t T,
list: type List,
atom: Atom$n
Definitions :
uall: [x:A]. B[x],
member: t T,
prop: ,
ses-legal-sequence: Legal(pas) given prvt,
all: x:A. B[x],
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
and: P 
Q,
int_seg: {i..j
},
uimplies: b supposing a,
lelt: i j < k
Lemmas :
int_seg_wf,
length_wf1,
l_contains_wf,
pa-used_wf,
select_wf,
concat_wf,
map_wf,
le_wf,
from-upto_wf,
pa-useable_wf,
protocol-action_wf
\mforall{}[prvt:Atom1]. \mforall{}[pas:ProtocolAction List]. (Legal(pas) given prvt \mmember{} \mBbbP{})
Date html generated:
2011_08_17-PM-07_37_57
Last ObjectModification:
2011_06_18-PM-01_31_57
Home
Index