int.why 573 Bytes
Newer Older
1 2 3 4
theory Test
  use import int.Int
  goal G1 : 5 * 10 = 50
  goal G2 : forall x:int. x + x - x + x  = 2 * x
5 6 7 8 9 10 11 12 13 14

  goal CompatOrderAdd  : forall x y z : int. x <= y -> x + z <= y + z
  goal CompatOrderMult : forall x y z : int. x <= y -> 0 <= z -> x * z <= y * z

  goal InvMult : forall x y : int. (-x) * y = - (x * y) = x * (-y)
  goal InvSquare : forall x : int. x * x = (-x) * (-x)
  goal ZeroMult : forall x : int. x * 0 = 0 = 0 * x
  goal SquareNonNeg1 : forall x : int. x <= 0 -> 0 <= x * x
  goal SquareNonNeg : forall x : int. 0 <= x * x
  goal ZeroLessOne : 0 <= 1
15
end