LOCAL
    types : SET  OF  STRING;
    refs_plus : SET OF maths_space;
  END_LOCAL;
  IF  (spc IN  refs) THEN
    RETURN  (FALSE);
  END_IF;
  types := TYPEOF  (spc);
  refs_plus := refs + spc;
  IF  (schema_prefix + 'FINITE_SPACE') IN  types THEN
    RETURN  (bool(SIZEOF (QUERY (sp <* QUERY (mem <* spc\finite_space.members |
      (schema_prefix + 'MATHS_SPACE') IN  TYPEOF (mem)) |
      NOT  no_cyclic_space_reference (sp, refs_plus))) = 0));
  END_IF;
  IF  (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN  types THEN
    RETURN  (no_cyclic_space_reference (spc\uniform_product_space.base, refs_plus));
  END_IF;
  IF  (schema_prefix + 'LISTED_PRODUCT_SPACE') IN  types THEN
    RETURN  (bool(SIZEOF (QUERY (fac <* spc\listed_product_space.factors |
      NOT no_cyclic_space_reference (fac, refs_plus))) = 0));
  END_IF;
  IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN types THEN
    RETURN  (no_cyclic_space_reference (spc\extended_tuple_space.base, refs_plus)
      AND no_cyclic_space_reference (spc\extended_tuple_space.extender, refs_plus));
  END_IF;
  -- spc contains no references TO other spaces
  RETURN (TRUE);