LOCAL
    spc1types : SET  OF  STRING  := stripped_typeof(spc1);
    spc2types : SET  OF  STRING := stripped_typeof(spc2);
    set1, set2 : SET  OF  maths_value;
    cum : LOGICAL := TRUE;
    base : maths_space;
    expnt : INTEGER;
    factors : LIST  OF  maths_space;
    factors2 : LIST OF  maths_space;
    fs1, fs2 : function_space;
    cum2 : LOGICAL;
  END_LOCAL;
  IF  spc1 = spc2 THEN   RETURN  (TRUE);  END_IF;
  -- Consider cases WHERE it is NOT  yet certain that spc1 <> spc2.
  IF  'FINITE_SPACE' IN  spc1types THEN
    set1 := spc1\finite_space.members;
    IF  'FINITE_SPACE' IN  spc2types THEN
      -- Members may have different but equivalent representations AND  in
      -- different orders.  May also have disguised repeats IN  same SET OF members.
      set2 := spc2\finite_space.members;
      REPEAT  i := 1 TO  SIZEOF  (set1);
        cum := cum AND  member_of (set1[i], spc2);
        IF  cum = FALSE  THEN   RETURN  (FALSE);  END_IF;
      END_REPEAT;
      IF  cum = TRUE THEN
        REPEAT  i := 1 TO  SIZEOF  (set2);
          cum := cum AND  member_of (set2[i], spc1);
          IF  cum = FALSE  THEN   RETURN  (FALSE);  END_IF;
        END_REPEAT;
      END_IF;
      RETURN  (cum);
    END_IF;
    IF  'FINITE_INTEGER_INTERVAL' IN  spc2types THEN
      set2 := [];
      REPEAT  i := spc2\finite_integer_interval.min TO  spc2\finite_integer_interval.max;
        set2 := set2 + [i];
      END_REPEAT;
      RETURN  (equal_maths_spaces(spc1,make_finite_space(set2)));
    END_IF;
  END_IF;
  IF  ('FINITE_INTEGER_INTERVAL' IN  spc1types) AND  ('FINITE_SPACE' IN  spc2types) THEN
    set1 := [];
    REPEAT  i := spc1\finite_integer_interval.min TO  spc1\finite_integer_interval.max;
      set1 := set1 + [i];
    END_REPEAT;
    RETURN  (equal_maths_spaces(make_finite_space(set1),spc2));
  END_IF;
  IF  ('CARTESIAN_COMPLEX_NUMBER_REGION' IN  spc1types) AND
    ('POLAR_COMPLEX_NUMBER_REGION' IN  spc2types) THEN
    -- Quadrants AND  half spaces have two representations
    RETURN  (equal_cregion_pregion(spc1,spc2));
  END_IF;
  IF  ('POLAR_COMPLEX_NUMBER_REGION' IN  spc1types) AND
    ('CARTESIAN_COMPLEX_NUMBER_REGION' IN  spc2types) THEN
    -- Quadrants AND  half spaces have two representations
    RETURN  (equal_cregion_pregion(spc2,spc1));
  END_IF;
  IF  'UNIFORM_PRODUCT_SPACE' IN  spc1types THEN
    base := spc1\uniform_product_space.base;
    expnt := spc1\uniform_product_space.exponent;
    IF  'UNIFORM_PRODUCT_SPACE' IN  spc2types THEN
      IF  expnt <> spc2\uniform_product_space.exponent THEN   RETURN  (FALSE);  END_IF;
      RETURN  (equal_maths_spaces(base,spc2\uniform_product_space.base));
    END_IF;
    IF  'LISTED_PRODUCT_SPACE' IN  spc2types THEN
      factors := spc2\listed_product_space.factors;
      IF  expnt <> SIZEOF  (factors) THEN   RETURN  (FALSE);  END_IF;
      REPEAT  i := 1 TO  SIZEOF  (factors);
        cum := cum AND  equal_maths_spaces(base,factors[i]);
        IF  cum = FALSE  THEN   RETURN  (FALSE);  END_IF;
      END_REPEAT;
      RETURN  (cum);
    END_IF;
  END_IF;
  IF  'LISTED_PRODUCT_SPACE' IN  spc1types THEN
    factors := spc1\listed_product_space.factors;
    IF  'UNIFORM_PRODUCT_SPACE' IN  spc2types THEN
      IF  spc2\uniform_product_space.exponent <> SIZEOF  (factors) THEN
        RETURN  (FALSE);
      END_IF;
      base := spc2\uniform_product_space.base;
      REPEAT  i := 1 TO  SIZEOF  (factors);
        cum := cum AND  equal_maths_spaces(base,factors[i]);
        IF  cum = FALSE  THEN   RETURN  (FALSE);  END_IF;
      END_REPEAT;
      RETURN  (cum);
    END_IF;
    IF  'LISTED_PRODUCT_SPACE' IN  spc2types THEN
      factors2 := spc2\listed_product_space.factors;
      IF  SIZEOF  (factors) <> SIZEOF  (factors2) THEN   RETURN  (FALSE);  END_IF;
      REPEAT i := 1 TO SIZEOF  (factors);
        cum := cum AND  equal_maths_spaces(factors[i],factors2[i]);
        IF  cum = FALSE  THEN   RETURN  (FALSE);  END_IF;
      END_REPEAT;
      RETURN  (cum);
    END_IF;
  END_IF;
  IF  ('EXTENDED_TUPLE_SPACE' IN  spc1types) AND
    ('EXTENDED_TUPLE_SPACE' IN  spc2types) THEN
    RETURN  (equal_maths_spaces(spc1\extended_tuple_space.extender,
      spc2\extended_tuple_space.extender) AND  equal_maths_spaces(
      spc1\extended_tuple_space.base, spc2\extended_tuple_space.base));
  END_IF;
  IF  ('FUNCTION_SPACE' IN  spc1types) AND
    ('FUNCTION_SPACE' IN  spc2types) THEN
    fs1 := spc1;
    fs2 := spc2;
    IF  fs1.domain_constraint <> fs2.domain_constraint THEN
      IF  (fs1.domain_constraint = sc_equal) OR  (fs2.domain_constraint = sc_equal) THEN
        RETURN  (FALSE);
      END_IF;
      IF  (fs1.domain_constraint <> sc_subspace) THEN
        fs1 := spc2;
        fs2 := spc1;
      END_IF;
      IF  (fs1.domain_constraint <> sc_subspace) OR
        (fs2.domain_constraint <> sc_member) THEN
        -- Safety check.  Should be unreachable.
        RETURN  (UNKNOWN);
      END_IF;
      IF  any_space_satisfies(fs1.domain_constraint,fs1.domain_argument) <>
        any_space_satisfies(fs2.domain_constraint,fs2.domain_argument) THEN
        RETURN  (FALSE);
      END_IF;
      IF  NOT  ('FINITE_SPACE' IN  stripped_typeof(fs2.domain_argument)) THEN
        RETURN  (FALSE);
      END_IF;
      IF  SIZEOF  (['FINITE_SPACE','FINITE_INTEGER_INTERVAL'] *
        stripped_typeof(fs1.domain_argument)) = 0 THEN
        RETURN  (FALSE);
      END_IF;
      -- Remaining cases too complex.
      RETURN  (UNKNOWN);
    END_IF;
    cum := equal_maths_spaces(fs1.domain_argument,fs2.domain_argument);
    IF  cum = FALSE THEN  RETURN  (FALSE);  END_IF;
    IF  fs1.range_constraint <> fs2.range_constraint THEN
      IF  (fs1.range_constraint = sc_equal) OR (fs2.range_constraint = sc_equal) THEN
        RETURN  (FALSE);
      END_IF;
      IF  (fs1.range_constraint <> sc_subspace) THEN
        fs1 := spc2;
        fs2 := spc1;
      END_IF;
      IF  (fs1.range_constraint <> sc_subspace) OR
        (fs2.range_constraint <> sc_member) THEN
        -- Safety check.  Should be unreachable.
        RETURN  (UNKNOWN);
      END_IF;
      IF  any_space_satisfies(fs1.range_constraint,fs1.range_argument) <>
        any_space_satisfies(fs2.range_constraint,fs2.range_argument) THEN
        RETURN  (FALSE);
      END_IF;
      IF  NOT ('FINITE_SPACE' IN stripped_typeof(fs2.range_argument)) THEN
        RETURN  (FALSE);
      END_IF;
      IF SIZEOF (['FINITE_SPACE','FINITE_INTEGER_INTERVAL'] *
        stripped_typeof(fs1.range_argument)) = 0 THEN
        RETURN  (FALSE);
      END_IF;
      -- Remaining cases too complex.
      RETURN  (UNKNOWN);
    END_IF;
    cum := cum AND equal_maths_spaces(fs1.range_argument,fs2.range_argument);
    RETURN  (cum);
  END_IF;
  RETURN (FALSE);