
\input defs

\input rmize

When this file is parsed only syntactical information is processed.
At present some of the definitions have only stubs on the right.  However
this prevents the file from being definition checked which needs to
be fixed. 

Definitions from logic:

$(\Not \pvar \Iff (\pvar \c \false))$

$(\ex a \Iff (a = a))$

$(\an x \pbar x \ident 1)$

$(\Some x \pbar x \Iff \ex \an x \pbar x)$

$(\Each x \pbar x \Iff \Not \Some x \Not \pbar x)$

$(\The x \pbar x \ident \an y \Each x(\pbar x \Iff x = y))$

$(\One x \pbar x \Iff \ex \The x \pbar x)$ 

$(\Unq x \pbar x \Iff (\Some x \pbar x \c \One x \pbar x))$

$(\Case x \ubar x \ident 1)$

$(\Tup x \ubar x \ident 1)$

$(\tup x \ubar x \ident 1)$


Definitions from set theory:

$(\setof x \pbar x \ident \The y \Each x (x \in y \Iff \pbar x \and \Some z(x \in z)))$ 

$(\sng x \ident \setof y (y = x))$

$(\Cmpl a \ident (\ex a \cond \setof y \Not(y \in a)))$

%precedence= 15 
$((a \dsj b) \ident (a + b))$

$(\bigcup x \ubar x \ident 1)$

$(\bigcap x \ubar x \ident 1)$

$(\sb a \ident (\ex a \cond \setof x (x \i a)))$ 

$(\sp a \ident (- a))$

$(\sigmabar a \ident (-a))$
$(\SI a \ident (-a))$

$(\{a\} \ident (a \in \U \cond \setof t (t = a)))$
$(\{a,b\} \ident (a,b, \in \U \cond \setof t (t = a \Or t = b)))$
$(\{ a,b,c \} \ident (a+b+c))$
$(\{ a,b,c,d \} \ident (a+b+c+d))$
$(\{ a,b,c,d,e \} \ident (a+b+c+d+e))$
$(\{ a,b,c,d,e,f \} \ident (a+b+c+d+e+f))$
$(\{ a,b,c,d,e,f,g \} \ident (a+b+c+d+e+f+g))$
$(\{ a,b,c,d,e,f,g,h \} \ident (a+b+c+d+e+f+g+h))$
$(\{ a,b,c,d,e,f,g,h,i \} \ident (a+b+c+d+e+f+g+h+i))$

$(\mel a \ident \an x (x \in a))$ 

$(\pwr a \ident (- a))$

$(\PI a \ident (- a))$

$(\partition a \ident (-a))$

$(\Close x \ubar x \ident (\Some x (\ubar x \i x)\cond\bigcap x : (\ubar x \i x)))$

$(\closes x \ubar x \Iff (1 = 1))$

$(\fnt \ident \Close x (\e \cup \setof (x \cup \{y\})\ls y \in \U\rs))$ 

$(\cbl \ident 1)$

$(\dsjn \ident 1)$

$(\scsr a \ident (-a))$


$(\omega \ident 1)$

$(\Omega \ident 1)$

$(\ss a \ident (\ex a \cond \setof \{x\}\ls x \in A\rs))$ 

Tuple definitions:

$(\bsdmn T \ident (-T))$

$(\crd a b \ident (a + b))$

$(\crd\p a \ident (- a))$

$(\crd\pp a \ident (- a))$

$(\sqr a \ident (-a ))$

$(\rct a b \ident (a + b))$

$(\disjoint \ident 1)$

%precedence= 17
$((A \lilx B) \ident (A + B))$

$((A\dscomma B)
\ident \bigcup x,y; (x \in A \and y \in B)\{\{\{a\},\{a,b\}\}\})$

$(\tup x; \pbar x \ubar x \ident \bigcup x; \pbar x 
	(\sng x \dscomma
	\{\e\}\cup \ss \ubar x))$ 

$(\tup x \ubar x\ident \tup x ; (1 = 1) \ubar x)$

$(\tuplep T \Iff (T = T))$

$(\bsdmn T \ident (- T))$


