Schema: mathematical_functions_schema

Source : ISO 10303-50



SCHEMA mathematical_functions_schema;

REFERENCE FROM ISO13584_generic_expressions_schema   -- ISO 13584-20
  (binary_generic_expression,
   environment,
   generic_expression,
   generic_literal,
   generic_variable,
   multiple_arity_generic_expression,
   simple_generic_expression,
   unary_generic_expression,
   variable_semantics);

REFERENCE FROM ISO13584_expressions_schema   -- ISO 13584-20
  (abs_function AS abs_expression,
   acos_function AS acos_expression,
   and_expression,
   asin_function AS asin_expression,
   atan_function AS atan_expression,
   binary_boolean_expression,
   binary_function_call AS binary_numeric_call_expression,
   binary_numeric_expression,
   boolean_defined_function AS boolean_defined_expression,
   boolean_expression,
   boolean_literal,
   boolean_variable,
   comparison_equal,
   comparison_expression,
   comparison_greater,
   comparison_greater_equal,
   comparison_less,
   comparison_less_equal,
   comparison_not_equal,
   concat_expression,
   cos_function AS cos_expression,
   defined_function AS defined_expression,
   div_expression,
   equals_expression,
   exp_function AS exp_expression,
   expression,
   format_function AS format_expression,
   index_expression,
   int_literal,
   int_numeric_variable,
   int_value_function AS int_value_expression,
   integer_defined_function AS integer_defined_expression,
   interval_expression,
   length_function AS length_expression,
   like_expression,
   literal_number,
   log_function AS log_expression,
   log10_function AS log10_expression,
   log2_function AS log2_expression,
   maximum_function AS maximum_expression,
   minimum_function AS minimum_expression,
   minus_expression,
   minus_function AS unary_minus_expression,
   mod_expression,
   mult_expression,
   multiple_arity_boolean_expression,
   multiple_arity_function_call AS multiple_arity_numeric_call_expression,
   multiple_arity_numeric_expression,
   not_expression,
   numeric_defined_function AS numeric_defined_expression,
   numeric_expression,
   numeric_variable,
   odd_function AS odd_expression,
   or_expression,
   plus_expression,
   power_expression,
   real_defined_function AS real_defined_expression,
   real_literal,
   real_numeric_variable,
   simple_boolean_expression,
   simple_numeric_expression,
   simple_string_expression,
   sin_function AS sin_expression,
   slash_expression,
   sql_mappable_defined_function AS sql_mappable_defined_expression,
   square_root_function AS square_root_expression,
   string_defined_function AS string_defined_expression,
   string_expression,
   string_literal,
   string_variable,
   substring_expression,
   tan_function AS tan_expression,
   unary_boolean_expression,
   unary_function_call AS unary_numeric_call_expression,
   unary_numeric_expression,
   value_function AS value_expression,
   variable,
   xor_expression);

REFERENCE FROM support_resource_schema   -- ISO 10303-41
  (label,
   text);

REFERENCE FROM external_reference_schema   -- ISO 10303-41
  (externally_defined_item);

REFERENCE FROM geometry_schema   -- ISO 10303-42
  (curve,
   dimension_of,
   point,
   surface,
   volume);


CONSTANT
  schema_prefix : := STRING := 'MATHEMATICAL_FUNCTIONS_SCHEMA.';;

  the_integers : := elementary_space := make_elementary_space(es_integers);;

  the_reals : := elementary_space := make_elementary_space(es_reals);;

  the_complex_numbers : := elementary_space := make_elementary_space(es_complex_numbers);;

  the_numbers : := elementary_space := make_elementary_space(es_numbers);;

  the_logicals : := elementary_space := make_elementary_space(es_logicals);;

  the_booleans : := elementary_space := make_elementary_space(es_booleans);;

  the_strings : := elementary_space := make_elementary_space(es_strings);;

  the_binarys : := elementary_space := make_elementary_space(es_binarys);;

  the_maths_spaces : := elementary_space := make_elementary_space(es_maths_spaces);;

  the_generics : := elementary_space := make_elementary_space(es_generics);;

  the_empty_space : := finite_space := make_finite_space([]);;

  the_nonnegative_reals : := real_interval_from_min := make_real_interval_from_min(0.0, closed);;

  the_zero_one_interval : := finite_real_interval := make_finite_real_interval( 0.0, closed, 1.0, closed);;

  the_zero_pi_interval : := finite_real_interval := make_finite_real_interval( 0.0, closed, pi, closed);;

  the_neg1_one_interval : := finite_real_interval := make_finite_real_interval( -1.0, closed, 1.0, closed);;

  the_neghalfpi_halfpi_interval : := finite_real_interval := make_finite_real_interval( -0.5*pi, closed, 0.5*pi, closed);;

  the_negpi_pi_interval : := finite_real_interval := make_finite_real_interval( -pi, open, pi, closed);;

  the_zero_tuple_space : := listed_product_space := make_listed_product_space([]);;

  the_tuples : := extended_tuple_space := make_extended_tuple_space( the_zero_tuple_space, the_generics);;

  the_integer_tuples : := extended_tuple_space := make_extended_tuple_space( the_zero_tuple_space, the_integers);;

  the_real_tuples : := extended_tuple_space := make_extended_tuple_space( the_zero_tuple_space, the_reals);;

  the_complex_tuples : := extended_tuple_space := make_extended_tuple_space( the_zero_tuple_space, the_complex_numbers);;

  the_empty_maths_tuple : := maths_tuple := [];;

  the_empty_maths_value : := maths_value := the_empty_maths_tuple;;

  the_empty_atom_based_tuple : := atom_based_tuple := [];;

  the_empty_atom_based_value : := atom_based_value := the_empty_atom_based_tuple;;

  cnlit : := STRING := schema_prefix + 'COMPLEX_NUMBER_LITERAL';;
END_CONSTANT;

TYPE nonnegative_integer = INTEGER ;
WHERE
  nonnegativity: SELF >= 0;
END_TYPE;

TYPE positive_integer = nonnegative_integer ;
WHERE
  positivity: SELF > 0;
END_TYPE;

TYPE zero_or_one = nonnegative_integer ;
WHERE
  in_range: (SELF = 0) OR (SELF = 1);
END_TYPE;

TYPE one_or_two = positive_integer ;
WHERE
  in_range: (SELF = 1) OR (SELF = 2);
END_TYPE;

TYPE maths_number = NUMBER;
END_TYPE;

TYPE maths_real = REAL;
END_TYPE;

TYPE maths_integer = INTEGER;
END_TYPE;

TYPE maths_logical = LOGICAL;
END_TYPE;

TYPE maths_boolean = BOOLEAN;
END_TYPE;

TYPE maths_string = STRING;
END_TYPE;

TYPE maths_binary = BINARY;
END_TYPE;

TYPE maths_simple_atom = SELECT
   (maths_number,
    maths_real,
    maths_number,
    maths_logical,
    maths_boolean,
    maths_string,
    maths_binary);
END_TYPE;

TYPE maths_atom = SELECT
   (maths_simple_atom,
    maths_enum_atom);
END_TYPE;

TYPE atom_based_tuple = LIST OF atom_based_value;
END_TYPE;

TYPE atom_based_value = SELECT
   (maths_atom,
    atom_based_tuple);
END_TYPE;

TYPE maths_tuple = LIST[0:?] OF maths_value;
END_TYPE;

TYPE maths_value = SELECT
   (atom_based_value,
    maths_tuple,
    generic_expression) ;
WHERE
  constancy: NOT ('GENERIC_EXPRESSION' IN stripped_typeof(SELF)) OR expression_is_constant(SELF);
END_TYPE;

TYPE maths_expression = SELECT
   (atom_based_value,
    maths_tuple,
    generic_expression);
END_TYPE;

TYPE maths_function_select = SELECT
   (maths_function,
    elementary_function_enumerators);
END_TYPE;

TYPE input_selector = positive_integer;
END_TYPE;

TYPE elementary_space_enumerators = ENUMERATION OF
   (es_numbers,
    es_complex_numbers,
    es_reals,
    es_integers,
    es_logicals,
    es_booleans,
    es_strings,
    es_binarys,
    es_maths_spaces,
    es_maths_functions,
    es_generics);
END_TYPE;

TYPE ordering_type = ENUMERATION OF
   (by_rows,
    by_columns);
END_TYPE;

TYPE lower_upper = ENUMERATION OF
   (lower,
    upper);
END_TYPE;

TYPE symmetry_type = ENUMERATION OF
   (identity,
    skew,
    hermitian,
    skew_hermitian);
END_TYPE;

TYPE elementary_function_enumerators = ENUMERATION OF
   (ef_and,
    ef_or,
    ef_not,
    ef_xor,
    ef_negate_i,
    ef_add_i,
    ef_subtract_i,
    ef_multiply_i,
    ef_divide_i,
    ef_mod_i,
    ef_exponentiate_i,
    ef_eq_i,
    ef_ne_i,
    ef_gt_i,
    ef_lt_i,
    ef_ge_i,
    ef_le_i,
    ef_abs_i,
    ef_max_i,
    ef_min_i,
    ef_if_i,
    ef_negate_r,
    ef_reciprocal_r,
    ef_add_r,
    ef_subtract_r,
    ef_multiply_r,
    ef_divide_r,
    ef_mod_r,
    ef_exponentiate_r,
    ef_exponentiate_ri,
    ef_eq_r,
    ef_ne_r,
    ef_gt_r,
    ef_lt_r,
    ef_ge_r,
    ef_le_r,
    ef_abs_r,
    ef_max_r,
    ef_min_r,
    ef_acos_r,
    ef_asin_r,
    ef_atan2_r,
    ef_cos_r,
    ef_exp_r,
    ef_ln_r,
    ef_log2_r,
    ef_log10_r,
    ef_sin_r,
    ef_sqrt_r,
    ef_tan_r,
    ef_if_r,
    ef_form_c,
    ef_rpart_c,
    ef_ipart_c,
    ef_negate_c,
    ef_reciprocal_c,
    ef_add_c,
    ef_subtract_c,
    ef_multiply_c,
    ef_divide_c,
    ef_exponentiate_c,
    ef_exponentiate_ci,
    ef_eq_c,
    ef_ne_c,
    ef_conjugate_c,
    ef_abs_c,
    ef_arg_c,
    ef_cos_c,
    ef_exp_c,
    ef_ln_c,
    ef_sin_c,
    ef_sqrt_c,
    ef_tan_c,
    ef_if_c,
    ef_subscript_s,
    ef_eq_s,
    ef_ne_s,
    ef_gt_s,
    ef_lt_s,
    ef_ge_s,
    ef_le_s,
    ef_subsequence_s,
    ef_concat_s,
    ef_size_s,
    ef_format,
    ef_value,
    ef_like,
    ef_if_s,
    ef_subscript_b,
    ef_eq_b,
    ef_ne_b,
    ef_gt_b,
    ef_lt_b,
    ef_ge_b,
    ef_le_b,
    ef_subsequence_b,
    ef_concat_b,
    ef_size_b,
    ef_if_b,
    ef_subscript_t,
    ef_eq_t,
    ef_ne_t,
    ef_concat_t,
    ef_size_t,
    ef_entuple,
    ef_detuple,
    ef_insert,
    ef_remove,
    ef_if_t,
    ef_sum_it,
    ef_product_it,
    ef_add_it,
    ef_subtract_it,
    ef_scalar_mult_it,
    ef_dot_prod_it,
    ef_sum_rt,
    ef_product_rt,
    ef_add_rt,
    ef_subtract_rt,
    ef_scalar_mult_rt,
    ef_dot_prod_rt,
    ef_norm_rt,
    ef_sum_ct,
    ef_product_ct,
    ef_add_ct,
    ef_subtract_ct,
    ef_scalar_mult_ct,
    ef_dot_prod_ct,
    ef_norm_ct,
    ef_if,
    ef_ensemble,
    ef_member_of);
END_TYPE;

TYPE open_closed = ENUMERATION OF
   (open,
    closed);
END_TYPE;

TYPE space_constraint_type = ENUMERATION OF
   (sc_equal,
    sc_subspace,
    sc_member);
END_TYPE;

TYPE repackage_options = ENUMERATION OF
   (ro_nochange,
    ro_wrap_as_tuple,
    ro_unwrap_tuple);
END_TYPE;

TYPE extension_options = ENUMERATION OF
   (eo_none,
    eo_cont,
    eo_cont_right,
    eo_cont_left);
END_TYPE;

TYPE maths_enum_atom = SELECT
   (elementary_space_enumerators,
    ordering_type,
    lower_upper,
    symmetry_type,
    elementary_function_enumerators,
    open_closed,
    space_constraint_type,
    repackage_options,
    extension_options);
END_TYPE;

TYPE dotted_express_identifier = STRING ;
WHERE
  syntax: dotted_identifiers_syntax(SELF);
END_TYPE;

TYPE express_identifier = dotted_express_identifier ;
WHERE
  syntax: dot_count(SELF) = 0;
END_TYPE;

TYPE product_space = SELECT
   (uniform_product_space,
    listed_product_space);
END_TYPE;

TYPE tuple_space = SELECT
   (product_space,
    extended_tuple_space);
END_TYPE;

TYPE maths_space_or_function = SELECT
   (maths_space,
    maths_function);
END_TYPE;

TYPE real_interval = SELECT
   (real_interval_from_min,
    real_interval_to_max,
    finite_real_interval,
    elementary_space) ;
WHERE
  WR1: NOT ('ELEMENTARY_SPACE' IN stripped_typeof(SELF)) OR (SELF\elementary_space.space_id = es_reals);
END_TYPE;

ENTITY quantifier_expression
  ABSTRACT SUPERTYPE
  SUBTYPE OF (multiple_arity_generic_expression);
  variables : LIST[1:?] OF UNIQUE generic_variable;
WHERE
  WR1: SIZEOF (QUERY (vrbl <* variables | NOT (vrbl IN SELF\multiple_arity_generic_expression.operands))) = 0;
  WR2: SIZEOF (QUERY (vrbl <* variables | NOT ((schema_prefix + 'BOUND_VARIABLE_SEMANTICS') IN TYPEOF (vrbl.interpretation.semantics)))) = 0;
END_ENTITY;

ENTITY dependent_variable_definition
  SUBTYPE OF (unary_generic_expression);
  name : label;
  description : text;
END_ENTITY;

ENTITY bound_variable_semantics
  SUBTYPE OF (variable_semantics);
END_ENTITY;

ENTITY free_variable_semantics
  SUBTYPE OF (variable_semantics);
END_ENTITY;

ENTITY complex_number_literal
  SUBTYPE OF (generic_literal);
  real_part : REAL;
  imag_part : REAL;
END_ENTITY;

ENTITY logical_literal
  SUBTYPE OF (generic_literal);
  lit_value : LOGICAL;
END_ENTITY;

ENTITY binary_literal
  SUBTYPE OF (generic_literal);
  lit_value : BINARY;
END_ENTITY;

ENTITY maths_enum_literal
  SUBTYPE OF (generic_literal);
  lit_value : maths_enum_atom;
END_ENTITY;

ENTITY real_tuple_literal
  SUBTYPE OF (generic_literal);
  lit_value : LIST[1:?] OF REAL;
END_ENTITY;

ENTITY integer_tuple_literal
  SUBTYPE OF (generic_literal);
  lit_value : LIST[1:?] OF INTEGER;
END_ENTITY;

ENTITY atom_based_literal
  SUBTYPE OF (generic_literal);
  lit_value : atom_based_value;
END_ENTITY;

ENTITY maths_tuple_literal
  SUBTYPE OF (generic_literal);
  lit_value : LIST OF maths_value;
END_ENTITY;

ENTITY maths_variable
  SUBTYPE OF (generic_variable);
  values_space : maths_space;
  name : label;
WHERE
  WR1: expression_is_constant(values_space);
END_ENTITY;

ENTITY maths_real_variable
  SUBTYPE OF (maths_variable, real_numeric_variable);
WHERE
  WR1: subspace_of_es(SELF\maths_variable.values_space,es_reals);
END_ENTITY;

ENTITY maths_integer_variable
  SUBTYPE OF (maths_variable, int_numeric_variable);
WHERE
  WR1: subspace_of_es(SELF\maths_variable.values_space,es_integers);
END_ENTITY;

ENTITY maths_boolean_variable
  SUBTYPE OF (maths_variable, boolean_variable);
WHERE
  WR1: subspace_of_es(SELF\maths_variable.values_space,es_booleans);
END_ENTITY;

ENTITY maths_string_variable
  SUBTYPE OF (maths_variable, string_variable);
WHERE
  WR1: subspace_of_es(SELF\maths_variable.values_space,es_strings);
END_ENTITY;

ENTITY function_application
  SUBTYPE OF (multiple_arity_generic_expression);
  func : maths_function_select;
  arguments : LIST[1:?] OF maths_expression;
DERIVE
  SELF\multiple_arity_generic_expression.operands : LIST[2:?] OF generic_expression := [convert_to_maths_function(func)] + convert_to_operands(arguments);
WHERE
  WR1: function_applicability(func, arguments);
END_ENTITY;

ENTITY maths_space
  ABSTRACT SUPERTYPE OF (ONEOF (elementary_space,
                                finite_integer_interval,
                                integer_interval_from_min,
                                integer_interval_to_max,
                                finite_real_interval,
                                real_interval_from_min,
                                real_interval_to_max,
                                cartesian_complex_number_region,
                                polar_complex_number_region,
                                finite_space,
                                uniform_product_space,
                                listed_product_space,
                                extended_tuple_space,
                                function_space))
  SUBTYPE OF (generic_expression);
END_ENTITY;

ENTITY elementary_space
  SUBTYPE OF (maths_space, generic_literal);
  space_id : elementary_space_enumerators;
END_ENTITY;

ENTITY finite_integer_interval
  SUBTYPE OF (maths_space, generic_literal);
  min : INTEGER;
  max : INTEGER;
DERIVE
  size : positive_integer := max - min + 1;
WHERE
  WR1: min <= max;
END_ENTITY;

ENTITY integer_interval_from_min
  SUBTYPE OF (maths_space, generic_literal);
  min : INTEGER;
END_ENTITY;

ENTITY integer_interval_to_max
  SUBTYPE OF (maths_space, generic_literal);
  max : INTEGER;
END_ENTITY;

ENTITY finite_real_interval
  SUBTYPE OF (maths_space, generic_literal);
  min : REAL;
  min_closure : open_closed;
  max : REAL;
  max_closure : open_closed;
WHERE
  WR1: min < max;
END_ENTITY;

ENTITY real_interval_from_min
  SUBTYPE OF (maths_space, generic_literal);
  min : REAL;
  min_closure : open_closed;
END_ENTITY;

ENTITY real_interval_to_max
  SUBTYPE OF (maths_space, generic_literal);
  max : REAL;
  max_closure : open_closed;
END_ENTITY;

ENTITY cartesian_complex_number_region
  SUBTYPE OF (maths_space, generic_literal);
  real_constraint : real_interval;
  imag_constraint : real_interval;
WHERE
  WR1: min_exists(real_constraint) OR max_exists(real_constraint) OR min_exists(imag_constraint) OR max_exists(imag_constraint);
END_ENTITY;

ENTITY polar_complex_number_region
  SUBTYPE OF (maths_space, generic_literal);
  centre : complex_number_literal;
  distance_constraint : real_interval;
  direction_constraint : finite_real_interval;
WHERE
  WR1: min_exists(distance_constraint) AND (real_min(distance_constraint) >= 0.0);
  WR2: {-PI <= direction_constraint.min < PI};
  WR3: direction_constraint.max - direction_constraint.min <= 2.0*PI;
  WR4: (direction_constraint.max - direction_constraint.min < 2.0*PI) OR (direction_constraint.min_closure = open);
  WR5: (direction_constraint.max - direction_constraint.min < 2.0*PI) OR (direction_constraint.max_closure = open) OR (direction_constraint.min = -PI);
  WR6: (real_min(distance_constraint) > 0.0) OR max_exists(distance_constraint) OR (direction_constraint.max - direction_constraint.min < 2.0*PI) OR (direction_constraint.max_closure = open);
END_ENTITY;

ENTITY finite_space
  SUBTYPE OF (maths_space, generic_literal);
  members : SET OF maths_value;
WHERE
  WR1: VALUE_UNIQUE(members);
  WR2: SIZEOF (QUERY (expr <* QUERY (member <* members | 'ISO13584_GENERIC_EXPRESSIONS_SCHEMA.GENERIC_EXPRESSION' IN TYPEOF (member)) | NOT expression_is_constant(expr))) = 0;
  WR3: no_cyclic_space_reference(SELF, []);
END_ENTITY;

ENTITY uniform_product_space
  SUBTYPE OF (maths_space, generic_literal);
  base : maths_space;
  exponent : positive_integer;
WHERE
  WR1: expression_is_constant(base);
  WR2: no_cyclic_space_reference(SELF, []);
  WR3: base <> the_empty_space;
END_ENTITY;

ENTITY listed_product_space
  SUBTYPE OF (maths_space, generic_literal);
  factors : LIST OF maths_space;
WHERE
  WR1: SIZEOF (QUERY (space <* factors | NOT (expression_is_constant(space)))) = 0;
  WR2: no_cyclic_space_reference(SELF, []);
  WR3: NOT (the_empty_space IN factors);
END_ENTITY;

ENTITY extended_tuple_space
  SUBTYPE OF (maths_space, generic_literal);
  base : product_space;
  extender : maths_space;
WHERE
  WR1: expression_is_constant(base) AND expression_is_constant(extender);
  WR2: no_cyclic_space_reference(SELF, []);
  WR3: extender <> the_empty_space;
END_ENTITY;

ENTITY function_space
  SUBTYPE OF (maths_space, generic_literal);
  domain_constraint : space_constraint_type;
  domain_argument : maths_space;
  range_constraint : space_constraint_type;
  range_argument : maths_space;
WHERE
  WR1: expression_is_constant(domain_argument) AND expression_is_constant(range_argument);
  WR2: (domain_argument <> the_empty_space) AND (range_argument <> the_empty_space);
  WR3: (domain_constraint <> sc_member) OR NOT member_of(the_empty_space,domain_argument);
  WR4: (range_constraint <> sc_member) OR NOT member_of(the_empty_space,range_argument);
  WR5: NOT (any_space_satisfies(domain_constraint,domain_argument) AND any_space_satisfies(range_constraint,range_argument));
