Nuprl Definition : pEnvType
pEnvType(T.M[T]) ==
t:ℕ+ ⟶ (ℕt ⟶ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))) ⟶ (ℕ × ℕ × Id)
Definitions occuring in Statement :
pInTransit: pInTransit(P.M[P]),
pMsg: pMsg(P.M[P]),
ldag: LabeledDAG(T),
Id: Id,
int_seg: {i..j-},
nat_plus: ℕ+,
nat: ℕ,
top: Top,
unit: Unit,
function: x:A ⟶ B[x],
product: x:A × B[x],
union: left + right,
natural_number: $n,
int: ℤ
FDL editor aliases :
pEnvType
Latex:
pEnvType(T.M[T]) ==
t:\mBbbN{}\msupplus{}
{}\mrightarrow{} (\mBbbN{}t {}\mrightarrow{} (\mBbbZ{} \mtimes{} Id \mtimes{} Id \mtimes{} pMsg(P.M[P])? \mtimes{} Top \mtimes{} LabeledDAG(pInTransit(P.M[P]))))
{}\mrightarrow{} (\mBbbN{} \mtimes{} \mBbbN{} \mtimes{} Id)
Date html generated:
2016_05_17-AM-10_40_08
Last ObjectModification:
2012_02_25-PM-03_40_12
Theory : process-model
Home
Index