{ 
[M:Type 
Type]
n2m:
pMsg(P.M[P]). l2m:Id pMsg(P.M[P]).
[A:pEnvType(P.M[P]) pRunType(P.M[P]) 
].
[B:EO+(pMsg(P.M[P])) ].
X,Y:InitialSystem(P.M[P]).
(system-equiv(P.M[P];X;Y)
assuming(env,r.A[env;r])
X |= eo.B[eo]
assuming(env,r.A[env;r])
Y |= eo.B[eo])
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
system-strongly-realizes: system-strongly-realizes,
InitialSystem: InitialSystem(P.M[P]),
pEnvType: pEnvType(T.M[T]),
pRunType: pRunType(T.M[T]),
system-equiv: system-equiv(T.M[T];S1;S2),
pMsg: pMsg(P.M[P]),
event-ordering+: EO+(Info),
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s1;s2],
so_apply: x[s],
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
universe: Type
Definitions :
false: False,
implies: P Q,
subtype: S 
T,
top: Top,
le: A 
B,
not: 
A,
so_lambda: 
x.t[x],
member: t 
T,
all: x:A. B[x],
prop: ,
nat: ,
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
System: System(P.M[P]),
InitialSystem: InitialSystem(P.M[P]),
std-initial: std-initial(S),
iff: P 
Q,
rev_implies: P Q,
lelt: i j < k,
exists: 
x:A. B[x],
and: P 
Q,
int_seg: {i..j
},
label: ...$L... t,
component: component(P.M[P]),
process-equiv: process-equiv,
suptype: suptype(S; T),
true: True,
squash: 
T,
cand: A c B,
so_apply: x[s1;s2],
uimplies: b supposing a,
uall: [x:A]. B[x],
system-equiv: system-equiv(T.M[T];S1;S2),
or: P 
Q,
guard: {T},
sq_type: SQType(T),
decidable: Dec(P),
inject: Inj(A;B;f),
let: let,
system-realizes: system-realizes,
system-strongly-realizes: system-strongly-realizes,
ldag: LabeledDAG(T)
Lemmas :
le_wf,
nat_wf,
pi1_wf_top,
select_wf,
upto_wf,
component_wf,
length_wf1,
int_seg_wf,
map_wf,
std-initial_wf,
top_wf,
length_wf_nat,
length_upto,
select_upto,
decidable_wf,
int_subtype_base,
subtype_base_sq,
process-equiv_wf,
Process_wf,
Id_wf,
pMsg_wf,
Process-stream_wf,
squash_wf,
increasing_inj,
non_neg_length,
increasing_wf,
sub-system_wf,
system-equiv_wf,
pRunType_wf,
pRun_functionality,
runEvents_wf,
run-eo_wf,
std-initial-property,
run-initialization_wf,
member_wf,
run-initialization-property,
run-event-step_wf,
run-info_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P]). \mforall{}l2m:Id {}\mrightarrow{} pMsg(P.M[P]).
\mforall{}[A:pEnvType(P.M[P]) {}\mrightarrow{} pRunType(P.M[P]) {}\mrightarrow{} \mBbbP{}]. \mforall{}[B:EO+(pMsg(P.M[P])) {}\mrightarrow{} \mBbbP{}].
\mforall{}X,Y:InitialSystem(P.M[P]).
(system-equiv(P.M[P];X;Y)
{}\mRightarrow{} assuming(env,r.A[env;r])
X |= eo.B[eo]
{}\mRightarrow{} assuming(env,r.A[env;r])
Y |= eo.B[eo])
supposing Continuous+(P.M[P])
Date html generated:
2011_08_17-PM-03_55_41
Last ObjectModification:
2011_06_18-AM-11_27_54
Home
Index