1 files changed, 95 insertions, 0 deletions
diff --git a/imports/codemirror/mode/stex/index.html b/imports/codemirror/mode/stex/index.html
new file mode 100755
index 00000000..ccd9dd83
--- /dev/null
+++ b/imports/codemirror/mode/stex/index.html
@@ -0,0 +1,95 @@
+<!doctype html>
+<html>
+  <head>
+    <title>CodeMirror: sTeX mode</title>
+    <link rel="stylesheet" href="../../lib/codemirror.css">
+    <script src="../../lib/codemirror.js"></script>
+    <script src="stex.js"></script>
+    <style>.CodeMirror {background: #f8f8f8;}</style>
+    <link rel="stylesheet" href="../../doc/docs.css">
+  </head>
+  <body>
+    <h1>CodeMirror: sTeX mode</h1>
+     <form><textarea id="code" name="code">
+\begin{module}[id=bbt-size]
+\importmodule[balanced-binary-trees]{balanced-binary-trees}
+\importmodule[\KWARCslides{dmath/en/cardinality}]{cardinality}
+\begin{frame}
+  \frametitle{Size Lemma for Balanced Trees}
+  \begin{itemize}
+  \item
+    \begin{assertion}[id=size-lemma,type=lemma] 
+    Let $G=\tup{V,E}$ be a \termref[cd=binary-trees]{balanced binary tree} 
+    of \termref[cd=graph-depth,name=vertex-depth]{depth}$n>i$, then the set
+     $\defeq{\livar{V}i}{\setst{\inset{v}{V}}{\gdepth{v} = i}}$ of
+    \termref[cd=graphs-intro,name=node]{nodes} at 
+    \termref[cd=graph-depth,name=vertex-depth]{depth} $i$ has
+    \termref[cd=cardinality,name=cardinality]{cardinality} $\power2i$.
+   \end{assertion}
+  \item
+    \begin{sproof}[id=size-lemma-pf,proofend=,for=size-lemma]{via induction over the depth $i$.}
+      \begin{spfcases}{We have to consider two cases}
+        \begin{spfcase}{$i=0$}
+          \begin{spfstep}[display=flow]
+            then $\livar{V}i=\set{\livar{v}r}$, where $\livar{v}r$ is the root, so
+            $\eq{\card{\livar{V}0},\card{\set{\livar{v}r}},1,\power20}$.
+          \end{spfstep}
+        \end{spfcase}
+        \begin{spfcase}{$i>0$}
+          \begin{spfstep}[display=flow]
+           then $\livar{V}{i-1}$ contains $\power2{i-1}$ vertexes 
+           \begin{justification}[method=byIH](IH)\end{justification}
+          \end{spfstep}
+          \begin{spfstep}
+           By the \begin{justification}[method=byDef]definition of a binary
+              tree\end{justification}, each $\inset{v}{\livar{V}{i-1}}$ is a leaf or has
+            two children that are at depth $i$.
+          \end{spfstep}
+          \begin{spfstep}
+           As $G$ is \termref[cd=balanced-binary-trees,name=balanced-binary-tree]{balanced} and $\gdepth{G}=n>i$, $\livar{V}{i-1}$ cannot contain
+            leaves.
+          \end{spfstep}
+          \begin{spfstep}[type=conclusion]
+           Thus $\eq{\card{\livar{V}i},{\atimes[cdot]{2,\card{\livar{V}{i-1}}}},{\atimes[cdot]{2,\power2{i-1}}},\power2i}$.
+          \end{spfstep}
+        \end{spfcase}
+      \end{spfcases}
+    \end{sproof}
+  \item 
+    \begin{assertion}[id=fbbt,type=corollary]   
+      A fully balanced tree of depth $d$ has $\power2{d+1}-1$ nodes.
+    \end{assertion}
+  \item
+      \begin{sproof}[for=fbbt,id=fbbt-pf]{}
+        \begin{spfstep}
+          Let $\defeq{G}{\tup{V,E}}$ be a fully balanced tree
+        \end{spfstep}
+        \begin{spfstep}
+          Then $\card{V}=\Sumfromto{i}1d{\power2i}= \power2{d+1}-1$.
+        \end{spfstep}
+      \end{sproof}
+    \end{itemize}
+  \end{frame}
+\begin{note}
+  \begin{omtext}[type=conclusion,for=binary-tree]
+    This shows that balanced binary trees grow in breadth very quickly, a consequence of
+    this is that they are very shallow (and this compute very fast), which is the essence of
+    the next result.
+  \end{omtext}
+\end{note}
+\end{module}
+%%% Local Variables: 
+%%% mode: LaTeX
+%%% TeX-master: "all"
+%%% End: \end{document}
+</textarea></form>
+    <script>
+      var editor = CodeMirror.fromTextArea(document.getElementById("code"), {});
+    </script>
+    <p><strong>MIME types defined:</strong> <code>text/stex</code>.</p>
+  </body>
+</html>

diff --git a/imports/codemirror/mode/stex/index.html b/imports/codemirror/mode/stex/index.html new file mode 100755 index 00000000..ccd9dd83 --- /dev/null +++ b/imports/codemirror/mode/stex/index.html
@@ -0,0 +1,95 @@
	1	<!doctype html>
	2	<html>
	3	<head>
	4	<title>CodeMirror: sTeX mode</title>
	5	<link rel="stylesheet" href="../../lib/codemirror.css">
	6	<script src="../../lib/codemirror.js"></script>
	7	<script src="stex.js"></script>
	8	<style>.CodeMirror {background: #f8f8f8;}</style>
	9	<link rel="stylesheet" href="../../doc/docs.css">
	10	</head>
	11	<body>
	12	<h1>CodeMirror: sTeX mode</h1>
	13	<form><textarea id="code" name="code">
	14	\begin{module}[id=bbt-size]
	15	\importmodule[balanced-binary-trees]{balanced-binary-trees}
	16	\importmodule[\KWARCslides{dmath/en/cardinality}]{cardinality}
	17
	18	\begin{frame}
	19	\frametitle{Size Lemma for Balanced Trees}
	20	\begin{itemize}
	21	\item
	22	\begin{assertion}[id=size-lemma,type=lemma]
	23	Let $G=\tup{V,E}$ be a \termref[cd=binary-trees]{balanced binary tree}
	24	of \termref[cd=graph-depth,name=vertex-depth]{depth}$n>i$, then the set
	25	$\defeq{\livar{V}i}{\setst{\inset{v}{V}}{\gdepth{v} = i}}$ of
	26	\termref[cd=graphs-intro,name=node]{nodes} at
	27	\termref[cd=graph-depth,name=vertex-depth]{depth} $i$ has
	28	\termref[cd=cardinality,name=cardinality]{cardinality} $\power2i$.
	29	\end{assertion}
	30	\item
	31	\begin{sproof}[id=size-lemma-pf,proofend=,for=size-lemma]{via induction over the depth $i$.}
	32	\begin{spfcases}{We have to consider two cases}
	33	\begin{spfcase}{$i=0$}
	34	\begin{spfstep}[display=flow]
	35	then $\livar{V}i=\set{\livar{v}r}$, where $\livar{v}r$ is the root, so
	36	$\eq{\card{\livar{V}0},\card{\set{\livar{v}r}},1,\power20}$.
	37	\end{spfstep}
	38	\end{spfcase}
	39	\begin{spfcase}{$i>0$}
	40	\begin{spfstep}[display=flow]
	41	then $\livar{V}{i-1}$ contains $\power2{i-1}$ vertexes
	42	\begin{justification}[method=byIH](IH)\end{justification}
	43	\end{spfstep}
	44	\begin{spfstep}
	45	By the \begin{justification}[method=byDef]definition of a binary
	46	tree\end{justification}, each $\inset{v}{\livar{V}{i-1}}$ is a leaf or has
	47	two children that are at depth $i$.
	48	\end{spfstep}
	49	\begin{spfstep}
	50	As $G$ is \termref[cd=balanced-binary-trees,name=balanced-binary-tree]{balanced} and $\gdepth{G}=n>i$, $\livar{V}{i-1}$ cannot contain
	51	leaves.
	52	\end{spfstep}
	53	\begin{spfstep}[type=conclusion]
	54	Thus $\eq{\card{\livar{V}i},{\atimes[cdot]{2,\card{\livar{V}{i-1}}}},{\atimes[cdot]{2,\power2{i-1}}},\power2i}$.
	55	\end{spfstep}
	56	\end{spfcase}
	57	\end{spfcases}
	58	\end{sproof}
	59	\item
	60	\begin{assertion}[id=fbbt,type=corollary]
	61	A fully balanced tree of depth $d$ has $\power2{d+1}-1$ nodes.
	62	\end{assertion}
	63	\item
	64	\begin{sproof}[for=fbbt,id=fbbt-pf]{}
	65	\begin{spfstep}
	66	Let $\defeq{G}{\tup{V,E}}$ be a fully balanced tree
	67	\end{spfstep}
	68	\begin{spfstep}
	69	Then $\card{V}=\Sumfromto{i}1d{\power2i}= \power2{d+1}-1$.
	70	\end{spfstep}
	71	\end{sproof}
	72	\end{itemize}
	73	\end{frame}
	74	\begin{note}
	75	\begin{omtext}[type=conclusion,for=binary-tree]
	76	This shows that balanced binary trees grow in breadth very quickly, a consequence of
	77	this is that they are very shallow (and this compute very fast), which is the essence of
	78	the next result.
	79	\end{omtext}
	80	\end{note}
	81	\end{module}
	82
	83	%%% Local Variables:
	84	%%% mode: LaTeX
	85	%%% TeX-master: "all"
	86	%%% End: \end{document}
	87	</textarea></form>
	88	<script>
	89	var editor = CodeMirror.fromTextArea(document.getElementById("code"), {});
	90	</script>
	91
	92	<p><strong>MIME types defined:</strong> <code>text/stex</code>.</p>
	93
	94	</body>
	95	</html>