# HG changeset patch
# User Chengsong
# Date 1688776568 -3600
# Node ID d8f82c690b32294a1d6e332f1c6d07cfb6579f5f
# Parent  2ad20ba5b1787ff9667ec29afc38118cc992964d
updated 4.2 diagram

diff -r 2ad20ba5b178 -r d8f82c690b32 ChengsongTanPhdThesis/Chapters/Bitcoded2.tex
--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Fri Jul 07 20:03:05 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Sat Jul 08 01:36:08 2023 +0100
@@ -8,12 +8,8 @@
 %simplifications and therefore introduce our version of the bitcoded algorithm and 
 %its correctness proof in 
 %Chapter 3\ref{Chapter3}. 
-{\color{red} \rule{\linewidth}{0.5mm}}
-New content starts.
-{\color{red} \rule{\linewidth}{0.5mm}}
-\marginpar{\em Added a completely new overview section, highlighting the contributions.}
-
 \section{Overview}
+\marginpar{\em Added a completely new \\overview section, \\highlighting contributions.}
 
 This chapter
 is the point from which novel contributions of this PhD project are introduced
@@ -27,7 +23,7 @@
 %are about to describe.
 The fundamental reason is we cannot extend the correctness proof of theorem 4
 because lemma 13 does not hold anymore when simplifications are involved.
-\marginpar{\em rephrased things so they make better sense.}
+\marginpar{\em rephrased things \\so why new \\proof makes sense.}
 %The proof details are necessary materials for this thesis
 %because it provides necessary context to explain why we need a
 %new framework for the proof of $\blexersimp$, which involves
@@ -155,24 +151,40 @@
     }
 }
 
-\begin{figure}[H]
+\begin{center}
 	\begin{tikzpicture}[->, >=stealth', shorten >= 1pt, auto, thick]
-		\node [rectangle, draw] (1)  at (-7, 2) {$\ldots$};
-		\node [rectangle, draw] (2) at  (-4, 2) {$_{bs'}(_Za+_Saa)^*$};
-		\node [rectangle, draw] (3) at  (4, 2) {$_{bs'}(_Z(_Z\ONE + _S(\ONE \cdot a)))\cdot(_0a+_1aa)^*$};
-		\node [rectangle, draw] (4) at  (7, 2) {$\ldots$};
-		\node [rectangle, draw] (5) at  (-7, -2) {$\ldots$};
-		\node [rectangle, draw] (6) at  (-4, -2) {$\Stars \; [\Left (a)]$};
-		\node [rectangle, draw] (7) at  ( 4, -2) {$\Seq (\Alt (\Left \; \Empty)) \; \Stars \, []$};
-		\node [rectangle, draw] (8) at  ( 7, -2) {$\ldots$};
-		\node [rectangle, draw] (9) at  (-7, -6) {$\ldots$};
-		\node [rectangle, draw] (10) at (-4, -6) {$\textit{bits} = \retrieve \; r_i\;v_i$};
-		\node [rectangle, draw] (11) at (4, -6) {$\textit{bits} = \retrieve \; r_{i+1}\;v_{i+1}$};
-		\node [rectangle, draw] (12) at  (7, -6) {$\ldots$};
+		\node [rectangle ] (1)  at (-7, 2) {$\ldots$};
+		\node [rectangle, draw] (2) at  (-4, 2) {$r_i = _{bs'}(_Za+_Saa)^*$};
+		\node [rectangle, draw] (3) at  (4, 2) {$r_{i+1} = _{bs'}(_Z(_Z\ONE + _S(\ONE \cdot a)))\cdot(_0a+_1aa)^*$};
+		\node [rectangle] (4) at  (9, 2) {$\ldots$};
+		\node [rectangle] (5) at  (-7, -2) {$\ldots$};
+		\node [rectangle, draw] (6) at  (-4, -2) {$v_i = \Stars \; [\Left (a)]$};
+		\node [rectangle, draw] (7) at  ( 4, -2) {$v_{i+1} = \Seq (\Alt (\Left \; \Empty)) \; \Stars \, []$};
+		\node [rectangle] (8) at  ( 9, -2) {$\ldots$};
+		\node [rectangle] (9) at  (-7, -6) {$\ldots$};
+		\node [rectangle, draw] (10) at (-4, -6) {$\textit{bits}_{i} = \retrieve \; r_i\;v_i$};
+		\node [rectangle, draw] (11) at (4, -6) {$\textit{bits}_{i+1} = \retrieve \; r_{i+1}\;v_{i+1}$};
+		\node [rectangle] (12) at  (9, -6) {$\ldots$};
 
 
 		\path (1) edge [] node {} (2);
+		\path (5) edge [] node {} (6);
+		\path (9) edge [] node {} (10);
+
+		\path (11) edge [] node {} (12);
+		\path (7) edge [] node {} (8);
+		\path (3) edge [] node {} (4);
+
+	
 		\path (2) edge [] node {$\backslash a$} (3);
+		\path (2) edge [dashed, <->] node {$\vdash v_i : r_i$} (6);
+		\path (3) edge [dashed, <->] node {$\vdash v_{i+1} : r_{i+1}$} (7);
+		%\path (6) edge [] node {$\vdash v_i : r_i$} (10);
+		%\path (7) edge [dashed, <->] node {$\vdash v_i : r_i$} (11);
+
+		\path (10) edge [dashed, <->] node {$=$} (11);
+
+		\path (7) edge [] node {$\inj \; r_{i+1} \; a \; v_i$} (6);
 
 %		\node [rectangle, draw] (r) at (-6, -1) {$(aa)^*(b+c)$};
 %		\node [rectangle, draw] (a) at (-6, 4)	  {$(aa)^*(_{Z}b + _{S}c)$};
@@ -200,8 +212,8 @@
 
 
 	\end{tikzpicture}
-	\caption{$\blexer$ with the regular expression $(aa)^*(b+c)$ and $aab$}
-\end{figure}
+	%\caption{$\blexer$ with the regular expression $(aa)^*(b+c)$ and $aab$}
+\end{center}
 
 When simplifications are added, the inhabitation relation no longer holds,
 causing the above diagram to break.