FUNCTION simplify_function_application

(* SCHEMA step_merged_ap_schema; *)
-- IN AP242
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 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) BY 1;
               IF NOT (tn IN TYPEOF(tpl[i])) THEN
                  RETURN (FALSE);
               END_IF;
            END_REPEAT;
            RETURN (TRUE);
         END_IF;
         RETURN (FALSE);
      END_FUNCTION;
      FUNCTION makec
         (x : REAL;
          y : REAL ) : complex_number_literal;
         RETURN (make_complex_number_literal(x, y));
      END_FUNCTION;
      PROCEDURE parts
         (c : complex_number_literal;
          VAR x : REAL;
          VAR y : REAL );
         x := c.real_part;
         y := c.imag_part;
      END_PROCEDURE;
   CONSTANT
      cnlit : STRING := schema_prefix + 'COMPLEX_NUMBER_LITERAL';
   END_CONSTANT;
   LOCAL
      types : SET OF STRING := stripped_typeof(expr.func);
      ef_val : elementary_function_enumerators;
      is_elementary : BOOLEAN := FALSE;
      v : maths_value;
      v1 : maths_value;
      v2 : maths_value;
      v3 : maths_value;
      vlist : LIST OF maths_value := [];
      gexpr : generic_expression;
      pairs : SET [1:?] OF LIST [2:2] OF maths_value;
      boo : BOOLEAN;
      lgc : LOGICAL;
      cum : LOGICAL;
      j : INTEGER;
      k : INTEGER;
      n : INTEGER;
      p : REAL;
      q : REAL;
      r : REAL;
      s : REAL;
      t : REAL;
      u : REAL;
      str : STRING;
      st2 : STRING;
      bin : BINARY;
      bi2 : BINARY;
      tpl : LIST OF maths_value;
      tp2 : LIST OF maths_value;
      mem : SET OF maths_value := [];
   END_LOCAL;
      REPEAT i := 1 TO SIZEOF(expr.arguments) BY 1;
         v := simplify_maths_value(expr.arguments[i]);
         INSERT( vlist, v, i - 1 );
      END_REPEAT;
      IF SIZEOF(vlist) >= 1 THEN
         v1 := vlist[1];
      END_IF;
      IF SIZEOF(vlist) >= 2 THEN
         v2 := vlist[2];
      END_IF;
      IF SIZEOF(vlist) >= 3 THEN
         v3 := vlist[3];
      END_IF;
      IF 'ELEMENTARY_FUNCTION_ENUMERATORS' IN types THEN
         ef_val := expr.func;
         is_elementary := TRUE;
      END_IF;
      IF 'ELEMENTARY_FUNCTION' IN types THEN
         ef_val := expr.func\elementary_function.func_id;
         is_elementary := TRUE;
      END_IF;
      IF is_elementary THEN
         CASE ef_val OF
            ef_and :
                  BEGIN
                     cum := TRUE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'LOGICAL' IN TYPEOF(vlist[i]) THEN
                           lgc := vlist[i];
                           cum := cum AND lgc;
                           IF lgc = FALSE THEN
                              RETURN (ctmv(FALSE));
                           END_IF;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(cum));
                     END_IF;
                     IF cum <> TRUE THEN
                        INSERT( vlist, ctmv(cum), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_or :
                  BEGIN
                     cum := FALSE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'LOGICAL' IN TYPEOF(vlist[i]) THEN
                           lgc := vlist[i];
                           cum := cum OR lgc;
                           IF lgc = TRUE THEN
                              RETURN (ctmv(TRUE));
                           END_IF;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(cum));
                     END_IF;
                     IF cum <> FALSE THEN
                        INSERT( vlist, ctmv(cum), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_not :
                  IF 'LOGICAL' IN TYPEOF(v1) THEN
                     lgc := v1;
                     RETURN (ctmv(NOT lgc));
                  END_IF;
            ef_xor :
                  BEGIN
                     IF 'LOGICAL' IN TYPEOF(v1) THEN
                        lgc := v1;
                        IF 'LOGICAL' IN TYPEOF(v2) THEN
                           cum := v2;
                           RETURN (ctmv(lgc XOR cum));
                        ELSE
                           IF lgc = FALSE THEN
                              RETURN (ctmv(v2));
                           ELSE
                              IF lgc = UNKNOWN THEN
                                 RETURN (ctmv(UNKNOWN));
                              ELSE
                                 RETURN (make_function_application(ef_not, [ v2 ]));
                              END_IF;
                           END_IF;
                        END_IF;
                     ELSE
                        IF 'LOGICAL' IN TYPEOF(v2) THEN
                           lgc := v2;
                           IF lgc = FALSE THEN
                              RETURN (ctmv(v1));
                           ELSE
                              IF lgc = UNKNOWN THEN
                                 RETURN (ctmv(UNKNOWN));
                              ELSE
                                 RETURN (make_function_application(ef_not, [ v1 ]));
                              END_IF;
                           END_IF;
                        END_IF;
                     END_IF;
                  END;
            ef_negate_i :
                  IF 'INTEGER' IN TYPEOF(v1) THEN
                     j := v1;
                     RETURN (ctmv(-j));
                  END_IF;
            ef_add_i :
                  BEGIN
                     j := 0;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'INTEGER' IN TYPEOF(vlist[i]) THEN
                           k := vlist[i];
                           j := j + k;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(j));
                     END_IF;
                     IF j <> 0 THEN
                        INSERT( vlist, ctmv(j), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_subtract_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     RETURN (ctmv(j - k));
                  END_IF;
            ef_multiply_i :
                  BEGIN
                     j := 1;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'INTEGER' IN TYPEOF(vlist[i]) THEN
                           k := vlist[i];
                           j := j * k;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(j));
                     END_IF;
                     IF j <> 1 THEN
                        INSERT( vlist, ctmv(j), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_divide_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     RETURN (ctmv(j DIV k));
                  END_IF;
            ef_mod_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     RETURN (ctmv(j MOD k));
                  END_IF;
            ef_exponentiate_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     n := 1;
                     REPEAT i := 1 TO ABS(k) BY 1;
                        n := n * j;
                     END_REPEAT;
                     IF k < 0 THEN
                        n := 1 DIV n;
                     END_IF;
                     RETURN (ctmv(n));
                  END_IF;
            ef_eq_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     RETURN (ctmv(j = k));
                  END_IF;
            ef_ne_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     RETURN (ctmv(j <> k));
                  END_IF;
            ef_gt_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     RETURN (ctmv(j > k));
                  END_IF;
            ef_lt_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     RETURN (ctmv(j < k));
                  END_IF;
            ef_ge_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     RETURN (ctmv(j >= k));
                  END_IF;
            ef_le_i :
                  IF ('INTEGER' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     j := v1;
                     k := v2;
                     RETURN (ctmv(j <= k));
                  END_IF;
            ef_abs_i :
                  IF 'INTEGER' IN TYPEOF(v1) THEN
                     j := v1;
                     RETURN (ctmv(ABS(j)));
                  END_IF;
            ef_max_i :
                  BEGIN
                     boo := FALSE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'INTEGER' IN TYPEOF(vlist[i]) THEN
                           IF boo THEN
                              k := vlist[i];
                              IF k > j THEN
                                 j := k;
                              END_IF;
                           ELSE
                              j := vlist[i];
                              boo := TRUE;
                           END_IF;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(j));
                     END_IF;
                     IF boo THEN
                        INSERT( vlist, ctmv(j), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_min_i :
                  BEGIN
                     boo := FALSE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'INTEGER' IN TYPEOF(vlist[i]) THEN
                           IF boo THEN
                              k := vlist[i];
                              IF k < j THEN
                                 j := k;
                              END_IF;
                           ELSE
                              j := vlist[i];
                              boo := TRUE;
                           END_IF;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(j));
                     END_IF;
                     IF boo THEN
                        INSERT( vlist, ctmv(j), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_negate_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(-r));
                  END_IF;
            ef_reciprocal_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(1 / r));
                  END_IF;
            ef_add_r :
                  BEGIN
                     r := 0;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'REAL' IN TYPEOF(vlist[i]) THEN
                           s := vlist[i];
                           r := r + s;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(r));
                     END_IF;
                     IF r <> 0 THEN
                        INSERT( vlist, ctmv(r), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_subtract_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(r - s));
                  END_IF;
            ef_multiply_r :
                  BEGIN
                     r := 1;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'REAL' IN TYPEOF(vlist[i]) THEN
                           s := vlist[i];
                           r := r * s;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(r));
                     END_IF;
                     IF r <> 1 THEN
                        INSERT( vlist, ctmv(r), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_divide_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(r / s));
                  END_IF;
            ef_mod_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     t := r / s;
                     j := t DIV 1;
                     IF (t < 0) AND (j <> t) THEN
                        j := j - 1;
                     END_IF;
                     RETURN (ctmv(r - j * s));
                  END_IF;
            ef_exponentiate_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(r ** s));
                  END_IF;
            ef_exponentiate_ri :
                  IF ('REAL' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     r := v1;
                     k := v2;
                     t := 1;
                     REPEAT i := 1 TO ABS(k) BY 1;
                        t := t * r;
                     END_REPEAT;
                     IF k < 0 THEN
                        t := 1 / t;
                     END_IF;
                     RETURN (ctmv(t));
                  END_IF;
            ef_eq_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(r = s));
                  END_IF;
            ef_ne_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(r <> s));
                  END_IF;
            ef_gt_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(r > s));
                  END_IF;
            ef_lt_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(r < s));
                  END_IF;
            ef_ge_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(r >= s));
                  END_IF;
            ef_le_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(r <= s));
                  END_IF;
            ef_abs_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(ABS(r)));
                  END_IF;
            ef_max_r :
                  BEGIN
                     boo := FALSE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'REAL' IN TYPEOF(vlist[i]) THEN
                           IF boo THEN
                              s := vlist[i];
                              IF s > r THEN
                                 r := s;
                              END_IF;
                           ELSE
                              r := vlist[i];
                              boo := TRUE;
                           END_IF;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(r));
                     END_IF;
                     IF boo THEN
                        INSERT( vlist, ctmv(r), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_min_r :
                  BEGIN
                     boo := FALSE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'REAL' IN TYPEOF(vlist[i]) THEN
                           IF boo THEN
                              s := vlist[i];
                              IF s < r THEN
                                 r := s;
                              END_IF;
                           ELSE
                              r := vlist[i];
                              boo := TRUE;
                           END_IF;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(r));
                     END_IF;
                     IF boo THEN
                        INSERT( vlist, ctmv(r), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_acos_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(ACOS(r)));
                  END_IF;
            ef_asin_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(ASIN(r)));
                  END_IF;
            ef_atan2_r :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (ctmv(atan2(r, s)));
                  END_IF;
            ef_cos_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(COS(r)));
                  END_IF;
            ef_exp_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(EXP(r)));
                  END_IF;
            ef_ln_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(LOG(r)));
                  END_IF;
            ef_log2_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(LOG2(r)));
                  END_IF;
            ef_log10_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(LOG10(r)));
                  END_IF;
            ef_sin_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(SIN(r)));
                  END_IF;
            ef_sqrt_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(sqrt(r)));
                  END_IF;
            ef_tan_r :
                  IF 'REAL' IN TYPEOF(v1) THEN
                     r := v1;
                     RETURN (ctmv(TAN(r)));
                  END_IF;
            ef_form_c :
                  IF ('REAL' IN TYPEOF(v1)) AND ('REAL' IN TYPEOF(v2)) THEN
                     r := v1;
                     s := v2;
                     RETURN (makec(r, s));
                  END_IF;
            ef_rpart_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     RETURN (ctmv(v1\complex_number_literal.real_part));
                  END_IF;
            ef_ipart_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     RETURN (ctmv(v1\complex_number_literal.imag_part));
                  END_IF;
            ef_negate_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     RETURN (makec(-p, -q));
                  END_IF;
            ef_reciprocal_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     t := p * p + q * q;
                     RETURN (makec(p / t, -q / t));
                  END_IF;
            ef_add_c :
                  BEGIN
                     p := 0;
                     q := 0;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF cnlit IN TYPEOF(vlist[i]) THEN
                           parts( vlist[i], r, s );
                           p := p + r;
                           q := q + s;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (makec(p, q));
                     END_IF;
                     IF p * p + q * q <> 0 THEN
                        INSERT( vlist, makec(p, q), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_subtract_c :
                  IF (cnlit IN TYPEOF(v1)) AND (cnlit IN TYPEOF(v2)) THEN
                     parts( v1, p, q );
                     parts( v2, r, s );
                     RETURN (makec(p - r, q - s));
                  END_IF;
            ef_multiply_c :
                  BEGIN
                     p := 1;
                     q := 0;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF cnlit IN TYPEOF(vlist[i]) THEN
                           parts( vlist[i], r, s );
                           p := p * r - q * s;
                           q := p * s + q * r;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (makec(p, q));
                     END_IF;
                     IF (p <> 1) OR (q <> 0) THEN
                        INSERT( vlist, makec(p, q), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_divide_c :
                  IF (cnlit IN TYPEOF(v1)) AND (cnlit IN TYPEOF(v2)) THEN
                     parts( v1, p, q );
                     parts( v2, r, s );
                     t := r * r + s * s;
                     RETURN (makec((p * r + q * s) / t, (q * r - p * s) / t));
                  END_IF;
            ef_exponentiate_c :
                  IF (cnlit IN TYPEOF(v1)) AND (cnlit IN TYPEOF(v2)) THEN
                     parts( v1, p, q );
                     parts( v2, r, s );
                     t := 0.500000 * LOG((p * p + q * q));
                     u := atan2(q, p);
                     p := r * t - s * u;
                     q := r * u + s * t;
                     r := EXP(p);
                     RETURN (makec(r * COS(q), r * SIN(q)));
                  END_IF;
            ef_exponentiate_ci :
                  IF (cnlit IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     parts( v1, p, q );
                     k := v2;
                     r := 1;
                     s := 0;
                     REPEAT i := 1 TO ABS(k) BY 1;
                        r := p * r - q * s;
                        s := p * s + q * r;
                     END_REPEAT;
                     IF k < 0 THEN
                        t := r * r + s * s;
                        r := r / t;
                        s := -s / t;
                     END_IF;
                     RETURN (makec(r, s));
                  END_IF;
            ef_eq_c :
                  IF (cnlit IN TYPEOF(v1)) AND (cnlit IN TYPEOF(v2)) THEN
                     parts( v1, p, q );
                     parts( v2, r, s );
                     RETURN (ctmv((p = r) AND (q = s)));
                  END_IF;
            ef_ne_c :
                  IF (cnlit IN TYPEOF(v1)) AND (cnlit IN TYPEOF(v2)) THEN
                     parts( v1, p, q );
                     parts( v2, r, s );
                     RETURN (ctmv((p <> r) OR (q <> s)));
                  END_IF;
            ef_conjugate_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     RETURN (makec(p, -q));
                  END_IF;
            ef_abs_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     RETURN (ctmv(sqrt(p * p + q * q)));
                  END_IF;
            ef_arg_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     RETURN (ctmv(atan2(q, p)));
                  END_IF;
            ef_cos_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     t := 0.500000 * EXP(-q);
                     u := 0.500000 * EXP(q);
                     RETURN (makec((t + u) * COS(p), (t - u) * SIN(p)));
                  END_IF;
            ef_exp_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     RETURN (makec(EXP(p) * COS(q), EXP(p) * SIN(q)));
                  END_IF;
            ef_ln_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     RETURN (makec(0.500000 * LOG((p * p + q * q)), atan2(q, p)));
                  END_IF;
            ef_sin_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     t := 0.500000 * EXP(-q);
                     u := 0.500000 * EXP(q);
                     RETURN (makec((t + u) * SIN(p), (u - t) * COS(p)));
                  END_IF;
            ef_sqrt_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     t := sqrt(sqrt(p * p + q * q));
                     u := 0.500000 * atan2(q, p);
                     RETURN (makec(t * COS(u), t * SIN(u)));
                  END_IF;
            ef_tan_c :
                  IF cnlit IN TYPEOF(v1) THEN
                     parts( v1, p, q );
                     t := EXP(2 * q) + EXP(-2 * q) + 2 * COS(2 * p);
                     RETURN (makec(2 * SIN(2 * p) / t, (EXP(-2 * q) - EXP(2 * q)) / t));
                  END_IF;
            ef_subscript_s :
                  IF ('STRING' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     str := v1;
                     k := v2;
                     RETURN (ctmv(str[k]));
                  END_IF;
            ef_eq_s :
                  IF ('STRING' IN TYPEOF(v1)) AND ('STRING' IN TYPEOF(v2)) THEN
                     str := v1;
                     st2 := v2;
                     RETURN (ctmv(str = st2));
                  END_IF;
            ef_ne_s :
                  IF ('STRING' IN TYPEOF(v1)) AND ('STRING' IN TYPEOF(v2)) THEN
                     str := v1;
                     st2 := v2;
                     RETURN (ctmv(str <> st2));
                  END_IF;
            ef_gt_s :
                  IF ('STRING' IN TYPEOF(v1)) AND ('STRING' IN TYPEOF(v2)) THEN
                     str := v1;
                     st2 := v2;
                     RETURN (ctmv(str > st2));
                  END_IF;
            ef_lt_s :
                  IF ('STRING' IN TYPEOF(v1)) AND ('STRING' IN TYPEOF(v2)) THEN
                     str := v1;
                     st2 := v2;
                     RETURN (ctmv(str < st2));
                  END_IF;
            ef_ge_s :
                  IF ('STRING' IN TYPEOF(v1)) AND ('STRING' IN TYPEOF(v2)) THEN
                     str := v1;
                     st2 := v2;
                     RETURN (ctmv(str >= st2));
                  END_IF;
            ef_le_s :
                  IF ('STRING' IN TYPEOF(v1)) AND ('STRING' IN TYPEOF(v2)) THEN
                     str := v1;
                     st2 := v2;
                     RETURN (ctmv(str <= st2));
                  END_IF;
            ef_subsequence_s :
                  IF (('STRING' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2))) AND ('INTEGER' IN TYPEOF(v3)) THEN
                     str := v1;
                     j := v2;
                     k := v3;
                     RETURN (ctmv(str[ j : k ]));
                  END_IF;
            ef_concat_s :
                  BEGIN
                     str := '';
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'STRING' IN TYPEOF(vlist[i]) THEN
                           st2 := vlist[i];
                           str := str + st2;
                           REMOVE( vlist, i );
                        ELSE
                           IF str <> '' THEN
                              INSERT( vlist, ctmv(str), i );
                              str := '';
                           END_IF;
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(str));
                     END_IF;
                     IF str <> '' THEN
                        INSERT( vlist, ctmv(str), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_size_s :
                  IF 'STRING' IN TYPEOF(v1) THEN
                     str := v1;
                     RETURN (ctmv(LENGTH(str)));
                  END_IF;
            ef_format :
                  IF ('NUMBER' IN TYPEOF(v1)) AND ('STRING' IN TYPEOF(v2)) THEN
                     RETURN (ctmv(FORMAT(v1, v2)));
                  END_IF;
            ef_value :
                  IF 'STRING' IN TYPEOF(v1) THEN
                     str := v1;
                     RETURN (ctmv(VALUE(str)));
                  END_IF;
            ef_like :
                  IF ('STRING' IN TYPEOF(v1)) AND ('STRING' IN TYPEOF(v2)) THEN
                     RETURN (ctmv(v1 LIKE v2));
                  END_IF;
            ef_subscript_b :
                  IF ('BINARY' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     bin := v1;
                     k := v2;
                     RETURN (ctmv(bin[k]));
                  END_IF;
            ef_eq_b :
                  IF ('BINARY' IN TYPEOF(v1)) AND ('BINARY' IN TYPEOF(v2)) THEN
                     bin := v1;
                     bi2 := v2;
                     RETURN (ctmv(bin = bi2));
                  END_IF;
            ef_ne_b :
                  IF ('BINARY' IN TYPEOF(v1)) AND ('BINARY' IN TYPEOF(v2)) THEN
                     bin := v1;
                     bi2 := v2;
                     RETURN (ctmv(bin <> bi2));
                  END_IF;
            ef_gt_b :
                  IF ('BINARY' IN TYPEOF(v1)) AND ('BINARY' IN TYPEOF(v2)) THEN
                     bin := v1;
                     bi2 := v2;
                     RETURN (ctmv(bin > bi2));
                  END_IF;
            ef_lt_b :
                  IF ('BINARY' IN TYPEOF(v1)) AND ('BINARY' IN TYPEOF(v2)) THEN
                     bin := v1;
                     bi2 := v2;
                     RETURN (ctmv(bin < bi2));
                  END_IF;
            ef_ge_b :
                  IF ('BINARY' IN TYPEOF(v1)) AND ('BINARY' IN TYPEOF(v2)) THEN
                     bin := v1;
                     bi2 := v2;
                     RETURN (ctmv(bin >= bi2));
                  END_IF;
            ef_le_b :
                  IF ('BINARY' IN TYPEOF(v1)) AND ('BINARY' IN TYPEOF(v2)) THEN
                     bin := v1;
                     bi2 := v2;
                     RETURN (ctmv(bin <= bi2));
                  END_IF;
            ef_subsequence_b :
                  IF (('BINARY' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2))) AND ('INTEGER' IN TYPEOF(v3)) THEN
                     bin := v1;
                     j := v2;
                     k := v3;
                     RETURN (ctmv(bin[ j : k ]));
                  END_IF;
            ef_concat_b :
                  BEGIN
                     boo := FALSE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'BINARY' IN TYPEOF(vlist[i]) THEN
                           IF boo THEN
                              bi2 := vlist[i];
                              bin := bin + bi2;
                           ELSE
                              bin := vlist[i];
                              boo := TRUE;
                           END_IF;
                           REMOVE( vlist, i );
                        ELSE
                           IF boo THEN
                              INSERT( vlist, ctmv(bin), i );
                              boo := FALSE;
                           END_IF;
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(bin));
                     END_IF;
                     IF boo THEN
                        INSERT( vlist, ctmv(bin), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_size_b :
                  IF 'BINARY' IN TYPEOF(v1) THEN
                     bin := v1;
                     RETURN (ctmv(BLENGTH(bin)));
                  END_IF;
            ef_subscript_t :
                  IF ('LIST' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     tpl := v1;
                     k := v2;
                     RETURN (ctmv(tpl[k]));
                  END_IF;
            ef_eq_t :
                  IF ('LIST' IN TYPEOF(v1)) AND ('LIST' IN TYPEOF(v2)) THEN
                     lgc := equal_maths_values(v1, v2);
                     IF lgc <> UNKNOWN THEN
                        RETURN (ctmv(lgc));
                     END_IF;
                  END_IF;
            ef_ne_t :
                  IF ('LIST' IN TYPEOF(v1)) AND ('LIST' IN TYPEOF(v2)) THEN
                     lgc := equal_maths_values(v1, v2);
                     IF lgc <> UNKNOWN THEN
                        RETURN (ctmv(NOT lgc));
                     END_IF;
                  END_IF;
            ef_concat_t :
                  BEGIN
                     tpl := [];
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF 'STRING' IN TYPEOF(vlist[i]) THEN
                           tp2 := vlist[i];
                           tpl := tpl + tp2;
                           REMOVE( vlist, i );
                        ELSE
                           IF SIZEOF(tpl) <> 0 THEN
                              INSERT( vlist, ctmv(tpl), i );
                              tpl := [];
                           END_IF;
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(tpl));
                     END_IF;
                     IF SIZEOF(tpl) <> 0 THEN
                        INSERT( vlist, ctmv(tpl), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_size_t :
                  IF 'LIST' IN TYPEOF(v1) THEN
                     tpl := v1;
                     RETURN (ctmv(SIZEOF(tpl)));
                  END_IF;
            ef_entuple :
                  RETURN (ctmv(vlist));
            ef_detuple :
                  IF 'LIST' IN TYPEOF(v1) THEN
                     tpl := v1;
                     RETURN (ctmv(tpl[1]));
                  END_IF;
            ef_insert :
                  IF ('LIST' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v3)) THEN
                     tpl := v1;
                     k := v3;
                     INSERT( tpl, v2, k );
                     RETURN (ctmv(tpl));
                  END_IF;
            ef_remove :
                  IF ('LIST' IN TYPEOF(v1)) AND ('INTEGER' IN TYPEOF(v2)) THEN
                     tpl := v1;
                     k := v2;
                     REMOVE( tpl, k );
                     RETURN (ctmv(tpl));
                  END_IF;
            ef_sum_it :
                  IF good_t(v1, 'INTEGER') THEN
                     tpl := v1;
                     j := 0;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        j := j + tpl[i];
                     END_REPEAT;
                     RETURN (ctmv(j));
                  END_IF;
            ef_product_it :
                  IF good_t(v1, 'INTEGER') THEN
                     tpl := v1;
                     j := 1;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        j := j * tpl[i];
                     END_REPEAT;
                     RETURN (ctmv(j));
                  END_IF;
            ef_add_it :
                  BEGIN
                     boo := FALSE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF good_t(vlist[i], 'INTEGER') THEN
                           IF NOT boo THEN
                              tpl := vlist[i];
                              boo := TRUE;
                           ELSE
                              tp2 := vlist[i];
                              IF SIZEOF(tpl) <> SIZEOF(tp2) THEN
                                 RETURN (?);
                              END_IF;
                              REPEAT l := 1 TO SIZEOF(tpl) BY 1;
                                 tpl[j] := tpl[j] + tp2[j];
                              END_REPEAT;
                           END_IF;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(tpl));
                     END_IF;
                     IF boo THEN
                        INSERT( vlist, ctmv(tpl), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_subtract_it :
                  IF good_t(v1, 'INTEGER') AND good_t(v2, 'INTEGER') THEN
                     tpl := v1;
                     tp2 := v2;
                     IF SIZEOF(tpl) <> SIZEOF(tp2) THEN
                        RETURN (?);
                     END_IF;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        tpl[i] := tpl[i] - tp2[i];
                     END_REPEAT;
                     RETURN (ctmv(tpl));
                  END_IF;
            ef_scalar_mult_it :
                  IF ('INTEGER' IN TYPEOF(v1)) AND good_t(v2, 'INTEGER') THEN
                     j := v1;
                     tpl := v2;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        tpl[i] := j * tpl[i];
                     END_REPEAT;
                     RETURN (ctmv(tpl));
                  END_IF;
            ef_dot_prod_it :
                  IF good_t(v1, 'INTEGER') AND good_t(v2, 'INTEGER') THEN
                     tpl := v1;
                     tp2 := v2;
                     j := 0;
                     IF SIZEOF(tpl) <> SIZEOF(tp2) THEN
                        RETURN (?);
                     END_IF;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        j := j + tpl[i] * tp2[i];
                     END_REPEAT;
                     RETURN (ctmv(j));
                  END_IF;
            ef_sum_rt :
                  IF good_t(v1, 'REAL') THEN
                     tpl := v1;
                     r := 0;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        r := r + tpl[i];
                     END_REPEAT;
                     RETURN (ctmv(r));
                  END_IF;
            ef_product_rt :
                  IF good_t(v1, 'REAL') THEN
                     tpl := v1;
                     r := 1;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        r := r * tpl[i];
                     END_REPEAT;
                     RETURN (ctmv(r));
                  END_IF;
            ef_add_rt :
                  BEGIN
                     boo := FALSE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF good_t(vlist[i], 'REAL') THEN
                           IF NOT boo THEN
                              tpl := vlist[i];
                              boo := TRUE;
                           ELSE
                              tp2 := vlist[i];
                              IF SIZEOF(tpl) <> SIZEOF(tp2) THEN
                                 RETURN (?);
                              END_IF;
                              REPEAT l := 1 TO SIZEOF(tpl) BY 1;
                                 tpl[j] := tpl[j] + tp2[j];
                              END_REPEAT;
                           END_IF;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(tpl));
                     END_IF;
                     IF boo THEN
                        INSERT( vlist, ctmv(tpl), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_subtract_rt :
                  IF good_t(v1, 'REAL') AND good_t(v2, 'REAL') THEN
                     tpl := v1;
                     tp2 := v2;
                     IF SIZEOF(tpl) <> SIZEOF(tp2) THEN
                        RETURN (?);
                     END_IF;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        tpl[i] := tpl[i] - tp2[i];
                     END_REPEAT;
                     RETURN (ctmv(tpl));
                  END_IF;
            ef_scalar_mult_rt :
                  IF ('REAL' IN TYPEOF(v1)) AND good_t(v2, 'REAL') THEN
                     r := v1;
                     tpl := v2;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        tpl[i] := r * tpl[i];
                     END_REPEAT;
                     RETURN (ctmv(tpl));
                  END_IF;
            ef_dot_prod_rt :
                  IF good_t(v1, 'REAL') AND good_t(v2, 'REAL') THEN
                     tpl := v1;
                     tp2 := v2;
                     r := 0;
                     IF SIZEOF(tpl) <> SIZEOF(tp2) THEN
                        RETURN (?);
                     END_IF;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        r := r + tpl[i] * tp2[i];
                     END_REPEAT;
                     RETURN (ctmv(r));
                  END_IF;
            ef_norm_rt :
                  IF good_t(v1, 'REAL') THEN
                     tpl := v1;
                     r := 0;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        r := r + tpl[i] * tpl[i];
                     END_REPEAT;
                     RETURN (ctmv(sqrt(r)));
                  END_IF;
            ef_sum_ct :
                  IF good_t(v1, cnlit) THEN
                     tpl := v1;
                     p := 0;
                     q := 0;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        parts( tpl[i], r, s );
                        p := p + r;
                        q := q + s;
                     END_REPEAT;
                     RETURN (makec(p, q));
                  END_IF;
            ef_product_ct :
                  IF good_t(v1, cnlit) THEN
                     tpl := v1;
                     p := 1;
                     q := 0;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        parts( tpl[i], r, s );
                        p := p * r - q * s;
                        q := p * s + q * r;
                     END_REPEAT;
                     RETURN (makec(p, q));
                  END_IF;
            ef_add_ct :
                  BEGIN
                     boo := FALSE;
                     REPEAT i := SIZEOF(vlist) TO 1 BY -1;
                        IF good_t(vlist[i], cnlit) THEN
                           IF NOT boo THEN
                              tpl := vlist[i];
                              boo := TRUE;
                           ELSE
                              tp2 := vlist[i];
                              IF SIZEOF(tpl) <> SIZEOF(tp2) THEN
                                 RETURN (?);
                              END_IF;
                              REPEAT l := 1 TO SIZEOF(tpl) BY 1;
                                 parts( tpl[j], p, q );
                                 parts( tp2[j], r, s );
                                 tpl[j] := makec(p + r, q + s);
                              END_REPEAT;
                           END_IF;
                           REMOVE( vlist, i );
                        END_IF;
                     END_REPEAT;
                     IF SIZEOF(vlist) = 0 THEN
                        RETURN (ctmv(tpl));
                     END_IF;
                     IF boo THEN
                        INSERT( vlist, ctmv(tpl), 0 );
                     END_IF;
                     IF SIZEOF(vlist) = 1 THEN
                        RETURN (vlist[1]);
                     END_IF;
                  END;
            ef_subtract_ct :
                  IF good_t(v1, cnlit) AND good_t(v2, cnlit) THEN
                     tpl := v1;
                     tp2 := v2;
                     IF SIZEOF(tpl) <> SIZEOF(tp2) THEN
                        RETURN (?);
                     END_IF;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        parts( tpl[i], p, q );
                        parts( tp2[i], r, s );
                        tpl[i] := makec(p - r, q - s);
                     END_REPEAT;
                     RETURN (ctmv(tpl));
                  END_IF;
            ef_scalar_mult_ct :
                  IF (cnlit IN TYPEOF(v1)) AND good_t(v2, cnlit) THEN
                     parts( v1, p, q );
                     tpl := v2;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        parts( tpl[i], r, s );
                        tpl[i] := makec(p * r - q * s, p * s + q * r);
                     END_REPEAT;
                     RETURN (ctmv(tpl));
                  END_IF;
            ef_dot_prod_ct :
                  IF good_t(v1, cnlit) AND good_t(v2, cnlit) THEN
                     tpl := v1;
                     tp2 := v2;
                     t := 0;
                     u := 0;
                     IF SIZEOF(tpl) <> SIZEOF(tp2) THEN
                        RETURN (?);
                     END_IF;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        parts( tpl[i], p, q );
                        parts( tp2[i], r, s );
                        t := t + p * r + q * s;
                        u := u + q * r - p * s;
                     END_REPEAT;
                     RETURN (makec(t, u));
                  END_IF;
            ef_norm_ct :
                  IF good_t(v1, cnlit) THEN
                     tpl := v1;
                     r := 0;
                     REPEAT i := 1 TO SIZEOF(tpl) BY 1;
                        parts( tpl[i], p, q );
                        r := r + p * p + q * q;
                     END_REPEAT;
                     RETURN (ctmv(sqrt(r)));
                  END_IF;
            ef_if :
                  IF 'LOGICAL' IN TYPEOF(v1) THEN
                     lgc := v1;
                     IF lgc THEN
                        RETURN (v2);
                     ELSE
                        RETURN (v3);
                     END_IF;
                  END_IF;
            ef_if_i :
                  IF 'LOGICAL' IN TYPEOF(v1) THEN
                     lgc := v1;
                     IF lgc THEN
                        RETURN (v2);
                     ELSE
                        RETURN (v3);
                     END_IF;
                  END_IF;
            ef_if_r :
                  IF 'LOGICAL' IN TYPEOF(v1) THEN
                     lgc := v1;
                     IF lgc THEN
                        RETURN (v2);
                     ELSE
                        RETURN (v3);
                     END_IF;
                  END_IF;
            ef_if_c :
                  IF 'LOGICAL' IN TYPEOF(v1) THEN
                     lgc := v1;
                     IF lgc THEN
                        RETURN (v2);
                     ELSE
                        RETURN (v3);
                     END_IF;
                  END_IF;
            ef_if_s :
                  IF 'LOGICAL' IN TYPEOF(v1) THEN
                     lgc := v1;
                     IF lgc THEN
                        RETURN (v2);
                     ELSE
                        RETURN (v3);
                     END_IF;
                  END_IF;
            ef_if_b :
                  IF 'LOGICAL' IN TYPEOF(v1) THEN
                     lgc := v1;
                     IF lgc THEN
                        RETURN (v2);
                     ELSE
                        RETURN (v3);
                     END_IF;
                  END_IF;
            ef_if_t :
                  IF 'LOGICAL' IN TYPEOF(v1) THEN
                     lgc := v1;
                     IF lgc THEN
                        RETURN (v2);
                     ELSE
                        RETURN (v3);
                     END_IF;
                  END_IF;
            ef_ensemble :
                  RETURN (make_finite_space(mem + vlist));
            ef_member_of :
                  IF schema_prefix + 'MATHS_SPACE' IN TYPEOF(v2) THEN
                     lgc := member_of(v1, v2);
                     IF lgc <> UNKNOWN THEN
                        RETURN (ctmv(lgc));
                     END_IF;
                  END_IF;
         END_CASE;
         RETURN (make_function_application(expr.func, vlist));
      END_IF;
      IF 'ABSTRACTED_EXPRESSION_FUNCTION' IN types THEN
         gexpr := substitute(expr.func\abstracted_expression_function.expr, expr.func\quantifier_expression.variables, vlist);
         RETURN (simplify_generic_expression(gexpr));
      END_IF;
      IF 'FINITE_FUNCTION' IN types THEN
         pairs := expr.func\finite_function.pairs;
         REPEAT i := 1 TO SIZEOF(pairs) BY 1;
            IF equal_maths_values(vlist[1], pairs[i][1]) THEN
               RETURN (simplify_maths_value(pairs[i][2]));
            END_IF;
         END_REPEAT;
         RETURN (make_function_application(expr.func, vlist));
      END_IF;
      RETURN (expr);
END_FUNCTION;

Referenced By

Defintion simplify_function_application is references by the following definitions:
DefinitionType
 simplify_generic_expression FUNCTION


[Top Level Definitions] [Exit]

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