Revision 6

MML Version: 2.5.1 => 3.0.1 Mizar Version: 5.3.01 March 7, 1998

The main result of the revision is the development of strong arithmetic of real numbers. Until now arithmetic was introduced axiomatically.

It consists in:

new articles devoted to preliminary steps (ARYTM_3, ARYTM_2, ARYTM_1),
the completion of old axiomatics articles ARYTM and AXIOMS; now they are regular Mizar articles.

It costs some changes in other articles. Please, observe that NAT is now a synonym of omega and the mother type of it and REAL is non empty set. So, if in your article the fact that NAT and REAL are non empty is needed, you should insert ARYTM as a clusters environment directive.

The order of processing of the MML is changed.

AT, CB, GB.

Revision 7

MML Version: 3.0.1 => 3.1.513 Mizar Version: 5.3.02 April 1, 1998

The seventh revision consisted in some parts:

A. Removing extended ASCII from modes, attributes and some functors definitions. Detailed list is available here as plain text.
B. "Commutativity" property has been added to some functors:

AFF_1 Line (AFF_1:def 2)
BHSP_1 + (NORMSP_1: def 5)
COMSEQ_1 + and (COMSEQ_1:def 2, def 3), theorems COMSEQ_1:8, 10 canceled.
EQREL_1 (EQREL_1:def 3)
EUCLID + (EUCLID:def 10), theorem EUCLID:29 removed
LATTICE3 and (LATTICE3:def 13, def 14) - moved from YELLOW_3
MIDSP_1 @ (MIDSP_1:def 1), MIDSP_1:12 canceled.
SEQ_1 + and (SEQ_1:def 3, def 4), theorems SEQ_1:19, 21 canceled.
SQUARE_1 min and max (SQUARE_1:def 1, def 2), SQUARE_1:37, 48 canceled.
TSEP_1 union (TSEP_1:def 2)

"Symmetry" property has been added to some predicates:

AFF_1 (AFF_1:def 5)
ANALMETR and (ANALMETR:def 16, def 15)
BHSP_1 are_ortogonal (BHSP_1:def 3)
BHSP_3 is_compared_to (BHSP_3:def 2)
TSEP_2 constitute_a_decomposition (TSEP_2:def 1, def 2)

"Reflexivity" property has been added to some predicates:

BHSP_3 is_compared_to (BHSP_3:def 2)
LMOD_6 c= (LMOD_6:def 7)

"Irreflexivity" property has been added to predicate from TSEP_2: constitute_a_decomposition (TSEP_2:def 1, def 2).

C. Irrelevant assumptions:

theorem :: TSEP_2:8
 A is non empty implies A,A do_not_constitute_a_decomposition;

theorem :: ANALMETR:72
 K is_line implies not K  K;

in definition of a converse map between 1-sorted structures (TOPS_2:def 4)

 dom f = T.

theorem :: NAT_2:10
 for i,j be non empty Nat st i  j holds j -' i = 0;

"non empty" removed.

theorem :: FUNCOP_1:14
 A <>  & f = A --> x implies dom f = A & rng f = {x};

(f is Function, A, x are sets) conjunct f = A --> x is irrelevant. We changed it into

 A <>  implies dom (A --> x) = A & rng (A --> x) = {x};

- WAYBEL11

 cluster trivial reflexive transitive non empty antisymmetric
  with_suprema finite strict RelStr;

"with_infima" has been added.
In a definition from WAYBEL_8 of a arithmetic LATTICE (WAYBEL_8:def 5) type from locus has been narrowed to "non empty reflexive RelStr"
- WAYBEL14

definition let L be complete non empty LATTICE,
            x be Element of L;
 cluster compactbelow x -> directed;
end;

locus changed for "complete sup-Semilattice"
D. removed repeated theorems and schemas:
- PSCOMP_1

scheme Fraenkel_Subset2 {P[Any,Any], A, B, C() -> non empty set,
                         F(Any,Any)->Element of C() }:
{F(x,y) where x is Element of A(), y is Element of B() : P[x, y]}
        is Subset of C();

is a repetition of a SubsetFD2 from COMPLSP1
- PRE_CIRC

scheme Fraenkel_Subset {P[Any], A, B() -> non empty set,
    F(Any)->Element of B() }: {F(x) where x is Element of A() : P[x]}
    is Subset of B();

is a repetition of SubsetFD from COMPLSP1
- ISOCAT_2

scheme ChoiceD{A()-> non empty set,B() -> non empty set, P[Any,Any]}:
 ex h being Function of A(), B() st
  for a being Element of A() holds P[a,h.a]
provided
  for a being Element of A() ex b being Element of B() st P[a,b];

the same as NUBFuncExD from CQC_SIM1.

