1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Zsec".
19 (* $Id: Zsec.v,v 1.5 2004/04/06 15:46:05 lcf Exp $ *)
21 (*#* printing {#Z} %\ensuremath{\mathrel\#_{\mathbb Z}}% *)
33 We consider the implementation of integers as signed binary sequences (the
34 datatype [Z] as defined in [ZArith], in the standard library).
37 We define the apartness as the negation of the Leibniz equality:
40 inline cic:/CoRN/model/structures/Zsec/ap_Z.con.
42 (*#* Some properties of apartness:
45 inline cic:/CoRN/model/structures/Zsec/ap_Z_irreflexive0.con.
47 inline cic:/CoRN/model/structures/Zsec/ap_Z_symmetric0.con.
49 inline cic:/CoRN/model/structures/Zsec/ap_Z_cotransitive0.con.
51 inline cic:/CoRN/model/structures/Zsec/ap_Z_tight0.con.
53 inline cic:/CoRN/model/structures/Zsec/ONE_neq_O.con.
56 Some properties of the addition. [Zplus] is also defined in the standard
60 inline cic:/CoRN/model/structures/Zsec/Zplus_wd0.con.
62 inline cic:/CoRN/model/structures/Zsec/Zplus_strext0.con.
64 (*#* ***Multiplication
65 The multiplication is extensional:
68 inline cic:/CoRN/model/structures/Zsec/Zmult_strext0.con.
73 inline cic:/CoRN/model/structures/Zsec/Zpos.con.
79 inline cic:/CoRN/model/structures/Zsec/a_very_specific_lemma1.con.
81 inline cic:/CoRN/model/structures/Zsec/a_very_specific_lemma2.con.
83 inline cic:/CoRN/model/structures/Zsec/a_very_specific_lemma3.con.
85 inline cic:/CoRN/model/structures/Zsec/a_very_specific_lemma4.con.
87 inline cic:/CoRN/model/structures/Zsec/a_very_specific_lemma5.con.
89 inline cic:/CoRN/model/structures/Zsec/Zpos_pos.con.
91 inline cic:/CoRN/model/structures/Zsec/Zpos_neg.con.
93 inline cic:/CoRN/model/structures/Zsec/Zpos_Zsgn.con.
95 inline cic:/CoRN/model/structures/Zsec/Zpos_Zsgn2.con.
97 inline cic:/CoRN/model/structures/Zsec/a_very_specific_lemma5'.con.