Clean up mistakes

3 files changed, 29 insertions, 52 deletions

diff --git a/.build.yml b/.build.yml
index 7d54b98..a6f6ce1 100644
--- a/.build.yml
+++ b/.build.yml
@@ -7,7 +7,7 @@ packages:
 sources:
   - https://git.sr.ht/~cnx/site
 tasks:
-  - katex: |
+  - inject: |
       mkdir -p site/_libs/katex
       cp /usr/lib/node_modules/katex/dist/katex.min.js site/_libs/katex
       cp -r /usr/lib/node_modules/katex/dist/{fonts,katex.min.css} site/_css
diff --git a/_css/style.css b/_css/style.css
index dbd1874..5185744 100644
--- a/_css/style.css
+++ b/_css/style.css
@@ -56,11 +56,6 @@ body { margin: 0 1rem }
 
 .franklin-content .right { float: right }
 
-.franklin-content .container img {
-    width: auto;
-    padding-left: 0;
-}
-
 /* Text geometry */
 .franklin-content p {
     hyphens: auto;
@@ -107,45 +102,25 @@ body { margin: 0 1rem }
 .franklin-content .bibref a,
 .franklin-content .eqref a { color: var(--link-fg) }
 
+.franklin-content .fndef {
+    border: none;
+    margin: 1ex 0;
+}
 .franklin-content .fndef tr { text-align: left }
+.franklin-content .fndef td { padding: 0 }
 .franklin-content .fndef td, .franklin-content sup { font-size: 80% }
-.franklin-content .fndef td.fndef-content { width: 100% }
 .franklin-content .fndef td.fndef-backref { padding-left: 0 }
-.franklin-content table.fndef {
-    border: none;
-    margin: 0;
-}
+.franklin-content .fndef td.fndef-content { padding-left: 1ch }
 
 /* Images */
 .franklin-content img {
     display: block;
     margin: auto;
     max-width: 100%;
-    width: auto;
 }
 
 /* KaTeX */
 .katex { font-size: 1em !important }
-.katex-display .katex {
-    /* Overwrite KaTeX settings. */
-    display: inline-block;
-
-    /* Allow display equations to wrap on small screens. */
-    white-space: normal;
-}
-
-/*
- * No numbering, for now
- * body { counter-reset: eqnum }
- *
- * .katex-display::after {
- *     counter-increment: eqnum;
- *     content: "(" counter(eqnum) ")";
- *     position: relative;
- *     float: right;
- *     padding-right: 5px;
- * }
- */
 
 /* Boxes */
 .franklin-content blockquote, .note {
diff --git a/blog/boolin.md b/blog/boolin.md
index 6acae55..00f118f 100644
--- a/blog/boolin.md
+++ b/blog/boolin.md
@@ -137,12 +137,12 @@ definitions of an environment marker
 \[\begin{aligned}
   (e_1, \ldots, e_{11})
   &\mapsto \bigvee_{\imath = 1}^n\bigwedge_{\jmath = 1}^{f(\imath)}
-  x(\jmath)\left(e_{k(\jmath)}\right)\\
+  x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)\\
   (e_1, \ldots, e_{11})
   &\mapsto \bigwedge_{\imath = 1}^n\bigvee_{\jmath = 1}^{f(\imath)}
-  x(\jmath)\left(e_{k(\jmath)}\right)
+  x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)
 \end{aligned}\]
-where $n \in \N$, $f: \N^* \to \N^*$, $x: \N^* \to X$, $k: \N^* \to I$
+where $n \in \N$, $f: \N_1 \to \N_1$, $x: \N_1^2 \to X$, $k: \N_1^2 \to I$
 and an empty Boolean expression is implicitly $c_\top$.
 
 Now it is possible to formalize inclusion for markers as
@@ -152,55 +152,57 @@ Thus, checking if a marker includes another is equivalent to evaluating
 the following expression, for all $(e_1, \ldots, e_{11}) \in E$
 \[\begin{aligned}
   r &= \bigvee_{\imath' = 1}^{n'}\bigwedge_{\jmath' = 1}^{f'(\imath')}
-       x'(\jmath')\left(e_{k'(\jmath')}\right)
+       x'(\imath', \jmath')\left(e_{k'(\imath', \jmath')}\right)
        \le \bigwedge_{\imath = 1}^n\bigvee_{\jmath = 1}^{f(\imath)}