theorem :: BINARI_2:1
  for z1 being Tuple of 1,BOOLEAN holds
   z1=<*FALSE*> implies Absval(z1) = 0;

theorem :: BINARI_2:2
  for z1 being Tuple of 1,BOOLEAN holds
   z1=<*TRUE*> implies Absval(z1)=1;

removed as equal to BINARITH:41, 42, respectively.

theorem :: ORDERS_1:21
 (A) = the carrier of A;

canceled as equal to PRE_TOPC:12
E. modification of an article: - NET_1 attribute "being_Petri_net" has been replaced with "Petri" (NET_1:def 1)

definition
  let N be Net;
  mode Elem of N -> set means
:: NET_1: def 3
    it = Elements(N);
 end;

has been removed from the MML.
Instead of a theorem (NET_1:10)

 Net (# ø, ø, ø #) is_Petri_net;

the following cluster has been added:

definition
 cluster Net (#ø, ø, ø#) -> Petri;
end;

definition let IT be Net;
  attr IT is Pnet-like means
:: NET_1: def 4
IT is_Petri_net;
 end;

has been removed as equivalent with "Petri" attribute definition.

F.modifications in vocabularies needed in part of the revision (see A.)

Six vocabularies have been removed and their content moved to the anothers:
GRCAT1D -> GRCAT_1
INCPROJP -> INCPROJ
MSSUBFA1 -> MSSUBFAM
MANYSORT -> MSUALG_1
OPEN -> WAYBEL_6
INT_2D -> INT_2

AG, RM.

Revision 8

MML Version: 3.1.513 => 3.2.513 Mizar Version: 5.3.02 April 30, 1998

Some parts of the revision: A.

A number of definitions and theorems from some topological articles (COMPTS_1, TOPS_1, BORSUK_1, WAYBEL18, TOPMETR2, PRE_TOPC, T_0TOPSP, CONNSP_1, CONNSP_3) proved for objects of type "non empty TopSpace" or "TopSpace" remains true even if they are "TopStruct", so in many cases the generalization has been done. Similar operation in the case of TOPS_2 fixed some theorems even for "1-sorted" structure.

Restriction of the "TopStruct" to its subset (PRE-TOPC:def 10) may be considered not only in the case if the subset is nonempty. In the result from the mother type of the functor attribute "non empty" has been deleted. However, for non empty subset we may need to have "non empty TopSpace" as a result of a restriction of non empty TopSpace to its nonempty subset. To assure this, one should add "clusters PRE_TOPC;" to environment declaration.

Changes in two definitions had rather big impact on the whole library: TOPREAL1:def 2 (is_an_arc_of) and TOPREAL_2:def 1 (being_simple_closed_curve). Deleting from there conjuncts P <> ô forced us to add some non empty attributes to types in some theorems in MML (TOPREAL1, TOPREAL2, TOPREAL4, JORDAN4, JORDAN5B, JORDAN5C, JORDAN6).

One fully automated revision took place, namely deleting of unnecessary assumptions from the definitions and theorems. 130 items has been generalized in more than 60 articles. The detailed list is available here.

AK, AG

Revision 9

MML Version: 3.2.513 => 3.3.592 Mizar Version: 5.3.12 June 30, 1999

During the revision the following changes in the MML have been done:

Some topological attributes are now clusterable (e.g. open, closed from PRE_TOPC, dense, nowhere_dense, boundary, condensed, closed_condensed, open_condensed from TOPS_1, compact from COMPTS_1, everywhere_dense from TOPS_3, discrete, maximal_discrete from TEX_2).
The environment "notation" directive SUBSET_1 has to be before STRUCT_0.
The definition of the mode from PRE_TOPC:
```
definition let T be 1-sorted;
  mode Subset-Family of T is Subset-Family of the carrier of T;
end;
```
is no longer used and has been deleted. Its clusterable equivalent (STRUCT_0:def 4) is:
```
definition let T be 1-sorted;
  mode Subset-Family of T -> Subset-Family of the carrier of T means
    not contradiction;
end;
```
The environment "notation" directive SETFAM_1 has to be before STRUCT_0. Two useful schemes have been added (SubFamExS to PRE_TOPC, SubFamExM to PCOMPS_1).

Two redefinitions (of singleton and doubleton) have been moved from ORDERS_1 to STRUCT_0:

definition let S be non empty 1-sorted,
               a be Element of the carrier of S;
 redefine func {a} -> Subset of S;
end;

definition let S be non empty 1-sorted,
               a1, a2 be Element of the carrier of S;
 redefine func {a1,a2} -> Subset of S;
end;

The result types of some functors have been widened as below:
```
  func A --> z :: FUNCOP_1:def 2

  func x .--> y :: CQC_LANG:def 2

  func (x1,x2) --> (y1,y2) :: CAT_3:def 2
```
from "Function" to "set" and
```
  func <*x*> :: FINSEQ_1:def 8

  func <*x,y*> :: FINSEQ_1:def 9

  func <*x,y,z*> :: FINSEQ_1:def 10
```
from "FinSequence" to "set".
If one wants to use this functors with old types one should add clusters FUNCOP_1, CQC_LANG, CAT_3, FINSEQ_1 to the environment declaration, respectively.
The redefinition from FINSEQ_4:
```
definition let D be set;
  redefine func <í>D -> empty FinSequence of D equals
   <í>;
end;
```
has been removed as equal to FINSEQ_1:def 6. In effect in many articles the "notation" and "constructors" environment directive FINSEQ_4 can now be omitted.
The "reflexivity" property has been added to the "meets" definition in BOOLE.
The unnecessary assumption has been removed from REAL_1:33:
```
 1/x=x" & (x <> 0 implies 1/x"=x);
```
Theorem WAYBEL12:1 has been canceled as equal to YELLOW_6:10.

In NATTRA_1, in redefinition

definition let A1, B1 be non empty set,
               f be Function of A1,B1,
               Y1 be non empty Subset of A1;
 redefine func f|Y1 -> Function of Y1,B1;
end;

non empty attribute has been deleted from the loci A1, Y1.

Two definitions (as special cases of SUBSET_1:def 1 and PRE_TOPC:def 2) have been removed:

RLVECT_2:def 3

definition let V be 1-sorted;
 func í.V -> empty finite Subset of V equals
    í;
end;

QC_LANG3:def 1

definition let V be non empty Subset of QC-variables;
 func í(V) -> empty Element of bool V equals
  í;
end;

FINSEQ_2:12 is equal to FUNCT_1:12 so removed.
TEX_2:11 is equal to TSEP_1:5 so removed.
Some theorems from TOPMETR, PCOMPS_1, TSEP_1, TDLAT_3, TOPS_3, COMPTS_1, TEX_2, WAYBEL18 have been generalized.
The definition of the attribute Automorphism-like has been removed (MOD_4:def 22).

One of the two equal definitions (in MIDSP_1 and VECTSP_2) has been removed.

definition
  func op2 -> BinOp of {í} means
:: MIDSP_1:def 2
not contradiction;
end;

Two definitions from VECTSP_2 (functors lop and rop) with the mother type Function of [:the carrier of R, {í}:], {í} has been removed. Their equivalents are pr1 and pr2 (see FUNCT_3).
The repeated redefinition from FUNCOP_1
```
definition let X;
  redefine func id X -> Function of X,X;
end;
```
has been deleted as equivalent to the one from FUNCT_2.
The structure IncProjStr from INCPROJ has been moved to INCSP_1 and IncStruct is now prefixed by IncProjStr. One of the selectors had to be changed (Inc1 to Inc). INCPROJ:def 4 has been removed.
The revision of AMI_1 took place: the selector Halt-Instruction has been deleted from the structure definition of AMI-Struct. Because of this change definitions of the attributes 'halting' and of the functor 'halt' had to be added. The numbers of the definitions and theorems are now quite different.
Definiens of the mode Function of X,Y has been changed: now the definition looks like:
```
definition let X,Y be set;
 mode Function of X,Y is quasi_total Function-like Relation of X,Y;
end;
```
Some theorems concerning mode PartFunc of X,Y can be applied in case when the variable is of the type Function of X,Y. One new definition has been added:
```
definition let X be set;
 mode ParametrizedSubset of X -> Relation means
:: TREES_2:def 9
 rng it c= X;
end;
```
Sometimes
```
clusters RELSET_1;
constructors PARTFUN1;
```
have to be added to the environment declaration. The order of notations is important: RELSET_1, PARTFUN1, FUNCT_2.

AT, AK, AG

Revision 10

MML Version: 3.3.592 => 3.5.610 Mizar Version: 5.3.12 November 9, 1999

A.Two additional requirements declarations have been implemented: SUBSET and BOOLE. If errors occur, one must add to environment declarations some identifiers from the following list:

requirements SUBSET, BOOLE;
notation BOOLE, SUBSET_1;
clusters SUBSET_1;(instead of TARSKI)

The order of notation is important. We propose as follows: TARSKI, BOOLE, SUBSET_1.

B.The structure FieldStr has been removed from the article VECTSP_1. All theorems concerning FieldStr deal with doubleLoopStr now. New auxiliary functor has been defined:

definition let F be non empty LoopStr;
 func comp F -> UnOp of the carrier of F means
:: VECTSP_1:def 25
  for x being Element of the carrier of F holds it.x = -x;
end;

The numbers of the next definitions from the article are now increased (by 1). A number of definitions and theorems has been generalized. Especially big impact may be seen in INT_3 so the care is advised.

AT, CB, AG, AK