system-equiv(T.M[T];S1;S2) ==
let Cs1,G1 = S1 in
let Cs2,G2 = S2 in
(G1 = G2)
(||Cs1|| = ||Cs2||)
(
k:
||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z) P
Q)
Definitions :
process-equiv: process-equiv,
Id: Id,
equal: s = t,
and: P Q,
select: l[i],
spread: spread def,
length: ||as||,
natural_number: $n,
int_seg: {i..j
},
all: x:A. B[x],
int: 
,
pInTransit: pInTransit(P.M[P]),
ldag: LabeledDAG(T)
FDL editor aliases :
system-equiv
system-equiv(T.M[T];S1;S2) ==
let Cs1,G1 = S1 in
let Cs2,G2 = S2 in
(G1 = G2)
\mwedge{} (||Cs1|| = ||Cs2||)
\mwedge{} (\mforall{}k:\mBbbN{}||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z) \mwedge{} P\mequiv{}Q)
Date html generated:
2010_08_27-PM-03_50_47
Last ObjectModification:
2010_06_30-PM-07_32_40
Home
Index