Comm-state() ==
  st:Id fp-> pi_prefix() List 
 (Id 
 (pi_prefix() List)) List 
 Id 
 
 
 
Definitions : 
fpf: a:A fp-> B[a], 
list: type List, 
pi_prefix: pi_prefix(), 
Id: Id, 
product: x:A 
 B[x], 
bool:
, 
nat:
FDL editor aliases : 
Comm-state
Comm-state()  ==    st:Id  fp->  pi\_prefix()  List  \mtimes{}  (Id  \mtimes{}  (pi\_prefix()  List))  List  \mtimes{}  Id  \mtimes{}  \mBbbB{}  \mtimes{}  \mBbbN{}
Date html generated:
2010_08_27-PM-08_46_28
Last ObjectModification:
2010_03_29-PM-12_33_23
Home
Index