END_ENTITY;

ENTITY maths_function
  ABSTRACT SUPERTYPE OF (ONEOF (finite_function,
                                constant_function,
                                selector_function,
                                elementary_function,
                                restriction_function,
                                repackaging_function,
                                reindexed_array_function,
                                series_composed_function,
                                parallel_composed_function,
                                explicit_table_function,
                                homogeneous_linear_function,
                                general_linear_function,
                                b_spline_basis,
                                b_spline_function,
                                rationalize_function,
                                partial_derivative_function,
                                definite_integral_function,
                                abstracted_expression_function,
                                expression_denoted_function,
                                imported_point_function,
                                imported_curve_function,
                                imported_surface_function,
                                imported_volume_function,
                                application_defined_function))
  SUBTYPE OF (generic_expression);
DERIVE
  domain : tuple_space := derive_function_domain(SELF);
  range : tuple_space := derive_function_range(SELF);
END_ENTITY;

ENTITY finite_function
  SUBTYPE OF (maths_function, generic_literal);
  pairs : SET[1:?] OF LIST;
WHERE
  WR1: VALUE_UNIQUE(list_selected_components(pairs, 1));
END_ENTITY;

ENTITY constant_function
  SUBTYPE OF (maths_function, generic_literal);
  sole_output : maths_value;
  source_of_domain : maths_space_or_function;
WHERE
  WR1: no_cyclic_domain_reference(source_of_domain, [SELF]);
  WR2: expression_is_constant(domain_from(source_of_domain));
END_ENTITY;

ENTITY selector_function
  SUBTYPE OF (maths_function, generic_literal);
  selector : input_selector;
  source_of_domain : maths_space_or_function;
WHERE
  WR1: no_cyclic_domain_reference(source_of_domain, [SELF]);
  WR2: expression_is_constant(domain_from(source_of_domain));
END_ENTITY;

ENTITY elementary_function
  SUBTYPE OF (maths_function, generic_literal);
  func_id : elementary_function_enumerators;
END_ENTITY;

