Overlapping regions Application Object

An Overlapping_regions is a relationship that is between two instances of Region (region_1 and region_2) and that indicates some points are within both region_1 and region_2.

HELP WANTED - I think that to make this definition precise and useful, we should specify that a region is an open point set. - DJL

EXPRESS specification:

*)
ENTITY Overlapping_regions;
  region_1  :  Region
  region_2  :  Region;
WHERE
  consistent_topological_dimension : 
    region_1.topological_dimension = region_2.topological_dimension; 
END_ENTITY;
(*

Attribute definitions:

region_1: the Region that contains points that are also in region_2.

region_2: the Region that contains points that are also in region_1.

Formal propositions:

consistent_topological_dimension: the overlapping instances of Region shall have the same topological_dimension.