metitarski.why 514 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12
theory P

  use import real.Real

  goal x_mul_x_pos :
    forall x:real. x * x >= 0.0

  function sqr (x:real) : real = x * x

  goal sqr_pos :
    forall x:real. sqr x >= 0.0

MARCHE Claude's avatar
MARCHE Claude committed
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
end

theory P2

  use import real.Real
  use import real.Square

  goal sqr_pos :
    forall x:real. sqr x >= 0.0

end

theory P3

  use import real.Real
  use import real.Trigonometry

  goal cos_bound :
    forall x:real. -1.0 <= cos x <= 1.0

  goal cos_bound_harder :
    forall x:real. 0.0 <= x <= 0.1 -> 0.1 <= cos x <= 1.0

end