ENTITY restriction_function
  SUBTYPE OF (maths_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_space;
END_ENTITY;

ENTITY repackaging_function
  SUBTYPE OF (maths_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_function;
  input_repack : repackage_options;
  output_repack : repackage_options;
  selected_output : nonnegative_integer;
WHERE
  WR1: (input_repack <> ro_wrap_as_tuple) OR ((space_dimension(operand.domain) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN TYPEOF (factor1(operand.domain))));
  WR2: (output_repack <> ro_unwrap_tuple) OR ((space_dimension(operand.range) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN TYPEOF (factor1(operand.range))));
  WR3: selected_output <= space_dimension( repackage( operand.range, output_repack));
END_ENTITY;

ENTITY reindexed_array_function
  SUBTYPE OF (maths_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_function;
  starting_indices : LIST[1:?] OF INTEGER;
WHERE
  WR1: function_is_array(SELF\unary_generic_expression.operand);
  WR2: SIZEOF(starting_indices) = SIZEOF(shape_of_array( SELF\unary_generic_expression.operand));
END_ENTITY;

ENTITY series_composed_function
  SUBTYPE OF (maths_function, multiple_arity_generic_expression);
  SELF\multiple_arity_generic_expression.operands : LIST[2:?] OF maths_function;
WHERE
  WR1: composable_sequence(SELF\multiple_arity_generic_expression.operands);
END_ENTITY;

ENTITY parallel_composed_function
  SUBTYPE OF (maths_function, multiple_arity_generic_expression);
  source_of_domain : maths_space_or_function;
  prep_functions : LIST[1:?] OF maths_function;
  final_function : maths_function_select;
DERIVE
  SELF\multiple_arity_generic_expression.operands : LIST[2:?] OF generic_expression := convert_to_operands_prcmfn(source_of_domain, prep_functions, final_function);
WHERE
  WR1: no_cyclic_domain_reference(source_of_domain, [SELF]);
  WR2: expression_is_constant(domain_from(source_of_domain));
  WR3: parallel_composed_function_domain_check(domain_from(source_of_domain), prep_functions);
  WR4: parallel_composed_function_composability_check(prep_functions, final_function);
END_ENTITY;

ENTITY explicit_table_function
  ABSTRACT SUPERTYPE OF (ONEOF (listed_real_data,
                                listed_integer_data,
                                listed_logical_data,
                                listed_string_data,
                                listed_complex_number_data,
                                listed_data,
                                externally_listed_data,
                                linearized_table_function,
                                basic_sparse_matrix))
  SUBTYPE OF (maths_function);
  index_base : zero_or_one;
  shape : LIST[1:?] OF positive_integer;
END_ENTITY;

ENTITY listed_real_data
  SUBTYPE OF (explicit_table_function, generic_literal);
  values : LIST[1:?] OF REAL;
DERIVE
  self\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
END_ENTITY;

ENTITY listed_integer_data
  SUBTYPE OF (explicit_table_function, generic_literal);
  values : LIST[1:?] OF INTEGER;
DERIVE
  self\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
END_ENTITY;

ENTITY listed_logical_data
  SUBTYPE OF (explicit_table_function, generic_literal);
  values : LIST[1:?] OF LOGICAL;
DERIVE
  self\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
END_ENTITY;

ENTITY listed_string_data
  SUBTYPE OF (explicit_table_function, generic_literal);
  values : LIST[1:?] OF STRING;
DERIVE
  self\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
END_ENTITY;

ENTITY listed_complex_number_data
  SUBTYPE OF (explicit_table_function, generic_literal);
  values : LIST[2:?] OF REAL;
DERIVE
  self\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)/2];
WHERE
  WR1: NOT ODD (SIZEOF (values));
END_ENTITY;

ENTITY listed_data
  SUBTYPE OF (explicit_table_function, generic_literal);
  values : LIST[1:?] OF maths_value;
  value_range : maths_space;
DERIVE
  SELF\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
WHERE
  WR1: expression_is_constant(value_range);
  WR2: SIZEOF (QUERY (val <* values | NOT (member_of( val, value_range)))) = 0;
END_ENTITY;

ENTITY externally_listed_data
  SUBTYPE OF (explicit_table_function, generic_literal, externally_defined_item);
  value_range : maths_space;
WHERE
  WR1: expression_is_constant(value_range);
END_ENTITY;

ENTITY linearized_table_function
  SUPERTYPE OF (ONEOF (standard_table_function,
                       regular_table_function,
                       triangular_matrix,
                       symmetric_matrix,
                       banded_matrix))
  SUBTYPE OF (explicit_table_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_function;
  first : integer;
DERIVE
  source : maths_function := SELF\unary_generic_expression.operand;
WHERE
  WR1: function_is_1d_array(source);
  WR2: member_of(first, source.domain);
END_ENTITY;

ENTITY standard_table_function
  SUBTYPE OF (linearized_table_function);
  order : ordering_type;
WHERE
  WR1: extremal_position_check(SELF);
END_ENTITY;

ENTITY regular_table_function
  SUBTYPE OF (linearized_table_function);
  increments : LIST[1:?] OF INTEGER;
WHERE
  WR1: SIZEOF (increments) = SIZEOF (self\explicit_table_function.shape);
  WR2: extremal_position_check(self);
END_ENTITY;

ENTITY triangular_matrix
  SUBTYPE OF (linearized_table_function);
  default_entry : maths_value;
  lo_up : lower_upper;
  order : ordering_type;
WHERE
  WR1: SIZEOF (SELF\explicit_table_function.shape) = 2;
  WR2: member_of(default_entry, SELF\maths_function.range);
END_ENTITY;

ENTITY strict_triangular_matrix
  SUBTYPE OF (triangular_matrix);
  main_diagonal_value : maths_value;
END_ENTITY;

ENTITY symmetric_matrix
  SUBTYPE OF (linearized_table_function);
  symmetry : symmetry_type;
  triangle : lower_upper;
  order : ordering_type;
WHERE
  WR1: SIZEOF (SELF\explicit_table_function.shape) = 2;
  WR2: SELF\explicit_table_function.shape[1] = SELF\explicit_table_function.shape[2];
  WR3: NOT (symmetry = skew) OR ( (space_dimension(SELF\linearized_table_function.source.range) = 1) AND subspace_of_es(factor1(SELF\linearized_table_function.source.range), es_numbers));
  WR4: NOT ((symmetry = hermitian) OR (symmetry = skew_hermitian)) OR ( (space_dimension(SELF\linearized_table_function.source.range) = 1) AND subspace_of_es(factor1(SELF\linearized_table_function.source.range), es_complex_numbers));
END_ENTITY;

ENTITY symmetric_banded_matrix
  SUBTYPE OF (symmetric_matrix);
  default_entry : maths_value;
  above : nonnegative_integer;
WHERE
  WR1: member_of(default_entry, factor1(SELF\linearized_table_function.source.range));
END_ENTITY;

ENTITY banded_matrix
  SUBTYPE OF (linearized_table_function);
  default_entry : maths_value;
  below : integer;
  above : integer;
  order : ordering_type;
WHERE
  WR1: SIZEOF (self\explicit_table_function.shape) = 2;
  WR2: -below <= above;
  WR3: member_of(default_entry, factor1(SELF\linearized_table_function.source.range));
END_ENTITY;

ENTITY basic_sparse_matrix
  SUBTYPE OF (explicit_table_function, multiple_arity_generic_expression);
  SELF\multiple_arity_generic_expression.operands : LIST[3:3] OF maths_function;
  default_entry : maths_value;
  order : ordering_type;
DERIVE
  index : maths_function := SELF\multiple_arity_generic_expression.operands[1];
  loc : maths_function := SELF\multiple_arity_generic_expression.operands[2];
  val : maths_function := SELF\multiple_arity_generic_expression.operands[3];
WHERE
  WR1: function_is_1d_table(index);
  WR2: function_is_1d_table(loc);
  WR3: function_is_1d_table(val);
  WR4: check_sparse_index_domain(index.domain, index_base, shape, order);
  WR5: check_sparse_index_to_loc(index.range, loc.domain);
  WR6: loc.domain = val.domain;
  WR7: check_sparse_loc_range(loc.range, index_base, shape, order);
  WR8: member_of(default_entry, val.range);
END_ENTITY;

ENTITY homogeneous_linear_function
  SUBTYPE OF (maths_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_function;
  sum_index : one_or_two;
DERIVE
  mat : maths_function := SELF\unary_generic_expression.operand;
WHERE
  WR1: function_is_2d_table(mat);
  WR2: (space_dimension(mat.range) = 1) AND subspace_of_es(factor1(mat.range),es_numbers);
END_ENTITY;

ENTITY general_linear_function
  SUBTYPE OF (maths_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_function;
  sum_index : one_or_two;
DERIVE
  mat : maths_function := SELF\unary_generic_expression.operand;
WHERE
  WR1: function_is_2d_table(mat);
  WR2: (space_dimension(mat.range) = 1) AND subspace_of_es(factor1(mat.range),es_numbers);
END_ENTITY;

ENTITY b_spline_basis
  SUBTYPE OF (maths_function, generic_literal);
  degree : nonnegative_integer;
  repeated_knots : LIST[2:?] OF REAL;
DERIVE
  order : positive_integer := degree + 1;
  num_basis : positive_integer := SIZEOF (repeated_knots) - order;
WHERE
  WR1: num_basis >= order;
  WR2: nondecreasing(repeated_knots);
  WR3: repeated_knots[order] < repeated_knots[num_basis+1];
END_ENTITY;

ENTITY b_spline_function
  SUBTYPE OF (maths_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_function;
  basis : LIST[1:?] OF b_spline_basis;
DERIVE
  coef : maths_function := SELF\unary_generic_expression.operand;
WHERE
  WR1: function_is_table(coef);
  WR2: (space_dimension(coef.range) = 1) AND (number_superspace_of(factor1(coef.range)) = the_reals);
  WR3: SIZEOF (basis) <= SIZEOF (shape_of_array(coef));
  WR4: compare_basis_and_coef(basis, coef);
END_ENTITY;

ENTITY rationalize_function
  SUBTYPE OF (maths_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_function;
DERIVE
  fun : maths_function := SELF\unary_generic_expression.operand;
WHERE
  WR1: (space_dimension(fun.domain) = 1) AND (space_dimension(fun.range) = 1);
  WR2: number_tuple_subspace_check(factor1(fun.range));
  WR3: space_dimension(factor1(fun.range)) > 1;
END_ENTITY;

ENTITY partial_derivative_function
  SUBTYPE OF (maths_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_function;
  d_variables : LIST[1:?] OF input_selector;
  extension : extension_options;
DERIVE
  derivand : maths_function := SELF\unary_generic_expression.operand;
WHERE
  WR1: space_is_continuum (derivand.range);
  WR2: partial_derivative_check (derivand.domain, d_variables);
END_ENTITY;

ENTITY partial_derivative_expression
  SUBTYPE OF (unary_generic_expression);
  d_variables : LIST[1:?] OF maths_variable;
  extension : extension_options;
DERIVE
  derivand : generic_expression := SELF\unary_generic_expression.operand;
WHERE
  WR1: has_values_space (derivand);
  WR2: space_is_continuum (values_space_of (derivand));
  WR3: SIZEOF (QUERY (vbl <* d_variables | (NOT subspace_of (values_space_of (vbl), the_reals)) AND (NOT subspace_of (values_space_of (vbl), the_complex_numbers)) )) = 0;
END_ENTITY;

ENTITY definite_integral_function
  SUBTYPE OF (maths_function, unary_generic_expression);
  SELF\unary_generic_expression.operand : maths_function;
  variable_of_integration : input_selector;
  lower_limit_neg_infinity : BOOLEAN;
  upper_limit_pos_infinity : BOOLEAN;
DERIVE
  integrand : maths_function := SELF\unary_generic_expression.operand;
WHERE
  WR1: space_is_continuum (integrand.range);
  WR2: definite_integral_check (integrand.domain, variable_of_integration, lower_limit_neg_infinity, upper_limit_pos_infinity);
END_ENTITY;

ENTITY definite_integral_expression
  SUBTYPE OF (quantifier_expression);
  lower_limit_neg_infinity : BOOLEAN;
  upper_limit_pos_infinity : BOOLEAN;
DERIVE
  integrand : generic_expression := SELF\multiple_arity_generic_expression.operands[1];
  variable_of_integration : maths_variable := SELF\multiple_arity_generic_expression.operands[2];
  SELF\quantifier_expression.variables : LIST[1:1] OF UNIQUE generic_variable := [variable_of_integration];
WHERE
  WR1: has_values_space (integrand);
  WR2: space_is_continuum (values_space_of (integrand));
  WR3: definite_integral_expr_check (SELF\multiple_arity_generic_expression.operands, lower_limit_neg_infinity, upper_limit_pos_infinity);
END_ENTITY;

ENTITY abstracted_expression_function
  SUBTYPE OF (maths_function, quantifier_expression);
DERIVE
  SELF\quantifier_expression.variables : LIST[1:?] OF UNIQUE generic_variable := remove_first(SELF\multiple_arity_generic_expression.operands);
  expr : generic_expression := SELF\multiple_arity_generic_expression.operands[1];
WHERE
  WR1: SIZEOF (QUERY ( operand <* SELF\multiple_arity_generic_expression.operands | NOT ( has_values_space( operand)))) = 0;
END_ENTITY;

ENTITY expression_denoted_function
  SUBTYPE OF (maths_function, unary_generic_expression);
DERIVE
  expr : generic_expression := SELF\unary_generic_expression.operand;
WHERE
  WR1: (schema_prefix + 'FUNCTION_SPACE') IN TYPEOF (values_space_of(expr));
END_ENTITY;

ENTITY imported_point_function
  SUBTYPE OF (maths_function, generic_literal);
  geometry : point;
END_ENTITY;

ENTITY imported_curve_function
  SUBTYPE OF (maths_function, generic_literal);
  geometry : curve;
  parametric_domain : tuple_space;
WHERE
  WR1: expression_is_constant(parametric_domain);
END_ENTITY;

ENTITY imported_surface_function
  SUBTYPE OF (maths_function, generic_literal);
  geometry : surface;
  parametric_domain : tuple_space;
WHERE
  WR1: expression_is_constant(parametric_domain);
END_ENTITY;

ENTITY imported_volume_function
  SUBTYPE OF (maths_function, generic_literal);
  geometry : volume;
  parametric_domain : tuple_space;
WHERE
  WR1: expression_is_constant(parametric_domain);
END_ENTITY;

ENTITY application_defined_function
  SUBTYPE OF (maths_function);
  explicit_domain : tuple_space;
  explicit_range : tuple_space;
  parameters : LIST OF maths_value;
WHERE
  WR1: expression_is_constant(explicit_domain);
  WR2: expression_is_constant(explicit_range);
END_ENTITY;

ENTITY mathematical_description;
  described : maths_expression;
  describing : STRING;
  encoding : label;
END_ENTITY;

FUNCTION all_members_of_es
 (sv : SET OF maths_value; es : elementary_space_enumerators) : LOGICAL;
  CONSTANT
    base_types : SET OF STRING := ['NUMBER','COMPLEX_NUMBER_LITERAL','REAL',
      'INTEGER','LOGICAL','BOOLEAN','STRING','BINARY','MATHS_SPACE',
      'MATHS_FUNCTION','LIST','ELEMENTARY_SPACE_ENUMERATORS','ORDERING_TYPE',
      'LOWER_UPPER','SYMMETRY_TYPE','ELEMENTARY_FUNCTION_ENUMERATORS',
      'OPEN_CLOSED','SPACE_CONSTRAINT_TYPE','REPACKAGE_OPTIONS',
      'EXTENSION_OPTIONS'];
  END_CONSTANT;
  LOCAL
    v : maths_value;
    key_type : STRING := '';
    types : SET OF STRING;
    ge : generic_expression;
    cum : LOGICAL := TRUE;
    vspc : maths_space;
  END_LOCAL;
  IF NOT EXISTS (sv) OR NOT EXISTS (es) THEN  RETURN (FALSE);  END_IF;
  CASE es OF
  es_numbers :         key_type := 'NUMBER';
  es_complex_numbers : key_type := 'COMPLEX_NUMBER_LITERAL';
  es_reals :           key_type := 'REAL';
  es_integers :        key_type := 'INTEGER';
  es_logicals :        key_type := 'LOGICAL';
  es_booleans :        key_type := 'BOOLEAN';
  es_strings :         key_type := 'STRING';
  es_binarys :         key_type := 'BINARY';
  es_maths_spaces :    key_type := 'MATHS_SPACE';
  es_maths_functions : key_type := 'MATHS_FUNCTION';
  es_generics :        RETURN (TRUE);
  END_CASE;
  REPEAT i := 1 TO SIZEOF (sv);
    IF NOT EXISTS (sv[i]) THEN  RETURN (FALSE);  END_IF;
    v := simplify_maths_value(sv[i]);
    types := stripped_typeof(v);
    IF key_type IN types THEN  SKIP;  END_IF;
    IF (es = es_numbers) AND ('COMPLEX_NUMBER_LITERAL' IN types) THEN  SKIP;  END_IF;
    IF SIZEOF (base_types * types) > 0 THEN  RETURN (FALSE);  END_IF;
    -- Must be a generic_expression which doesn't simplify and which is not a
    -- complex_number_literal, maths_space, or maths_function.
    ge := v;
    IF has_values_space(ge) THEN
      vspc := values_space_of(ge);
      IF NOT subspace_of_es(vspc,es) THEN
        IF NOT compatible_spaces(vspc,make_elementary_space(es)) THEN
          RETURN (FALSE);
        END_IF;
        cum := UNKNOWN;
      END_IF;
    ELSE
      cum := UNKNOWN;
    END_IF;
    IF cum = FALSE THEN  RETURN (FALSE);  END_IF;
  END_REPEAT;
  RETURN (cum);
                              
END_FUNCTION;

FUNCTION any_space_satisfies
 (sc : space_constraint_type; spc : maths_space) : BOOLEAN;
  LOCAL
    spc_id : elementary_space_enumerators;
  END_LOCAL;
  IF (sc = sc_equal) OR NOT ('ELEMENTARY_SPACE' IN stripped_typeof(spc)) THEN
    RETURN (FALSE);
  END_IF;
  spc_id := spc\elementary_space.space_id;
  IF sc = sc_subspace THEN
    RETURN (bool(spc_id = es_generics));
  END_IF;
  IF sc = sc_member THEN
    RETURN (bool((spc_id = es_generics) OR (spc_id = es_maths_spaces)));
  END_IF;
  -- Should be unreachable.
  RETURN (?);
                              
END_FUNCTION;

FUNCTION assoc_product_space
 (ts1 : tuple_space; ts2 : tuple_space) : tuple_space;
  LOCAL
    types1 : SET OF STRING := stripped_typeof (ts1);
    types2 : SET OF STRING := stripped_typeof (ts2);
    up1, up2 : uniform_product_space := make_uniform_product_space(the_reals,1);
    lp1, lp2, lps : listed_product_space := the_zero_tuple_space;
    et1, et2, ets : extended_tuple_space := the_tuples;
    use_up1, use_up2, use_lp1, use_lp2 : BOOLEAN;
    factors : LIST OF maths_space := [];
    tspace : tuple_space;
  END_LOCAL;
  -- Identify type of first operand
  IF 'UNIFORM_PRODUCT_SPACE' IN types1 THEN
    up1 := ts1;  use_up1 := true;  use_lp1 := false;
  ELSE
    IF 'LISTED_PRODUCT_SPACE' IN types1 THEN
      lp1 := ts1;  use_up1 := false;  use_lp1 := true;
    ELSE
      IF NOT ('EXTENDED_TUPLE_SPACE' IN types1) THEN
        -- Unreachable when this function was written.
        RETURN (?);
      END_IF;
      et1 := ts1;  use_up1 := false;  use_lp1 := false;
    END_IF;
  END_IF;
  -- Identify type of second operand
  IF 'UNIFORM_PRODUCT_SPACE' IN types2 THEN
    up2 := ts2;  use_up2 := true;  use_lp2 := false;
  ELSE
    IF 'LISTED_PRODUCT_SPACE' IN types2 THEN
      lp2 := ts2;  use_up2 := false;  use_lp2 := true;
    ELSE
      IF NOT ('EXTENDED_TUPLE_SPACE' IN types2) THEN
        -- Unreachable when this function was written.
        RETURN (?);
      END_IF;
      et2 := ts2;  use_up2 := false;  use_lp2 := false;
    END_IF;
  END_IF;
  -- Construction for each combination of cases
  IF use_up1 THEN
    IF use_up2 THEN
      IF up1.base = up2.base THEN
        tspace := make_uniform_product_space(up1.base, up1.exponent + up2.exponent);
      ELSE
        factors := [up1.base : up1.exponent, up2.base : up2.exponent];
        tspace := make_listed_product_space(factors);
      END_IF;
    ELSE
      IF use_lp2 THEN
        -- Avoid compiler confusion by breaking into two lines.
        factors := [up1.base : up1.exponent];
        factors := factors + lp2.factors;
        tspace := make_listed_product_space(factors);
      ELSE
        tspace := assoc_product_space(up1, et2.base);
        tspace := make_extended_tuple_space(tspace, et2.extender);
      END_IF;
    END_IF;
  ELSE
    IF use_lp1 THEN
      IF use_up2 THEN
        -- Avoid compiler confusion by breaking into two lines.
        factors := [up2.base : up2.exponent];
        factors := lp1.factors + factors;
        tspace := make_listed_product_space(factors);
      ELSE
        IF use_lp2 THEN
          tspace := make_listed_product_space(lp1.factors + lp2.factors);
        ELSE
          tspace := assoc_product_space(lp1, et2.base);
          tspace := make_extended_tuple_space(tspace, et2.extender);
        END_IF;
      END_IF;
    ELSE
      IF use_up2 THEN
        IF et1.extender = up2.base THEN
          tspace := assoc_product_space(et1.base, up2);
          tspace := make_extended_tuple_space(tspace, et1.extender);
        ELSE
          -- No subtype is available to represent this cartesian product.
          RETURN (?);
        END_IF;
      ELSE
        IF use_lp2 THEN
          factors := lp2.factors;
          REPEAT i := 1 TO SIZEOF (factors);
            IF et1.extender <> factors[i] THEN
              -- No subtype available to represent this cartesian product.
              RETURN (?);
            END_IF;
          END_REPEAT;
          tspace := assoc_product_space(et1.base, lp2);
          tspace := make_extended_tuple_space(tspace, et1.extender);
        ELSE
          IF et1.extender = et2.extender THEN
            -- Next line may assign indeterminate (?) to tspace.
            tspace := assoc_product_space(et1, et2.base);
          ELSE
            -- No subtype available to represent this cartesian product.
            RETURN (?);
          END_IF;
        END_IF;
      END_IF;
    END_IF;
  END_IF;
  RETURN (tspace);
                              
END_FUNCTION;

FUNCTION atan2
 (y : REAL; x : REAL) : REAL;
  LOCAL
    r : REAL;
  END_LOCAL;
  IF (y = 0.0) AND (x = 0.0) THEN  RETURN (?);  END_IF;
  r := atan(y,x);
  IF x < 0.0 THEN
    IF y < 0.0 THEN  r := r - PI;
    ELSE             r := r + PI;  END_IF;
  END_IF;
  RETURN (r);
                              
END_FUNCTION;

FUNCTION bool
 (lgcl : LOGICAL) : BOOLEAN;
  IF NOT EXISTS (lgcl) THEN  RETURN (FALSE);  END_IF;
  IF lgcl <> TRUE      THEN  RETURN (FALSE);  END_IF;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION check_sparse_index_domain
 (idxdom : tuple_space; base : zero_or_one; shape : LIST[1:?] OF positive_integer; order : ordering_type) : BOOLEAN;
  LOCAL
    mthspc : maths_space;
    interval : finite_integer_interval;
    i : INTEGER;
  END_LOCAL;
  mthspc := factor1(idxdom);
  -- A consequence of WR1 of basic_sparse_matrix is that here we need only
  -- consider the case that mthspc is a finite integer interval and is the only
  -- factor space of idxdom.
  interval := mthspc;
  IF order = by_rows THEN  i := 1;  ELSE  i := 2;  END_IF;
  RETURN (bool((interval.min <= base) AND (interval.max >= base + shape[i])));
  -- The index function is evaluated at (base+shape[i]) when determining the
  -- upper search bound for entries of the last row or column, respectively.
                              
END_FUNCTION;

FUNCTION check_sparse_loc_range
 (locrng : tuple_space; base : zero_or_one; shape : LIST[1:?] OF positive_integer; order : ordering_type) : BOOLEAN;
  LOCAL
    mthspc : maths_space;
    interval : finite_integer_interval;
    i : INTEGER;
  END_LOCAL;
  IF space_dimension(locrng) <> 1 THEN  RETURN (FALSE);  END_IF;
  mthspc := factor1(locrng);
  IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (mthspc)) THEN
    RETURN (FALSE);
  END_IF;
  interval := mthspc;
  IF order = by_rows THEN  i := 2;  ELSE  i := 1;  END_IF;
  RETURN (bool((interval.min >= base) AND (interval.max <= base + shape[i] - 1)));
                              
END_FUNCTION;

FUNCTION check_sparse_index_to_loc
 (index_range : tuple_space; loc_domain : tuple_space) : BOOLEAN;
  LOCAL
    temp : maths_space;
    idx_rng_itvl, loc_dmn_itvl : finite_integer_interval;
  END_LOCAL;
  temp := factor1 (index_range);
  IF (schema_prefix + 'TUPLE_SPACE') IN TYPEOF (temp) THEN
    temp := factor1 (temp);
  END_IF;
  IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
    RETURN (FALSE);
  END_IF;
  idx_rng_itvl := temp;
  temp := factor1 (loc_domain);
  IF (schema_prefix + 'TUPLE_SPACE') IN TYPEOF (temp) THEN
    temp := factor1 (temp);
  END_IF;
  IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
    RETURN (FALSE);
  END_IF;
  loc_dmn_itvl := temp;
  RETURN (bool((loc_dmn_itvl.min <= idx_rng_itvl.min) AND
    (idx_rng_itvl.max <= loc_dmn_itvl.max+1)));
                              
END_FUNCTION;

FUNCTION compare_basis_and_coef
 (basis : LIST[1:?] OF b_spline_basis; coef : maths_function) : BOOLEAN;
  LOCAL
    shape : LIST OF positive_integer;
  END_LOCAL;
  IF NOT EXISTS (basis) OR NOT EXISTS (coef) THEN  RETURN (FALSE);  END_IF;
  shape := shape_of_array(coef);
  IF NOT EXISTS (shape) THEN  RETURN (FALSE);  END_IF;
  IF SIZEOF (shape) < SIZEOF (basis) THEN  RETURN (FALSE);  END_IF;
  REPEAT i := 1 TO SIZEOF (basis);
    IF (basis[i].num_basis = shape[i]) <> TRUE THEN  RETURN (FALSE);  END_IF;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION compare_list_and_value
 (lv : LIST OF GENERICG; op : elementary_function_enumerators; v : GENERIC) : BOOLEAN;
  IF NOT EXISTS (lv) OR NOT EXISTS (op) OR NOT EXISTS (v) THEN
    RETURN (FALSE);
  END_IF;
  REPEAT i := 1 TO SIZEOF (lv);
    IF NOT compare_values(lv[i], op, v) THEN
      RETURN (FALSE);
    END_IF;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION compare_values
 (v1 : GENERIC; op : elementary_function_enumerators; v2 : GENERIC) : BOOLEAN;
  -- This algorithm assumes a comparison between "incompatible" types will
  -- produce the indeterminate value (or UNKNOWN?).
  LOCAL
    logl : LOGICAL := UNKNOWN;
  END_LOCAL;
  IF NOT EXISTS (v1) OR NOT EXISTS (op) OR NOT EXISTS (v2) THEN
    RETURN (FALSE);
  END_IF;
  CASE op OF
  ef_eq_i : logl := (v1 = v2);
  ef_ne_i : logl := (v1 <> v2);
  ef_gt_i : logl := (v1 > v2);
  ef_lt_i : logl := (v1 < v2);
  ef_ge_i : logl := (v1 >= v2);
  ef_le_i : logl := (v1 <= v2);
  END_CASE;
  IF EXISTS (logl) THEN
    IF logl = TRUE THEN  RETURN (TRUE);  END_IF;
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION compatible_complex_number_regions
 (sp1 : maths_space; sp2 : maths_space) : BOOLEAN;
  LOCAL
    typenames : SET OF string := stripped_typeof (sp1);
    crgn1, crgn2 : cartesian_complex_number_region;
    prgn1, prgn2, prgn1c2, prgn2c1 : polar_complex_number_region;
    sp1_is_crgn, sp2_is_crgn : BOOLEAN;
  END_LOCAL;
  IF 'CARTESIAN_COMPLEX_NUMBER_REGION' IN typenames THEN
    sp1_is_crgn := TRUE;
    crgn1 := sp1;
  ELSE
    IF 'POLAR_COMPLEX_NUMBER_REGION' IN typenames THEN
      sp1_is_crgn := FALSE;
      prgn1 := sp1;
    ELSE
      -- Improper usage: Default response is to assume compatibility.
      RETURN (TRUE);
    END_IF;
  END_IF;
  typenames := stripped_typeof (sp2);
  IF 'CARTESIAN_COMPLEX_NUMBER_REGION' IN typenames THEN
    sp2_is_crgn := TRUE;
    crgn2 := sp2;
  ELSE
    IF 'POLAR_COMPLEX_NUMBER_REGION' IN typenames THEN
      sp2_is_crgn := FALSE;
      prgn2 := sp2;
    ELSE
      -- Improper usage: Default response is to assume compatibility.
      RETURN (TRUE);
    END_IF;
  END_IF;
  IF sp1_is_crgn AND sp2_is_crgn THEN
    -- two cartesian regions
    RETURN (compatible_intervals(crgn1.real_constraint, crgn2.real_constraint)
      AND compatible_intervals(crgn1.imag_constraint, crgn2.imag_constraint));
  END_IF;
  IF NOT sp1_is_crgn AND NOT sp2_is_crgn AND
    (prgn1.centre.real_part = prgn2.centre.real_part) AND
    (prgn1.centre.imag_part = prgn2.centre.imag_part) THEN
    -- two polar regions with common centre
    IF NOT compatible_intervals(prgn1.distance_constraint,
      prgn2.distance_constraint) THEN
      RETURN (FALSE);
    END_IF;
    IF compatible_intervals(prgn1.direction_constraint,
      prgn2.direction_constraint) THEN
      RETURN (TRUE);
    END_IF;
    -- Deal with direction ambiguity by 2 pi.
    IF (prgn1.direction_constraint.max > PI) AND (prgn2.direction_constraint.max < PI)
      THEN
      RETURN (compatible_intervals(prgn2.direction_constraint,
        make_finite_real_interval(-PI,open,prgn1.direction_constraint.max-2.0*PI,
        prgn1.direction_constraint.max_closure)));
    END_IF;
    IF (prgn2.direction_constraint.max > PI) AND (prgn1.direction_constraint.max < PI)
      THEN
      RETURN (compatible_intervals(prgn1.direction_constraint,
        make_finite_real_interval(-PI,open,prgn2.direction_constraint.max-2.0*PI,
        prgn2.direction_constraint.max_closure)));
    END_IF;
    RETURN (FALSE);
  END_IF;
  -- Make do with imperfect tests for remaining cases.
  IF sp1_is_crgn AND NOT sp2_is_crgn THEN
    crgn2 := enclose_pregion_in_cregion(prgn2);
    prgn1 := enclose_cregion_in_pregion(crgn1,prgn2.centre);
    RETURN (compatible_complex_number_regions(crgn1,crgn2)
      AND compatible_complex_number_regions(prgn1,prgn2));
  END_IF;
  IF NOT sp1_is_crgn AND sp2_is_crgn THEN
    crgn1 := enclose_pregion_in_cregion(prgn1);
    prgn2 := enclose_cregion_in_pregion(crgn2,prgn1.centre);
    RETURN (compatible_complex_number_regions(crgn1,crgn2)
      AND compatible_complex_number_regions(prgn1,prgn2));
  END_IF;
  -- Two polar regions with different centres
  prgn1c2 := enclose_pregion_in_pregion(prgn1,prgn2.centre);
  prgn2c1 := enclose_pregion_in_pregion(prgn2,prgn1.centre);
  RETURN (compatible_complex_number_regions(prgn1,prgn2c1)
    AND compatible_complex_number_regions(prgn1c2,prgn2));
                              
END_FUNCTION;

FUNCTION compatible_es_values
 (esval1 : elementary_space_enumerators; esval2 : elementary_space_enumerators) : BOOLEAN;
  LOCAL
    esval1_is_numeric, esval2_is_numeric : LOGICAL;
  END_LOCAL;
  IF (esval1 = esval2) OR (esval1 = es_generics) OR (esval2 = es_generics) THEN
    RETURN (TRUE);
  END_IF;
  esval1_is_numeric := (esval1 >= es_numbers) AND (esval1 <= es_integers);
  esval2_is_numeric := (esval2 >= es_numbers) AND (esval2 <= es_integers);
  IF (esval1_is_numeric AND (esval2 = es_numbers)) OR
    (esval2_is_numeric AND (esval1 = es_numbers)) THEN
    RETURN (TRUE);
  END_IF;
  IF esval1_is_numeric XOR esval2_is_numeric THEN
    RETURN (FALSE);
  END_IF;
  IF ((esval1 = es_logicals) AND (esval2 = es_booleans)) OR
    ((esval1 = es_booleans) AND (esval2 = es_logicals)) THEN
    RETURN (TRUE);
  END_IF;
  -- All other cases are incompatible
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION compatible_intervals
 (sp1 : maths_space; sp2 : maths_space) : BOOLEAN;
  LOCAL
    amin, amax : REAL;
  END_LOCAL;
  IF min_exists(sp1) AND max_exists(sp2) THEN
    amin := real_min(sp1);  amax := real_max(sp2);
    IF amin > amax THEN  RETURN (FALSE);  END_IF;
    IF amin = amax THEN
      RETURN (min_included(sp1) AND max_included(sp2));
    END_IF;
  END_IF;
  IF min_exists(sp2) AND max_exists(sp1) THEN
    amin := real_min(sp2);  amax := real_max(sp1);
    IF amin > amax THEN  RETURN (FALSE);  END_IF;
    IF amin = amax THEN
      RETURN (min_included(sp2) AND max_included(sp1));
    END_IF;
  END_IF;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION compatible_spaces
 (sp1 : maths_space; sp2 : maths_space) : BOOLEAN;
  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;
    -- Should be unreachable.
    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;
    -- Should be unreachable.
    RETURN (TRUE);
  END_IF;
  IF subspace_of_es(sp1,es_integers) THEN  -- Note that sp1 finite already handled.
    IF subspace_of_es(sp2,es_integers) THEN  -- Note that sp2 finite already handled.
      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  -- Note that sp1 finite already handled.
    IF subspace_of_es(sp2,es_reals) THEN  -- Note that sp2 finite already handled.
      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  -- Note sp1 finite already handled.
    IF subspace_of_es(sp2,es_complex_numbers) THEN  -- Note sp2 finite already handled.
      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;
    -- Should be unreachable.
    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;
    -- Should be unreachable.
    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;
    -- Should be unreachable.
    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;
    -- Should be unreachable.
    RETURN (TRUE);
  END_IF;
  -- Should be unreachable.
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION composable_sequence
 (operands : LIST[2:?] OF maths_function) : BOOLEAN;
  REPEAT i := 1 TO SIZEOF (operands) - 1;
    IF NOT compatible_spaces (operands[i].range, operands[i+1].domain) THEN
      RETURN (FALSE);
    END_IF;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION convert_to_literal
 (val : maths_atom) : generic_literal;
  LOCAL
    types : SET OF STRING := TYPEOF (val);
  END_LOCAL;
  IF 'INTEGER' IN types THEN  RETURN (make_int_literal (val));      END_IF;
  IF 'REAL'    IN types THEN  RETURN (make_real_literal (val));     END_IF;
  IF 'BOOLEAN' IN types THEN  RETURN (make_boolean_literal (val));  END_IF;
  IF 'STRING'  IN types THEN  RETURN (make_string_literal (val));   END_IF;
  IF 'LOGICAL' IN types THEN  RETURN (make_logical_literal (val));  END_IF;
  IF 'BINARY'  IN types THEN  RETURN (make_binary_literal (val));   END_IF;
  IF (schema_prefix + 'MATHS_ENUM_ATOM') IN types THEN
    RETURN (make_maths_enum_literal (val));
  END_IF;
  -- Should be unreachable
  RETURN (?);
                              
END_FUNCTION;

FUNCTION convert_to_maths_function
 (func : maths_function_select) : maths_function;
  LOCAL
    efenum : elementary_function_enumerators;
    mthfun : maths_function;
  END_LOCAL;
  IF (schema_prefix + 'MATHS_FUNCTION') IN TYPEOF (func) THEN
    mthfun := func;
  ELSE
    efenum := func;
    mthfun := make_elementary_function (efenum);
  END_IF;
  RETURN (mthfun);
                              
END_FUNCTION;

FUNCTION convert_to_maths_value
 (val : GENERIC) : maths_value;
  LOCAL
    types : SET OF STRING := TYPEOF (val);
    ival  : maths_integer;
    rval  : maths_real;
    nval  : maths_number;
    tfval : maths_boolean;
    lval  : maths_logical;
    sval  : maths_string;
    bval  : maths_binary;
    tval  : maths_tuple := the_empty_maths_tuple;
    mval  : maths_value;
  END_LOCAL;
  IF (schema_prefix + 'MATHS_VALUE') IN types THEN  RETURN (val);  END_IF;
  IF 'INTEGER' IN types THEN  ival := val;   RETURN (ival);   END_IF;
  IF 'REAL'    IN types THEN  rval := val;   RETURN (rval);   END_IF;
  IF 'NUMBER'  IN types THEN  nval := val;   RETURN (nval);   END_IF;
  IF 'BOOLEAN' IN types THEN  tfval := val;  RETURN (tfval);  END_IF;
  IF 'LOGICAL' IN types THEN  lval := val;   RETURN (lval);   END_IF;
  IF 'STRING'  IN types THEN  sval := val;   RETURN (sval);   END_IF;
  IF 'BINARY'  IN types THEN  bval := val;   RETURN (bval);   END_IF;
  IF 'LIST' IN types THEN
    REPEAT i := 1 TO SIZEOF (val);
      mval := convert_to_maths_value (val[i]);
      IF NOT EXISTS (mval) THEN  RETURN (?);  END_IF;
      INSERT (tval, mval, i-1);
    END_REPEAT;
    RETURN (tval);
  END_IF;
  RETURN (?);
                              
END_FUNCTION;

FUNCTION convert_to_operand
 (val : maths_value) : generic_expression;
  LOCAL
    types  : SET OF STRING := stripped_typeof (val);
  END_LOCAL;
  -- Use intermediate variables of appropriate declared types to help the compilers.
  IF 'GENERIC_EXPRESSION' IN types THEN  RETURN (val);  END_IF;
  IF 'MATHS_ATOM' IN types THEN  RETURN (convert_to_literal (val));  END_IF;
  IF 'ATOM_BASED_VALUE' IN types THEN  RETURN (make_atom_based_literal(val));  END_IF;
  IF 'MATHS_TUPLE' IN types THEN  RETURN (make_maths_tuple_literal(val));  END_IF;
  -- Should be unreachable
  RETURN (?);
                              
END_FUNCTION;

FUNCTION convert_to_operands
 (values : AGGREGATE OF maths_value) : LIST OF generic_expression;
  LOCAL
    operands : LIST OF generic_expression := [];
    loc : INTEGER := 0;
  END_LOCAL;
  IF NOT EXISTS (values) THEN  RETURN (?);  END_IF;
  REPEAT i := LOINDEX (values) TO HIINDEX (values);
    INSERT (operands, convert_to_operand (values[i]), loc);
    loc := loc + 1;
  END_REPEAT;
  RETURN (operands);
                              
END_FUNCTION;

FUNCTION convert_to_operands_prcmfn
 (srcdom : maths_space_or_function; prepfun : LIST OF maths_function; finfun : maths_function_select) : LIST[2:?] OF generic_expression;
  LOCAL
    operands : LIST OF generic_expression := [];
  END_LOCAL;
  INSERT (operands, srcdom, 0);
  REPEAT i := 1 TO SIZEOF (prepfun);
    INSERT (operands, prepfun[i], i);
  END_REPEAT;
  INSERT (operands, convert_to_maths_function (finfun), SIZEOF (prepfun)+1);
  RETURN (operands);
                              
END_FUNCTION;

FUNCTION definite_integral_check
 (domain : tuple_space; vrblint : input_selector; lowerinf : BOOLEAN; upperinf : BOOLEAN) : BOOLEAN;
  LOCAL
    domn : tuple_space := domain;
    fspc : maths_space;
    dim : nonnegative_integer;
    k : positive_integer;
  END_LOCAL;
  IF (space_dimension (domain) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
    TYPEOF (factor1 (domain))) THEN
    domn := factor1 (domain);
  END_IF;
  dim := space_dimension (domn);
  k := vrblint;
  IF k > dim THEN  RETURN (FALSE);  END_IF;
  fspc := factor_space (domn, k);
  IF NOT ((schema_prefix + 'REAL_INTERVAL') IN TYPEOF (fspc)) THEN
    RETURN (FALSE);
  END_IF;
  IF lowerinf AND min_exists (fspc) THEN  RETURN (FALSE);  END_IF;
  IF upperinf AND max_exists (fspc) THEN  RETURN (FALSE);  END_IF;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION definite_integral_expr_check
 (operands : LIST[2:?] OF generic_expression; lowerinf : BOOLEAN; upperinf : BOOLEAN) : BOOLEAN;
  LOCAL
    nops : INTEGER := 2;
    vspc : maths_space;
    dim : nonnegative_integer;
    k : positive_integer;
    bspc : maths_space;
  END_LOCAL;
  IF NOT lowerinf THEN  nops := nops + 1;  END_IF;
  IF NOT upperinf THEN  nops := nops + 1;  END_IF;
  IF SIZEOF (operands) <> nops THEN  RETURN (FALSE);  END_IF;
  IF NOT ('GENERIC_VARIABLE' IN stripped_typeof(operands[2])) THEN
    RETURN (FALSE);
  END_IF;
  IF NOT has_values_space (operands[2]) THEN  RETURN (FALSE);  END_IF;
  vspc := values_space_of (operands[2]);
  IF NOT ('REAL_INTERVAL' IN stripped_typeof(vspc)) THEN  RETURN (FALSE);  END_IF;
  IF lowerinf THEN
    IF min_exists (vspc) THEN  RETURN (FALSE);  END_IF;
    k := 3;
  ELSE
    IF NOT has_values_space (operands[3]) THEN  RETURN (FALSE);  END_IF;
    bspc := values_space_of (operands[3]);
    IF NOT compatible_spaces (bspc, vspc) THEN  RETURN (FALSE);  END_IF;
    k := 4;
  END_IF;
  IF upperinf THEN
    IF max_exists (vspc) THEN  RETURN (FALSE);  END_IF;
  ELSE
    IF NOT has_values_space (operands[k]) THEN  RETURN (FALSE);  END_IF;
    bspc := values_space_of (operands[k]);
    IF NOT compatible_spaces (bspc, vspc) THEN  RETURN (FALSE);  END_IF;
  END_IF;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION derive_definite_integral_domain
 (igrl : definite_integral_function) : tuple_space;

  -- Internal utility function:
  FUNCTION process_product_space(spc         : product_space;
                                 idx, prefix : INTEGER;
                                 vdomn       : maths_space) : product_space;
    LOCAL
      uspc : uniform_product_space;
      expnt : INTEGER;
      factors : LIST OF maths_space;
    END_LOCAL;
    IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN TYPEOF (spc) THEN
      uspc := spc;
      expnt := uspc.exponent + prefix;
      IF idx <= uspc.exponent THEN  expnt := expnt - 1;  END_IF;
      IF expnt = 0 THEN
        RETURN (make_listed_product_space([]));
      ELSE
        RETURN (make_uniform_product_space(uspc.base,expnt));
      END_IF;
    ELSE
      factors := spc\listed_product_space.factors;
      IF idx <= SIZEOF (factors) THEN  REMOVE (factors, idx);  END_IF;
      IF prefix > 0 THEN
        INSERT (factors, vdomn, 0);
        IF prefix > 1 THEN  INSERT (factors, vdomn, 0);  END_IF;
      END_IF;
      RETURN (make_listed_product_space(factors));
    END_IF;
                              
END_FUNCTION;

FUNCTION derive_elementary_function_domain
 (ef_val : elementary_function_enumerators) : tuple_space;
  IF NOT EXISTS (ef_val) THEN  RETURN (?);  END_IF;
  CASE ef_val OF
  ef_and : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_logicals));
  ef_or : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_logicals));
  ef_not : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_xor : RETURN (make_uniform_product_space (the_logicals, 2));
  ef_negate_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_add_i : RETURN (the_integer_tuples);
  ef_subtract_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_multiply_i : RETURN (the_integer_tuples);
  ef_divide_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_mod_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_exponentiate_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_eq_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_ne_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_gt_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_lt_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_ge_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_le_i : RETURN (make_uniform_product_space (the_integers, 2));
  ef_abs_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_if_i : RETURN (make_listed_product_space ([the_logicals, the_integers,
    the_integers]));
  ef_negate_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_reciprocal_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_add_r : RETURN (the_real_tuples);
  ef_subtract_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_multiply_r : RETURN (the_real_tuples);
  ef_divide_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_mod_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_exponentiate_r : RETURN (make_listed_product_space ([the_nonnegative_reals,
    the_reals]));
  ef_exponentiate_ri : RETURN (make_listed_product_space ([the_reals, the_integers]));
  ef_eq_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_ne_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_gt_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_lt_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_ge_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_le_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_abs_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_acos_r : RETURN (make_uniform_product_space (the_neg1_one_interval, 1));
  ef_asin_r : RETURN (make_uniform_product_space (the_neg1_one_interval, 1));
  ef_atan2_r : RETURN (make_uniform_product_space (the_reals, 2));
  ef_cos_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_exp_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_ln_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
  ef_log2_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
  ef_log10_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
  ef_sin_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_sqrt_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
  ef_tan_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_if_r : RETURN (make_listed_product_space ([the_logicals, the_reals, the_reals]));
  ef_negate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_reciprocal_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_add_c : RETURN (the_complex_tuples);
  ef_subtract_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
  ef_multiply_c : RETURN (the_complex_tuples);
  ef_divide_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
  ef_exponentiate_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
  ef_exponentiate_ci : RETURN (make_listed_product_space ([the_complex_numbers,
    the_integers]));
  ef_eq_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
  ef_ne_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
  ef_conjugate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_abs_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_arg_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_cos_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_exp_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_ln_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_sin_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_sqrt_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_tan_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_if_c : RETURN (make_listed_product_space ([the_logicals, the_complex_numbers,
    the_complex_numbers]));
  ef_subscript_s : RETURN (make_listed_product_space ([the_strings, the_integers]));
  ef_eq_s : RETURN (make_uniform_product_space (the_strings, 2));
  ef_ne_s : RETURN (make_uniform_product_space (the_strings, 2));
  ef_gt_s : RETURN (make_uniform_product_space (the_strings, 2));
  ef_lt_s : RETURN (make_uniform_product_space (the_strings, 2));
  ef_ge_s : RETURN (make_uniform_product_space (the_strings, 2));
  ef_le_s : RETURN (make_uniform_product_space (the_strings, 2));
  ef_subsequence_s : RETURN (make_listed_product_space ([the_strings, the_integers,
    the_integers]));
  ef_concat_s : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_strings));
  ef_size_s : RETURN (make_uniform_product_space (the_strings, 1));
  ef_format : RETURN (make_listed_product_space ([the_numbers, the_strings]));
  ef_value : RETURN (make_uniform_product_space (the_strings, 1));
  ef_like : RETURN (make_uniform_product_space (the_strings, 2));
  ef_if_s : RETURN (make_listed_product_space ([the_logicals, the_strings,
    the_strings]));
  ef_subscript_b : RETURN (make_listed_product_space ([the_binarys, the_integers]));
  ef_eq_b : RETURN (make_uniform_product_space (the_binarys, 2));
  ef_ne_b : RETURN (make_uniform_product_space (the_binarys, 2));
  ef_gt_b : RETURN (make_uniform_product_space (the_binarys, 2));
  ef_lt_b : RETURN (make_uniform_product_space (the_binarys, 2));
  ef_ge_b : RETURN (make_uniform_product_space (the_binarys, 2));
  ef_le_b : RETURN (make_uniform_product_space (the_binarys, 2));
  ef_subsequence_b : RETURN (make_listed_product_space ([the_binarys, the_integers,
    the_integers]));
  ef_concat_b : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_binarys));
  ef_size_b : RETURN (make_uniform_product_space (the_binarys, 1));
  ef_if_b : RETURN (make_listed_product_space ([the_logicals, the_binarys,
    the_binarys]));
  ef_subscript_t : RETURN (make_listed_product_space ([the_tuples, the_integers]));
  ef_eq_t : RETURN (make_uniform_product_space (the_tuples, 2));
  ef_ne_t : RETURN (make_uniform_product_space (the_tuples, 2));
  ef_concat_t : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_tuples));
  ef_size_t : RETURN (make_uniform_product_space (the_tuples, 1));
  ef_entuple : RETURN (the_tuples);
  ef_detuple : RETURN (make_uniform_product_space (the_generics, 1));
  ef_insert : RETURN (make_listed_product_space ([the_tuples, the_generics,
    the_integers]));
  ef_remove : RETURN (make_listed_product_space ([the_tuples, the_integers]));
  ef_if_t : RETURN (make_listed_product_space ([the_logicals, the_tuples,
    the_tuples]));
  ef_sum_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
  ef_product_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
  ef_add_it : RETURN (make_extended_tuple_space (the_integer_tuples,
    the_integer_tuples));
  ef_subtract_it : RETURN (make_uniform_product_space (the_integer_tuples, 2));
  ef_scalar_mult_it : RETURN (make_listed_product_space ([the_integers,
    the_integer_tuples]));
  ef_dot_prod_it : RETURN (make_uniform_product_space (the_integer_tuples, 2));
  ef_sum_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
  ef_product_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
  ef_add_rt : RETURN (make_extended_tuple_space (the_real_tuples, the_real_tuples));
  ef_subtract_rt : RETURN (make_uniform_product_space (the_real_tuples, 2));
  ef_scalar_mult_rt : RETURN (make_listed_product_space ([the_reals,
    the_real_tuples]));
  ef_dot_prod_rt : RETURN (make_uniform_product_space (the_real_tuples, 2));
  ef_norm_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
  ef_sum_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
  ef_product_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
  ef_add_ct : RETURN (make_extended_tuple_space (the_complex_tuples,
    the_complex_tuples));
  ef_subtract_ct : RETURN (make_uniform_product_space (the_complex_tuples, 2));
  ef_scalar_mult_ct : RETURN (make_listed_product_space ([the_complex_numbers,
    the_complex_tuples]));
  ef_dot_prod_ct : RETURN (make_uniform_product_space (the_complex_tuples, 2));
  ef_norm_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
  ef_if : RETURN (make_listed_product_space ([the_logicals, the_generics,
    the_generics]));
  ef_ensemble : RETURN (the_tuples);
  ef_member_of : RETURN (make_listed_product_space ([the_generics, the_maths_spaces]));
  OTHERWISE : RETURN (?);
  END_CASE;
                              
