mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
61 lines
1.9 KiB
Plaintext
61 lines
1.9 KiB
Plaintext
Int: THEORY
|
|
BEGIN
|
|
% do not edit above this line
|
|
|
|
% Obsolete chunk unit_def
|
|
% unit_def: LEMMA FORALL (x:int): (infix_pl(x, zero) = x)
|
|
|
|
% Obsolete chunk assoc
|
|
% assoc: LEMMA FORALL (x:int, y:int, z:int): (infix_pl(infix_pl(x, y),
|
|
% z) = infix_pl(x, infix_pl(y, z)))
|
|
|
|
% Obsolete chunk inv_def
|
|
% inv_def: LEMMA FORALL (x:int): (infix_pl(x, prefix_mn(x)) = zero)
|
|
|
|
% Obsolete chunk comm
|
|
% comm: LEMMA FORALL (x:int, y:int): (infix_pl(x, y) = infix_pl(y, x))
|
|
|
|
% Obsolete chunk assoc1
|
|
% assoc1: LEMMA FORALL (x:int, y:int, z:int): (infix_as(infix_as(x, y),
|
|
% z) = infix_as(x, infix_as(y, z)))
|
|
|
|
% Obsolete chunk mul_distr
|
|
% mul_distr: LEMMA FORALL (x:int, y:int, z:int): (infix_as(x, infix_pl(y,
|
|
% z)) = infix_pl(infix_as(x, y), infix_as(x, z)))
|
|
|
|
% Obsolete chunk comm1
|
|
% comm1: LEMMA FORALL (x:int, y:int): (infix_as(x, y) = infix_as(y, x))
|
|
|
|
% Obsolete chunk unitary
|
|
% unitary: LEMMA FORALL (x:int): (infix_as(one, x) = x)
|
|
|
|
% Obsolete chunk nontrivialring
|
|
% nontrivialring: LEMMA NOT (zero = one)
|
|
|
|
% Obsolete chunk refl
|
|
% refl: LEMMA FORALL (x:int): infix_lseq(x, x)
|
|
|
|
% Obsolete chunk trans
|
|
% trans: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
|
|
% (infix_lseq(y, z) => infix_lseq(x, z))
|
|
|
|
% Obsolete chunk antisymm
|
|
% antisymm: LEMMA FORALL (x:int, y:int): infix_lseq(x, y) => (infix_lseq(y,
|
|
% x) => (x = y))
|
|
|
|
% Obsolete chunk total
|
|
% total: LEMMA FORALL (x:int, y:int): infix_lseq(x, y) OR infix_lseq(y, x)
|
|
|
|
% Obsolete chunk zerolessone
|
|
% zerolessone: LEMMA infix_lseq(zero, one)
|
|
|
|
% Obsolete chunk compatorderadd
|
|
% compatorderadd: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
|
|
% infix_lseq(infix_pl(x, z), infix_pl(y, z))
|
|
|
|
% Obsolete chunk compatordermult
|
|
% compatordermult: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
|
|
% (infix_lseq(zero, z) => infix_lseq(infix_as(x, z), infix_as(y, z)))
|
|
|
|
END Int
|
|
|