#include<civlc.h>
$input double y;

void main() {
  $assume y > 10;
  $assume $forall {int i | i > 0} $forall {double x | x > 0} i*x == $O(x);
  $assume $forall {double z | z > 0} z*$O(z) == $O(z*z);
  $assert 6.0 == $O(1);
  $assert 3*y == $O(y);
  $assert 3*y*y == $O(y*y);
}