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
52
53
54
55
56
57
58
59
60
61
|
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
|
