diff --git a/content/normal-modal-logic/axioms-systems/more-proofs-in-K.tex b/content/normal-modal-logic/axioms-systems/more-proofs-in-K.tex
index 1205f13c..80e1854d 100644
--- a/content/normal-modal-logic/axioms-systems/more-proofs-in-K.tex
+++ b/content/normal-modal-logic/axioms-systems/more-proofs-in-K.tex
@@ -71,11 +71,11 @@
 
 \begin{proof}
   \begin{derivation}
-    1. & $\Log{K} \Proves \lnot !A \lif (\lnot !B \lif \lnot (!A \lor !B)$ & \Taut \\
+    1. & $\Log{K} \Proves \lnot !A \lif (\lnot !B \lif \lnot (!A \lor !B))$ & \Taut \\
     2. & $\Log{K} \Proves \Box\lnot !A \lif
-    (\Box\lnot!B \lif \Box \lnot (!A \lor !B)$ & \RK\\
+    (\Box\lnot!B \lif \Box \lnot (!A \lor !B))$ & \RK\\
     3. & $\Log{K} \Proves \Box\lnot !A \lif (\lnot \Box \lnot (!A \lor!B)
-    \lif \lnot\Box\lnot !B))$ & \PL, 2\\
+    \lif \lnot\Box\lnot !B)$ & \PL, 2\\
     4. & $\Log{K} \Proves \lnot \Box \lnot(!A \lor !B) \lif (\Box \lnot !A \lif 
     \lnot\Box\lnot !B)$ & \PL, 3\\
     5. & $\Log{K} \Proves \lnot \Box \lnot(!A\lor!B) \lif (\lnot
diff --git a/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex b/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex
index 63359fa7..fc4a5d2e 100644
--- a/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex
+++ b/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex
@@ -31,7 +31,7 @@
       \begin{derivation}
         1. & $\Log{KT5} \Proves \Diamond!A \lif \Box\Diamond!A$ & \Ax{5}\\
         2. & $\Log{KT5} \Proves !A \lif \Diamond!A$ & $\Ax{T_\Diamond}$\\
-        3. & $\Log{KT5} \Proves !A \lif \Box\Diamond!A$ & \PL.
+        3. & $\Log{KT5} \Proves !A \lif \Box\Diamond!A$ & \PL, 2, 1.
       \end{derivation}
     \item $\Log{KT5} \Proves \Ax{4}$:
       \begin{derivation}
@@ -39,7 +39,7 @@
         with $\Box!A$ for $p$\\
         2. & $\Log{KT5} \Proves \Box!A \lif \Diamond\Box!A$ & $\Ax{T_\Diamond}$
         with $\Box!A$ for $p$\\
-        3. & $\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$ & \PL, 1, 2\\
+        3. & $\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$ & \PL, 2, 1\\
         4. & $\Log{KT5} \Proves \Diamond\Box!A \lif \Box!A$ & $\Ax{5_\Diamond}$\\
         5. & $\Log{KT5} \Proves \Box\Diamond\Box!A \lif \Box\Box!A$ & \RK{}, 4 \\
         6. & $\Log{KT5} \Proves \Box!A \lif \Box\Box!A$ & \PL, 3, 5. \\
@@ -49,9 +49,9 @@
         1. & $\Log{KDB4} \Proves \Diamond\Box!A \lif !A $ & $\Ax{B_\Diamond}$ \\
         2. & $\Log{KDB4} \Proves \Box\Box!A \lif \Diamond\Box!A$ & $\Ax{D}$
         with $\Box!A$ for $p$\\
-        3. & $\Log{KDB4} \Proves \Box\Box!A \lif !A$ & \PL 1, 2\\
-        4. &  $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$ & \Ax{4} \\
-        5. & $\Log{KDB4} \Proves \Box!A \lif !A$ & \PL, 1, 4. \\
+        3. & $\Log{KDB4} \Proves \Box\Box!A \lif !A$ & \PL, 1, 2\\
+        4. & $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$ & \Ax{4} \\
+        5. & $\Log{KDB4} \Proves \Box!A \lif !A$ & \PL, 4, 3. \\
       \end{derivation}
     \item $\Log{KB4} \Proves \Ax{5}$:
       \begin{derivation}
diff --git a/content/normal-modal-logic/axioms-systems/systems-distinct.tex b/content/normal-modal-logic/axioms-systems/systems-distinct.tex
index b22d424a..a5362cba 100644
--- a/content/normal-modal-logic/axioms-systems/systems-distinct.tex
+++ b/content/normal-modal-logic/axioms-systems/systems-distinct.tex
@@ -92,7 +92,7 @@
         $\mSat/{{}}{\Box\Diamond\lnot p}$}, right=of w1] {$w_2$} ;
     \draw[reflexive above] (w2) to (w2);
     \node[world] (w3) [label={right:\mFalse{p}},right=of w2] {$w_3$};
-    \draw[reflexive above] (w2) to (w2);
+    \draw[reflexive above] (w3) to (w3);
     \draw[->, bend left] (w1) to (w2);  
     \draw[->, bend left] (w2) to (w3);  
     \draw[->, bend left] (w3) to (w2);  
diff --git a/content/normal-modal-logic/tableaux/countermodels.tex b/content/normal-modal-logic/tableaux/countermodels.tex
index 19d23d38..cd9e721c 100644
--- a/content/normal-modal-logic/tableaux/countermodels.tex
+++ b/content/normal-modal-logic/tableaux/countermodels.tex
@@ -111,7 +111,7 @@
     [\pFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}{1},
       just = \TAss, checked
       [\pFmla{\True}{\Box(p \lor q)}{1},
-        just = {\TRule{\False}{\lif}[1]}, 
+        just = {\TRule{\False}{\lif}[1]}, checked
         [\pFmla{\False}{\Box p \lor \Box q}{1},
           just = {\TRule{\False}{\lif}[1]}, checked
           [\pFmla{\False}{\Box p}{1},