LOCAL
    spc1 : maths_space := simplify_maths_space(space1);
    spc2 : maths_space := simplify_maths_space(space2);
    types1 : SET  OF  STRING  := stripped_typeof (spc1);
    types2 : SET OF STRING := stripped_typeof (spc2);
    lgcl, cum : LOGICAL;
    es_val : elementary_space_enumerators;
    bnd1, bnd2 : REAL;
    n : INTEGER;
    sp1, sp2 : maths_space;
    prgn1, prgn2 : polar_complex_number_region;
    aitv : finite_real_interval;
  END_LOCAL;
  IF  NOT  EXISTS  (spc1) OR  NOT  EXISTS (spc2) THEN
    RETURN  (FALSE);
  END_IF;
  IF  spc2 = the_generics THEN
    RETURN  (TRUE);
  END_IF;
  IF  'ELEMENTARY_SPACE' IN  types1 THEN
    IF  NOT  ('ELEMENTARY_SPACE' IN  types2) THEN
      RETURN  (FALSE);
    END_IF;
    es_val := spc2\elementary_space.space_id;
    IF  spc1\elementary_space.space_id = es_val THEN
      RETURN  (TRUE);
    END_IF;
    -- Note that the cases (spc2=the_generics) AND  (spc1=spc2) have been handled.
    CASE  spc1\elementary_space.space_id OF
    es_numbers :  RETURN  (FALSE);
    es_complex_numbers :  RETURN  (es_val = es_numbers);
    es_reals :  RETURN  (es_val = es_numbers);
    es_integers :  RETURN  (es_val = es_numbers);
    es_logicals :  RETURN  (FALSE);
    es_booleans :  RETURN  (es_val = es_logicals);
    es_strings :  RETURN  (FALSE);
    es_binarys :  RETURN  (FALSE);
    es_maths_spaces :  RETURN  (FALSE);
    es_maths_functions :  RETURN  (FALSE);
    es_generics :  RETURN  (FALSE);
    END_CASE;
    -- Should be unreachable.
    RETURN  (UNKNOWN);
  END_IF;
  IF  'FINITE_INTEGER_INTERVAL' IN  types1 THEN
    cum := TRUE;
    REPEAT  i := spc1\finite_integer_interval.min TO  spc1\finite_integer_interval.max;
      cum := cum AND  member_of (i, spc2);
      IF  cum = FALSE  THEN
        RETURN  (FALSE);
      END_IF;
    END_REPEAT;
    RETURN  (cum);
  END_IF;
  IF  'INTEGER_INTERVAL_FROM_MIN' IN  types1 THEN
    IF  'ELEMENTARY_SPACE' IN  types2 THEN
      es_val := spc2\elementary_space.space_id;
      RETURN  ((es_val = es_numbers) OR  (es_val = es_integers));
    END_IF;
    IF  'INTEGER_INTERVAL_FROM_MIN' IN  types2 THEN
      RETURN  (spc1\integer_interval_from_min.min>=spc2\integer_interval_from_min.min);
    END_IF;
    RETURN  (FALSE);
  END_IF;
  IF  'INTEGER_INTERVAL_TO_MAX' IN  types1 THEN
    IF  'ELEMENTARY_SPACE' IN  types2 THEN
      es_val := spc2\elementary_space.space_id;
      RETURN  ((es_val = es_numbers) OR  (es_val = es_integers));
    END_IF;
    IF  'INTEGER_INTERVAL_TO_MAX' IN  types2 THEN
      RETURN  (spc1\integer_interval_to_max.max <= spc2\integer_interval_to_max.max);
    END_IF;
    RETURN  (FALSE);
  END_IF;
  IF  'FINITE_REAL_INTERVAL' IN  types1 THEN
    IF  'ELEMENTARY_SPACE' IN  types2 THEN
      es_val := spc2\elementary_space.space_id;
      RETURN  ((es_val = es_numbers) OR  (es_val = es_reals));
    END_IF;
    IF  ('FINITE_REAL_INTERVAL' IN  types2) OR
      ('REAL_INTERVAL_FROM_MIN' IN  types2) OR
      ('REAL_INTERVAL_TO_MAX' IN  types2) THEN
      IF  min_exists (spc2) THEN
        bnd1 := spc1\finite_real_interval.min;
        bnd2 := real_min (spc2);
        IF  (bnd1 < bnd2) OR  ((bnd1 = bnd2) AND  min_included (spc1) AND  NOT
          min_included (spc2)) THEN
          RETURN  (FALSE);
        END_IF;
      END_IF;
      IF  max_exists (spc2) THEN
        bnd1 := spc1\finite_real_interval.max;
        bnd2 := real_max (spc2);
        IF  (bnd1 > bnd2) OR  ((bnd1 = bnd2) AND  max_included (spc1) AND  NOT
          max_included (spc2)) THEN
          RETURN  (FALSE);
        END_IF;
      END_IF;
      RETURN  (TRUE);
    END_IF;
    RETURN  (FALSE);
  END_IF;
  IF  'REAL_INTERVAL_FROM_MIN' IN  types1 THEN
    IF  'ELEMENTARY_SPACE' IN  types2 THEN
      es_val := spc2\elementary_space.space_id;
      RETURN  ((es_val = es_numbers) OR  (es_val = es_reals));
    END_IF;
    IF  'REAL_INTERVAL_FROM_MIN' IN  types2 THEN
      bnd1 := spc1\real_interval_from_min.min;
      bnd2 := spc2\real_interval_from_min.min;
      RETURN  ((bnd2 < bnd1) OR  ((bnd2 = bnd1) AND  (min_included (spc2) OR
        NOT  min_included (spc1))));
    END_IF;
    RETURN  (FALSE);
  END_IF;
  IF  'REAL_INTERVAL_TO_MAX' IN  types1 THEN
    IF  'ELEMENTARY_SPACE' IN  types2 THEN
      es_val := spc2\elementary_space.space_id;
      RETURN  ((es_val = es_numbers) OR  (es_val = es_reals));
    END_IF;
    IF  'REAL_INTERVAL_TO_MAX' IN  types2 THEN
      bnd1 := spc1\real_interval_to_max.max;
      bnd2 := spc2\real_interval_to_max.max;
      RETURN  ((bnd2 > bnd1) OR  ((bnd2 = bnd1) AND  (max_included (spc2) OR
        NOT  max_included (spc1))));
    END_IF;
    RETURN  (FALSE);
  END_IF;
  IF  'CARTESIAN_COMPLEX_NUMBER_REGION' IN  types1 THEN
    IF  'ELEMENTARY_SPACE' IN  types2 THEN
      es_val := spc2\elementary_space.space_id;
      RETURN  ((es_val = es_numbers) OR  (es_val = es_complex_numbers));
    END_IF;
    IF  'CARTESIAN_COMPLEX_NUMBER_REGION' IN  types2 THEN
      RETURN  (subspace_of(spc1\cartesian_complex_number_region.real_constraint,
        spc2\cartesian_complex_number_region.real_constraint) AND
        subspace_of(spc1\cartesian_complex_number_region.imag_constraint,
        spc2\cartesian_complex_number_region.imag_constraint));
    END_IF;
    IF  'POLAR_COMPLEX_NUMBER_REGION' IN  types2 THEN
      RETURN  (subspace_of(enclose_cregion_in_pregion(spc1,
        spc2\polar_complex_number_region.centre),spc2));
    END_IF;
    RETURN  (FALSE);
  END_IF;
  IF  'POLAR_COMPLEX_NUMBER_REGION' IN  types1 THEN
    IF  'ELEMENTARY_SPACE' IN  types2 THEN
      es_val := spc2\elementary_space.space_id;
      RETURN  ((es_val = es_numbers) OR  (es_val = es_complex_numbers));
    END_IF;
    IF  'CARTESIAN_COMPLEX_NUMBER_REGION' IN  types2 THEN
      RETURN  (subspace_of(enclose_pregion_in_cregion(spc1),spc2));
    END_IF;
    IF  'POLAR_COMPLEX_NUMBER_REGION' IN  types2 THEN
      prgn1 := spc1;
      prgn2 := spc2;
      IF  prgn1.centre = prgn2.centre THEN
        IF  prgn2.direction_constraint.max > PI THEN
          aitv := make_finite_real_interval(-PI,open,prgn2.direction_constraint.max
            -2.0*PI,prgn2.direction_constraint.max_closure);
          RETURN  (subspace_of(prgn1.distance_constraint,prgn2.distance_constraint)
            AND  (subspace_of(prgn1.direction_constraint,prgn2.direction_constraint)
              OR subspace_of(prgn1.direction_constraint,aitv)));
        ELSE
          RETURN  (subspace_of(prgn1.distance_constraint,prgn2.distance_constraint)
            AND  subspace_of(prgn1.direction_constraint,prgn2.direction_constraint));
        END_IF;
      END_IF;
      RETURN  (subspace_of(enclose_pregion_in_pregion(prgn1,prgn2.centre),prgn2));
    END_IF;
    RETURN  (FALSE);
  END_IF;
  IF  'FINITE_SPACE' IN  types1 THEN
    cum := TRUE;
    REPEAT  i := 1 TO  SIZEOF (spc1\finite_space.members);
      cum := cum AND  member_of (spc1\finite_space.members[i], spc2);
      IF  cum = FALSE  THEN
        RETURN  (FALSE);
      END_IF;
    END_REPEAT;
    RETURN  (cum);
  END_IF;
  IF  'PRODUCT_SPACE' IN  types1 THEN
    IF  'PRODUCT_SPACE' IN  types2 THEN
      IF  space_dimension (spc1) = space_dimension (spc2) THEN
        cum := TRUE;
        REPEAT  i := 1 TO  space_dimension (spc1);
          cum := cum AND  subspace_of (factor_space(spc1,i), factor_space(spc2,i));
          IF  cum = FALSE  THEN
            RETURN  (FALSE);
          END_IF;
        END_REPEAT;
        RETURN  (cum);
      END_IF;
    END_IF;
    IF  'EXTENDED_TUPLE_SPACE' IN  types2 THEN
      IF  space_dimension (spc1) >= space_dimension (spc2) THEN
        cum := TRUE;
        REPEAT  i := 1 TO  space_dimension (spc1);
          cum := cum AND  subspace_of (factor_space(spc1,i), factor_space(spc2,i));
          IF  cum = FALSE  THEN
            RETURN  (FALSE);
          END_IF;
        END_REPEAT;
        RETURN  (cum);
      END_IF;
    END_IF;
    RETURN  (FALSE);
  END_IF;
  IF  'EXTENDED_TUPLE_SPACE' IN  types1 THEN
    IF  'EXTENDED_TUPLE_SPACE' IN  types2 THEN
      n := space_dimension (spc1);
      IF  n < space_dimension (spc2) THEN
        n := space_dimension (spc2);
      END_IF;
      cum := TRUE;
      REPEAT i := 1 TO n+1;
        cum := cum AND  subspace_of (factor_space(spc1,i), factor_space(spc2,i));
        IF  cum = FALSE  THEN
          RETURN  (FALSE);
        END_IF;
      END_REPEAT;
      RETURN  (cum);
    END_IF;
    RETURN  (FALSE);
  END_IF;
  IF  'FUNCTION_SPACE' IN  types1 THEN
    IF  'ELEMENTARY_SPACE' IN  types2 THEN
      RETURN  (spc2\elementary_space.space_id = es_maths_functions);
    END_IF;
    IF  'FUNCTION_SPACE' IN types2 THEN
      cum := TRUE;
      sp1 := spc1\function_space.domain_argument;
      sp2 := spc2\function_space.domain_argument;
      CASE  spc1\function_space.domain_constraint OF
      sc_equal : BEGIN
        CASE  spc2\function_space.domain_constraint OF
        sc_equal : cum := cum AND  equal_maths_spaces (sp1, sp2);
        sc_subspace : cum := cum AND  subspace_of (sp1, sp2);
        sc_member : cum := cum AND  member_of (sp1, sp2);
        END_CASE;
        END;
      sc_subspace : BEGIN
        CASE  spc2\function_space.domain_constraint OF
        sc_equal : RETURN  (FALSE);
        sc_subspace : cum := cum AND  subspace_of (sp1, sp2);
        sc_member : BEGIN
          IF  NOT  member_of (sp1, sp2) THEN
            RETURN  (FALSE);
          END_IF;
          cum := UNKNOWN;
          END;
        END_CASE;
        END;
      sc_member : BEGIN
        CASE  spc2\function_space.domain_constraint OF
        sc_equal : cum := cum AND  space_is_singleton(sp1) AND
          equal_maths_spaces(singleton_member_of(sp1),sp2);
        sc_subspace : BEGIN
          IF  NOT  member_of (sp2, sp1) THEN
            RETURN  (FALSE);
          END_IF;
          cum := UNKNOWN;
          END;
        sc_member : cum := cum AND  (subspace_of (sp1, sp2));
        END_CASE;
        END;
      END_CASE;
      IF  cum = FALSE THEN
        RETURN  (FALSE);
      END_IF;
      sp1 := spc1\function_space.range_argument;
      sp2 := spc2\function_space.range_argument;
      CASE  spc1\function_space.range_constraint OF
      sc_equal : BEGIN
        CASE  spc2\function_space.range_constraint OF
        sc_equal : cum := cum AND  equal_maths_spaces (sp1, sp2);
        sc_subspace : cum := cum AND  subspace_of (sp1, sp2);
        sc_member : cum := cum AND  member_of (sp1, sp2);
        END_CASE;
        END;
      sc_subspace : BEGIN
        CASE  spc2\function_space.domain_constraint OF
        sc_equal : RETURN  (FALSE);
        sc_subspace : cum := cum AND  subspace_of (sp1, sp2);
        sc_member : BEGIN
          IF  NOT  member_of (sp1, sp2) THEN
            RETURN  (FALSE);
          END_IF;
          cum := UNKNOWN;
          END;
        END_CASE;
        END;
      sc_member : BEGIN
        CASE spc2\function_space.domain_constraint OF
        sc_equal : cum := cum AND  space_is_singleton(sp1) AND
          equal_maths_spaces(singleton_member_of(sp1),sp2);
        sc_subspace : BEGIN
          IF NOT member_of (sp2, sp1) THEN
            RETURN  (FALSE);
          END_IF;
          cum := UNKNOWN;
          END;
        sc_member : cum := cum AND subspace_of (sp1, sp2);
        END_CASE;
        END;
      END_CASE;
      RETURN  (cum);
    END_IF;
    RETURN  (FALSE);
  END_IF;
  -- Should be unreachable
  RETURN (UNKNOWN);