.Open The standard MATHS assumptions and definitions
. Definition of the standard package
As with the Ada STANDARD package, all MATHS documents can use the definitions collected in STANDARD without having to explicitly refer to it.  In other words it is as if the term STANDARD is asserted at the start of all MATHS documents.    This invisible term is defined as a package of conventions as follows:
STANDARD::=Net{
.See COERCIONS 

.See MAPS

.See ARROWS 

.See UNARY 

.See INFIX 

.See SERIAL_AND_PARALLEL

.See ASSIGNMENTS

.See RELATIONS 

.See MODULUS 

.See QUOTIENT_SETS 

.See MORPHISMS

.See INDEXED_SETS

.See PARTIALLY_ADDITITIVE

}=::STANDARD.

Non-standard MATHS is indicated by asserting the term "NONSTANDARD" which removes the (invisible) assertion of STANDARD.  Thus the term STANDARD is still defined and so individual parts can be referred to ans asserted if needed.  Because non-standard MATHS invalidates nearly a megabyte of documentation its use is to be deprecated.

. Serial and Parallel Operators
In normal mathemetics
	a<b<c	means (a<b) and (b<c)

but
	a+b+c	means (a+b)+c.

I call operaters like '<' `parallel` operators and those like '+'
`serial`.  The words catch the image in my mind of the kind of electrical
circuit that would combine operators in a similar way.

A serial operator is an operator that is used like "+" so that 1+2+3 is 6. A
parallel operator is used like "=" so that 1=2=3 is false.

In Gries and Schneider's text "A Logical Approach to Discrete Math",
a parallel operator is called conjunctive.  They use a similar notation
to my `serial` notation for most operators.

