\documentclass{article}

\usepackage{xspace}
\usepackage{hyperref}
\usepackage{bm}
\usepackage[english]{babel}
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{mathtools}
\newcommand{\jh}[1]{{\leavevmode\color{blue!50!red}#1}}

\input{notation.tex}
\input{glossary.tex}
\pagenumbering{arabic}
\pagestyle{plain}

\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}

\begin{document}

% \maketitle

\definition{monotone}{define monotone}
\definition{image}{define set image}
\definition{lubglb}{define glb and lub}
\definition{topbot}{define $\top$ and $\bot$}
\definition{completelattice}{define complete lattice}

Hello world\cite{tarskilatticetheoretical1955}
First, we generalize Knaster-Tarski Fixpoint Theorem.

$$\fixpointsOf(S)$$


\begin{theorem}[Tarski-Knaster Fixpoint Theorem~\cite{tarskilatticetheoretical1955}]\label{tarskitheorem}
    For a \Monotone function $o$ over a \CompleteLattice $\langle \L, \lte \rangle$, we have that $\langle \fixpointsOf(o), \lte \rangle$ is a \CompleteLattice.
\end{theorem}

\begin{theorem}
    Trivial attempt using set preimage / image to attain LUB / GLB in image lattice does not work.

    Consider antichain of 2 that map to a chain in image.
    The antichain's LUB does maps to a third, distinct element which extends the chain to three in the image

    If we attain LUB of preimage, then its not the least element :)
\end{theorem}

\begin{theorem}\label{imagelattice}
    For a \Monotone function $o$ over a \CompleteLattice $\langle \L, \lte \rangle$, we have that $\langle o\imageNoLink{\L}, \lte \rangle$ is a \CompleteLattice.
\end{theorem}
\begin{proof}
    Consider $\langle \L', \lte \rangle$ where
    \begin{align*}
        \L' \define \{ x' ~|~ x \in \L \} \\
        x' \lte y' \iff x \lte y \textrm{ where } x, y \in \L
    \end{align*}
    Clearly, $\langle \L', \lte' \rangle$ is a \CompleteLattice.
    Combining $\L$ and $\L'$, we formulate $\L^*$:
    \begin{align*}
        \L^* &\define \{ \top^*, \bot^* \} \union \L \union \L' \\
        \forall x^*, y^* \in \L^*, x^* \lte y^* &\iff \begin{cases}
            (x^* = \bot^*) \lor (y^* = \top^*), \\
            \textrm{or } x, y \in \L, \\ 
            \textrm{or } x', y' \in \L'
        \end{cases}
    \end{align*}
    It is easy to show that $\langle \L^*, \lte \rangle$ is a \CompleteLattice.
    Consider the operator $o^*$ that maps elements from $\L$ to $\L'$ and every element in $\L'$ to itself.
    \begin{align*}
        o^*(x) \define \begin{cases}
            o(x)' & \textrm{if } x \in \L \\
            x & \textrm{otherwise}
        \end{cases}
    \end{align*}
    We have $o^*\image{\L \union \L'} \subseteq L'$ and $\fixpointsOf(o^*) = o\image{\L}' \union \{ \bot^*, \top^* \}$.
    By Tarski-Knaster Fixpoint Theorem (Theorem \ref{tarskitheorem}), $\fixpointsOf(o^*)$ is a \CompleteLattice.
    Thus, $o\image{\L} \union \{ \bot^*, \top^* \}$ is a \CompleteLattice. For any $S \subseteq \L$, we have $\glb S \not\in \{ \bot^*, \top^* \}$ and $\lub S \not\in \{ \bot^*, \top^* \}$, thus $\langle o\image{\L}, \preceq \rangle$ is a \CompleteLattice.
\end{proof}

The following follows directly from the contrapositive of Theorem \ref{imagelattice}.
\begin{corollary}
    If $\langle o\image{\L}, \lte \rangle$ is not a \CompleteLattice, then $o$ is not \Monotone.
\end{corollary}


\begin{definition}
    An approximator set $H$ captures a nondeterministic approximator $o$ if for each consistent pair $(x, y)$
    \begin{align*}
        (H\image{(x, y)}_1, H\image{(x, y)}_2) = o(x, y)
    \end{align*}
\end{definition}

\begin{theorem}
    A nondeterministic approximator $o$ has a set of 
\end{theorem}

\begin{theorem}
    For any nondeterministic approximator $o$, there exists an approximator set $H$ s.t.\ gamma stable models correspond to n-stable models
\end{theorem}
\begin{proof}
    foo
\end{proof}


\bibliographystyle{plain}
\bibliography{references}

\end{document}