mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
14 lines
267 B
Plaintext
14 lines
267 B
Plaintext
Abs: THEORY
|
|
BEGIN
|
|
IMPORTING Int
|
|
% do not edit above this line
|
|
|
|
% Why3 abs_le
|
|
abs_le: LEMMA FORALL (x:int, y:int): (abs(x) <= y) <=> (((-y) <= x) AND
|
|
(x <= y))
|
|
|
|
% Obsolete chunk abs_pos
|
|
% abs_pos: LEMMA FORALL (x:int): (abs1(x) >= 0)
|
|
|
|
END Abs
|
|
|