-       x(\jmath)\left(e_{k(\jmath)}\right)\\
+       x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)\\
     &= \bigwedge_{\imath' = 1}^{n'}\left(\bigwedge_{\jmath' = 1}^{f'(\imath')}
-       x'(\jmath')\left(e_{k'(\jmath')}\right)
+       x'(\imath', \jmath')\left(e_{k'(\imath', \jmath')}\right)
        \le \bigwedge_{\imath = 1}^n\bigvee_{\jmath = 1}^{f(\imath)}
-       x(\jmath)\left(e_{k(\jmath)}\right)\right)\\
+       x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)\right)\\
     &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n
        \left(\bigwedge_{\jmath' = 1}^{f'(\imath')}
-       x'(\jmath')\left(e_{k'(\jmath')}\right)
+       x'(\imath', \jmath')\left(e_{k'(\imath', \jmath')}\right)
        \le \bigvee_{\jmath = 1}^{f(\imath)}
-       x(\jmath)\left(e_{k(\jmath)}\right)\right)
+       x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)\right)
 \end{aligned}\]
 where $r$ is whether the original marker (defined by $n$, $f$, $x$ and $k$)
 includes the declared one (defined by $n'$, $f'$, $x'$ and $k'$). Let
 \[\begin{aligned}
   g(\imath, \ell) &= \{\jmath \mid \jmath \in [1, f(\imath)]
-                              \land k(\jmath) = \ell\}\\
+                              \land k(\imath, \jmath) = \ell\}\\
   g'(\imath, \ell) &= \{\jmath \mid \jmath \in [1, f'(\imath)]
-                               \land k'(\jmath) = \ell\}
+                               \land k'(\imath, \jmath) = \ell\}
 \end{aligned}\]
 and assume $e_1, \ldots, e_{11}$ are orthogonal, we have
 \[\begin{aligned}
   r &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n\bigvee_{\ell \in I}
        \left(\bigwedge_{\jmath' \in g'(\imath', \ell)}
-       x'(\jmath')\left(e_{\ell}\right)
+       x'(\imath', \jmath')\left(e_{\ell}\right)
        \le \bigvee_{\jmath \in g(\imath, \ell)}
-       x(\jmath)\left(e_{\ell}\right)\right)\\
+       x(\imath, \jmath)\left(e_{\ell}\right)\right)\\
     &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n\bigvee_{\ell \in I}
        \left(\bigwedge_{\jmath' \in g'(\imath', \ell)}
-       x'(\jmath')\left(e_{\ell}\right)
+       x'(\imath', \jmath')\left(e_{\ell}\right)
        \land \lnot \bigvee_{\jmath \in g(\imath, \ell)}
-       x(\jmath)\left(e_{\ell}\right) = \bot\right)
+       x(\imath, \jmath)\left(e_{\ell}\right) = \bot\right)
 \end{aligned}\]
 where $\bot$ is the Boolean algebra bottom element.  By [De Morgan's laws],
 \[\begin{aligned}
   r &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n\bigvee_{\ell \in I}
        \left(\bigwedge_{\jmath' \in g'(\imath', \ell)}
-       x'(\jmath')\left(e_{\ell}\right)
+       x'(\imath', \jmath')\left(e_{\ell}\right)
        \land \bigwedge_{\jmath \in g(\imath, \ell)}
-       \lnot x(\jmath)\left(e_{\ell}\right) = \bot\right)
+       \lnot x(\imath, \jmath)\left(e_{\ell}\right) = \bot\right)
 \end{aligned}\]
 
 Essentially, checking if
-\[\bigwedge_{\jmath' \in g'(\imath', \ell)} x'(\jmath')\left(e_{\ell}\right)
+\[\bigwedge_{\jmath' \in g'(\imath', \ell)}
+  x'(\imath', \jmath')\left(e_{\ell}\right)
   \land \bigwedge_{\jmath \in g(\imath, \ell)}
-  \lnot x(\jmath)\left(e_{\ell}\right)\]
+  \lnot x(\imath, \jmath)\left(e_{\ell}\right)\]
 is unsatisfiable for all $e_{\ell}$ is a [SAT problem] which we can write
-a solver for.
+a solver for.  Indeed, the original expression could be formulated as a SAT,
+but it would be more complex due to the multiple dimensions of environments.
 
 ## Implementation