1
2
3
4
5
6
7
8
9
10
11
12
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
PowerInt: THEORY
BEGIN
IMPORTING int@Int
IMPORTING Real
% do not edit above this line
% Why3 infix_sldt
infix_sldt(x:real, y:real): real = Real.infix_sl(x, y)
% Why3 inv
inv(x:real): real = Real.inv(x)
power_total(x: int) : real
% Why3 power
power(x:real,
x1:int): MACRO real = IF x = 0 AND x1 < 0 THEN power_total(x1) ELSE x^x1 ENDIF
% Why3 power_0
power_0: LEMMA FORALL (x:real): (power(x, 0) = 1)
% Why3 power_s
power_s: LEMMA FORALL (x:real, n:int): (n >= 0) => (power(x,
(n + 1)) = (x * power(x, n)))
% Why3 power_s_alt
power_s_alt: LEMMA FORALL (x:real, n:int): (n > 0) => (power(x,
n) = (x * power(x, (n - 1))))
% Why3 power_1
power_1: LEMMA FORALL (x:real): (power(x, 1) = x)
% Why3 power_sum
power_sum: LEMMA FORALL (x:real, n:int, m:int): (0 <= n) => ((0 <= m) =>
(power(x, (n + m)) = (power(x, n) * power(x, m))))
% Why3 power_mult
power_mult: LEMMA FORALL (x:real, n:int, m:int): (0 <= n) => ((0 <= m) =>
(power(x, (n * m)) = power(power(x, n), m)))
% Why3 power_mult2
power_mult2: LEMMA FORALL (x:real, y:real, n:int): (0 <= n) =>
(power((x * y), n) = (power(x, n) * power(y, n)))
% Why3 pow_ge_one
pow_ge_one: LEMMA FORALL (x:real, n:int): ((0 <= n) AND (1 <= x)) =>
(1 <= power(x, n))
END PowerInt
|
