%%\documentclass{article}
%%
%%\usepackage[margin=30mm,a4paper]{geometry}
%%\usepackage{circus}
%%
%%\newcommand{\opt}{~\textrm{opt}~}
%%
%%%\AddToShipoutPicture{\AtTextLowerLeft{\framebox(\LenToUnit{\textwidth},\LenToUnit{\textheight}){}}}
%%
%%\begin{document}

\begin{zsection}
\SECTION ZFormalSyntax \parents basic\_toolkit
\end{zsection}

%%Zinword \& &

\begin{zed}
[GenName, OperatorTemplate]
\end{zed}

\begin{zed}
DeclName ::= decl\ldata NAME \rdata\\
RefName ::= ref\ldata NAME \rdata\\
Formals == \seq_1 NAME
\end{zed}

Declaration of names used in the mathematical toolkit.

\begin{axdef}
UPTO,FFUN,FUN,MAPSTO:NAME\\
MINUS,PLUS, IN, DOM:NAME\\
OVERRIDE: NAME\\
EQUAL,GT: NAME\\
NATURAL,INTEGER:NAME
\end{axdef}

\begin{zed}
STROKECHAR ::= primestroke | outputstroke | inputstroke\\
DECIMAL == 0..9\\
STROKE ::= char \ldata STROKECHAR \rdata | decimal \ldata DECIMAL \rdata\\
%NUMERAL == \seq_1 DECIMAL
\end{zed}

\begin{zed}
Declaration ::= variable\ldata (\seq_1 DeclName) \cross Expression \rdata |\\
		constant\ldata DeclName \cross Expression \rdata |\\
		expression\ldata Expression \rdata\\
\&\\
Predicate ::= newline\ldata Predicate \cross Predicate \rdata |\\
	      semicolon\ldata Predicate \cross Predicate \rdata |\\
	      forall\ldata SchemaText \cross Predicate \rdata |\\
	      exists\ldata SchemaText \cross Predicate \rdata |\\
	      unique\ldata SchemaText \cross Predicate \rdata |\\
	      equivalence\ldata Predicate \cross Predicate \rdata |\\
	      implication\ldata Predicate \cross Predicate \rdata |\\
	      disjunction\ldata Predicate \cross Predicate \rdata |\\
	      conjunction\ldata Predicate \cross Predicate \rdata |\\
	      negation\ldata Predicate \rdata |\\
	      relationapplication\ldata Relation \rdata |\\
	      schemapredicate\ldata Expression \rdata |\\
	      TRUE |\\
	      FALSE |\\
	      parenthesizedpredicate\ldata Predicate \rdata\\
\&\\
Relation ::= rel\ldata NAME \cross \seq Expression \rdata\\
\&\\
Application ::= app\ldata NAME \cross \seq Expression \rdata\\
\&\\
SchemaText ::= schematext\ldata \opt DeclPart \cross \opt Predicate \rdata\\
\&\\
DeclPart ::= declpart\ldata \seq_1 Declaration \rdata\\
\&\\
Expression ::= schemaforall\ldata SchemaText \cross Expression \rdata |\\
	       schemaexists\ldata SchemaText \cross Expression \rdata |\\
	       schemaunique\ldata SchemaText \cross Expression \rdata |\\
	       functionconstruction\ldata SchemaText \cross Expression \rdata |\\
	       definitedescription\ldata SchemaText \cross Expression \rdata |\\
	       substitution\ldata \seq_1 (DeclName \cross Expression) \cross Expression \rdata |\\
	       schemaequivalence\ldata Expression \cross Expression \rdata |\\
	       schemaimplication\ldata Expression \cross Expression \rdata |\\
	       schemadisjunction\ldata Expression \cross Expression \rdata |\\
	       schemaconjunction\ldata Expression \cross Expression \rdata |\\
	       schemanegation\ldata Expression \rdata |\\
	       conditional\ldata Predicate \cross Expression \cross Expression \rdata |\\
	       composition\ldata Expression \cross Expression \rdata |\\
	       piping\ldata Expression \cross Expression \rdata |\\
	       hiding\ldata Expression \cross \seq_1 DeclName \rdata |\\
	       projection\ldata Expression \cross Expression \rdata |\\
	       precondition \ldata Expression \rdata |\\
	       product \ldata Expression \cross Expression \rdata |\\
	       powerset \ldata Expression \rdata|\\
	       functionapplication \ldata Application \rdata |\\
	       application \ldata Expression \cross Expression \rdata |\\
	       decoration \ldata Expression \cross STROKE \rdata |\\
	       schemarenaming \ldata Expression \cross \seq_1 (DeclName \cross DeclName) \rdata |\\
	       bindingselection \ldata Expression \cross RefName \rdata |\\
	       tupleselection \ldata Expression \cross \nat \rdata |\\
	       bindingconstruction \ldata Expression \cross \seq STROKE \rdata |\\
	       reference \ldata RefName \rdata |\\
	       genericinstantitaion \ldata RefName \cross \seq_1 Expression \rdata |\\
	       numberliteral \ldata \num \rdata |\\
	       setextension \ldata \seq Expression \rdata |\\
	       setcomprehension \ldata SchemaText \cross Expression \rdata |\\
	       characteristicsetcomprehension \ldata (SchemaText \setminus \{schematext(\langle \rangle, \langle \rangle)\}) \setminus \{e: Expression; p: \opt Predicate @ schematext(\langle declpart(\langle expression(e)\rangle) \rangle,p)\}\rdata |\\
	       schemaconstruction \ldata SchemaText \setminus \{e: Expression; p: \opt Predicate @ schematext(\langle declpart(\langle expression(e)\rangle) \rangle,p)\}\rdata |\\
	       bindingextension \ldata \seq(DeclName \cross Expression) \rdata |\\
	       tupleextension \ldata \{s: \seq Expression | \# s \geq 2\} \rdata |\\
	       characteristicdefinitedescription \ldata SchemaText \rdata |\\
	       parenthesizedexpression \ldata Expression \rdata |\\
	       sequence \ldata \seq Expression \rdata\\
\&\\
Branch ::= branch \ldata DeclName \cross \opt Expression \rdata\\
\&\\
Freetype ::= freetype \ldata NAME \cross \seq Branch \rdata\\
\&\\
Paragraph ::= giventypes \ldata \seq_1 NAME \rdata |\\
	      axiomaticdescription \ldata SchemaText \rdata |\\
	      schemadefinition \ldata NAME \cross SchemaText \rdata |\\
	      genericaxiomaticdescription \ldata Formals \cross SchemaText \rdata |\\
	      genericschemadefinition \ldata NAME \cross Formals \cross SchemaText \rdata |\\
	      horizontaldefinition \ldata DeclName \cross Expression \rdata |\\
	      generichorizontaldefinition \ldata NAME \cross Formals \cross Expression \rdata |\\
	      genericoperatordefinition \ldata GenName \cross Expression \rdata |\\
	      freetypes \ldata \seq_1 Freetype \rdata |\\
	      conjecture \ldata Predicate \rdata |\\
	      genericconjecture \ldata Formals \cross Predicate \rdata |\\
	      operatortemplate \ldata OperatorTemplate \rdata
\end{zed}
\end{document}