END_FUNCTION;

FUNCTION derive_elementary_function_range
 (ef_val : elementary_function_enumerators) : tuple_space;
  IF NOT EXISTS (ef_val) THEN  RETURN (?);  END_IF;
  CASE ef_val OF
  ef_and : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_or : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_not : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_xor : RETURN (make_uniform_product_space (the_logicals, 2));
  ef_negate_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_add_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_subtract_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_multiply_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_divide_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_mod_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_exponentiate_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_eq_i : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ne_i : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_gt_i : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_lt_i : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ge_i : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_le_i : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_abs_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_if_i : RETURN (make_uniform_product_space (the_integers, 1));
  ef_negate_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_reciprocal_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_add_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_subtract_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_multiply_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_divide_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_mod_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_exponentiate_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_exponentiate_ri : RETURN (make_uniform_product_space (the_reals, 1));
  ef_eq_r : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ne_r : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_gt_r : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_lt_r : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ge_r : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_le_r : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_abs_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
  ef_acos_r : RETURN (make_uniform_product_space (the_zero_pi_interval, 1));
  ef_asin_r : RETURN (make_uniform_product_space (the_neghalfpi_halfpi_interval, 1));
  ef_atan2_r : RETURN (make_uniform_product_space (the_negpi_pi_interval, 1));
  ef_cos_r : RETURN (make_uniform_product_space (the_neg1_one_interval, 1));
  ef_exp_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
  ef_ln_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_log2_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_log10_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_sin_r : RETURN (make_uniform_product_space (the_neg1_one_interval, 1));
  ef_sqrt_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
  ef_tan_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_if_r : RETURN (make_uniform_product_space (the_reals, 1));
  ef_negate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_reciprocal_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_add_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_subtract_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_multiply_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_divide_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_exponentiate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_exponentiate_ci : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_eq_c : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ne_c : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_conjugate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_abs_c : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
  ef_arg_c : RETURN (make_uniform_product_space (the_negpi_pi_interval, 1));
  ef_cos_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_exp_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_ln_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_sin_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_sqrt_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_tan_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_if_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_subscript_s : RETURN (make_uniform_product_space (the_strings, 1));
  ef_eq_s : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ne_s : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_gt_s : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_lt_s : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ge_s : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_le_s : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_subsequence_s : RETURN (make_uniform_product_space (the_strings, 1));
  ef_concat_s : RETURN (make_uniform_product_space (the_strings, 1));
  ef_size_s : RETURN (make_uniform_product_space (the_integers, 1));
  ef_format : RETURN (make_uniform_product_space (the_strings, 1));
  ef_value : RETURN (make_uniform_product_space (the_reals, 1));
  ef_like : RETURN (make_uniform_product_space (the_booleans, 1));
  ef_if_s : RETURN (make_uniform_product_space (the_strings, 1));
  ef_subscript_b : RETURN (make_uniform_product_space (the_binarys, 1));
  ef_eq_b : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ne_b : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_gt_b : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_lt_b : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ge_b : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_le_b : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_subsequence_b : RETURN (make_uniform_product_space (the_binarys, 1));
  ef_concat_b : RETURN (make_uniform_product_space (the_binarys, 1));
  ef_size_b : RETURN (make_uniform_product_space (the_integers, 1));
  ef_if_b : RETURN (make_uniform_product_space (the_binarys, 1));
  ef_subscript_t : RETURN (make_uniform_product_space (the_generics, 1));
  ef_eq_t : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_ne_t : RETURN (make_uniform_product_space (the_logicals, 1));
  ef_concat_t : RETURN (make_uniform_product_space (the_tuples, 1));
  ef_size_t : RETURN (make_uniform_product_space (the_integers, 1));
  ef_entuple : RETURN (make_uniform_product_space (the_tuples, 1));
  ef_detuple : RETURN (the_tuples);
  ef_insert : RETURN (make_uniform_product_space (the_tuples, 1));
  ef_remove : RETURN (make_uniform_product_space (the_tuples, 1));
  ef_if_t : RETURN (make_uniform_product_space (the_tuples, 1));
  ef_sum_it : RETURN (make_uniform_product_space (the_integers, 1));
  ef_product_it : RETURN (make_uniform_product_space (the_integers, 1));
  ef_add_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
  ef_subtract_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
  ef_scalar_mult_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
  ef_dot_prod_it : RETURN (make_uniform_product_space (the_integers, 1));
  ef_sum_rt : RETURN (make_uniform_product_space (the_reals, 1));
  ef_product_rt : RETURN (make_uniform_product_space (the_reals, 1));
  ef_add_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
  ef_subtract_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
  ef_scalar_mult_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
  ef_dot_prod_rt : RETURN (make_uniform_product_space (the_reals, 1));
  ef_norm_rt : RETURN (make_uniform_product_space (the_reals, 1));
  ef_sum_ct : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_product_ct : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_add_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
  ef_subtract_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
  ef_scalar_mult_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
  ef_dot_prod_ct : RETURN (make_uniform_product_space (the_complex_numbers, 1));
  ef_norm_ct : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
  ef_if : RETURN (make_uniform_product_space (the_generics, 1));
  ef_ensemble : RETURN (make_uniform_product_space (the_maths_spaces, 1));
  ef_member_of : RETURN (make_uniform_product_space (the_logicals, 1));
  OTHERWISE : RETURN (?);
  END_CASE;
                              
END_FUNCTION;

FUNCTION derive_finite_function_domain
 (pairs : SET[1:?] OF LIST) : tuple_space;
  LOCAL
    result : SET OF maths_value := [];
  END_LOCAL;
-- An ambiguity in ISO 10303-11:1994 pages 99-101 leaves the result of the following
-- three lines ambiguous in those cases where an operand is simultaneously a member
-- of the base type and the aggregate type.
-- REPEAT i := 1 TO SIZEOF (pairs);
--   result := result + pairs[i][1];
-- END_REPEAT;
-- The next line unions an empty set and the desired list to get the desired set.
  result := result + list_selected_components (pairs, 1);
  RETURN (one_tuples_of (make_finite_space (result)));
                              
END_FUNCTION;

FUNCTION derive_finite_function_range
 (pairs : SET[1:?] OF LIST) : tuple_space;
  LOCAL
    result : SET OF maths_value := [];
  END_LOCAL;
-- An ambiguity in ISO 10303-11:1994 pages 99-101 leaves the result of the following
-- three lines ambiguous in those cases where an operand is simultaneously a member
-- of the base type and the aggregate type.
-- REPEAT i := 1 TO SIZEOF (pairs);
--   result := result + pairs[i][2];
-- END_REPEAT;
-- The next line unions an empty set and the desired list to get the desired set.
  result := result + list_selected_components (pairs, 2);
  RETURN (one_tuples_of (make_finite_space (result)));
                              
END_FUNCTION;

FUNCTION derive_function_domain
 (func : maths_function) : tuple_space;
  LOCAL
    typenames : SET OF STRING := stripped_typeof(func);
    tspace : tuple_space := make_listed_product_space ([]);
    shape : LIST OF positive_integer;
    sidxs  : LIST OF INTEGER := [0];
    itvl   : finite_integer_interval;
    factors : LIST OF finite_integer_interval := [];
    is_uniform : BOOLEAN := TRUE;
  END_LOCAL;
  IF 'FINITE_FUNCTION' IN typenames THEN
    RETURN (derive_finite_function_domain (func\finite_function.pairs));
  END_IF;
  IF 'CONSTANT_FUNCTION' IN typenames THEN
    RETURN (domain_from (func\constant_function.source_of_domain));
  END_IF;
  IF 'SELECTOR_FUNCTION' IN typenames THEN
    RETURN (domain_from (func\selector_function.source_of_domain));
  END_IF;
  IF 'ELEMENTARY_FUNCTION' IN typenames THEN
    RETURN (derive_elementary_function_domain (func\elementary_function.func_id));
  END_IF;
  IF 'RESTRICTION_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (func\restriction_function.operand));
  END_IF;
  IF 'REPACKAGING_FUNCTION' IN typenames THEN
    IF func\repackaging_function.input_repack = ro_nochange THEN
      RETURN (func\repackaging_function.operand.domain);
    END_IF;
    IF func\repackaging_function.input_repack = ro_wrap_as_tuple THEN
      RETURN (factor1 (func\repackaging_function.operand.domain));
    END_IF;
    IF func\repackaging_function.input_repack = ro_unwrap_tuple THEN
      RETURN (one_tuples_of (func\repackaging_function.operand.domain));
    END_IF;
    -- Unreachable, as there is no other possible value for input_repack.
    RETURN (?);
  END_IF;
  IF 'REINDEXED_ARRAY_FUNCTION' IN typenames THEN
    shape := shape_of_array(func\unary_generic_expression.operand);
    sidxs := func\reindexed_array_function.starting_indices;
    REPEAT i := 1 TO SIZEOF (shape);
      itvl := make_finite_integer_interval (sidxs[i], sidxs[i]+shape[i]-1);
      INSERT (factors, itvl, i-1);
      IF shape[i] <> shape[1] THEN  is_uniform := FALSE;  END_IF;
    END_REPEAT;
    IF is_uniform THEN
      RETURN (make_uniform_product_space (factors[1], SIZEOF (shape)));
    END_IF;
    RETURN (make_listed_product_space (factors));
  END_IF;
  IF 'SERIES_COMPOSED_FUNCTION' IN typenames THEN
    RETURN (func\series_composed_function.operands[1].domain);
  END_IF;
  IF 'PARALLEL_COMPOSED_FUNCTION' IN typenames THEN
    RETURN (domain_from (func\parallel_composed_function.source_of_domain));
  END_IF;
  IF 'EXPLICIT_TABLE_FUNCTION' IN typenames THEN
    shape := func\explicit_table_function.shape;
    sidxs[1] := func\explicit_table_function.index_base;
    REPEAT i := 1 TO SIZEOF (shape);
      itvl := make_finite_integer_interval (sidxs[1], sidxs[1]+shape[i]-1);
      INSERT (factors, itvl, i-1);
      IF shape[i] <> shape[1] THEN  is_uniform := FALSE;  END_IF;
    END_REPEAT;
    IF is_uniform THEN
      RETURN (make_uniform_product_space (factors[1], SIZEOF (shape)));
    END_IF;
    RETURN (make_listed_product_space (factors));
  END_IF;
  IF 'HOMOGENEOUS_LINEAR_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_uniform_product_space
      (factor1 (func\homogeneous_linear_function.mat.range),
      func\homogeneous_linear_function.mat\explicit_table_function.shape
      [func\homogeneous_linear_function.sum_index])));
  END_IF;
  IF 'GENERAL_LINEAR_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_uniform_product_space
      (factor1 (func\general_linear_function.mat.range),
      func\general_linear_function.mat\explicit_table_function.shape
      [func\general_linear_function.sum_index] - 1)));
  END_IF;
  IF 'B_SPLINE_BASIS' IN typenames THEN
    RETURN (one_tuples_of (make_finite_real_interval
      (func\b_spline_basis.repeated_knots[func\b_spline_basis.order], closed,
      func\b_spline_basis.repeated_knots[func\b_spline_basis.num_basis+1], closed)));
  END_IF;
  IF 'B_SPLINE_FUNCTION' IN typenames THEN
    REPEAT i := 1 TO SIZEOF (func\b_spline_function.basis);
      tspace := assoc_product_space (tspace, func\b_spline_function.basis[i].domain);
    END_REPEAT;
    RETURN (one_tuples_of (tspace));
  END_IF;
  IF 'RATIONALIZE_FUNCTION' IN typenames THEN
    RETURN (func\rationalize_function.fun.domain);
  END_IF;
  IF 'PARTIAL_DERIVATIVE_FUNCTION' IN typenames THEN
    RETURN (func\partial_derivative_function.derivand.domain);
  END_IF;
  IF 'DEFINITE_INTEGRAL_FUNCTION' IN typenames THEN
    RETURN (derive_definite_integral_domain(func));
  END_IF;
  IF 'ABSTRACTED_EXPRESSION_FUNCTION' IN typenames THEN
    REPEAT i := 1 TO SIZEOF (func\abstracted_expression_function.variables);
      tspace := assoc_product_space (tspace, one_tuples_of (values_space_of
        (func\abstracted_expression_function.variables[i])));
    END_REPEAT;
    RETURN (tspace);
  END_IF;
  IF 'EXPRESSION_DENOTED_FUNCTION' IN typenames THEN
    RETURN (values_space_of (func\expression_denoted_function.expr)\function_space.
      domain_argument);
  END_IF;
  IF 'IMPORTED_POINT_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_listed_product_space ([])));
  END_IF;
  IF 'IMPORTED_CURVE_FUNCTION' IN typenames THEN
    RETURN (func\imported_curve_function.parametric_domain);
  END_IF;
  IF 'IMPORTED_SURFACE_FUNCTION' IN typenames THEN
    RETURN (func\imported_surface_function.parametric_domain);
  END_IF;
  IF 'IMPORTED_VOLUME_FUNCTION' IN typenames THEN
    RETURN (func\imported_volume_function.parametric_domain);
  END_IF;
  IF 'APPLICATION_DEFINED_FUNCTION' IN typenames THEN
    RETURN (func\application_defined_function.explicit_domain);
  END_IF;
  -- Unreachable, as no other subtypes of maths_function are permissible without
  -- first modifying this function to account for them.
  RETURN (?);
                              
