\documentclass[11pt]{article}
\usepackage[fleqn]{amsmath}
% \DeclareSymbolFont{AMSa}{U}{msa}{m}{n}
% \DeclareSymbolFont{AMSb}{U}{msb}{m}{n}
% \begingroup \catcode`\"=12
% \DeclareMathDelimiter\ulcorner{\mathopen} {AMSa}{"70}{AMSa}{"70}
% \DeclareMathDelimiter\urcorner{\mathclose}{AMSa}{"71}{AMSa}{"71}
% \endgroup
\addtolength{\oddsidemargin}{-.25in}
\addtolength{\leftmargini}{18pt}
\addtolength{\labelsep}{12pt}
\addtolength{\textheight}{.75in}
%\advance\voffset-.75in

\DeclareMathOperator{\limp}{\;\to\;}
\DeclareMathOperator{\lequiv}{\;\leftrightarrow\;}
%\DeclareMathOperator{\proves}{\vdash}
\DeclareMathOperator{\proves}{|\!---\;}
%\DeclareMathOperator*{\disj}{\bigvee}
%\DeclareMathOperator*{\conj}{\bigwedge}
\def\leqn{\approx}
% \let\plainlor\lor
% \let\plainland\land

\def\phi{\varphi}
%\def\n#1{\bar{#1}}
% \newdimen\temp
% \def\n#1{{\setbox1\hbox{$#1$}\hbox
% to\wd1{\hss\temp=\wd1\advance\temp
% by-2.5pt\ifdim\temp<.3em\temp=.3em\fi
% $\overline{\hbox to\temp{\hss\box1\hss}}$\hss}}}
%\def\n{}
\def\n#1{\overline{\!#1\!}}

\def\fm#1{\mathop{\rm #1}\nolimits}
\def\qt#1{\text{``}#1\text{''}}
%\def\gn#1{{}^\ulcorner {#1}\, {}^\urcorner}
\def\gn#1{{\scriptscriptstyle{}^\lceil} {#1}{\scriptscriptstyle {}^\rceil}}
\def\concat{{}^\frown}

\begin{document}
%\DeclareMathOperator{\lor}{{\scriptstyle\lor}}
%\DeclareMathOperator{\land}{{\scriptstyle\land}}
%\DeclareMathOperator{\lnot}{\lnot}
%\DeclareMathOperator{\leq}{\approx}
%\def\proves{\mathrel\vdash}
%\def\limp{\mathbin{\,\,\to}\,\,}

% \renewcommand\lor{\mathbin{\scriptstyle\,\plainlor}\,}
% \renewcommand\land{\mathbin{\scriptstyle\,\plainland}\,}

%\def\disj{\bigvee}
%\def\conj{bigwedge}

This is the +-term example I gave in class on Friday.
\begin{enumerate}
%\renewcommand{\theenumi}{\Alph{enumi}}
%\renewcommand{\labelenumi}{\theenumi)}

\item $\n0$ is a +-term.
\item Any variable is a +-term.
\item If $\tau,\ \pi$ are +-terms, so is $\tau+\pi$.
\item Nothing is a +-term except as required by
1, 2, and 3.
\end{enumerate}

To give a formula representing the set of +-terms, we'll need
two other useful formulas, beside what we already have:
\begin{description}
\item[$\fm{Var}(x)$] ``x is a variable'', i.e., the 5-bit
bytes in $x$ are all equal to $\gn\nu$.

\item[$\fm{concat}(u,v,y)$] ``$y$ is the concatenation of $u$
and $v$''.
\end{description}
Concatenating two strings is just putting them
together.  We have, for any two strings of symbols $\alpha,\ \beta$,
\[\proves \forall y (\fm{concat}(\n{\gn\alpha},\n{\gn\beta},y)
\lequiv y\leqn \n{\gn{\alpha\beta}})\]
Another handy notation for concatenation is $u\concat v$.  As
with any other ``defined'' function, we use it with the
understanding that its occurences within formulas are merely
abbreviations for something else: for example, a formula
\[y\leqn u\concat v \text{\qquad abbreviates\qquad}
\forall z(\fm{concat}(u,v,z)\limp y\leqn z)\]

You should give definitions for both $\fm{Var}(x)$ and
$\fm{concat}(u,v,y)$.

This is the idea for the representing formula for the set of
+-terms:
\begin{quote}$\alpha$ is a +-term if and only if there is a sequence such
that each term is either  $\n0$, or is a variable, or is $\tau+\pi$
for some
two previous terms $\tau$ and $\pi$, and $\alpha$ is a term of
this sequence.
\end{quote}
Now here is the representing formula itself:

\begin{eqnarray*}\lefteqn{\exists z(\fm{seq}(z) \land \forall i (\n0<i<\fm{ln}(z) \limp
(z)_i\leqn \n{\gn{\n0}} \lor  \fm{Var}((z)_i) \lor}\\
&&\exists j\exists k
(\n0<j<i \land \n0<k<i \land (z)_i\leqn (z)_j\concat\,
\n{\gn+}{}\concat\,
 (z)_k)) \land \exists i (x\leqn (z)_i))
\end{eqnarray*}

\end{document}
