FUNCTION subspace_of

(* SCHEMA step_merged_ap_schema; *)
-- IN AP242
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 : LOGICAL;
      cum : LOGICAL;
      es_val : elementary_space_enumerators;
      bnd1 : REAL;
      bnd2 : REAL;
      n : INTEGER;
      sp1 : maths_space;
      sp2 : maths_space;
      prgn1 : polar_complex_number_region;
      prgn2 : polar_complex_number_region;
      aitv : finite_real_interval;
   END_LOCAL;
      IF NOT EXISTS(spc1) OR NOT EXISTS(spc2) THEN
         RETURN (FALSE);
      END_IF;
      IF spc2 = the_generics THEN
         RETURN (TRUE);
      END_IF;
      IF 'ELEMENTARY_SPACE' IN types1 THEN
         IF NOT ('ELEMENTARY_SPACE' IN types2) THEN
            RETURN (FALSE);
         END_IF;
         es_val := spc2\elementary_space.space_id;
         IF spc1\elementary_space.space_id = es_val THEN
            RETURN (TRUE);
         END_IF;
         CASE spc1\elementary_space.space_id OF
            es_numbers :
                  RETURN (FALSE);
            es_complex_numbers :
                  RETURN (es_val = es_numbers);
            es_reals :
                  RETURN (es_val = es_numbers);
            es_integers :
                  RETURN (es_val = es_numbers);
            es_logicals :
                  RETURN (FALSE);
            es_booleans :
                  RETURN (es_val = es_logicals);
            es_strings :
                  RETURN (FALSE);
            es_binarys :
                  RETURN (FALSE);
            es_maths_spaces :
                  RETURN (FALSE);
            es_maths_functions :
                  RETURN (FALSE);
            es_generics :
                  RETURN (FALSE);
         END_CASE;
         RETURN (UNKNOWN);
      END_IF;
      IF 'FINITE_INTEGER_INTERVAL' IN types1 THEN
         cum := TRUE;
         REPEAT i := spc1\finite_integer_interval.min TO spc1\finite_integer_interval.max BY 1;
            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 > 3.14159 THEN
                  aitv := make_finite_real_interval(-3.14159, open, prgn2.direction_constraint.max - 2 * 3.14159, 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) BY 1;
            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) BY 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;
         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) BY 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;
         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 BY 1;
               cum := cum AND subspace_of(factor_space(spc1, i), factor_space(spc2, i));
               IF cum = FALSE THEN
                  RETURN (FALSE);
               END_IF;
            END_REPEAT;
            RETURN (cum);
         END_IF;
         RETURN (FALSE);
      END_IF;
      IF 'FUNCTION_SPACE' IN types1 THEN
         IF 'ELEMENTARY_SPACE' IN types2 THEN
            RETURN (spc2\elementary_space.space_id = es_maths_functions);
         END_IF;
         IF 'FUNCTION_SPACE' IN types2 THEN
            cum := TRUE;
            sp1 := spc1\function_space.domain_argument;
            sp2 := spc2\function_space.domain_argument;
            CASE spc1\function_space.domain_constraint OF
               sc_equal :
                     BEGIN
                        CASE spc2\function_space.domain_constraint OF
                           sc_equal :
                                 cum := cum AND equal_maths_spaces(sp1, sp2);
                           sc_subspace :
                                 cum := cum AND subspace_of(sp1, sp2);
                           sc_member :
                                 cum := cum AND member_of(sp1, sp2);
                        END_CASE;
                     END;
               sc_subspace :
                     BEGIN
                        CASE spc2\function_space.domain_constraint OF
                           sc_equal :
                                 RETURN (FALSE);
                           sc_subspace :
                                 cum := cum AND subspace_of(sp1, sp2);
                           sc_member :
                                 BEGIN
                                    IF NOT member_of(sp1, sp2) THEN
                                       RETURN (FALSE);
                                    END_IF;
                                    cum := UNKNOWN;
                                 END;
                        END_CASE;
                     END;
               sc_member :
                     BEGIN
                        CASE spc2\function_space.domain_constraint OF
                           sc_equal :
                                 cum := (cum AND space_is_singleton(sp1)) AND equal_maths_spaces(singleton_member_of(sp1), sp2);
                           sc_subspace :
                                 BEGIN
                                    IF NOT member_of(sp2, sp1) THEN
                                       RETURN (FALSE);
                                    END_IF;
                                    cum := UNKNOWN;
                                 END;
                           sc_member :
                                 cum := cum AND subspace_of(sp1, sp2);
                        END_CASE;
                     END;
            END_CASE;
            IF cum = FALSE THEN
               RETURN (FALSE);
            END_IF;
            sp1 := spc1\function_space.range_argument;
            sp2 := spc2\function_space.range_argument;
            CASE spc1\function_space.range_constraint OF
               sc_equal :
                     BEGIN
                        CASE spc2\function_space.range_constraint OF
                           sc_equal :
                                 cum := cum AND equal_maths_spaces(sp1, sp2);
                           sc_subspace :
                                 cum := cum AND subspace_of(sp1, sp2);
                           sc_member :
                                 cum := cum AND member_of(sp1, sp2);
                        END_CASE;
                     END;
               sc_subspace :
                     BEGIN
                        CASE spc2\function_space.domain_constraint OF
                           sc_equal :
                                 RETURN (FALSE);
                           sc_subspace :
                                 cum := cum AND subspace_of(sp1, sp2);
                           sc_member :
                                 BEGIN
                                    IF NOT member_of(sp1, sp2) THEN
                                       RETURN (FALSE);
                                    END_IF;
                                    cum := UNKNOWN;
                                 END;
                        END_CASE;
                     END;
               sc_member :
                     BEGIN
                        CASE spc2\function_space.domain_constraint OF
                           sc_equal :
                                 cum := (cum AND space_is_singleton(sp1)) AND equal_maths_spaces(singleton_member_of(sp1), sp2);
                           sc_subspace :
                                 BEGIN
                                    IF NOT member_of(sp2, sp1) THEN
                                       RETURN (FALSE);
                                    END_IF;
                                    cum := UNKNOWN;
                                 END;
                           sc_member :
                                 cum := cum AND subspace_of(sp1, sp2);
                        END_CASE;
                     END;
            END_CASE;
            RETURN (cum);
         END_IF;
         RETURN (FALSE);
      END_IF;
      RETURN (UNKNOWN);
END_FUNCTION;

Referenced By

Defintion subspace_of is references by the following definitions:
DefinitionType
 compatible_spaces FUNCTION
 member_of FUNCTION
 partial_derivative_expression ENTITY


[Top Level Definitions] [Exit]

Generated by STEP Tools® EXPRESS to HTML Converter
2017-01-19T11:17:24-05:00