.Open Lexemes for MATHS
. Informal Introduction
.See http://www/dick/samples/comp.text.ASCII.html
digit::="0".."9",
letter::=lower_case | uppercase,
lower_case::="a".."z"
upper_case::="A".."Z".

eoln::= #whitespace (ASCII.CR | ASCII.LF) #whitespace.
break::= eoln eoln #eoln, -- two or more eolns can break comments up into paragraph.
indentation::= (ASCII.SP | ASCII.HT) #(ASCII.SP | ASCII.HT).

quote::="\"", -- a backslash changes the meaning of the next char exactly as it does in ANSI C.
backslash::="\\" -- as in C a backslash is an escape character and so two are needed to represent one.

Formal statements are distinguished by the presence of the double colon some
where in the line or else by white space character at the start of a line:
.As_is 	::=	is defined to be the same as
.As_is 	::	is declared to be a
Indented formula can be labeled:
.As_is 		(label):	display and name a formula, if indented at start of line
.As_is 	(label):		Allows a label to be attached to an informal statemnt.
.As_is 	|-(label):	State an assumption or axiom.
.As_is 	(reasons)|-(label):	assert a provable theorem
In a logically complete document for each provable theorem labeled `l` has a
proof in a section headed ".Proof of `l`".  All the steps in the
proof are either standard (and well known) or are listed as reasons.
The reasons will all be labels of formula that have appeared previous
to the statemnt of the theorem.
.As_is 	|- yada::=		Indicates a definition for `yada` has been introduced earlier.
The above is most useful when you want to include a package with many
definitions in it and then draw the reader's attention to particular
ones.  This also creates a visible link in this document to the
quoted definition.

The ASCII characters "@#$ ^&|~" are used in place of written symbols used in discrete mathematics:
.As_is 	&	intersection
.As_is 	|	union/alternate syntaxes
.As_is 	~	complement
.See http://www.csci.csusb.edu/dick/maths/logic_30_Sets.html
.As_is 	@	Subsets of/Subsets defined by
.See http://www.csci.csusb.edu/dick/maths/logic_31_Families_of_Sets.html
.As_is 	#	Numbered sequences of
.See http://www.csci.csusb.edu/dick/maths/logic_6_Numbers..Strings.html
.See http://www.csci.csusb.edu/dick/maths/math_62_Strings.html
.As_is 	$	Structured Set/Set defined by documentation
.See http://www.csci.csusb.edu/dick/maths/notn_13_Docn_Syntax.html
.See http://www.csci.csusb.edu/dick/maths/notn_14_Docn_Semantics.html
.See http://www.csci.csusb.edu/dick/maths/notn_15_Naming_Documentn.html

.As_is 	^	Power, raise up, superscript

. Parentheses, Brackets and Braces
.As_is	{}	Sets, alternately use SET(...)
.As_is 	()	Order of operations, lists, sequences, function application
.As_is 	[]	Lower/subscript/map from, else use MAP[...]
.As_is 	\<...\>	BNF Brockets (broken brackets -- term from Physics)
.As_is 	\[...\]	Semantic brackets (shown like this [[...]] in some texts).

Additional non-ASCII symbols a described by using any of nroff or TEX code or by concatenating these symbols "~-*><:=." together.  Here are some special arrows
and crosses
.As_is 	+>	Maplet
.As_is	->	Mappings and functions
.As_is	<>->	Partial Mappings and functions
.As_is	><	Cartesian and Cross Products

.As_is 	=>	Substitution

.As_is 	<=	Less than or equal
.As_is 	>=	greater than or equal
.As_is 	<>	not equal (Pascal and BASIC)

.As_is 	==>	subset
.As_is 	=>>	proper subset
.As_is 	>==	partitioning
.See http://www.csci.csusb.edu/dick/maths/logic_30_Sets.html

.As_is	||	"where" in intensional set descriptions {x:T || P}
.As_is	.	"where" in intensional set descriptions {x:T. P}

The slash("/") is used as a prefixed inversion/converse operator, rather 
than having "^{-1}" afterwards - it can be thought of as a generalised 
"root" symbol(sqrt=/(^2)), or possibly being short for "arc" (arcsin=/sin).

Lists, strings, and sequences can be treated as functions.  Functions as 
relations.  For example (a,b,c) = ( 1+>a | 2+>b | 3+>c).  Further they can
be inverted, so that for example: /(a,b,c) = ( a+>1 | b+>2 | c+>3 ).

All functions can used in prefix, postfix and infix form and are overloaded
to also apply to sequences and sets of elements.

However some functions have a `serial` interpretation (for example 
+(1,2,3)=1+2+3), while others have a `parallel` interpretation (for example
<(1,2,3)=(1<2<3)=(1<2 and 2<3)).  This obviates the need for special signs
for the same operations(with apologies to Lagrange who was the first to use
\Sigma where MATHS uses "+").

Identifiers can be used for variables, constants, functions, operators etc.
however there are two kinds of identifier.  The mathemaatical is short and
used locally in algebraic formula - for example "x", "\lambda", ...  The
others a longer and made up of words in the client's language.  These
have a wider scope and should indicate their meaning clearly, if at
all possible.  Here are some special identifiers with predefined meanings:
.As_is	and	Boolean conjunction
.As_is	or	Boolean inclusive disjunction
.As_is	if	Start of conditional
.As_is 	then	Separates premise from conclusion in conditional
.As_is	for	Introduces a series of quantifiers
.As_is 	all, some, one, no, 1,2,3,4,...	Quantifiers
.As_is 	not	Boolean complement
.As_is 	the	definite description of an object

. Formal Treatment
.See http://www.csci.csusb.edu/dick/maths/notn_10_Lexicon.html

.Close Lexemes of MATH