$(\Tup x; \pbar x \ubar x \ident 
\setof T (\tuplep T \and \bsdmn T = \setof x \pbar x \and 
	\Each x; \pbar x (\crd x T \in \ubar x)))$

$(\Tup x \ubar x \ident \Tup x ; (1 = 1) \ubar x)$

$(\Pwr An \ident (n \in\omega\cond \Tup x \in n A))$


$(\Crd x {\cal T} \ident \bigcup T \in {\cal T}  \{ \crd x T \})$

$(\Crd\p {\cal T} \ident \Crd \e {\cal T})$

$(\Crd\pp  {\cal T} \ident \Crd \scsr\e {\cal T})$

$(\Fld  T \ident ( - T))$
%	\Case n;({\cal T}\i\Pwrn\U n)
%	\bigcup i\in\. n\e \Crd i {\cal T})$

Relation definitions:

$(\relationp a \Iff (a = a))$

$(\hs a b \ident (a + b))$

$(\vs a b \ident (a + b))$

$(\rng a \ident (-a))$

$(\dmn a \ident (-a))$

$(\strc a b \ident (a + b))$

$(\strn a b \ident (a + b))$

$(\histar a b \ident (a + b))$

$(\lostar a b \ident (a + b))$

$(\id A \ident \bigcup x \in A \{ (x,x) \})$

$(\inv R \ident \bigcup x,y; ((x,y) \in R)\{(y,x)\})$

$(\antisymmetric \ident \setof R \subset \sqr \U 
(R \cap \inv R \subset \id \U))$

$(\transitive \ident \setof R \subset 
\sqr \U (R \cmp R \subset R))$

$(\equivalence \ident \setof R (R \cmp R 
\subset R \subset \inv R))$

$(\eqclass R \ident (R \in \equivalence \cond
	\bigcup x \in \dmn R \{ \vs Rx \}))$

$(\porder \ident (\transitive \cap \antisymmetric ))$

$((A \lilx B) \ident \bigcup x,y;
(x \in A \and y \in B)\{(x,y)\})$


%precedence=  6
$((R \orders S) \Iff (R  \in \porder  
 \and  \Each x,y,\ne ,\in S (x,y\in R\Or y,x\in R)))$

Function definitons:
$(\functionp f \Iff
(f \i \U \lilx \U \and \Each x \Unq y((x,y)\in f)))$

$(\function \ident \setof f \functionp f)$ 

$(\relation \ident 1)$

$(\functionp a \Iff (a = a))$

$(\.fx \ident (\functionp f
\cond \The y ((x,y) \in f)))$

$(\lonzo x \ubar x \ident \setof (x,\ubar x) \ls x \rs)$

$(\. a b \ident (a + b))$

$(\. a : b \into c \Iff (a = b = c))$

$(\. a : b \onto c \Iff (a = b = c))$

$(\. a : b \oneto c \Iff (a = b = c))$

$(\. a : b \Iff c \Iff (a = b = c))$

$(\Dot a b \ident (a + b))$

$(\Dot a : b \into c \Iff (a = b = c))$

$(\Dot a : b \onto c \Iff (a = b = c))$

$(\Dot a : b \oneto c \Iff (a = b = c))$

$(\cyclic a \ident (- a))$

$(\permute a \ident (-a))$

$(\onetoone \ident 1)$

$(\prj\p \ident \lonzo x \crd\p x)$

$(\prj\pp \ident \lonzo x \crd\pp x)$

$(\prj t \ident \lonzo x \crd tx)$

Numerical definitions:

$(\Pwrn An \ident (n \in\nats\cond\Pwr A \. n\e))$

$(\num a \ident (-a))$

 $(\divisor x \ident(x \in \ints \cond \setof y \in \ints
\Some z \in \ints (y \cdot z = x)))$

$(\gcd x y \ident \The z (\divisor z = \divisor x \cap \divisor y))$


Finite Sequence Definitions 

$(\Int a \ident (- a))$

$(\Fsqnc a \ident (- a))$

$(\Nfsqnc a\ident (-a))$

