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  ; 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  ; 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 ; RETURN ( UNKNOWN ) ;