1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
theory Test
use int.Int
goal G1 : 5 * 10 = 50
goal G2 : forall x:int. x + x - x + x = 2 * x
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
end
theory MinMax
use int.MinMax
goal G : min 1 (min 3 2) = 1
end
|
