%% These examples illustrate the new rational simplification feature that is available in PVS 6.0
%% These formulas don't have an intended semantics

rat_examples : THEORY
BEGIN

  rat1 : FORMULA
    FORALL(u,s:real):
      u >= 0.78 AND
      s > 0 AND
      s < 4 AND
      u < 0.9 IMPLIES
     -(0.78 * 1.05504 * (0.92 - 0.78) * s) -
       0.78 * 1.08016 * (0.9 - 0.78) * s
       - 1.256 * (0.9 - 0.78) * s * u
       - 0.92944 * (0.92 - 0.78) * s * u
       - 1.08016 * (0.9 - 0.78) * (0.92 - 0.78) * s
       - 4 * (0.78 * 1.256 * (0.9 - 0.78))
       - 4 * (1.08016 * (0.9 - 0.78) * u)
       + 4 * (0.78 * 1.08016 * (0.9 - 0.78))
       + 4 * (1.256 * (0.9 - 0.78) * u)
       + 4 * (1.08016 * (0.9 - 0.78) * (0.92 - 0.78))
       + 0.78 * 1.256 * (0.9 - 0.78) * s
       + 0.78 * 0.92944 * (0.92 - 0.78) * s
       + 0.92944 * (0.9 - 0.78) * (0.92 - 0.78) * s
       + 1.05504 * (0.92 - 0.78) * s * u
       + 1.08016 * (0.9 - 0.78) * s * u
       >= 0

%|- rat1 : PROOF
%|- (then (skeep) (assert) (postpone))
%|- QED

  IMPORTING vectors@vectors_2D

  SQRT1 : posreal
  SQRT2 : posreal
  D     : MACRO posreal = 5

  rat2 : FORMULA
    ((# x := D + (1 / 100) * D, y := 0 #) +
        1 / 4 *
         ((# x := -D - (1 / 100) * D, y := (1 / 100) * D #) +
           (10205 * D / 10201 - D * SQRT1 / 50) *
            ((1 / (2 * (SQRT2 / 100 * D))) *
              ((# x := D + (1 / 100) * D, y := 0 #) +
                10201 / 10205 *
                 ((# x := -D - (1 / 100) * D, y := (1 / 100) * D #) -
                   (# x := 0, y := -(1 / 100) * D #))))
           -
           ((# x := 0, y := -(1 / 100) * D #) +
             (10205 * D / 10201 - D * SQRT1 / 50) *
              ((1 / (2 * (SQRT2 / 100 * D))) *
                (-(# x := D + (1 / 100) * D, y := 0 #) +
                  10201 / 10205 *
                   ((# x := 0, y := -(1 / 100) * D #) -
                     (# x := -D - (1 / 100) * D,
                        y := (1 / 100) * D #)))))))
       *
       ((# x := D + (1 / 100) * D, y := 0 #) +
         1 / 4 *
          ((# x := -D - (1 / 100) * D, y := (1 / 100) * D #) +
            (10205 * D / 10201 - D * SQRT1 / 50) *
             ((1 / (2 * (SQRT2 / 100 * D))) *
               ((# x := D + (1 / 100) * D, y := 0 #) +
                 10201 / 10205 *
                  ((# x := -D - (1 / 100) * D, y := (1 / 100) * D #) -
                    (# x := 0, y := -(1 / 100) * D #))))
            -
            ((# x := 0, y := -(1 / 100) * D #) +
              (10205 * D / 10201 - D * SQRT1 / 50) *
               ((1 / (2 * (SQRT2 / 100 * D))) *
                 (-(# x := D + (1 / 100) * D, y := 0 #) +
                   10201 / 10205 *
                    ((# x := 0, y := -(1 / 100) * D #) -
                      (# x := -D - (1 / 100) * D,
                         y := (1 / 100) * D #)))))))
       < D * D

%|- rat2 : PROOF
%|- (then (grind) (field) (postpone))
%|- QED

END rat_examples