.

betastable/report.out

@@ -3,3 +3,4 @@
 \BOOKMARK [1][-]{section.3}{\376\377\000D\000e\000t\000e\000r\000m\000i\000n\000i\000s\000t\000i\000c\000\040\000A\000F\000T}{}% 3
 \BOOKMARK [1][-]{section.4}{\376\377\000S\000k\000e\000t\000c\000h\000\040\000N\000o\000v\000\040\0002\0000}{}% 4
 \BOOKMARK [1][-]{section.5}{\376\377\000S\000k\000e\000t\000c\000h\000\040\000J\000a\000n\000\040\0002\0000}{}% 5
+\BOOKMARK [1][-]{section.6}{\376\377\000S\000k\000e\000t\000c\000h\000\040\000J\000a\000n\000\040\0002\0004\000t\000h}{}% 6

betastable/report.tex

@@ -75,8 +75,8 @@ pdfpagemode=FullScreen,
 
 
 
-
-
+\section{Sketch Jan 24th}
+\input{sections/sketchjan24.tex}
 
 \bibliographystyle{plain}
 \bibliography{../references}

betastable/sections/sketchjan24.tex

@@ -0,0 +1,14 @@
+\begin{propositionOf}{ndaoSmonotone}
+    S for \Ndao s is monotone
+\end{propositionOf}
+\begin{proof}
+    Have $(x, y) \ltePrecision (x', y')$.
+
+    Assume downwards closed, $S(o)(x', y')_1$ is nonempty.
+    Let $x^{*} \in S(o)(x', y')_1$
+
+    We have $x^{*} \in o(x^{*}, y')$.
+    By the \Monotonicity of $o$, $\exists x^{**} \in o(x^{*}, y)$ s.t. $x^{**} \lte x^{*}$.
+    By transfinite induction, generate a chain of prefixpoints using the process above.
+    By downwards closed, there is a minimal, that is a fixpoint?
+\end{proof}

glossary.tex

@@ -18,6 +18,7 @@
 \newcommand{\LeastFixpoint}{\definitionLink{leastfixpoint}{least fixpoint}}
 \newcommand{\ConsistentPair}{\definitionLink{consistentpair}{consistent}}
 \newcommand{\Monotone}{\definitionLink{monotone}{monotone}}
+\newcommand{\Monotonicity}{\definitionLink{monotonicity}{monotonicity}}
 \newcommand{\Exact}{\definitionLink{deterministicexactapproximator}{exact}}
 \newcommand{\Symmetric}{\definitionLink{deterministicsymmetricapproximator}{symmetric}}
 \newcommand{\Symmetry}{\definitionLink{deterministicsymmetricapproximator}{symmetry}}