END_FUNCTION;

FUNCTION derive_function_range
 (func : maths_function) : tuple_space;
  LOCAL
    typenames : SET OF STRING := stripped_typeof(func);
    tspace : tuple_space := make_listed_product_space ([]);
    m, n : nonnegative_integer := 0;
  END_LOCAL;
  IF 'FINITE_FUNCTION' IN typenames THEN
    RETURN (derive_finite_function_range (func\finite_function.pairs));
  END_IF;
  IF 'CONSTANT_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_finite_space ([func\constant_function.sole_output])));
  END_IF;
  IF 'SELECTOR_FUNCTION' IN typenames THEN
    tspace := func.domain;
    IF (space_dimension(tspace) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
      TYPEOF (tspace)) THEN
      tspace := factor1 (tspace);
    END_IF;
    RETURN (one_tuples_of (factor_space (tspace, func\selector_function.selector)));
  END_IF;
  IF 'ELEMENTARY_FUNCTION' IN typenames THEN
    RETURN (derive_elementary_function_range (func\elementary_function.func_id));
  END_IF;
  IF 'RESTRICTION_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (func\restriction_function.operand));
  END_IF;
  IF 'REPACKAGING_FUNCTION' IN typenames THEN
    tspace := func\repackaging_function.operand.range;
    IF func\repackaging_function.output_repack = ro_wrap_as_tuple THEN
      tspace := one_tuples_of (tspace);
    END_IF;
    IF func\repackaging_function.output_repack = ro_unwrap_tuple THEN
      tspace := factor1 (tspace);
    END_IF;
    IF func\repackaging_function.selected_output > 0 THEN
      tspace := one_tuples_of (factor_space (tspace,
        func\repackaging_function.selected_output));
    END_IF;
    RETURN (tspace);
  END_IF;
  IF 'REINDEXED_ARRAY_FUNCTION' IN typenames THEN
    RETURN (func\unary_generic_expression.operand\maths_function.range);
  END_IF;
  IF 'SERIES_COMPOSED_FUNCTION' IN typenames THEN
    RETURN (func\series_composed_function.operands[SIZEOF
      (func\series_composed_function.operands)].range);
  END_IF;
  IF 'PARALLEL_COMPOSED_FUNCTION' IN typenames THEN
    RETURN (func\parallel_composed_function.final_function.range);
  END_IF;
  IF 'EXPLICIT_TABLE_FUNCTION' IN typenames THEN
    IF 'LISTED_REAL_DATA' IN typenames THEN
      RETURN (one_tuples_of (the_reals));
    END_IF;
    IF 'LISTED_INTEGER_DATA' IN typenames THEN
      RETURN (one_tuples_of (the_integers));
    END_IF;
    IF 'LISTED_LOGICAL_DATA' IN typenames THEN
      RETURN (one_tuples_of (the_logicals));
    END_IF;
    IF 'LISTED_STRING_DATA' IN typenames THEN
      RETURN (one_tuples_of (the_strings));
    END_IF;
    IF 'LISTED_COMPLEX_NUMBER_DATA' IN typenames THEN
      RETURN (one_tuples_of (the_complex_numbers));
    END_IF;
    IF 'LISTED_DATA' IN typenames THEN
      RETURN (one_tuples_of (func\listed_data.value_range));
    END_IF;
    IF 'EXTERNALLY_LISTED_DATA' IN typenames THEN
      RETURN (one_tuples_of (func\externally_listed_data.value_range));
    END_IF;
    IF 'LINEARIZED_TABLE_FUNCTION' IN typenames THEN
      RETURN (func\linearized_table_function.source.range);
    END_IF;
    IF 'BASIC_SPARSE_MATRIX' IN typenames THEN
      RETURN (func\basic_sparse_matrix.val.range);
    END_IF;
    -- Unreachable, as no other subtypes of explicit_table_function are permissible
    -- without first modifying this function to account for them.
    RETURN (?);
  END_IF;
  IF 'HOMOGENEOUS_LINEAR_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_uniform_product_space
      (factor1 (func\homogeneous_linear_function.mat.range),
      func\homogeneous_linear_function.mat\explicit_table_function.shape
      [3 - func\homogeneous_linear_function.sum_index])));
  END_IF;
  IF 'GENERAL_LINEAR_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_uniform_product_space
      (factor1 (func\general_linear_function.mat.range),
      func\general_linear_function.mat\explicit_table_function.shape
      [3 - func\general_linear_function.sum_index])));
  END_IF;
  IF 'B_SPLINE_BASIS' IN typenames THEN
    RETURN (one_tuples_of (make_uniform_product_space (the_reals,
      func\b_spline_basis.num_basis)));
  END_IF;
  IF 'B_SPLINE_FUNCTION' IN typenames THEN
    tspace := factor1 (func\b_spline_function.coef.domain);
    m := SIZEOF (func\b_spline_function.basis);
    n := space_dimension (tspace);
    IF m = n THEN
      RETURN (one_tuples_of (the_reals));
    END_IF;
    IF m = n - 1 THEN
      RETURN (one_tuples_of (make_uniform_product_space (the_reals,
        factor_space (tspace, n)\finite_integer_interval.size)));
    END_IF;
    tspace := extract_factors (tspace, m+1, n);
    RETURN (one_tuples_of (make_function_space (sc_equal, tspace, sc_subspace,
      number_superspace_of (func\b_spline_function.coef.range))));
  END_IF;
  IF 'RATIONALIZE_FUNCTION' IN typenames THEN
    tspace := factor1 (func\rationalize_function.fun.range);
    n := space_dimension (tspace);
    RETURN (one_tuples_of (make_uniform_product_space (number_superspace_of (
      factor1 (tspace)), n-1)));
  END_IF;
  IF 'PARTIAL_DERIVATIVE_FUNCTION' IN typenames THEN
    RETURN (drop_numeric_constraints (
      func\partial_derivative_function.derivand.range));
  END_IF;
  IF 'DEFINITE_INTEGRAL_FUNCTION' IN typenames THEN
    RETURN (drop_numeric_constraints (
      func\definite_integral_function.integrand.range));
  END_IF;
  IF 'ABSTRACTED_EXPRESSION_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of(values_space_of(func\abstracted_expression_function.expr)));
  END_IF;
  IF 'EXPRESSION_DENOTED_FUNCTION' IN typenames THEN
    RETURN (values_space_of (func\expression_denoted_function.expr)\function_space.
      range_argument);
  END_IF;
  IF 'IMPORTED_POINT_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_uniform_product_space (the_reals,
      dimension_of (func\imported_point_function.geometry))));
  END_IF;
  IF 'IMPORTED_CURVE_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_uniform_product_space (the_reals,
      dimension_of (func\imported_curve_function.geometry))));
  END_IF;
  IF 'IMPORTED_SURFACE_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_uniform_product_space (the_reals,
      dimension_of (func\imported_surface_function.geometry))));
  END_IF;
  IF 'IMPORTED_VOLUME_FUNCTION' IN typenames THEN
    RETURN (one_tuples_of (make_uniform_product_space (the_reals,
      dimension_of (func\imported_volume_function.geometry))));
  END_IF;
  IF 'APPLICATION_DEFINED_FUNCTION' IN typenames THEN
    RETURN (func\application_defined_function.explicit_range);
  END_IF;
  -- Unreachable, as no other subtypes of maths_function are permissible without
  -- first modifying this function to account for them.
  RETURN (?);
                              
END_FUNCTION;

FUNCTION domain_from
 (ref : maths_space_or_function) : tuple_space;
  LOCAL
    typenames : SET OF STRING := stripped_typeof(ref);
    func      : maths_function;
  END_LOCAL;
  IF NOT EXISTS (ref) THEN  RETURN (?);  END_IF;
  IF 'TUPLE_SPACE' IN typenames THEN  RETURN (ref);                  END_IF;
  IF 'MATHS_SPACE' IN typenames THEN  RETURN (one_tuples_of (ref));  END_IF;
  func := ref;
  IF 'CONSTANT_FUNCTION' IN typenames THEN
    RETURN (domain_from (func\constant_function.source_of_domain));
  END_IF;
  IF 'SELECTOR_FUNCTION' IN typenames THEN
    RETURN (domain_from (func\selector_function.source_of_domain));
  END_IF;
  IF 'PARALLEL_COMPOSED_FUNCTION' IN typenames THEN
    RETURN (domain_from (func\parallel_composed_function.source_of_domain));
  END_IF;
  RETURN (func.domain);
                              
END_FUNCTION;

FUNCTION dot_count
 (str : STRING) : INTEGER;
  LOCAL
    n : INTEGER := 0;
  END_LOCAL;
  REPEAT i := 1 TO LENGTH (str);
    IF str[i] = '.' THEN  n := n + 1;  END_IF;
  END_REPEAT;
  RETURN (n);
                              
END_FUNCTION;

FUNCTION dotted_identifiers_syntax
 (str : STRING) : BOOLEAN;
  LOCAL
    k : positive_integer;
    m : positive_integer;
  END_LOCAL;
  IF NOT EXISTS (str) THEN  RETURN (FALSE);  END_IF;
  k := parse_express_identifier (str, 1);
  IF k = 1 THEN  RETURN (FALSE);  END_IF;
  REPEAT WHILE k <= LENGTH (str);
    IF (str[k] <> '.') OR (k = LENGTH (str)) THEN  RETURN (FALSE);  END_IF;
    m := parse_express_identifier (str, k+1);
    IF m = k + 1 THEN  RETURN (FALSE);  END_IF;
    k := m;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION drop_numeric_constraints
 (spc : maths_space) : maths_space;
  LOCAL
    typenames : SET OF STRING := stripped_typeof(spc);
    tspc : listed_product_space;
    factors : LIST OF maths_space := [];
    xspc : extended_tuple_space;
  END_LOCAL;
  IF 'UNIFORM_PRODUCT_SPACE' IN typenames THEN
    RETURN (make_uniform_product_space (drop_numeric_constraints (
      spc\uniform_product_space.base), spc\uniform_product_space.exponent));
  END_IF;
  IF 'LISTED_PRODUCT_SPACE' IN typenames THEN
    tspc := spc;
    REPEAT i := 1 TO SIZEOF (tspc.factors);
      INSERT (factors, drop_numeric_constraints (tspc.factors[i]), i-1);
    END_REPEAT;
    RETURN (make_listed_product_space (factors));
  END_IF;
  IF 'EXTENDED_TUPLE_SPACE' IN typenames THEN
    xspc := spc;
    RETURN (make_extended_tuple_space (drop_numeric_constraints (xspc.base),
      drop_numeric_constraints (xspc.extender)));
  END_IF;
  IF subspace_of_es (spc, es_numbers) THEN
    RETURN (number_superspace_of (spc));
  END_IF;
  RETURN (spc);
                              
END_FUNCTION;

FUNCTION enclose_cregion_in_pregion
 (crgn : cartesian_complex_number_region; centre : complex_number_literal) : polar_complex_number_region;
  -- Find equivalent direction in range -PI < a <= PI.
  FUNCTION angle(a : REAL) : REAL;
    REPEAT WHILE a > PI;    a := a - 2.0*PI;  END_REPEAT;
    REPEAT WHILE a <= -PI;  a := a + 2.0*PI;  END_REPEAT;
    RETURN (a);
                              
END_FUNCTION;

FUNCTION strictly_in
 (z : REAL; zitv : real_interval) : LOGICAL;
    RETURN ((NOT min_exists(zitv) OR (z > real_min(zitv))) AND
      (NOT max_exists(zitv) OR (z < real_max(zitv))));
                              
END_FUNCTION;

FUNCTION enclose_pregion_in_cregion
 (prgn : polar_complex_number_region) : cartesian_complex_number_region;
  PROCEDURE nearest_good_direction(acart    : REAL;
                                   aitv     : finite_real_interval;
                                   VAR a    : REAL;
                                   VAR a_in : BOOLEAN);
    a := acart;                    a_in := TRUE;
    IF      a < aitv.min THEN
      -- a+2.0*PI > aitv.min automatically!
      IF a+2.0*PI < aitv.max THEN                               RETURN;  END_IF;
      IF a+2.0*PI = aitv.max THEN  a_in := max_included(aitv);  RETURN;  END_IF;
    ELSE IF a = aitv.min THEN      a_in := min_included(aitv);  RETURN;
    ELSE IF a < aitv.max THEN                                   RETURN;
    ELSE IF a = aitv.max THEN      a_in := max_included(aitv);  RETURN;
    END_IF;  END_IF;  END_IF;  END_IF;
    IF COS(acart - aitv.max) >= COS(acart - aitv.min) THEN
      a := aitv.max;               a_in := max_included(aitv);
    ELSE
      a := aitv.min;               a_in := min_included(aitv);
    END_IF;
                              
END_FUNCTION;

FUNCTION enclose_pregion_in_pregion
 (prgn : polar_complex_number_region; centre : complex_number_literal) : polar_complex_number_region;
  -- Find equivalent direction in range -PI < a <= PI.
  FUNCTION angle(a : REAL) : REAL;
    REPEAT WHILE a > PI;    a := a - 2.0*PI;  END_REPEAT;
    REPEAT WHILE a <= -PI;  a := a + 2.0*PI;  END_REPEAT;
    RETURN (a);
                              
END_FUNCTION;

FUNCTION strictly_in
 (a : REAL; aitv : finite_real_interval) : LOGICAL;
    a := angle(a);
    RETURN ({aitv.min < a < aitv.max} OR {aitv.min < a+2.0*PI < aitv.max});
                              
END_FUNCTION;

FUNCTION equal_cregion_pregion
 (crgn : cartesian_complex_number_region; prgn : polar_complex_number_region) : LOGICAL;
  LOCAL
    arng, amin, xc, yc : REAL;
    aitv, xitv, yitv : real_interval;
    c_in : BOOLEAN;
  END_LOCAL;
  IF NOT EXISTS (crgn) OR NOT EXISTS (prgn) THEN  RETURN (FALSE);  END_IF;
  IF max_exists(prgn.distance_constraint) THEN  RETURN (FALSE);  END_IF;
  IF real_min(prgn.distance_constraint) <> 0.0 THEN  RETURN (FALSE);  END_IF;
  c_in := min_included(prgn.distance_constraint);
  aitv := prgn.direction_constraint;
  amin := aitv.min;
  arng := aitv.max - amin;
  xc := prgn.centre.real_part;
  yc := prgn.centre.imag_part;
  xitv := crgn.real_constraint;
  yitv := crgn.imag_constraint;
  IF arng = 0.5*PI THEN
    IF amin = 0.0 THEN  -- quadrant to upper right
      RETURN (NOT max_exists(xitv) AND NOT max_exists(yitv) AND min_exists(xitv)
        AND min_exists(yitv) AND (real_min(xitv) = xc) AND (real_min(yitv) = yc)
        AND ((c_in AND min_included(aitv) AND max_included(aitv)
              AND min_included(xitv) AND min_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND max_included(aitv)
              AND min_included(xitv) AND NOT min_included(yitv))
          OR (NOT c_in AND min_included(aitv) AND NOT max_included(aitv)
              AND NOT min_included(xitv) AND min_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
              AND NOT min_included(xitv) AND NOT min_included(yitv))));
    END_IF;
    IF amin = 0.5*PI THEN  -- quadrant to upper left
      RETURN (max_exists(xitv) AND NOT max_exists(yitv) AND NOT min_exists(xitv)
        AND min_exists(yitv) AND (real_max(xitv) = xc) AND (real_min(yitv) = yc)
        AND ((c_in AND min_included(aitv) AND max_included(aitv)
              AND max_included(xitv) AND min_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND max_included(aitv)
              AND max_included(xitv) AND NOT min_included(yitv))
          OR (NOT c_in AND min_included(aitv) AND NOT max_included(aitv)
              AND NOT max_included(xitv) AND min_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
              AND NOT max_included(xitv) AND NOT min_included(yitv))));
    END_IF;
    IF amin = -PI THEN  -- quadrant to lower left
      RETURN (max_exists(xitv) AND max_exists(yitv) AND NOT min_exists(xitv)
        AND NOT min_exists(yitv) AND (real_max(xitv) = xc) AND (real_max(yitv) = yc)
        AND ((c_in AND min_included(aitv) AND max_included(aitv)
              AND max_included(xitv) AND max_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND max_included(aitv)
              AND max_included(xitv) AND NOT max_included(yitv))
          OR (NOT c_in AND min_included(aitv) AND NOT max_included(aitv)
              AND NOT max_included(xitv) AND max_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
              AND NOT max_included(xitv) AND NOT max_included(yitv))));
    END_IF;
    IF amin = -0.5*PI THEN  -- quadrant to lower right
      RETURN (NOT max_exists(xitv) AND max_exists(yitv) AND min_exists(xitv)
        AND NOT min_exists(yitv) AND (real_min(xitv) = xc) AND (real_max(yitv) = yc)
        AND ((c_in AND min_included(aitv) AND max_included(aitv)
              AND min_included(xitv) AND max_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND max_included(aitv)
              AND min_included(xitv) AND NOT max_included(yitv))
          OR (NOT c_in AND min_included(aitv) AND NOT max_included(aitv)
              AND NOT min_included(xitv) AND max_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
              AND NOT min_included(xitv) AND NOT max_included(yitv))));
    END_IF;
  END_IF;
  IF arng = PI THEN
    IF amin = 0.0 THEN  -- upper half space
      RETURN (NOT max_exists(xitv) AND NOT max_exists(yitv) AND NOT min_exists(xitv)
        AND min_exists(yitv) AND (real_min(yitv) = yc)
        AND ((c_in AND min_included(aitv) AND max_included(aitv)
              AND min_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
              AND NOT min_included(yitv))));
    END_IF;
    IF amin = 0.5*PI THEN  -- left half space
      RETURN (max_exists(xitv) AND NOT max_exists(yitv) AND NOT min_exists(xitv)
        AND NOT min_exists(yitv) AND (real_max(xitv) = xc)
        AND ((c_in AND min_included(aitv) AND max_included(aitv)
              AND max_included(xitv))
          OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
              AND NOT max_included(xitv))));
    END_IF;
    IF amin = -PI THEN  -- lower half space
      RETURN (NOT max_exists(xitv) AND max_exists(yitv) AND NOT min_exists(xitv)
        AND NOT min_exists(yitv) AND (real_max(yitv) = yc)
        AND ((c_in AND min_included(aitv) AND max_included(aitv)
              AND max_included(yitv))
          OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
              AND NOT max_included(yitv))));
    END_IF;
    IF amin = -0.5*PI THEN  -- right half space
      RETURN (NOT max_exists(xitv) AND NOT max_exists(yitv) AND min_exists(xitv)
        AND NOT min_exists(yitv) AND (real_min(xitv) = xc)
        AND ((c_in AND min_included(aitv) AND max_included(aitv)
              AND min_included(xitv))
          OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
              AND NOT min_included(xitv))));
    END_IF;
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION equal_maths_functions
 (fun1 : maths_function; fun2 : maths_function) : LOGICAL;
  LOCAL
    cum : LOGICAL;
  END_LOCAL;
  IF fun1 = fun2 THEN  RETURN (TRUE);   END_IF;
  cum := equal_maths_spaces(fun1.domain,fun2.domain);
  IF cum = FALSE THEN  RETURN (FALSE);  END_IF;
  cum := cum AND equal_maths_spaces(fun1.range,fun2.range);
  IF cum = FALSE THEN  RETURN (FALSE);  END_IF;
  -- A lot of further analysis is possible, but not required.
  RETURN (UNKNOWN);
                              
END_FUNCTION;

FUNCTION equal_maths_spaces
 (spc1 : maths_space; spc2 : maths_space) : LOGICAL;
  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);
                              
END_FUNCTION;

FUNCTION equal_maths_values
 (val1 : maths_value; val2 : maths_value) : LOGICAL;
  FUNCTION mem_of_vs(val1, val2 : maths_value) : LOGICAL;
    IF NOT has_values_space(val2) THEN RETURN (UNKNOWN);  END_IF;
    IF NOT member_of(val1,values_space_of(val2)) THEN  RETURN (FALSE);  END_IF;
    RETURN (UNKNOWN);
                              
END_FUNCTION;

FUNCTION es_subspace_of_es
 (es1 : elementary_space_enumerators; es2 : elementary_space_enumerators) : BOOLEAN;
  IF NOT EXISTS (es1) OR NOT EXISTS (es2) THEN  RETURN (FALSE);  END_IF;
  IF es1 = es2 THEN  RETURN (TRUE);  END_IF;
  IF es2 = es_generics THEN  RETURN (TRUE);  END_IF;
  IF (es1 = es_booleans) AND (es2 = es_logicals) THEN  RETURN (TRUE);  END_IF;
  IF (es2 = es_numbers) AND ((es1 = es_complex_numbers) OR (es1 = es_reals) OR
    (es1 = es_integers)) THEN  RETURN (TRUE);  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION expression_is_constant
 (expr : generic_expression) : BOOLEAN;
  RETURN (bool(SIZEOF (free_variables_of (expr)) = 0));
                              
END_FUNCTION;

FUNCTION extract_factors
 (tspace : tuple_space; m : INTEGER; n : INTEGER) : tuple_space;
  LOCAL
    tsp : tuple_space := the_zero_tuple_space;
  END_LOCAL;
  REPEAT i := m TO n;
    tsp := assoc_product_space (tsp, factor_space (tspace, i));
  END_REPEAT;
  RETURN (tsp);
                              
