FDL > PVS > Graphs > graphs > size : const-decl

size(G): nat = card[T](vert(G));