mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
51 lines
1.3 KiB
Plaintext
51 lines
1.3 KiB
Plaintext
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
|
|
|