END_FUNCTION;

FUNCTION extremal_position_check
 (fun : linearized_table_function) : BOOLEAN;
  LOCAL
    source_domain : maths_space;
    source_interval : finite_integer_interval;
    index : INTEGER := 1;
    base : INTEGER;
    shape : LIST OF positive_integer;
    ndim : positive_integer;
    slo, shi : INTEGER;
    sublo : LIST OF INTEGER := [];
    subhi : LIST OF INTEGER := [];
  END_LOCAL;
  IF NOT EXISTS (fun) THEN  RETURN (FALSE);  END_IF;
  source_domain := factor1 (fun.source.domain);
  IF (schema_prefix + 'TUPLE_SPACE') IN TYPEOF (source_domain) THEN
    source_domain := factor1 (source_domain);
  END_IF;
  IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (source_domain)) THEN
    RETURN (FALSE);
  END_IF;
  source_interval := source_domain;
  base := fun\explicit_table_function.index_base;
  shape := fun\explicit_table_function.shape;
  IF (schema_prefix + 'STANDARD_TABLE_FUNCTION') IN TYPEOF (fun) THEN
    REPEAT j := 1 TO SIZEOF (shape);
      index := index * shape[j];
    END_REPEAT;
    index := fun.first + index - 1;
    RETURN (bool({source_interval.min <= index <= source_interval.max}));
  END_IF;
  IF (schema_prefix + 'REGULAR_TABLE_FUNCTION') IN TYPEOF (fun) THEN
    ndim := SIZEOF (fun\explicit_table_function.shape);
    REPEAT j:= 1 TO ndim;
      slo := base;
      shi := base + shape[j] - 1;
      IF fun\regular_table_function.increments[j] >= 0 THEN
        INSERT (sublo, slo, j-1);
        INSERT (subhi, shi, j-1);
      ELSE
        INSERT (sublo, shi, j-1);
        INSERT (subhi, slo, j-1);
      END_IF;
    END_REPEAT;
    index := regular_indexing (sublo, base, shape,
      fun\regular_table_function.increments, fun.first);
    IF NOT ({source_interval.min <= index <= source_interval.max}) THEN
      RETURN (FALSE);
    END_IF;
    index := regular_indexing (subhi, base, shape,
      fun\regular_table_function.increments, fun.first);
    IF NOT ({source_interval.min <= index <= source_interval.max}) THEN
      RETURN (FALSE);
    END_IF;
    RETURN (TRUE);
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION factor1
 (tspace : tuple_space) : maths_space;
  LOCAL
    typenames : SET OF STRING := TYPEOF (tspace);
  END_LOCAL;
  IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN typenames THEN
    RETURN (tspace\uniform_product_space.base);
  END_IF;
  IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN typenames THEN
    RETURN (tspace\listed_product_space.factors[1]);
    -- This path could return the indeterminate value if the list is empty.
    -- This is the correct result for this case.
  END_IF;
  IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN typenames THEN
    RETURN (factor1 (tspace\extended_tuple_space.base));
  END_IF;
  -- Should not be reachable.
  RETURN (?);
                              
END_FUNCTION;

FUNCTION factor_space
 (tspace : tuple_space; idx : positive_integer) : maths_space;
  LOCAL
    typenames : SET OF STRING := TYPEOF (tspace);
  END_LOCAL;
  IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN typenames THEN
    IF idx <= tspace\uniform_product_space.exponent THEN
      RETURN (tspace\uniform_product_space.base);
    END_IF;
    RETURN (?);
  END_IF;
  IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN typenames THEN
    IF idx <= SIZEOF (tspace\listed_product_space.factors) THEN
      RETURN (tspace\listed_product_space.factors[idx]);
    END_IF;
    RETURN (?);
  END_IF;
  IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN typenames THEN
    IF idx <= space_dimension (tspace\extended_tuple_space.base) THEN
      RETURN (factor_space (tspace\extended_tuple_space.base, idx));
    END_IF;
    RETURN (tspace\extended_tuple_space.extender);
  END_IF;
  -- Should not be reachable.
  RETURN (?);
                              
END_FUNCTION;

FUNCTION free_variables_of
 (expr : generic_expression) : SET OF generic_variable;
  LOCAL
    typenames : SET OF STRING := stripped_typeof(expr);
    result : SET OF generic_variable := [];
    exprs : LIST OF generic_expression := [];
  END_LOCAL;
  IF 'GENERIC_LITERAL' IN typenames THEN
    RETURN (result);
  END_IF;
  IF 'GENERIC_VARIABLE' IN typenames THEN
    result := result + expr;
    RETURN (result);
  END_IF;
  IF 'QUANTIFIER_EXPRESSION' IN typenames THEN
    exprs := QUERY (ge <* expr\multiple_arity_generic_expression.operands |
      NOT (ge IN expr\quantifier_expression.variables));
    REPEAT i := 1 TO SIZEOF (exprs);
      result := result + free_variables_of (exprs[i]);
    END_REPEAT;
    REPEAT i := 1 TO SIZEOF (expr\quantifier_expression.variables);
      result := result - expr\quantifier_expression.variables[i];
    END_REPEAT;
    RETURN (result);
  END_IF;
  IF 'UNARY_GENERIC_EXPRESSION' IN typenames THEN
    RETURN (free_variables_of (expr\unary_generic_expression.operand));
  END_IF;
  IF 'BINARY_GENERIC_EXPRESSION' IN typenames THEN
    result := free_variables_of (expr\binary_generic_expression.operands[1]);
    RETURN (result + free_variables_of (expr\binary_generic_expression.operands[2]));
  END_IF;
  IF 'MULTIPLE_ARITY_GENERIC_EXPRESSION' IN typenames THEN
    REPEAT i := 1 TO SIZEOF (expr\multiple_arity_generic_expression.operands);
      result := result + free_variables_of (
        expr\multiple_arity_generic_expression.operands[i]);
    END_REPEAT;
    RETURN (result);
  END_IF;
  -- In this case the subtype shall not contain any variable (see IP1 in
  -- generic_expression).
  RETURN (result);
                              
END_FUNCTION;

FUNCTION function_applicability
 (func : maths_function_select; arguments : LIST[1:?] OF maths_value) : BOOLEAN;
  LOCAL
    domain : tuple_space := convert_to_maths_function(func).domain;
    domain_types : SET OF STRING := TYPEOF (domain);
    narg : positive_integer := SIZEOF (arguments);
    arg : generic_expression;
  END_LOCAL;
  IF (schema_prefix + 'PRODUCT_SPACE') IN domain_types THEN
    IF space_dimension (domain) <> narg THEN  RETURN (FALSE);  END_IF;
  ELSE
    IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN domain_types THEN
      IF space_dimension (domain) > narg THEN  RETURN (FALSE);  END_IF;
    ELSE
      RETURN (FALSE);  -- Should be unreachable
    END_IF;
  END_IF;
  REPEAT i := 1 TO narg;
    arg := convert_to_operand (arguments[i]);
    IF NOT has_values_space (arg) THEN  RETURN (FALSE);  END_IF;
    IF NOT compatible_spaces (factor_space (domain, i), values_space_of (arg)) THEN
      RETURN (FALSE);
    END_IF;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION function_is_1d_array
 (func : maths_function) : BOOLEAN;
  LOCAL
    temp : maths_space;
  END_LOCAL;
  IF NOT EXISTS (func) THEN  RETURN (FALSE);  END_IF;
  IF space_dimension (func.domain) <> 1 THEN  RETURN (FALSE);  END_IF;
  temp := factor1 (func.domain);
  IF (schema_prefix + 'PRODUCT_SPACE') IN TYPEOF (temp) THEN
    IF space_dimension (temp) <> 1 THEN  RETURN (FALSE);  END_IF;
    temp := factor1 (temp);
  END_IF;
  IF (schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp) THEN
    RETURN (TRUE);
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION function_is_1d_table
 (func : maths_function) : BOOLEAN;
  LOCAL
    temp : maths_space;
    itvl : finite_integer_interval;
  END_LOCAL;
  IF NOT EXISTS (func) THEN  RETURN (FALSE);  END_IF;
  IF space_dimension (func.domain) <> 1 THEN  RETURN (FALSE);  END_IF;
  temp := factor1 (func.domain);
  IF (schema_prefix + 'PRODUCT_SPACE') IN TYPEOF (temp) THEN
    IF space_dimension (temp) <> 1 THEN  RETURN (FALSE);  END_IF;
    temp := factor1 (temp);
  END_IF;
  IF (schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp) THEN
    itvl := temp;
    RETURN (bool((itvl.min = 0) OR (itvl.min = 1)));
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION function_is_2d_table
 (func : maths_function) : BOOLEAN;
  LOCAL
    temp : maths_space;
    pspace : product_space;
    itvl1, itvl2 : finite_integer_interval;
  END_LOCAL;
  IF NOT EXISTS (func) THEN  RETURN (FALSE);  END_IF;
  IF space_dimension (func.domain) <> 1 THEN  RETURN (FALSE);  END_IF;
  temp := factor1 (func.domain);
  IF NOT ('PRODUCT_SPACE' IN stripped_typeof(temp)) THEN  RETURN (FALSE);  END_IF;
  pspace := temp;
  IF space_dimension (pspace) <> 2 THEN  RETURN (FALSE);  END_IF;
  temp := factor1 (pspace);
  IF NOT ('FINITE_INTEGER_INTERVAL' IN stripped_typeof(temp)) THEN
    RETURN (FALSE);
  END_IF;
  itvl1 := temp;
  temp := factor_space (pspace, 2);
  IF NOT ('FINITE_INTEGER_INTERVAL' IN stripped_typeof(temp)) THEN
    RETURN (FALSE);
  END_IF;
  itvl2 := temp;
  RETURN (bool((itvl1.min = itvl2.min) AND ((itvl1.min = 0) OR (itvl1.min = 1))));
                              
END_FUNCTION;

FUNCTION function_is_array
 (func : maths_function) : BOOLEAN;
  LOCAL
    tspace : tuple_space;
    temp : maths_space;
  END_LOCAL;
  IF NOT EXISTS (func) THEN  RETURN (FALSE);  END_IF;
  tspace := func.domain;
  IF (space_dimension (tspace) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
    TYPEOF (factor1 (tspace))) THEN
    tspace := factor1 (tspace);
  END_IF;
  IF NOT ((schema_prefix + 'PRODUCT_SPACE') IN TYPEOF (tspace)) THEN
    RETURN (FALSE);
  END_IF;
  REPEAT i := 1 TO space_dimension (tspace);
    temp := factor_space (tspace, i);
    IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
      RETURN (FALSE);
    END_IF;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION function_is_table
 (func : maths_function) : BOOLEAN;
  LOCAL
    tspace : tuple_space;
    temp : maths_space;
    base : INTEGER;
  END_LOCAL;
  IF NOT EXISTS (func) THEN  RETURN (FALSE);  END_IF;
  tspace := func.domain;
  IF (space_dimension (tspace) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
    TYPEOF (factor1 (tspace))) THEN
    tspace := factor1 (tspace);
  END_IF;
  IF NOT ((schema_prefix + 'PRODUCT_SPACE') IN TYPEOF (tspace)) THEN
    RETURN (FALSE);
  END_IF;
  temp := factor1 (tspace);
  IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
    RETURN (FALSE);
  END_IF;
  base := temp\finite_integer_interval.min;
  IF (base <> 0) AND (base <> 1) THEN
    RETURN (FALSE);
  END_IF;
  REPEAT i := 2 TO space_dimension (tspace);
    temp := factor_space (tspace, i);
    IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
      RETURN (FALSE);
    END_IF;
    IF temp\finite_integer_interval.min <> base THEN  RETURN (FALSE);  END_IF;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION has_values_space
 (expr : generic_expression) : BOOLEAN;
  LOCAL
    typenames : SET OF STRING := stripped_typeof (expr);
  END_LOCAL;
  IF 'EXPRESSION' IN typenames THEN
    RETURN (bool(('NUMERIC_EXPRESSION' IN typenames) OR
      ('STRING_EXPRESSION' IN typenames) OR
      ('BOOLEAN_EXPRESSION' IN typenames)));
  END_IF;
  IF 'MATHS_FUNCTION' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'FUNCTION_APPLICATION' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'MATHS_SPACE' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'MATHS_VARIABLE' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'DEPENDENT_VARIABLE_DEFINITION' IN typenames THEN
    RETURN (has_values_space (expr\unary_generic_expression.operand));
  END_IF;
  IF 'COMPLEX_NUMBER_LITERAL' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'LOGICAL_LITERAL' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'BINARY_LITERAL' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'MATHS_ENUM_LITERAL' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'REAL_TUPLE_LITERAL' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'INTEGER_TUPLE_LITERAL' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'ATOM_BASED_LITERAL' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'MATHS_TUPLE_LITERAL' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'PARTIAL_DERIVATIVE_EXPRESSION' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  IF 'DEFINITE_INTEGRAL_EXPRESSION' IN typenames THEN
    RETURN (TRUE);
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION list_selected_components
 (aggr : LIST OF LIST; k : positive_integer) : LIST OF maths_value;
  LOCAL
    result : LIST OF maths_value := [];
    j : INTEGER := 0;
  END_LOCAL;
  REPEAT i := LOINDEX (aggr) TO HIINDEX (aggr);
    IF k <= SIZEOF (aggr[i]) THEN
      INSERT (result, aggr[i][k], j);
      j := j + 1;
    END_IF;
  END_REPEAT;
  RETURN (result);
                              
END_FUNCTION;

FUNCTION make_abstracted_expression_function
 (operands : LIST[2:?] OF generic_expression) : abstracted_expression_function;
  RETURN (abstracted_expression_function()
    || maths_function()
      || generic_expression()
    || quantifier_expression (remove_first (operands))  -- derived
      || multiple_arity_generic_expression (operands) );
                              
END_FUNCTION;

FUNCTION make_atom_based_literal
 (lit_value : atom_based_value) : atom_based_literal;
  RETURN (atom_based_literal (lit_value)
    || generic_literal()
      || simple_generic_expression()
        || generic_expression() );
                              
END_FUNCTION;