$(\Sqnc a \ident (- a))$

$(\fsqnc \ident 1)$

$(\nfsqnc \ident 1)$

$(\sqnc \ident 1)$

$(\Enum a \ident (- a))$

$(\first a \ident (-a))$

$(\last a \ident (-a))$

$(\concat ab \ident (a + b))$

$(\splice a b \ident (a + b))$

$(\slice fmn \ident(f+m+n))$

%precedence= 13 
$((a \Mod b) \ident (a + b))$

$(\repeaters a \ident (-a))$

$(\Rev a \ident (- a))$

$(\ddmn a \ident \setof x \in \dmn a (a + 1 \in \dmn a))$

$(\indc\p a b \ident (a + b))$

$(\indc\pp a b \ident (a + b))$

$(\sum x \ubar x \ident 1)$

$(\bigg x \pbar x \Iff (1 = 1))$

$(\even \ident 1)$

$(\odd \ident 1)$

$(\Symdif x \ubar x \ident 1)$

$(\Trnum a \ident (- a))$

$(\Trroot a \ident (-a ))$

Order definitions
$(\Max a \ident (- a))$

$(\Min a \ident (- a))$

$(\period a \ident \Min \repeaters a)$

$(\lbrack a,b\rbrack \ident (a+b))$

$(\langle a,b\rangle \ident (a+b))$

$(\totallyordered \ident 1)$


Space definitions
$(\Struct ab \ident (a + b))$

$(\Set a \ident (- a))$

$(\Space \ident 1)$

$(\newspace a b \ident (a + b))$

$(\ptt x \ident (x \in \U \cond x \els \e))$

$(\fptt f \ident \ptt \setof x,y\in f \One t(x,t \in f))$

$(\extendFn fg \ident (f \cup \strc \fptt g \Cmpl \dmn f))$

$(\endow Af \ident (A \in \Space \cond \bigcup x \in A \{\extendFn xf\}))$

$(\structsub tSS\p \ident 1)$

$(\structdmn S \ident 1)$

$(\subspace S \ident (S \in \Space \cond
\setof S\p \in \Space(\Set S\p \i \Set S \and$
\lineb $ \Each t \in \structdmn S(\Struct S\p t = \structsub gSS\p))))$

$(\ultimes \ident 1)$

$(\ultopology \ident 1)$

$(\ulgraph \ident 1)$

$(\dbara \ident 1)$
$(\dbarb \ident 1)$
$(\dbarc \ident 1)$
$(\dbard \ident 1)$
$(\dbare \ident 1)$
$(\dbarf \ident 1)$
$(\dbarg \ident 1)$
$(\dbarh \ident 1)$
$(\dbari \ident 1)$
$(\dbarj \ident 1)$
$(\dbark \ident 1)$
$(\dbarl \ident 1)$
$(\dbarm \ident 1)$
$(\dbarn \ident 1)$
$(\dbaro \ident 1)$
$(\dbarp \ident 1)$
$(\dbarq \ident 1)$
$(\dbarr \ident 1)$
$(\dbars \ident 1)$
$(\dbart \ident 1)$
$(\dbaru \ident 1)$
$(\dbarv \ident 1)$
$(\dbarw \ident 1)$
$(\dbarx \ident 1)$
$(\dbary \ident 1)$
$(\dbarz \ident 1)$

Algebra definitions
$(\group \ident 1)$

Topological definitions

$(\topologicalSpace \ident 1)$

Limit Definition

$(\lin x \ubar x \ident 1)$

Definition that got Commented Out 

$(\connectsedges abcd \ident (a + b + c + d))$ 
Non-definitions for new syntax

%precedence= 6 
$((a \In b) \Iff (a = a))$

$(\sfun \ident 1)$
 
$(\bfun \ident 1)$

$(\clonzo z \ubar z \ident 1)$

Group Theory

$(\Sym X \ident 1)$

$(\lab X \rab \ident 1)$

For Geometry Example

$(\Point \ident 1)$

$(\Line \ident 1)$

%precedence= 6
$((x\times y) \Iff (x < y))$