SERIAL_AND_PARALLEL::=Net{  -- syntax

 Uses SEMANTICS.  
	|- SEMANTICS::=Net{... [Compare Theory of MATHS types]
	  For x:: #lexeme, T::Types, v::T, symbol(x, T, v) ::@=`symbol x in T means v `. ...
	  For x, T, v, unique_symbol(x, T, v) ::= symbol(x,T,v) and for one v:T(symbol(x, T, v)).
	  For x, T,  if unique_symbol(x, T, v) then x.T::T= the[v:T](symbol(x, T, v)).
	  For x,y, T,  x equivalent(T) y::@= (x.T = y.T).
	}.

(maps)|-For T:Types, associative(T) ::={f:T><T->T || for all x,y,z:T(f(f(x,y),z)=f(x, f(y,z)) }.
 
(strings)|-For T:Types, n:2.., a:T^n, front(a) ! last(a) = a, front(a) =(a1, a2, ..., a[n-1]).  

INFIX::syntax=Net{ f:#char,  s:@#char,  S:=  f P(s) | P(s) dot f | "(" L(s, f) ")" }.
Example_infix::={
So,
	INFIX(f=>"<", s=>expression, S=>relation)
which is short for
	expression::=  "+" P(product) | P(product) dot "+" |  "(" L(product, "+") ")",
and
	INFIX(f=>"+", s=>product, S=>expression)
means
	relation::=  "<" P(expression) | P(expression) dot "<" | "(" L(expression, "<" ) ")".
}=::Example_infix.
 
SERIALITY::=Net{
	INFIX(f, s, S), 
	T::Types,  
	g:: associative(T). 
	|- unique_symbol(f, T><T->T, g). 
	E::@#A=S | s dot  f | f P(s).    
 
 We wish to link a unique value of Type T to each string in E.
 First the formal equivalent of
		|- for a,b:T, a g b = (a,b).g = g(a,b),
		|- for a,b,c:T, a g b g c= (a,b,c).g = g(a,b,c)=g(g(a,b),c),
		|- for n:3.., a:T^n, g(a) = a.g = g( g(front(a)), a(n)).
	|- For a,b:s, symbol( a f b, T, g(a.T,b.T)).
	|- For a,b,c:s, symbol( a f b f c, T, g(g(a.T,b.T), c.T).
	|- For a,b,c:s, symbol( f"(" a ","  b "," c ")" , T, g(g(a.T,b.T), c.T) ).
	()|- For a,b,c:s, a f b f c equivalent(T)  f"(" a ","  b "," c ")".
 
	|- For a:S, b:s, if symbol( a, T, v) then symbol( a f b, T, g(v, a.T) ).
	|- For n:1.., a:s^n, b:s, if symbol(a,T,v) then  symbol( f "(" a ! b")" , T, g(v, b.T) ).
	()|- For s:S, one v:T, symbol(s, T, v). 
 
 Next establish the formal version of 
		for a:T, a.g = g(a) = a.
	|- For a:s, symbol(a"."f, T, a.T) and symbol(f"("a")", T, a.T).
	()|- For e:E, one v:T, symbol(e, T, v).
 
	()|- if units(g) then one units(g).
	|-if units(g) then for n:=(), g(n)=(n).g=the units(g).
	()|- if units(g) then for e:E|"()", one v:T, symbol( e, T, v).
 
}=::SERIALITY.
 
 For E,e,f,g,t, SERIAL(E, e,f,g,t) ::=SERIALITY(T=>t, s=>e, f=>f, g=>g, E=>E).
 
Example -  SERIAL(disjunction, conjunction, "or", or, @)
 
Clearly the formal and precise statements that a given symbol string s, in
a given context T, has a particular value v (symbol( s, T, v) ) are a 
translation of the informal definition... and in the next example the 
formal translation is ommitted:
 
PARALLELISM::=Net{
	INFIX. 
	T::Types,  g:: T><T->@. 
	|- symbol( f, T><T->@, g).
	|- For a,b:T, a g b = (a,b).g = g(a,b).
	|- For a,b,c:T, a g b g c= (a,b,c).g = g(a,b,c)=g(a,b)and g(b,c).
	|- for n:4.., a:T^n, g(a) = a.g = g ( g(front(a)) and g(a(n-1),a(n) )  ).
}=::PARALLELISM.
 
 For E,e,f,t, PARALLEL(E,e,f,g,t) ::=PARALLELISM(T=>t, s=>e, f=>f,g=>g, S=>E).
 
Example - PARALLEL( equivalences, implication, "iff",  iff, @).
 
 |- For T:Types, R:@(T, T), r:#A, if symbol (r, @(T, T), R ) then PARALLEL(relational_proposition, expression(T),r, R, @).

}=::SERIAL_AND_PARALLEL.

. Coercions
COERCIONS::=Net{
	For T:Types, x:T.
	(x) ::%T=(1+>x), 
	set(x) ::@T={x}, 
	bag(x) ::T->Nat0=(x+>1), 
	x::@T=set(x), 
	x::#T=(x), 
	x::%T= (x), 
	x::T->Nat0=bag(x).

	For x:#T, x::@T=img(x).
	For x:%T, x::@T=img(x).

For T, X:@T, 
	the::@X<>->X=rel[A,a](A={a} ), 
	the::#X<>->X=rel[A,a](A=(a) ), 
	the::%X<>->X=rel [A,a] (A=(a) ), 
	the::(X->Nat0)<>->X=rel[A,a](for some n:Nat(A=(a+>n))). 

}=::COERCIONS.

. Functions and Mappings 
MAPS::=Net{
 For X:Set, (_) ::X^X=map[x](x).
 |- For X, Y:Set, f:Y^X, x:X ( f(x)=x.f ),

 For X, Y, Z:Set, f:Z^Y, f::Y^X->Z^X = map [g:Y^X] ( map [x:X](f(g(x)) )  ).
   (def)|-(MAP0): f(g) = fun[x] f(g((x))) = f(g(_))).

 For Set X,Y, x:X, y:Y, x+>y::X->Y={(x,y)}.

 For Set X,Y, A:@X, y:Y, A+>y::X->Y={(a,y) || a:A}.

}=::MAPS.

ARROWS::=Net{
Arrows::={ ->, >->, -->, >--, ---, ==>, >==, >=>, ...}.
The arrows are used to describe sets of maps/functions.
	For Types T1,T2, A:@T1, B:@T2, a:Arrows, (A a B) :: @(T1><T2).
	For Types T1,T2, A:@T1, B:@T2, a:Arrows, m:morphisms, ((m)A a B) :: @(A a B).
.See MORPHISMS
}=::ARROWS.

. Unary operations
We can define the idea of an UNARY operator `u`, as a symbol which can be put in front or after its argument `a`:
	UNARY::syntax=Net{ u:#char, a:@#char, e:= a | u a | a dot u }.
Example::={
Given this definition then the following MATHS statement,
	|-UNARY( u=>"sqrt", a=>term, e=>expression)
generates the following documentation:
	expression::= term | "sqrt" term | term dot "sqrt".
}=::Example.

UNARY::semantics=Net{
	$MAP.
   For X:Set, unary(X) ::=X^X.
   For X:Set, f:unary(X),   f:: @X->@X =  map [A:@X]  {f(a) || a:A},
    For X:Set, f:unary(X),  f:: #X->#X =  map [a:#X]  (map [i:1..|a|](f(a[i])).
(M0)|-(U0):   For X:Set, f:unary(X),   f::X^A->X^A= map [g:X^A] ( map [a:A](f(g(a))).
	For X:Set, f:unary(X), fixed_points(f) ::@X= {x:X. f(x)=x}.
}=::UNARY.

.Open Infix operations
INFIX::semantics=Net{
For X:Sets,
       infix(X) ::= X^( X><X ),
        associative(X) ::={*:infix(X)||for all x,y,z:X(x * (y * z)=(x * y) * z)},
        commutative(X) ::={*:infix(X)||for all x,y:X  (x * y   =  y * x)},
        idempotent(X) ::={*:infix(X)||for all   x:X  (x * x = x)},
  For *:infix(X),
        units(X,*)       ::={u:X||x * u  =  u * x  =  x},
        zeroes(X,*)      ::={z:X||for all x:X( z * x = x * z  =  z},
        idempotents(X,*) ::={i:X||i * i = i}.

Mathematicians have made an extensive survey of systems made up
of a set of elements with an associative operator:
.See http://www/dick/maths/math_31_One_Associative_Op.html

. Mappings and infix operations
  For *:infix(X), x:X, (x *_) ::= map [y:X](x * y),
	For *:infix(X), y:X, (_* y) ::= map [x:X](y * x),
	For *:infix(X), (*) ::=map [x,y](x*y).
(def)|-(I0):  For *:infix(X), x, y:X, (x*y) = (*)(x,y) = (x,y).(*) = (x*_)(y)=y.(x*_)=(_*y)(x)=x.(_*y).
(M0)|-(I1):  For *:infix(X), x, y:X,
	(_*x);(_*y)=(_*(x*y))
	and	(x*_);(y*_)=((y*x)*_)
	and 	(x*_)=x*(_)
	and 	(_*y)=(_)*y.

Note.  (_)*(_) and (*) have different domains, (_)*(_) is a unary operator  but (*) is a binary one.
. Overloadings -- Sets and maps in infix expressions
  For *:infix(X), *::(@X)><(@X)=  map [A,B] {a * b|| a:A, b:B},
	For *:infix(X), *::( X)><(@X)=  map [x,B] {x * b|| b:B},
	For *:infix(X), *::(@X)><( X)=  map [A,x] {a * x|| a:A}.
	{1,2,3} + 1 = 1+ {1,2,3} = {2,3,4}.
	{1,2} + {3,4} = {4,5,6}.
	
          For *:infix(X), *::(X^A)><(X^A)= map [f,g] (map [a:A]  ( f(a) * g(a) ) ),
          For *:infix(X), *::( X) ><( X^A)=map [x,f] (map [a:A]  (  x   * f(a) ) ),
          For *:infix(X), *::(X^A)><( X)=  map [f,x] (map [a:A]  ( f(a) *   x  ) ).

Notice: since (+):infix(Number), the maps from a set into a class of 
Numbers are thersfore bags or multisets.
Maps from 1..`n` into Real numbers gives the beginning of vectors.
These definitions also give us  Bits and bitwise operators.

. Serial operations   
  For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X), +A in X,
         |-(Ser0): if |A|=0 then +A=0,
         |-(Ser1): if |A|=1 then +A=the (A),
         |-(Ser2): if |A|>1 then for all Y:@A(+(A&Y) + +(A~Y))}.
(def, induction)|-(Ser3):  for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets,  p:A(1)-(1)A, +p(A)=+A ).
(def, induction)|-(Ser4):  for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets,  for B, (if B<==A then +A = +(A&B) ).
(def, induction)|-(Ser5):  for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets,  for P:@@A( if P==<A then +A = +[p:P](+p)).


  For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X), f:X^A, +f in X,
          |- if |A|=0 then +f=0,
          |- if |A|=1 then for some y:A(+f=f(y)),
          |- if |A|>1 then for all Y:@A( +f=+(f o Y) + +(f o (A~Y)).

  For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X), x:variable(type(A), e(x):expression(type(A), +[x:A]e(x) ::= +map[x:A]e(x).

By the definitions in the calculus of relations and maps, notice that if f:X^A and B==>A then  (f o B) is the function f restricted to domain B.
(def, induction)|-(Ser6):  for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, f:X^A, p:A(1)-(1)A, +(f o p)=+f ).
(def, induction)|-(Ser7):  for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, f:X^A,  for B, (if B<==A then +f = +(f o (A&B) ).
(def, induction)|-(Ser8):  for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, f:X^A,  for P:@@A( if P==<A then +f = +[p:P](+(f o p)).

Note that if (+) has an inverse operation (-) then +(f o (A|B)) = +(f o B) + +(f o B) - +(f o (A&B)).  see Group theory
.See http://www/dick/maths/math_34_Groups.html#Properties


)=::INFIX.

. Assignment operators 
ASSIGNMENTS::=Net{

.See http://www/dick/maths/math_14_Dynamics.html

 For U:documentation, x:variable(U), e:expression(type(x)), (*):infix(type(x)), x:=e::= (x'=(e))
 For U:documentation, x:variable(U), e:expression(type(x)), (*):infix(type(x)), x:*e::= (x'=x*(e)),
 For U:documentation, x:variable(U), e:expression(type(x)), (*):infix(type(x)), e*:x::= ((e)*x=x').
}=::ASSIGNMENTS.


.Close Infix operations

. Indexed Sets and Families
INDEXED_SETS::=Net{
 For Type T, Sets S, Indexed(S) ::={I->S || I:@T}.
 For A:Indexed(Set), index(A) ::=dom(A).
}=::INDEXED_SETS.

Some call x:A->X a family, and write (x[i] || i:A) ::= fun[i:A](x[i]).

. Additivity
PARTIALLY_ADDITITIVE::=Net{
It is sometimes possible to generalize the standard MATHS convention for serial operations from finite sets to functions over `countable` infinite sets. See Chapter 3 of Manes and Arbib [86]. For example
		 (summable)Natural->Rational is the set of summable series and
		(_^-2)=map[i](1/i^2) in (summable)Natural->Rational

  summable::=|[a:Arrows, A:Countable, X:Sets]((summable)A a X). 

 For X:Sets, A:Countable,  a:Arrows, ((summable)A a X) ::@(A a X).
 For X:Sets, A:Countable,  a:Arrows,  +::((summable)A a X)->X.


	|- (PA0):  For a:Things, all X, f:{}->X(f in summable and +f=0).
	|- (PA1):  For a:Things, all X, f:{a}->X(f in summable and +f=f(a)).
	|- (PA3):  For A, \beta in partition(A) & countable, f:A->X, f in summable iff for all B:\beta(f o B in summable) and fun[B:\beta]( +(f o B) ) in summable and +f = +[B:\beta]( +(f o B) ).

|- (PA4):  For A,X, f:A->X, if for all F:finite(A) (f o F in summable) then f in summable.
(above)|-(PA5): For all A,f:(summable)A->X, B:@A, B;f = f o B = in summable.
(above)|-(PA6): For all f:{}->X ( f:summable and +f=0 ).
}=::PARTIALLY_ADDITITIVE.

Example. 
|- PARTIALLY_ADDITITIVE(X=>Sets, +=>(|), summable=>|[A]A->X).

.Open Binary Relations
RELATIONS::=Net{ 
. Parallelism
In normal mathematics, unlike must programming language, we have
	x = y = z iff x=y and y=z.
So, this convention is adopted in MATHS.  It is also generalized so that
	=(x,y,z) iff x=y and y=z.
This turns out to be useful short hand in many special formal systems.
A precisely similar convention is adopted by David Gries and Fred
Schneider in thier "A Logical Approach to Discrete Mathematics".  Operators
with the aboveproperty are said (by them) to be "conjunctional".  I
call them "parallel operators.

For X:Sets, R:@(X,X), w,x,y,z:X, L:#X,
	x R z::=R(x,y) ::=(x,y).R,
	x R y R z ::= R(x,y,z) ::= (x R y) and (y R z),
	w R x R y R z ::=R(w,x,y,z) ::=(w R x) and (x R y) and (y R z),
	if |L| > 1 then R(L) ::= (L.1st R L.2nd) and R(L.rest).

This can be extended so that
	(x < y <= z = w) iff (x<y and y<=z and z=w).

For X:Sets, R,S,T:@(X,X), w,x,y,z:X,
	x R y S z ::= (x R y) and (y S z),
	w R x S y T z ::=(w R x) and (x S y) and (y T z),

. Kinds of relations
For X:Sets, Y:=@(X,X), I:=Id(X), 0:Y:={},
	Transitive(X)   ::={R:Y || R;R ==> R },
	Reflexive(X)    ::={R:Y || R = /R },
	Irreflexive(X)  ::={R:Y || 0 = I & /R },
	Antireflexive(X) ::={R:Y || 0 = R & /R },
        Dichotomettic(X) ::={R:Y || Y  >== {R, /R }},
        Trichotmettic(X) ::={R:Y || Y  >== {R, /R, I}},
	Symmetric(X)    ::={R:Y || R = /R },
	Antisymmetric(X) ::={R:Y || R & /R = I},
	Asymmetric(X)   ::={R:Y || R ==> Y ~/R },
	Total(X)	::={R:Y || Y ~R = /R },
	Complete(X)	::={R:Y || Y = R | /R },
	Euclidean(X)	::={R:Y || /R;R ==> R },
	Dense(X)	::={R:Y || R ==> R;R },
	Confluent(X)	::={R:Y || /R;R ==> R;/R },
	Rooted(X)	::={R:Y || Y = do(/R);do(R) },
	Transitively_Connected(X)::={R:Y || Y = do(/R|R) },

	Connected(X)	::= $Total(X) &  $Complete(X),
	Serial(X)	::=($Transitive(X) & $Connected(X))~$Reflexive(X).

(above)|-(ITisAT): $Irreflexive(X) & $Transitive(X) = $Asymmetric(X) & $Transitive(X).
. Ordering
Orders are defined by special kinds of relations:
	Strict_partial_orders(X) ::=$Irreflexive(X) & $Transitive(X).
	Quasi_orders(X) ::= $Reflexive(X) & $Transitive(X) .
	Partial_orders(X) ::=$Quasi_orders(X) & $Antisymmetric(X).

The symbols <, <=, >, and >= are used to indicate orders and the
following 
.Key interval notation
is standard:
	x..y ::= {z. x<=z<=y).
	x..* ::= {z. x<=z).
	*..y ::= {z. z<=y}.

Note that a completely rigorous treatment of intervals requires us to be
very clear about the types of data we are refering so.

For more see
.See http://www/dick/maths/math_21_Order.html


. Left and Right Limited relations.
Limited relations can not be repeated for ever either forward or backward.
For example if one repeatedly takes smaller positive numbers
then we ultimately hit 1 and stop.

        Right_limited(X) ::={R:Y || for no S:@Nat-->X (  R(S) ) },
        Left_limited(X) ::={R:Y || for no S:@Nat-->X ( /R(S) ) }.

|- (Nat_well_ordered): < in Left_limited(Nat)~Right_Limited(Nat). 
 These left and right limited orders are used to prove the termination and correctness of algorithms.

(above)|-(LR): For all X, R, R in $Left_limited iff /R in $Right_limited.
. Equivalence  Relations

Equivalences(X) ::=$Reflexive(X) & $Symmetric(X) & $Transitive(X).

equivalence_relation::=$Equivalences.

(partitions)|-(EP): For X:Sets, R:equivalence_relation(X), X>==X/R. [See Logic.Sets.partitions.]

 For f:B^A, congruences(f) ::{R:equivalence_relation(A)|| for all x,y:A(if x R y then f(x) R f(y))}.

 For f:C^(A><A), congruences(f) ::={R:equivalence_relation(A)  || for all x,y, x2,y2:A(if x R y and x2 R y2 then f(x,x2)R f(y,y2))}.

. Properties of specifications
.Source Mili et al. 89, Jaoua Mili et al 91
 For X,Y: Sets, R,S: @(X,Y), R is_more_defined_than S::=pre(S)==>pre(R) and for all x:pre(S) (x.R==>x.S).
|-(Semi Inv): for all R, R==>R;/R;R.
 For X,Y, Regular(X,Y) ::@@(X,Y)={R || R;/R;R ==> R}, 
  Rational(X,Y) ::@@(X,Y)={R||for some X, f,g :dom(R)->X(R=f;/g)},
  Uniform(X,Y) ::@@(X,Y)={R || (post(R)>=={u.R||u:pre(R)}) }. 
|-(RRU): For X,Y, Regular(X,Y) = Rational(X,Y) = Uniform(X,Y).
|-(RI): Regular(X,Y) = {R || R;/R;R=R}.
 For X,Y, R, kernel(R) ::@(X,X)= ({}<>(2nd).R==>(1st).R), nucleus(R)::@(X,X)=R;/R.
()|-(KR): kernel(R) in reflexive & transitive.
()|-(NR): nucleus(R) in reflexive & symmetric.
()|-(ER): For all X,Y, if equivalence(R) then R is Regular(X,Y).
()|-(CR): For all X,Y, R,  W:Sets, f:W->X,  if R:Regular(X,Y) then f;R is Regular(W,Y).
()|-(RNK): For all X,Y, R, if R:Regular(X,Y), nucleus(R) = kernel (R) in reflexive & symmetric & transitive.
()|-(Ass R): form(x'=f(x,...)) is regular.
 ...

}=::RELATIONS.

MODULUS::=following,
.Net
Mathematicians are familiar with
	17 = 1 modulo 16
meaning that multiples of 16 can be ignored.  This is easy to generalize and turns out to be a useful idea.  Formally  a function always indicates a degree of ignorance of its arguments:
|- For A,B:Sets, R:@(B,B) , f:A->B,  R mod f::@(A,A)=f;R;/f.

Hence
 For A,B:Sets, R:@(B,B) , f:A->B,	(x R y wrt f) ::@= x (R mod f) y.
.Close.Net
.Close Binary relations
QUOTIENT_SETS::=Net{
.Source Godement.

The quotient set lemmas give conditions guaranteeing that there is only one  `g` that fits in this diagram:
.As_is 	S----f----->X
.As_is 	S>==S/E--g->X
.As_is 	|   ???        
.As_is 	S>==S/f
(Quotient set lemma)|-(QS0):For S,X:Sets, E:equivalence_relation(S), f:S->X ( E==>(= mod f)  iff for one g:S/E->X(f=g o map [e](e/E])),

(Quotient set lemma)|-(QS1):For S,X:Sets, E:equivalence_relation(S), f:S->X (  E=(= mod f)   iff for one g:S/E-->X(f=g o map [e](e/E])).

}=::QUOTIENT_SETS.


. Structure preserving Maps and functions
MORPHISMS::=Net{
If B is a mathematical structure and f:B^A then A/f can have an identical structure defined on it.

When A and B have structures of the same type AND the mapping f in some sense or other `preserves` the structure then the mapping is called a "morphism".

.See ARROWS.
We will symbolize sets of morphisms by (name_of_structure) A arrow B
where
	name_of_structure:{unary, semigroup, monoid, group, semiring,...},
	arrow:Arrows,
 A,B describe the systems - typically a set and some operations.
If several structures are preserved then their names can be listed:
	(N1,N2,N3,...) A arrow B::= &[i:1..](N[i])A arrow B

If S is the name of the structure we have:
.As_is       arrow  Names		Relationship
.As_is       ->   S morphism,		(0.. )-(1)
.As_is       >--   S epimorphism,	(1.. )-(1)
.As_is       -->   S monomorphism,	(0..1)-(1)
.As_is       ---   S isomorphism,	(  1 )-(1)
.As_is       ==>   sub_S, S injection,	(1)-(1) and equallity
.As_is       >==   S_partition,		(1.. )-(1), and membership 

For example, given a system with name `SYS`, with objects of class `T=$ $SYS` with  a `n`-ary operator `f:T^n->T` then there is a natural morphism `m` defined on objects of type T:
 For X,Y:T, f:(T^n) ->T, a:arrow, (f)X a Y ::={ m:X a Y||m o (f.X)=(f.Y) o m}, 
-- (m is implicitly extended from X->Y to X^n->Y^n).

. Example
 double:(+)Nat->Nat.  double:(-)Int->Int.

A special case is when n = 0, then f.X is an element in X and f.Y in Y and f.Y=m(f.X) and we write:
	(X,f.X)a(Y,f.Y) ::=(f)X a Y

There is also a common way for n-ary relations to be preserved:
 For X,Y:T, R:@(#T), (R)X->Y::={m:X->Y || for all x:#X( if x in R then m(x) in R )}.


For example if `R` is a partial order on sets `X` and `Y` then `(R)X->Y` are the monotone mappings from `X` to `Y`.

Notice that it is possible for `f:(R)X->Y` and not `x in R` and `f(x) in R`.

Since `X~R=rel [x,y:X](not(x R y))` then `(~R)X->Y` are those maps that `do not add new relationships`

 For m:((~R)X->Y) & ((R)X->Y), for all x, x in R iff f(x) in R.

A strong way to preserve a map `f:T^n->T2` (for some `T2<>T`) is clearly: for all x:X^n( f(x)=f(m(x))).

There are similar natural structure transforming mappings between sets with different operations and mappings - Here are the simple cases:

 For a:Arrows, X,Y:Sets, x:X,y:Y, (X,x)a(Y,y) ={f:X a Y || f(x)=y}.
 For a:Arrows, X,Y:Sets, +:infix(X),*:infix(Y), (X,+)a(Y,*) ::={f:X a Y || for all x1,x2:X (f(x1+x2)=f(x1)*f(x2))}.
 For a:Arrows, X,Y:Sets, R:@(X,X), S:@(Y,Y), (X,R)a(Y,S) ::={f:X a Y || for all x1,x2:X, if x1 R x2 then f(x1) S f(x2))}.

Hence to declarations like
	log:: (Positive&Numbers,(<),*,1)---(Numbers,(<),+,0).

From here we can either progress to the general theory of all objects and morphisms (
.See http://www/dick/maths/math_25_Categories.html
and
.See  http://www/dick/maths/math_43_Algebras.html
), or to the special cases for each type of logistic system.

}=::MORPHISMS.

.Close The standard MATHS assumptions and definitions