LOCAL types1 : SET  OF  STRING  := stripped_typeof ( sp1 ) ; types2 : SET OF  STRING := stripped_typeof ( sp2 ) ; lgcl : LOGICAL := UNKNOWN  ; m , n : INTEGER ; s1 , s2 : maths_space ; END_LOCAL ; IF  'finite_space' IN  types1 THEN  REPEAT  i := 1 TO  SIZEOF  ( sp1 \ finite_space . members ) ; lgcl := member_of ( sp1 \ finite_space . members [ i ] , sp2 ) ; IF  lgcl <> FALSE  THEN  RETURN  ( TRUE  ) ; END_IF  ; END_REPEAT  ; RETURN  ( FALSE  ) ; END_IF  ; IF  'finite_space' IN  types2 THEN  REPEAT  i := 1 TO  SIZEOF  ( sp2 \ finite_space . members ) ; lgcl := member_of ( sp2 \ finite_space . members [ i ] , sp1 ) ; IF  lgcl <> FALSE  THEN  RETURN  ( TRUE  ) ; END_IF  ; END_REPEAT  ; RETURN  ( FALSE  ) ; END_IF  ; IF  'elementary_space' IN  types1 THEN  IF  sp1 \ elementary_space . space_id = es_generics THEN  RETURN  ( TRUE  ) ; END_IF  ; IF  'elementary_space' IN  types2 THEN  RETURN  ( compatible_es_values ( sp1 \ elementary_space . space_id , sp2 \ elementary_space . space_id ) ) ; END_IF  ; IF  ( 'finite_integer_interval' IN  types2 ) OR  ( 'integer_interval_from_min' IN  types2 ) OR  ( 'integer_interval_to_max' IN  types2 ) THEN  RETURN  ( compatible_es_values ( sp1 \ elementary_space . space_id , es_integers ) ) ; END_IF  ; IF  ( 'finite_real_interval' IN  types2 ) OR  ( 'real_interval_from_min' IN  types2 ) OR  ( 'real_interval_to_max' IN  types2 ) THEN  RETURN  ( compatible_es_values ( sp1 \ elementary_space . space_id , es_reals ) ) ; END_IF  ; IF  ( 'cartesian_complex_number_region' IN  types2 ) OR  ( 'polar_complex_number_region' IN  types2 ) THEN  RETURN  ( compatible_es_values ( sp1 \ elementary_space . space_id , es_complex_numbers ) ) ; END_IF  ; IF  'tuple_space' IN  types2 THEN  RETURN  ( FALSE  ) ; END_IF  ; IF  'function_space' IN  types2 THEN  RETURN  ( bool ( sp1 \ elementary_space . space_id = es_maths_functions ) ) ; END_IF  ; RETURN  ( TRUE  ) ; END_IF  ; IF  'elementary_space' IN  types2 THEN  IF  sp2 \ elementary_space . space_id = es_generics THEN  RETURN  ( TRUE  ) ; END_IF  ; IF  ( 'finite_integer_interval' IN  types1 ) OR  ( 'integer_interval_from_min' IN  types1 ) OR  ( 'integer_interval_to_max' IN  types1 ) THEN  RETURN  ( compatible_es_values ( sp2 \ elementary_space . space_id , es_integers ) ) ; END_IF  ; IF  ( 'finite_real_interval' IN  types1 ) OR  ( 'real_interval_from_min' IN  types1 ) OR  ( 'real_interval_to_max' IN  types1 ) THEN  RETURN  ( compatible_es_values ( sp2 \ elementary_space . space_id , es_reals ) ) ; END_IF  ; IF  ( 'cartesian_complex_number_region' IN  types1 ) OR  ( 'polar_complex_number_region' IN  types1 ) THEN  RETURN  ( compatible_es_values ( sp2 \ elementary_space . space_id , es_complex_numbers ) ) ; END_IF  ; IF  'tuple_space' IN  types1 THEN  RETURN  ( FALSE  ) ; END_IF  ; IF  'function_space' IN  types1 THEN  RETURN  ( bool ( sp2 \ elementary_space . space_id = es_maths_functions ) ) ; END_IF  ; RETURN  ( TRUE  ) ; END_IF  ; IF  subspace_of_es ( sp1 , es_integers ) THEN  IF  subspace_of_es ( sp2 , es_integers ) THEN  RETURN  ( compatible_intervals ( sp1 , sp2 ) ) ; END_IF  ; RETURN  ( FALSE  ) ; END_IF  ; IF  subspace_of_es ( sp2 , es_integers ) THEN  RETURN  ( FALSE  ) ; END_IF  ; IF  subspace_of_es ( sp1 , es_reals ) THEN  IF  subspace_of_es ( sp2 , es_reals ) THEN  RETURN  ( compatible_intervals ( sp1 , sp2 ) ) ; END_IF  ; RETURN  ( FALSE  ) ; END_IF  ; IF  subspace_of_es ( sp2 , es_reals ) THEN  RETURN  ( FALSE  ) ; END_IF  ; IF  subspace_of_es ( sp1 , es_complex_numbers ) THEN  IF  subspace_of_es ( sp2 , es_complex_numbers ) THEN  RETURN  ( compatible_complex_number_regions ( sp1 , sp2 ) ) ; END_IF  ; RETURN  ( FALSE  ) ; END_IF  ; IF  subspace_of_es ( sp2 , es_complex_numbers ) THEN  RETURN  ( FALSE  ) ; END_IF  ; IF  'uniform_product_space' IN  types1 THEN  IF  'uniform_product_space' IN  types2 THEN  IF  sp1 \ uniform_product_space . exponent <> sp2 \ uniform_product_space . exponent THEN  RETURN  ( FALSE  ) ; END_IF  ; RETURN  ( compatible_spaces ( sp1 \ uniform_product_space . base , sp2 \ uniform_product_space . base ) ) ; END_IF  ; IF  'listed_product_space' IN  types2 THEN  n := SIZEOF  ( sp2 \ listed_product_space . factors ) ; IF  sp1 \ uniform_product_space . exponent <> n THEN  RETURN  ( FALSE  ) ; END_IF  ; REPEAT  i := 1 TO  n ; IF  NOT  compatible_spaces ( sp1 \ uniform_product_space . base , sp2 \ listed_product_space . factors [ i ] ) THEN  RETURN  ( FALSE  ) ; END_IF  ; END_REPEAT  ; RETURN  ( TRUE  ) ; END_IF  ; IF  'extended_tuple_space' IN  types2 THEN  m := sp1 \ uniform_product_space . exponent ; n := space_dimension ( sp2 \ extended_tuple_space . base ) ; IF  m < n THEN  RETURN  ( FALSE  ) ; END_IF  ; IF  m = n THEN  RETURN  ( compatible_spaces ( sp1 , sp2 \ extended_tuple_space . base ) ) ; END_IF  ; RETURN  ( compatible_spaces ( sp1 , assoc_product_space ( sp2 \ extended_tuple_space . base , make_uniform_product_space ( sp2 \ extended_tuple_space . extender , m - n ) ) ) ) ; END_IF  ; IF  'function_space' IN  types2 THEN  RETURN  ( FALSE  ) ; END_IF  ; RETURN  ( TRUE  ) ; END_IF  ; IF  'listed_product_space' IN  types1 THEN  n := SIZEOF  ( sp1 \ listed_product_space . factors ) ; IF  'uniform_product_space' IN  types2 THEN  IF  n <> sp2 \ uniform_product_space . exponent THEN  RETURN  ( FALSE  ) ; END_IF  ; REPEAT  i := 1 TO  n ; IF  NOT  compatible_spaces ( sp2 \ uniform_product_space . base , sp1 \ listed_product_space . factors [ i ] ) THEN  RETURN  ( FALSE  ) ; END_IF  ; END_REPEAT  ; RETURN  ( TRUE  ) ; END_IF  ; IF  'listed_product_space' IN  types2 THEN  IF  n <> SIZEOF ( sp2 \ listed_product_space . factors ) THEN  RETURN  ( FALSE  ) ; END_IF  ; REPEAT i := 1 TO n ; IF  NOT  compatible_spaces ( sp1 \ listed_product_space . factors [ i ] , sp2 \ listed_product_space . factors [ i ] ) THEN  RETURN  ( FALSE  ) ; END_IF  ; END_REPEAT ; RETURN  ( TRUE  ) ; END_IF  ; IF  'extended_tuple_space' IN  types2 THEN  m := space_dimension ( sp2 \ extended_tuple_space . base ) ; IF  n < m THEN  RETURN  ( FALSE  ) ; END_IF  ; IF  n = m THEN  RETURN  ( compatible_spaces ( sp1 , sp2 \ extended_tuple_space . base ) ) ; END_IF  ; RETURN  ( compatible_spaces ( sp1 , assoc_product_space ( sp2 \ extended_tuple_space . base , make_uniform_product_space ( sp2 \ extended_tuple_space . extender , n - m ) ) ) ) ; END_IF  ; IF  ( schema_prefix + 'function_space' ) IN  types2 THEN  RETURN  ( FALSE  ) ; END_IF  ; RETURN  ( TRUE  ) ; END_IF  ; IF  'extended_tuple_space' IN  types1 THEN  IF  ( 'uniform_product_space' IN  types2 ) OR ( 'listed_product_space' IN  types2 ) THEN  RETURN  ( compatible_spaces ( sp2 , sp1 ) ) ; END_IF  ; IF  'extended_tuple_space' IN  types2 THEN  IF  NOT compatible_spaces ( sp1 \ extended_tuple_space . extender , sp2 \ extended_tuple_space . extender ) THEN  RETURN  ( FALSE  ) ; END_IF  ; n := space_dimension ( sp1 \ extended_tuple_space . base ) ; m := space_dimension ( sp2 \ extended_tuple_space . base ) ; IF  n < m THEN  RETURN  ( compatible_spaces ( assoc_product_space ( sp1 \ extended_tuple_space . base , make_uniform_product_space ( sp1 \ extended_tuple_space . extender , m - n ) ) , sp2 \ extended_tuple_space . base ) ) ; END_IF  ; IF  n = m THEN  RETURN  ( compatible_spaces ( sp1 \ extended_tuple_space . base , sp2 \ extended_tuple_space . base ) ) ; END_IF  ; IF  n > m THEN  RETURN  ( compatible_spaces ( sp1 \ extended_tuple_space . base , assoc_product_space ( sp2 \ extended_tuple_space . base , make_uniform_product_space ( sp2 \ extended_tuple_space . extender , n - m ) ) ) ) ; END_IF  ; END_IF  ; IF  'function_space' IN  types2 THEN  RETURN  ( FALSE  ) ; END_IF  ; RETURN  ( TRUE  ) ; END_IF  ; IF  'function_space' IN  types1 THEN  IF  'function_space' IN types2 THEN  s1 := sp1 \ function_space . domain_argument ; s2 := sp2 \ function_space . domain_argument ; CASE  sp1 \ function_space . domain_constraint OF  sc_equal : BEGIN  CASE  sp2 \ function_space . domain_constraint OF  sc_equal : lgcl := subspace_of ( s1 , s2 ) AND  subspace_of ( s2 , s1 ) ; sc_subspace : lgcl := subspace_of ( s1 , s2 ) ; sc_member : lgcl := member_of ( s1 , s2 ) ; END_CASE  ; END  ; sc_subspace : BEGIN  CASE  sp2 \ function_space . domain_constraint OF  sc_equal : lgcl := subspace_of ( s2 , s1 ) ; sc_subspace : lgcl := compatible_spaces ( s1 , s2 ) ; sc_member : lgcl := UNKNOWN  ; END_CASE  ; END  ; sc_member : BEGIN  CASE  sp2 \ function_space . domain_constraint OF  sc_equal : lgcl := member_of ( s2 , s1 ) ; sc_subspace : lgcl := UNKNOWN  ; sc_member : lgcl := compatible_spaces ( s1 , s2 ) ; END_CASE  ; END  ; END_CASE  ; IF  lgcl = FALSE  THEN  RETURN  ( FALSE  ) ; END_IF  ; s1 := sp1 \ function_space . range_argument ; s2 := sp2 \ function_space . range_argument ; CASE  sp1 \ function_space . range_constraint OF  sc_equal : BEGIN  CASE  sp2 \ function_space . range_constraint OF  sc_equal : lgcl := subspace_of ( s1 , s2 ) AND subspace_of ( s2 , s1 ) ; sc_subspace : lgcl := subspace_of ( s1 , s2 ) ; sc_member : lgcl := member_of ( s1 , s2 ) ; END_CASE  ; END  ; sc_subspace : BEGIN  CASE  sp2 \ function_space . range_constraint OF  sc_equal : lgcl := subspace_of ( s2 , s1 ) ; sc_subspace : lgcl := compatible_spaces ( s1 , s2 ) ; sc_member : lgcl := UNKNOWN  ; END_CASE  ; END  ; sc_member : BEGIN CASE sp2 \ function_space . range_constraint OF sc_equal : lgcl := member_of ( s2 , s1 ) ; sc_subspace : lgcl := UNKNOWN ; sc_member : lgcl := compatible_spaces ( s1 , s2 ) ; END_CASE  ; END ; END_CASE ; IF lgcl = FALSE  THEN RETURN  ( FALSE ) ; END_IF  ; RETURN  ( TRUE  ) ; END_IF  ; RETURN  ( TRUE  ) ; END_IF ; RETURN ( TRUE ) ;