Nuprl Definition : system-equiv
system-equiv(T.M[T];S1;S2) ==
let Cs1,G1 = S1
in let Cs2,G2 = S2
in (G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P])))
∧ (||Cs1|| = ||Cs2|| ∈ ℤ)
∧ (∀k:ℕ||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z ∈ Id) ∧ P≡Q)
Definitions occuring in Statement :
pInTransit: pInTransit(P.M[P]),
process-equiv: process-equiv,
ldag: LabeledDAG(T),
Id: Id,
select: L[n],
length: ||as||,
int_seg: {i..j-},
all: ∀x:A. B[x],
and: P ∧ Q,
spread: spread def,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
system-equiv
Latex:
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:
2016_05_17-AM-10_36_55
Last ObjectModification:
2012_02_25-PM-03_38_53
Theory : process-model
Home
Index