FUNCTION make_b_spline_basis
 (degree : nonnegative_integer; repeated_knots : LIST[2:?] OF REAL) : b_spline_basis;
  RETURN (b_spline_basis (degree, repeated_knots)
    || maths_function()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_b_spline_function
 (coef : maths_function; bases : LIST[1:?] OF b_spline_basis) : b_spline_function;
  RETURN (b_spline_function (bases)
    || maths_function()
      || generic_expression()
    || unary_generic_expression (coef) );
                              
END_FUNCTION;

FUNCTION make_banded_matrix
 (index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; source : maths_function; first : INTEGER; default_entry : maths_value; below : INTEGER; above : INTEGER; order : ordering_type) : banded_matrix;
  RETURN (banded_matrix (default_entry, below, above, order)
    || linearized_table_function (first)
      || explicit_table_function (index_base, shape)
        || maths_function()
          || generic_expression()
      || unary_generic_expression (source) );
                              
END_FUNCTION;

FUNCTION make_basic_sparse_matrix
 (index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; operands : LIST[3:3] OF maths_function; default_entry : maths_value; order : ordering_type) : basic_sparse_matrix;
  RETURN (basic_sparse_matrix (default_entry, order)
    || explicit_table_function (index_base, shape)
      || maths_function()
        || generic_expression()
    || multiple_arity_generic_expression (operands) );
                              
END_FUNCTION;

FUNCTION make_binary_literal
 (lit_value : BINARY) : binary_literal;
  RETURN (binary_literal (lit_value)
    || generic_literal()
      || simple_generic_expression()
        || generic_expression() );
                              
END_FUNCTION;

FUNCTION make_boolean_literal
 (lit_value : BOOLEAN) : boolean_literal;
  RETURN (boolean_literal (lit_value)
    || simple_boolean_expression()
      || boolean_expression()
        || expression()
          || generic_expression()
      || simple_generic_expression()
    || generic_literal() );
                              
END_FUNCTION;

FUNCTION make_cartesian_complex_number_region
 (real_constraint : real_interval; imag_constraint : real_interval) : cartesian_complex_number_region;
  RETURN (cartesian_complex_number_region (real_constraint, imag_constraint)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_complex_number_literal
 (rpart : REAL; ipart : REAL) : complex_number_literal;
  RETURN (complex_number_literal (rpart, ipart)
    || generic_literal()
      || simple_generic_expression()
        || generic_expression() );
                              
END_FUNCTION;

FUNCTION make_constant_function
 (sole_value : maths_value; src_of_domn : maths_space_or_function) : constant_function;
  RETURN (constant_function (sole_value, src_of_domn)
    || maths_function()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_cos_expression
 (operand : numeric_expression) : cos_expression;
  RETURN (cos_expression()
    || unary_numeric_call_expression()
      || unary_numeric_expression()
        || numeric_expression()
          || expression()
            || generic_expression()
        || unary_generic_expression (operand) );
                              
END_FUNCTION;

FUNCTION make_definite_integral_expression
 (operands : LIST[2:4] OF generic_expression; loinf : BOOLEAN; upinf : BOOLEAN) : definite_integral_expression;
  RETURN (definite_integral_expression (loinf, upinf)
    || quantifier_expression ([operands[2]])
      || multiple_arity_generic_expression (operands)
        || generic_expression() );
                              
END_FUNCTION;

FUNCTION make_definite_integral_function
 (integrand : maths_function; varintg : input_selector; loinf : BOOLEAN; upinf : BOOLEAN) : definite_integral_function;
  RETURN (definite_integral_function (varintg, loinf, upinf)
    || maths_function()
      || generic_expression()
    || unary_generic_expression (integrand) );
                              
END_FUNCTION;

FUNCTION make_elementary_function
 (func_id : elementary_function_enumerators) : elementary_function;
  RETURN (elementary_function (func_id)
    || maths_function()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_elementary_space
 (space_id : elementary_space_enumerators) : elementary_space;
  RETURN (elementary_space (space_id)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_environment
 (varbl : generic_variable; sem : variable_semantics) : environment;
  RETURN (environment (varbl, sem) );
                              
END_FUNCTION;

FUNCTION make_expression_denoted_function
 (expression : generic_expression) : expression_denoted_function;
  RETURN (expression_denoted_function()
    || maths_function()
      || generic_expression()
    || unary_generic_expression (expression) );
                              
END_FUNCTION;

FUNCTION make_extended_tuple_space
 (base : product_space; extender : maths_space) : extended_tuple_space;
  RETURN (extended_tuple_space (base, extender)
    || maths_space ()
      || generic_expression()
    || generic_literal ()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_finite_function
 (pairs : SET[1:?] OF LIST) : finite_function;
  RETURN (finite_function (pairs)
    || maths_function()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_finite_integer_interval
 (min : INTEGER; max : INTEGER) : finite_integer_interval;
  RETURN (finite_integer_interval (min, max)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_finite_real_interval
 (min : REAL; minclo : open_closed; max : REAL; maxclo : open_closed) : finite_real_interval;
  RETURN (finite_real_interval (min, minclo, max, maxclo)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_finite_space
 (members : SET OF maths_value) : finite_space;
  RETURN (finite_space (members)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_function_application
 (afunction : maths_function_select; arguments : LIST[1:?] OF maths_value) : function_application;
  RETURN (function_application (afunction, arguments)
    || multiple_arity_generic_expression (convert_to_maths_function (afunction) +
      convert_to_operands (arguments))  -- derived
      || generic_expression() );
                              
END_FUNCTION;

FUNCTION make_function_space
 (domain_constraint : space_constraint_type; domain_argument : maths_space; range_constraint : space_constraint_type; range_argument : maths_space) : function_space;
  RETURN (function_space (domain_constraint, domain_argument, range_constraint,
    range_argument)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_general_linear_function
 (mat : maths_function; sum_index : one_or_two) : general_linear_function;
  RETURN (general_linear_function (sum_index)
    || maths_function()
      || generic_expression()
    || unary_generic_expression (mat) );
                              
END_FUNCTION;

FUNCTION make_int_literal
 (lit_value : INTEGER) : int_literal;
  RETURN (int_literal ()
    || literal_number(lit_value)
      || simple_numeric_expression()
        || numeric_expression()
          || expression()
            || generic_expression()
        || simple_generic_expression()
      || generic_literal() );
                              
END_FUNCTION;

FUNCTION make_integer_interval_from_min
 (min : INTEGER) : integer_interval_from_min;
  RETURN (integer_interval_from_min (min)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_listed_complex_number_data
 (index_base : zero_or_one; values : LIST[2:?] OF REAL) : listed_complex_number_data;
  RETURN (listed_complex_number_data (values)
    || explicit_table_function (index_base, [SIZEOF (values)/2])  -- 2nd derived
      || maths_function()
        || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_listed_data
 (index_base : zero_or_one; values : LIST[2:?] OF maths_value; value_range : maths_space) : listed_data;
  RETURN (listed_data (values, value_range)
    || explicit_table_function (index_base, [SIZEOF (values)])  -- 2nd derived
      || maths_function()
        || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_listed_integer_data
 (index_base : zero_or_one; values : LIST[1:?] OF INTEGER) : listed_integer_data;
  RETURN (listed_integer_data (values)
    || explicit_table_function (index_base, [SIZEOF (values)])  -- 2nd derived
      || maths_function()
        || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_listed_product_space
 (factors : LIST OF maths_space) : listed_product_space;
  RETURN (listed_product_space (factors)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_listed_real_data
 (index_base : zero_or_one; values : LIST[1:?] OF REAL) : listed_real_data;
  RETURN (listed_real_data (values)
    || explicit_table_function (index_base, [SIZEOF (values)])  -- 2nd derived
      || maths_function()
        || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_logical_literal
 (lit_value : LOGICAL) : logical_literal;
  RETURN (logical_literal (lit_value)
    || generic_literal()
      || simple_generic_expression()
        || generic_expression() );
                              
END_FUNCTION;

FUNCTION make_maths_enum_literal
 (lit_value : maths_enum_atom) : maths_enum_literal;
  RETURN (maths_enum_literal (lit_value)
    || generic_literal()
      || simple_generic_expression()
        || generic_expression() );
                              
END_FUNCTION;

FUNCTION make_maths_real_variable
 (values_space : maths_space; name : label) : maths_real_variable;
  RETURN (maths_real_variable()
    || maths_variable (values_space, name)
      || generic_variable()
        || simple_generic_expression()
          || generic_expression()
    || real_numeric_variable()
      || numeric_variable()
        || variable() );
                              
END_FUNCTION;

FUNCTION make_maths_tuple_literal
 (lit_value : LIST OF maths_value) : maths_tuple_literal;
  RETURN (maths_tuple_literal (lit_value)
    || generic_literal()
      || simple_generic_expression()
        || generic_expression() );
                              
END_FUNCTION;

FUNCTION make_mult_expression
 (operands : LIST[2:?] OF generic_expression) : mult_expression;
  RETURN (mult_expression()
    || multiple_arity_numeric_expression()
      || numeric_expression()
        || expression()
          || generic_expression()
      || multiple_arity_generic_expression (operands) );
                              
END_FUNCTION;

FUNCTION make_parallel_composed_function
 (srcdom : maths_space_or_function; prepfuncs : LIST[2:?] OF maths_function; finfunc : maths_function_select) : parallel_composed_function;
  RETURN (parallel_composed_function (srcdom, prepfuncs, finfunc)
    || maths_function()
      || generic_expression()
    || multiple_arity_generic_expression (convert_to_operands_prcmfn (
      srcdom, prepfuncs, finfunc)) );  -- derived
                              
END_FUNCTION;

FUNCTION make_partial_derivative_expression
 (derivand : generic_expression; dvars : LIST[1:?] OF maths_variable; extend : extension_options) : partial_derivative_expression;
  RETURN (partial_derivative_expression (dvars, extend)
    || unary_generic_expression (derivand)
      || generic_expression() );
                              
END_FUNCTION;

FUNCTION make_partial_derivative_function
 (derivand : maths_function; dvars : LIST[1:?] OF input_selector; extend : extension_options) : partial_derivative_function;
  RETURN (partial_derivative_function (dvars, extend)
    || maths_function()
      || generic_expression()
    || unary_generic_expression (derivand) );
                              
END_FUNCTION;

FUNCTION make_polar_complex_number_region
 (centre : complex_number_literal; dis_constraint : real_interval; dir_constraint : finite_real_interval) : polar_complex_number_region;
  RETURN (polar_complex_number_region (centre, dis_constraint, dir_constraint)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_rationalize_function
 (fun : maths_function) : rationalize_function;
  RETURN (rationalize_function()
    || maths_function()
      || generic_expression()
    || unary_generic_expression (fun) );
                              
END_FUNCTION;

FUNCTION make_real_interval_from_min
 (min : REAL; minclo : open_closed) : real_interval_from_min;
  RETURN (real_interval_from_min (min, minclo)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_real_interval_to_max
 (max : REAL; maxclo : open_closed) : real_interval_to_max;
  RETURN (real_interval_to_max (max, maxclo)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_real_literal
 (lit_value : REAL) : real_literal;
  RETURN (real_literal ()
    || literal_number(lit_value)
      || simple_numeric_expression()
        || numeric_expression()
          || expression()
            || generic_expression()
        || simple_generic_expression()
      || generic_literal() );
                              
END_FUNCTION;

FUNCTION make_regular_table_function
 (index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; operand : maths_function; first : INTEGER; increments : LIST[1:?] OF INTEGER) : regular_table_function;
  RETURN (regular_table_function (increments)
    || linearized_table_function (first)
      || explicit_table_function (index_base, shape)
        || maths_function()
          || generic_expression()
      || unary_generic_expression (operand) );
                              
END_FUNCTION;

FUNCTION make_reindexed_array_function
 (func : maths_function; start_idxs : LIST[1:?] OF INTEGER) : reindexed_array_function;
  RETURN (reindexed_array_function(start_idxs)
    || maths_function()
      || generic_expression()
    || unary_generic_expression (func) );
                              
END_FUNCTION;

FUNCTION make_repackaging_function
 (operand : maths_function; input_repack : repackage_options; output_repack : repackage_options; selected_output : nonnegative_integer) : repackaging_function;
  RETURN (repackaging_function (input_repack, output_repack, selected_output)
    || maths_function()
      || generic_expression()
    || unary_generic_expression (operand) );
                              
END_FUNCTION;

FUNCTION make_selector_function
 (selector : input_selector; src_of_domn : maths_space_or_function) : selector_function;
  RETURN (selector_function (selector, src_of_domn)
    || maths_function()
       || generic_expression()
    || generic_literal()
       || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION make_series_composed_function
 (functions : LIST[2:?] OF maths_function) : series_composed_function;
  RETURN (series_composed_function()
    || maths_function()
      || generic_expression()
    || multiple_arity_generic_expression (functions) );
                              
END_FUNCTION;

FUNCTION make_sin_expression
 (operand : numeric_expression) : sin_expression;
  RETURN (sin_expression()
    || unary_numeric_call_expression()
      || unary_numeric_expression()
        || numeric_expression()
          || expression()
            || generic_expression()
        || unary_generic_expression (operand) );
                              
END_FUNCTION;

FUNCTION make_standard_table_function
 (index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; operand : maths_function; first : INTEGER; order : ordering_type) : standard_table_function;
  RETURN (standard_table_function (order)
    || linearized_table_function (first)
      || explicit_table_function (index_base, shape)
        || maths_function()
          || generic_expression()
      || unary_generic_expression (operand) );
                              
END_FUNCTION;

FUNCTION make_strict_triangular_matrix
 (index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; source : maths_function; first : INTEGER; default_entry : maths_value; lo_up : lower_upper; order : ordering_type; main_diagonal_value : maths_value) : strict_triangular_matrix;
  RETURN (strict_triangular_matrix (main_diagonal_value)
    || triangular_matrix (default_entry, lo_up, order)
      || linearized_table_function (first)
        || explicit_table_function (index_base, shape)
          || maths_function()
            || generic_expression()
        || unary_generic_expression (source) );
                              
END_FUNCTION;

FUNCTION make_string_literal
 (lit_value : STRING) : string_literal;
  RETURN (string_literal (lit_value)
    || simple_string_expression()
      || string_expression()
        || expression()
          || generic_expression()
      || simple_generic_expression()
    || generic_literal() );
                              
END_FUNCTION;

FUNCTION make_unary_minus_expression
 (operand : numeric_expression) : unary_minus_expression;
  RETURN (unary_minus_expression()
    || unary_numeric_call_expression()
      || unary_numeric_expression()
        || numeric_expression()
          || expression()
            || generic_expression()
        || unary_generic_expression (operand) );
                              
END_FUNCTION;

FUNCTION make_uniform_product_space
 (base : maths_space; exponent : positive_integer) : uniform_product_space;
  RETURN (uniform_product_space (base, exponent)
    || maths_space()
      || generic_expression()
    || generic_literal()
      || simple_generic_expression() );
                              
END_FUNCTION;

FUNCTION max_exists
 (spc : maths_space) : BOOLEAN;
  LOCAL
    types : SET OF STRING := TYPEOF (spc);
  END_LOCAL;
  RETURN (bool(((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) OR
    ((schema_prefix + 'INTEGER_INTERVAL_TO_MAX') IN types) OR
    ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) OR
    ((schema_prefix + 'REAL_INTERVAL_TO_MAX') IN types)));
                              
END_FUNCTION;

FUNCTION max_included
 (spc : maths_space) : BOOLEAN;
  LOCAL
    types : SET OF STRING := TYPEOF (spc);
  END_LOCAL;
  IF ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) OR
    ((schema_prefix + 'INTEGER_INTERVAL_TO_MAX') IN types) THEN
    RETURN (TRUE);
  END_IF;
  IF ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) THEN
    RETURN (bool(spc\finite_real_interval.max_closure = closed));
  END_IF;
  IF ((schema_prefix + 'REAL_INTERVAL_TO_MAX') IN types) THEN
    RETURN (bool(spc\real_interval_to_max.max_closure = closed));
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION member_of
 (val : GENERIC; spc : maths_space) : LOGICAL;

  -- Trivial function introduced to avoid NIST Fedex compiler error
  FUNCTION fedex(val : AGGREGATE OF GENERIC:X;
                 i   : INTEGER) : GENERIC:X;
    RETURN (val[i]);
                              
END_FUNCTION;

FUNCTION min_exists
 (spc : maths_space) : BOOLEAN;
  LOCAL
    types : SET OF STRING := TYPEOF (spc);
  END_LOCAL;
  RETURN (bool(((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) OR
    ((schema_prefix + 'INTEGER_INTERVAL_FROM_MIN') IN types) OR
    ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) OR
    ((schema_prefix + 'REAL_INTERVAL_FROM_MIN') IN types)));
                              
END_FUNCTION;

FUNCTION min_included
 (spc : maths_space) : BOOLEAN;
  LOCAL
    types : SET OF STRING := TYPEOF (spc);
  END_LOCAL;
  IF ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) OR
    ((schema_prefix + 'INTEGER_INTERVAL_FROM_MIN') IN types) THEN
    RETURN (TRUE);
  END_IF;
  IF ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) THEN
    RETURN (bool(spc\finite_real_interval.min_closure = closed));
  END_IF;
  IF ((schema_prefix + 'REAL_INTERVAL_FROM_MIN') IN types) THEN
    RETURN (bool(spc\real_interval_from_min.min_closure = closed));
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION no_cyclic_domain_reference
 (ref : maths_space_or_function; used : SET OF maths_function) : BOOLEAN;
  LOCAL
    typenames : SET OF STRING := TYPEOF (ref);
    func      : maths_function;
  END_LOCAL;
  IF (NOT EXISTS (ref)) OR (NOT EXISTS (used)) THEN
    RETURN (FALSE);
  END_IF;
  IF (schema_prefix + 'MATHS_SPACE') IN typenames THEN
    RETURN (TRUE);
  END_IF;
  func := ref;
  IF func IN used THEN
    RETURN (FALSE);
  END_IF;
  IF (schema_prefix + 'CONSTANT_FUNCTION') IN typenames THEN
    RETURN (no_cyclic_domain_reference (func\constant_function.source_of_domain,
      used + [func]));
  END_IF;
  IF (schema_prefix + 'SELECTOR_FUNCTION') IN typenames THEN
    RETURN (no_cyclic_domain_reference (func\selector_function.source_of_domain,
      used + [func]));
  END_IF;
  IF (schema_prefix + 'PARALLEL_COMPOSED_FUNCTION') IN typenames THEN
    RETURN (no_cyclic_domain_reference (
      func\parallel_composed_function.source_of_domain, used + [func]));
  END_IF;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION no_cyclic_space_reference
 (spc : maths_space; refs : SET OF maths_space) : BOOLEAN;
  LOCAL
    types : SET OF STRING;
    refs_plus : SET OF maths_space;
  END_LOCAL;
  IF (spc IN refs) THEN
    RETURN (FALSE);
  END_IF;
  types := TYPEOF (spc);
  refs_plus := refs + spc;
  IF (schema_prefix + 'FINITE_SPACE') IN types THEN
    RETURN (bool(SIZEOF (QUERY (sp <* QUERY (mem <* spc\finite_space.members |
      (schema_prefix + 'MATHS_SPACE') IN TYPEOF (mem)) |
      NOT no_cyclic_space_reference (sp, refs_plus))) = 0));
  END_IF;
  IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN types THEN
    RETURN (no_cyclic_space_reference (spc\uniform_product_space.base, refs_plus));
  END_IF;
  IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN types THEN
    RETURN (bool(SIZEOF (QUERY (fac <* spc\listed_product_space.factors |
      NOT no_cyclic_space_reference (fac, refs_plus))) = 0));
  END_IF;
  IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN types THEN
    RETURN (no_cyclic_space_reference (spc\extended_tuple_space.base, refs_plus)
      AND no_cyclic_space_reference (spc\extended_tuple_space.extender, refs_plus));
  END_IF;
  -- spc contains no references to other spaces
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION nondecreasing
 (lr : LIST OF REAL) : BOOLEAN;
  IF NOT EXISTS (lr) THEN
    RETURN (FALSE);
  END_IF;
  REPEAT j := 2 TO SIZEOF (lr);
    IF lr[j] < lr[j-1] THEN
      RETURN (FALSE);
    END_IF;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION number_superspace_of
 (spc : maths_space) : elementary_space;
  IF subspace_of_es(spc,es_integers) THEN  RETURN (the_integers);  END_IF;
  IF subspace_of_es(spc,es_reals)    THEN  RETURN (the_reals);     END_IF;
  IF subspace_of_es(spc,es_complex_numbers) THEN  RETURN (the_complex_numbers); END_IF;
  IF subspace_of_es(spc,es_numbers)  THEN  RETURN (the_numbers);   END_IF;
  RETURN (?);
                              
END_FUNCTION;

FUNCTION number_tuple_subspace_check
 (spc : maths_space) : LOGICAL;
  LOCAL
    types : SET OF STRING := stripped_typeof(spc);
    factors : LIST OF maths_space;
    cum : LOGICAL := TRUE;
  END_LOCAL;
  IF 'UNIFORM_PRODUCT_SPACE' IN types THEN
    RETURN (subspace_of_es(spc\uniform_product_space.base,es_numbers));
  END_IF;
  IF 'LISTED_PRODUCT_SPACE' IN types THEN
    factors := spc\listed_product_space.factors;
    REPEAT i := 1 TO SIZEOF (factors);
      cum := cum AND subspace_of_es(factors[i],es_numbers);
    END_REPEAT;
    RETURN (cum);
  END_IF;
  IF 'EXTENDED_TUPLE_SPACE' IN types THEN
    cum := subspace_of_es(spc\extended_tuple_space.extender,es_numbers);
    cum := cum AND number_tuple_subspace_check(spc\extended_tuple_space.base);
    RETURN (cum);
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION one_tuples_of
 (spc : maths_space) : tuple_space;
  RETURN (make_uniform_product_space (spc, 1));
                              
END_FUNCTION;

FUNCTION parallel_composed_function_composability_check
 (funcs : LIST OF maths_function; final : maths_function_select) : BOOLEAN;
  LOCAL
    tplsp : tuple_space := the_zero_tuple_space;
    finfun : maths_function := convert_to_maths_function (final);
  END_LOCAL;
  REPEAT i := 1 TO SIZEOF (funcs);
    tplsp := assoc_product_space (tplsp, funcs[i].range);
  END_REPEAT;
  RETURN (compatible_spaces (tplsp, finfun.domain));
                              
END_FUNCTION;

FUNCTION parallel_composed_function_domain_check
 (comdom : tuple_space; funcs : LIST OF maths_function) : BOOLEAN;
  REPEAT i := 1 TO SIZEOF (funcs);
    IF NOT (compatible_spaces (comdom, funcs[i].domain)) THEN
      RETURN (FALSE);
    END_IF;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION parse_express_identifier
 (s : STRING; i : positive_integer) : positive_integer;
  LOCAL
    k : positive_integer;
  END_LOCAL;
  k := i;
  IF i <= LENGTH (s) THEN
    IF (s[i] LIKE '@') THEN
      REPEAT UNTIL (k > LENGTH (s)) OR
        ((s[k] <> '_') AND NOT (s[k] LIKE '@') AND NOT (s[k] LIKE '#'));
        k := k + 1;
      END_REPEAT;
    END_IF;
  END_IF;
  RETURN (k);
                              
END_FUNCTION;

FUNCTION partial_derivative_check
 (domain : tuple_space; d_vars : LIST[1:?] OF input_selector) : BOOLEAN;
  LOCAL
    domn : tuple_space := domain;
    fspc : maths_space;
    dim : INTEGER;
    k : INTEGER;
  END_LOCAL;
  IF (space_dimension (domain) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
    TYPEOF (factor1 (domain))) THEN
    domn := factor1 (domain);
  END_IF;
  dim := space_dimension (domn);
  REPEAT i := 1 TO SIZEOF (d_vars);
    k := d_vars[i];
    IF k > dim THEN
       RETURN (FALSE);
    END_IF;
    fspc := factor_space (domn, k);
    IF (NOT subspace_of_es (fspc,es_reals)) AND
      (NOT subspace_of_es (fspc,es_complex_numbers)) THEN
      RETURN (FALSE);
    END_IF;
  END_REPEAT;
  RETURN (TRUE);
                              
END_FUNCTION;

FUNCTION real_max
 (spc : maths_space) : REAL;
  LOCAL
    types : SET OF STRING := TYPEOF (spc);
  END_LOCAL;
  IF ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) THEN
    RETURN (spc\finite_integer_interval.max);
  END_IF;
  IF ((schema_prefix + 'INTEGER_INTERVAL_TO_MAX') IN types) THEN
    RETURN (spc\integer_interval_to_max.max);
  END_IF;
  IF ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) THEN
    RETURN (spc\finite_real_interval.max);
  END_IF;
  IF ((schema_prefix + 'REAL_INTERVAL_TO_MAX') IN types) THEN
    RETURN (spc\real_interval_to_max.max);
  END_IF;
  RETURN (?);
                              
END_FUNCTION;

FUNCTION real_min
 (spc : maths_space) : REAL;
  LOCAL
    types : SET OF STRING := TYPEOF (spc);
  END_LOCAL;
  IF ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) THEN
    RETURN (spc\finite_integer_interval.min);
  END_IF;
  IF ((schema_prefix + 'INTEGER_INTERVAL_FROM_MIN') IN types) THEN
    RETURN (spc\integer_interval_from_min.min);
  END_IF;
  IF ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) THEN
    RETURN (spc\finite_real_interval.min);
  END_IF;
  IF ((schema_prefix + 'REAL_INTERVAL_FROM_MIN') IN types) THEN
    RETURN (spc\real_interval_from_min.min);
  END_IF;
  RETURN (?);
                              
END_FUNCTION;

FUNCTION regular_indexing
 (sub : LIST OF INTEGER; base : zero_or_one; shape : LIST[1:?] OF positive_integer; inc : LIST[1:?] OF INTEGER; first : INTEGER) : INTEGER;
  LOCAL
    k : INTEGER;
    index : INTEGER;
  END_LOCAL;
  IF NOT EXISTS (sub) OR NOT EXISTS (base) OR NOT EXISTS (shape) OR
    NOT EXISTS (inc) OR NOT EXISTS (first) THEN
    RETURN (?);
  END_IF;
  IF (SIZEOF (sub) <> SIZEOF (inc)) OR (SIZEOF (sub) <> SIZEOF (shape)) THEN
    RETURN (?);
  END_IF;
  index := first;
  REPEAT j := 1 TO SIZEOF (sub);
    IF NOT EXISTS (sub[j]) OR NOT EXISTS (inc[j]) THEN
      RETURN (?);
    END_IF;
    k := sub[j] - base;
    IF NOT ({0 <= k < shape[j]}) THEN
      RETURN (?);
    END_IF;
    index := index + k*inc[j];
  END_REPEAT;
  RETURN (index);
                              
END_FUNCTION;

FUNCTION remove_first
 (alist : LIST OF GENERICGEN) : LIST OF GENERICGEN;
  LOCAL
    blist : LIST OF GENERIC:GEN := alist;
  END_LOCAL;
  IF SIZEOF (blist) > 0 THEN
    REMOVE (blist, 1);
  END_IF;
  RETURN (blist);
                              
END_FUNCTION;

FUNCTION repackage
 (tspace : tuple_space; repckg : repackage_options) : tuple_space;
  CASE repckg OF
  ro_nochange : RETURN (tspace);
  ro_wrap_as_tuple : RETURN (one_tuples_of (tspace));
  ro_unwrap_tuple : RETURN (factor1 (tspace));
  OTHERWISE : RETURN (?);
  END_CASE;
                              
END_FUNCTION;

FUNCTION shape_of_array
 (func : maths_function) : LIST OF positive_integer;
  LOCAL
    tspace : tuple_space;
    temp : maths_space;
    result : LIST OF positive_integer := [];
  END_LOCAL;
  IF (schema_prefix + 'EXPLICIT_TABLE_FUNCTION') IN TYPEOF (func) THEN
    RETURN (func\explicit_table_function.shape);
  END_IF;
  tspace := func.domain;
  IF (space_dimension (tspace) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
    TYPEOF (factor1 (tspace))) THEN
    tspace := factor1 (tspace);
  END_IF;
  REPEAT i := 1 TO space_dimension (tspace);
    temp := factor_space (tspace, i);
    IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
      RETURN (?);
    END_IF;
    INSERT (result, temp\finite_integer_interval.size, i-1);
  END_REPEAT;
  RETURN (result);
                              
END_FUNCTION;

FUNCTION simplify_function_application
 (expr : function_application) : maths_value;
  FUNCTION ctmv(x : GENERIC:G) : maths_value;
    RETURN (convert_to_maths_value(x));
                              
END_FUNCTION;

FUNCTION makec
 (x : REAL; y : REAL) : complex_number_literal;
    RETURN (make_complex_number_literal(x,y));
                              
END_FUNCTION;

FUNCTION good_t
 (v : maths_value; tn : STRING) : BOOLEAN;
    LOCAL
      tpl : LIST OF maths_value;
    END_LOCAL;
    IF 'LIST' IN TYPEOF (v) THEN
      tpl := v;
      REPEAT i := 1 TO SIZEOF (tpl);
        IF NOT (tn IN TYPEOF (tpl[i])) THEN  RETURN (FALSE);  END_IF;
      END_REPEAT;
      RETURN (TRUE);
    END_IF;
    RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION simplify_generic_expression
 (expr : generic_expression) : maths_value;
  FUNCTION restore_unary(expr : unary_generic_expression;
                         opnd : generic_expression) : generic_expression;
    expr.operand := opnd;
    RETURN (expr);
                              
END_FUNCTION;

FUNCTION restore_binary
 (expr : binary_generic_expression; opd1 : generic_expression; opd2 : generic_expression) : generic_expression;
    expr.operands[1] := opd1;
    expr.operands[2] := opd2;
    RETURN (expr);
                              
END_FUNCTION;

FUNCTION restore_mulary
 (expr : multiple_arity_generic_expression; ops : LIST OF generic_expression) : generic_expression;
    expr.operands := ops;
    RETURN (expr);
                              
END_FUNCTION;

FUNCTION make_number_literal
 (nmb : NUMBER) : generic_literal;
    IF 'INTEGER' IN TYPEOF (nmb) THEN  RETURN (make_int_literal(nmb));  END_IF;
    RETURN (make_real_literal(nmb));
                              
END_FUNCTION;

FUNCTION simplify_maths_space
 (spc : maths_space) : maths_space;
  LOCAL
    stypes : SET OF STRING := stripped_typeof (spc);
    sset : SET OF maths_value;
    zset : SET OF maths_value := [];
    zval : maths_value;
    zspc : maths_space;
    zallint : BOOLEAN := TRUE;
    zint, zmin, zmax : INTEGER;
    factors : LIST OF maths_space;
    zfactors : LIST OF maths_space := [];
    rspc : maths_space;
  END_LOCAL;
  IF 'FINITE_SPACE' IN stypes THEN
    sset := spc\finite_space.members;
    REPEAT i := 1 TO SIZEOF (sset);
      zval := simplify_maths_value(sset[i]);
      zset := zset + [zval];
      IF zallint AND ('INTEGER' IN TYPEOF (zval)) THEN
        zint := zval;
        IF i = 1 THEN
          zmin := zint;
          zmax := zint;
        ELSE
          IF zint < zmin THEN
            zmin := zint;
          END_IF;
          IF zint > zmax THEN
            zmax := zint;
          END_IF;
        END_IF;
      ELSE
        zallint := FALSE;
      END_IF;
    END_REPEAT;
    IF zallint AND (SIZEOF(zset) = zmax-zmin+1) THEN
      RETURN (make_finite_integer_interval(zmin,zmax));
    END_IF;
    RETURN (make_finite_space(zset));
  END_IF;
  IF 'UNIFORM_PRODUCT_SPACE' IN stypes THEN
    zspc := simplify_maths_space(spc\uniform_product_space.base);
    RETURN (make_uniform_product_space(zspc,spc\uniform_product_space.exponent));
  END_IF;
  IF 'LISTED_PRODUCT_SPACE' IN stypes THEN
    factors := spc\listed_product_space.factors;
    REPEAT i := 1 TO SIZEOF (factors);
      INSERT (zfactors, simplify_maths_space(factors[i]), i-1);
    END_REPEAT;
    RETURN (make_listed_product_space(zfactors));
  END_IF;
  IF 'EXTENDED_TUPLE_SPACE' IN stypes THEN
    zspc := simplify_maths_space(spc\extended_tuple_space.base);
    rspc := simplify_maths_space(spc\extended_tuple_space.extender);
    RETURN (make_extended_tuple_space(zspc,rspc));
  END_IF;
  IF 'FUNCTION_SPACE' IN stypes THEN
    zspc := simplify_maths_space(spc\function_space.domain_argument);
    rspc := simplify_maths_space(spc\function_space.range_argument);
    RETURN (make_function_space(spc\function_space.domain_constraint,zspc,
      spc\function_space.range_constraint,rspc));
  END_IF;
  RETURN (spc);
                              
END_FUNCTION;

FUNCTION simplify_maths_value
 (val : maths_value) : maths_value;
  LOCAL
    vtypes : SET OF STRING := stripped_typeof(val);
    vlist : LIST OF maths_value;
    nlist : LIST OF maths_value := [];
  END_LOCAL;
  IF 'GENERIC_EXPRESSION' IN vtypes THEN
    RETURN (simplify_generic_expression(val));
  END_IF;
  IF 'LIST' IN vtypes THEN
    vlist := val;
    REPEAT i := 1 TO SIZEOF (vlist);
      INSERT (nlist, simplify_maths_value(vlist[i]), i-1);
    END_REPEAT;
    RETURN (convert_to_maths_value(nlist));
  END_IF;
  RETURN (val);
                              
END_FUNCTION;

FUNCTION singleton_member_of
 (spc : maths_space) : maths_value;
  LOCAL
    types : SET OF STRING := stripped_typeof (spc);
  END_LOCAL;
  IF 'FINITE_SPACE' IN types THEN
    IF SIZEOF (spc\finite_space.members) = 1 THEN
      RETURN (spc\finite_space.members[1]);
    END_IF;
    RETURN (?);
  END_IF;
  IF 'FINITE_INTEGER_INTERVAL' IN types THEN
    IF spc\finite_integer_interval.size = 1 THEN
      RETURN (spc\finite_integer_interval.min);
    END_IF;
    RETURN (?);
  END_IF;
  RETURN (?);
                              
END_FUNCTION;

FUNCTION space_dimension
 (tspace : tuple_space) : nonnegative_integer;
  LOCAL
    types : SET OF STRING := TYPEOF (tspace);
  END_LOCAL;
  IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN types THEN
    RETURN (tspace\uniform_product_space.exponent);
  END_IF;
  IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN types THEN
    RETURN (SIZEOF (tspace\listed_product_space.factors));
  END_IF;
  IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN types THEN
    -- In the case of an extended_tuple_space, the minimum dimension is returned.
    RETURN (space_dimension (tspace\extended_tuple_space.base));
  END_IF;
  -- Should be unreachable
  RETURN (?);
                              
END_FUNCTION;

FUNCTION space_is_continuum
 (space : maths_space) : BOOLEAN;
  LOCAL
    typenames : SET OF STRING := TYPEOF (space);
    factors : LIST OF maths_space;
  END_LOCAL;
  IF NOT EXISTS (space) THEN
    RETURN (FALSE);
  END_IF;
  IF subspace_of_es(space,es_reals) OR subspace_of_es(space,es_complex_numbers) THEN
    RETURN (TRUE);
  END_IF;
  IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN typenames THEN
    RETURN (space_is_continuum(space\uniform_product_space.base));
  END_IF;
  IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN typenames THEN
    factors := space\listed_product_space.factors;
    IF SIZEOF(factors) = 0 THEN
      RETURN (FALSE);
    END_IF;
    REPEAT i := 1 TO SIZEOF (factors);
      IF NOT space_is_continuum(factors[i]) THEN
        RETURN (FALSE);
      END_IF;
    END_REPEAT;
    RETURN (TRUE);
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION space_is_singleton
 (spc : maths_space) : BOOLEAN;
  LOCAL
    types : SET OF STRING := stripped_typeof (spc);
  END_LOCAL;
  IF 'FINITE_SPACE' IN types THEN
    RETURN (bool(SIZEOF (spc\finite_space.members) = 1));
  END_IF;
  IF 'FINITE_INTEGER_INTERVAL' IN types THEN
    RETURN (bool(spc\finite_integer_interval.size = 1));
  END_IF;
  RETURN (FALSE);
                              
END_FUNCTION;

FUNCTION stripped_typeof
 (arg : GENERIC) : SET OF STRING;
  LOCAL
    types : SET OF STRING := TYPEOF (arg);
    stypes : SET OF STRING := [];
    n : INTEGER := LENGTH (schema_prefix);
  END_LOCAL;
  REPEAT i := 1 TO SIZEOF (types);
    IF types[i][1:n] = schema_prefix THEN
       stypes := stypes + [types[i][n+1:LENGTH(types[i])]];
    ELSE
       stypes := stypes + [types[i]];
    END_IF;
  END_REPEAT;
  RETURN (stypes);
                              
END_FUNCTION;

FUNCTION subspace_of
 (space1 : maths_space; space2 : maths_space) : LOGICAL;
  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);
                              
END_FUNCTION;

FUNCTION subspace_of_es
 (spc : maths_space; es : elementary_space_enumerators) : LOGICAL;
  LOCAL
    types : SET OF STRING := stripped_typeof(spc);
  END_LOCAL;
  IF NOT EXISTS (spc) OR NOT EXISTS (es) THEN  RETURN (FALSE);  END_IF;
  IF 'ELEMENTARY_SPACE' IN types THEN
    RETURN (es_subspace_of_es(spc\elementary_space.space_id,es));
  END_IF;
  IF 'FINITE_SPACE' IN types THEN
    RETURN (all_members_of_es(spc\finite_space.members,es));
  END_IF;
  CASE es OF
  es_numbers : RETURN (
    ('FINITE_INTEGER_INTERVAL' IN types) OR
    ('INTEGER_INTERVAL_FROM_MIN' IN types) OR
    ('INTEGER_INTERVAL_TO_MAX' IN types) OR
    ('FINITE_REAL_INTERVAL' IN types) OR
    ('REAL_INTERVAL_FROM_MIN' IN types) OR
    ('REAL_INTERVAL_TO_MAX' IN types) OR
    ('CARTESIAN_COMPLEX_NUMBER_REGION' IN types) OR
    ('POLAR_COMPLEX_NUMBER_REGION' IN types) );
  es_complex_numbers : RETURN (
    ('CARTESIAN_COMPLEX_NUMBER_REGION' IN types) OR
    ('POLAR_COMPLEX_NUMBER_REGION' IN types) );
  es_reals : RETURN (
    ('FINITE_REAL_INTERVAL' IN types) OR
    ('REAL_INTERVAL_FROM_MIN' IN types) OR
    ('REAL_INTERVAL_TO_MAX' IN types) );
  es_integers : RETURN (
    ('FINITE_INTEGER_INTERVAL' IN types) OR
    ('INTEGER_INTERVAL_FROM_MIN' IN types) OR
    ('INTEGER_INTERVAL_TO_MAX' IN types) );
  es_logicals : RETURN (FALSE);
  es_booleans : RETURN (FALSE);
  es_strings : RETURN (FALSE);
  es_binarys : RETURN (FALSE);
  es_maths_spaces : RETURN (FALSE);
  es_maths_functions : RETURN ('FUNCTION_SPACE' IN types);
  es_generics : RETURN (TRUE);
  END_CASE;
  RETURN (UNKNOWN);
                              
END_FUNCTION;

FUNCTION substitute
 (expr : generic_expression; vars : LIST[1:?] OF generic_variable; vals : LIST[1:?] OF maths_value) : generic_expression;
  LOCAL
    types : SET OF STRING := stripped_typeof(expr);
    opnds : LIST OF generic_expression;
    op1, op2 : generic_expression;
    qvars : LIST OF generic_variable;
    srcdom : maths_space_or_function;
    prpfun : LIST [1:?] OF maths_function;
    finfun : maths_function_select;
  END_LOCAL;
  IF SIZEOF (vars) <> SIZEOF (vals) THEN  RETURN (?);  END_IF;
  IF 'GENERIC_LITERAL' IN types THEN  RETURN (expr);  END_IF;
  IF 'GENERIC_VARIABLE' IN types THEN
    REPEAT i := 1 TO SIZEOF (vars);
      IF expr :=: vars[i] THEN  RETURN (vals[i]);  END_IF;
    END_REPEAT;
    RETURN (expr);
  END_IF;
  IF 'QUANTIFIER_EXPRESSION' IN types THEN
    qvars := expr\quantifier_expression.variables;
    -- Variables subject to a quantifier do not participate in this kind of
    -- substitution process.
    REPEAT i := SIZEOF (vars) TO 1 BY -1;
      IF vars[i] IN qvars THEN
        REMOVE (vars, i);
        REMOVE (vals, i);
      END_IF;
    END_REPEAT;
    opnds := expr\multiple_arity_generic_expression.operands;
    REPEAT i := 1 TO SIZEOF (opnds);
      IF NOT (opnds[i] IN qvars) THEN
        expr\multiple_arity_generic_expression.operands[i] :=
          substitute(opnds[i],vars,vals);
        -- This technique will not work on subtypes of quantifier_expression
        -- which derive their operands from other attributes!
      END_IF;
    END_REPEAT;
    RETURN (expr);  -- operands modified!
  END_IF;
  IF 'UNARY_GENERIC_EXPRESSION' IN types THEN
    op1 := expr\unary_generic_expression.operand;
    expr\unary_generic_expression.operand := substitute(op1, vars, vals);
    -- This technique will not work on subtypes of unary_generic_expression
    -- which derive their operands from other attributes!
  END_IF;
  IF 'BINARY_GENERIC_EXPRESSION' IN types THEN
    op1 := expr\binary_generic_expression.operands[1];
    expr\binary_generic_expression.operands[1] := substitute(op1, vars, vals);
    op2 := expr\binary_generic_expression.operands[2];
    expr\binary_generic_expression.operands[2] := substitute(op2, vars, vals);
    -- This technique will not work on subtypes of binary_generic_expression
    -- which derive their operands from other attributes!
  END_IF;
  IF 'PARALLEL_COMPOSED_FUNCTION' IN types THEN
    -- Subtype of multiple_arity_generic_expression which derives its operands.
    srcdom := expr\parallel_composed_function.source_of_domain;
    prpfun := expr\parallel_composed_function.prep_functions;
    finfun := expr\parallel_composed_function.final_function;
    srcdom := substitute(srcdom,vars,vals);
    REPEAT i := 1 TO SIZEOF (prpfun);
      prpfun[i] := substitute(prpfun[i],vars,vals);
    END_REPEAT;
    IF 'MATHS_FUNCTION' IN stripped_typeof(finfun) THEN
      finfun := substitute(finfun,vars,vals);
    END_IF;
    RETURN (make_parallel_composed_function(srcdom,prpfun,finfun));
  END_IF;
  IF 'MULTIPLE_ARITY_GENERIC_EXPRESSION' IN types THEN
    opnds := expr\multiple_arity_generic_expression.operands;
    REPEAT i := 1 TO SIZEOF (opnds);
      expr\multiple_arity_generic_expression.operands[i] :=
        substitute(opnds[i],vars,vals);
        -- This technique will not work on subtypes of multiple_arity_generic_
        -- expression which derive their operands from other attributes!
    END_REPEAT;
  END_IF;
  RETURN (expr);
                              
END_FUNCTION;

FUNCTION values_space_of
 (expr : generic_expression) : maths_space;
  LOCAL
    e_prefix : STRING := 'ISO13584_EXPRESSIONS_SCHEMA.';
    typenames : SET OF STRING := TYPEOF (expr);
  END_LOCAL;
  IF (schema_prefix + 'MATHS_VARIABLE') IN typenames THEN
    RETURN (expr\maths_variable.values_space);
  END_IF;
  IF (e_prefix + 'EXPRESSION') IN typenames THEN
    IF (e_prefix + 'NUMERIC_EXPRESSION') IN typenames THEN
      IF expr\numeric_expression.is_int THEN
        IF (e_prefix + 'INT_LITERAL') IN typenames THEN
          RETURN (make_finite_space ([expr\int_literal.the_value]));
        ELSE
          RETURN (the_integers);
        END_IF;
      ELSE
        IF (e_prefix + 'REAL_LITERAL') IN typenames THEN
          RETURN (make_finite_space ([expr\real_literal.the_value]));
        ELSE
          RETURN (the_reals);
        END_IF;
      END_IF;
    END_IF;
    IF (e_prefix + 'BOOLEAN_EXPRESSION') IN typenames THEN
      IF (e_prefix + 'BOOLEAN_LITERAL') IN typenames THEN
        RETURN (make_finite_space ([expr\boolean_literal.the_value]));
      ELSE
        RETURN (the_booleans);
      END_IF;
    END_IF;
    IF (e_prefix + 'STRING_EXPRESSION') IN typenames THEN
      IF (e_prefix + 'STRING_LITERAL') IN typenames THEN
        RETURN (make_finite_space ([expr\string_literal.the_value]));
      ELSE
        RETURN (the_strings);
      END_IF;
    END_IF;
    RETURN (?);  -- unknown subtype of expression
  END_IF;
  IF (schema_prefix + 'MATHS_FUNCTION') IN typenames THEN
    IF expression_is_constant (expr) THEN
      RETURN (make_finite_space ([expr]));
    ELSE
      RETURN (make_function_space (sc_equal, expr\maths_function.domain,
        sc_equal, expr\maths_function.range));
    END_IF;
  END_IF;
  IF (schema_prefix + 'FUNCTION_APPLICATION') IN typenames THEN
    RETURN (expr\function_application.func.range);
  END_IF;
  IF (schema_prefix + 'MATHS_SPACE') IN typenames THEN
    IF expression_is_constant (expr) THEN
      RETURN (make_finite_space ([expr]));
    ELSE
      -- This case cannot occur in this version of the schema.
      -- When it becomes possible, the subtypes should be analysed and
      -- more finely defined spaces returned.
      RETURN (make_elementary_space (es_maths_spaces));
    END_IF;
  END_IF;
  IF (schema_prefix + 'DEPENDENT_VARIABLE_DEFINITION') IN typenames THEN
    RETURN (values_space_of (expr\unary_generic_expression.operand));
  END_IF;
  IF (schema_prefix + 'COMPLEX_NUMBER_LITERAL') IN typenames THEN
    RETURN (make_finite_space ([expr]));
  END_IF;
  IF (schema_prefix + 'LOGICAL_LITERAL') IN typenames THEN
    RETURN (make_finite_space ([expr\logical_literal.lit_value]));
  END_IF;
  IF (schema_prefix + 'BINARY_LITERAL') IN typenames THEN
    RETURN (make_finite_space ([expr\binary_literal.lit_value]));
  END_IF;
  IF (schema_prefix + 'MATHS_ENUM_LITERAL') IN typenames THEN
    RETURN (make_finite_space ([expr\maths_enum_literal.lit_value]));
  END_IF;
  IF (schema_prefix + 'REAL_TUPLE_LITERAL') IN typenames THEN
    RETURN (make_finite_space ([expr\real_tuple_literal.lit_value]));
  END_IF;
  IF (schema_prefix + 'INTEGER_TUPLE_LITERAL') IN typenames THEN
    RETURN (make_finite_space ([expr\integer_tuple_literal.lit_value]));
  END_IF;
  IF (schema_prefix + 'ATOM_BASED_LITERAL') IN typenames THEN
    RETURN (make_finite_space ([expr\atom_based_literal.lit_value]));
  END_IF;
  IF (schema_prefix + 'MATHS_TUPLE_LITERAL') IN typenames THEN
    RETURN (make_finite_space ([expr\maths_tuple_literal.lit_value]));
  END_IF;
  IF (schema_prefix + 'PARTIAL_DERIVATIVE_EXPRESSION') IN typenames THEN
    RETURN (drop_numeric_constraints (values_space_of (
      expr\partial_derivative_expression.derivand)));
  END_IF;
  IF (schema_prefix + 'DEFINITE_INTEGRAL_EXPRESSION') IN typenames THEN
    RETURN (drop_numeric_constraints (values_space_of (
      expr\definite_integral_expression.integrand)));
  END_IF;
  RETURN (?);  -- not recognized as a mathematical expression
                              
END_FUNCTION;

PROCEDURE angle_minmax (ab : REAL; a : REAL; a_in : BOOLEAN; VAR amin : REAL; amax : REAL; VAR amin_in : BOOLEAN; amax_in : BOOLEAN) : ;
    a := angle(a - ab);
    IF amin = a THEN  amin_in := amin_in OR a_in;  END_IF;
    IF amin > a THEN  amin := a;  amin_in := a_in;  END_IF;
    IF amax = a THEN  amax_in := amax_in OR a_in;  END_IF;
    IF amax < a THEN  amax := a;  amax_in := a_in;  END_IF;
                              

END_PROCEDURE;

PROCEDURE range_max (r : REAL; incl : BOOLEAN; VAR rmax : REAL; VAR rmax_in : BOOLEAN) : ;
    IF rmax = r THEN  rmax_in := rmax_in OR incl;   END_IF;
    IF rmax < r THEN  rmax := r;  rmax_in := incl;  END_IF;
                              

END_PROCEDURE;

PROCEDURE range_min (r : REAL; incl : BOOLEAN; VAR rmin : REAL; VAR rmin_in : BOOLEAN) : ;
    IF rmin = r THEN  rmin_in := rmin_in OR incl;  END_IF;
    IF (rmin < 0.0) OR (rmin > r) THEN  rmin := r;  rmin_in := incl;  END_IF;
                              

END_PROCEDURE;

PROCEDURE angle_range (VAR amin : REAL; amax : REAL) : ;
    amin := angle(amin);
    IF amin = PI THEN  amin := -PI;  END_IF;
    amax := angle(amax);
    IF amax <= amin THEN  amax := amax + 2.0*PI;  END_IF;
                              

END_PROCEDURE;

PROCEDURE find_aminmax (ab : REAL; a0 : REAL; a1 : REAL; a2 : REAL; a3 : REAL; in0 : BOOLEAN; in1 : BOOLEAN; in2 : BOOLEAN; in3 : BOOLEAN; VAR amin : REAL; amax : REAL; VAR amin_in : BOOLEAN; amax_in : BOOLEAN) : ;
    LOCAL
      a : REAL;
    END_LOCAL;
    amin := angle(a0-ab);                  amin_in := in0;
    amax := amin;                          amax_in := in0;
    a := angle(a1-ab);
    IF a = amin THEN                       amin_in := amin_in OR in1;  END_IF;
    IF a < amin THEN  amin := a;           amin_in := in1;             END_IF;
    IF a = amax THEN                       amax_in := amax_in OR in1;  END_IF;
    IF a > amax THEN  amax := a;           amax_in := in1;             END_IF;
    a := angle(a2-ab);
    IF a = amin THEN                       amin_in := amin_in OR in2;  END_IF;
    IF a < amin THEN  amin := a;           amin_in := in2;             END_IF;
    IF a = amax THEN                       amax_in := amax_in OR in2;  END_IF;
    IF a > amax THEN  amax := a;           amax_in := in2;             END_IF;
    a := angle(a3-ab);
    IF a = amin THEN                       amin_in := amin_in OR in3;  END_IF;
    IF a < amin THEN  amin := a;           amin_in := in3;             END_IF;
    IF a = amax THEN                       amax_in := amax_in OR in3;  END_IF;
    IF a > amax THEN  amax := a;           amax_in := in3;             END_IF;
    amin := amin+ab;
    amax := amax+ab;
    angle_range(amin,amax);
                              

END_PROCEDURE;

PROCEDURE parts (c : complex_number_literal; VAR x : REAL; y : REAL) : ;
    x := c.real_part;  y := c.imag_part;
                              

END_PROCEDURE;

END_SCHEMA;  -- mathematical_functions_schema