diff -r f83271c585d2 -r 664322da08fe thys2/Journal/Paper.thy
--- a/thys2/Journal/Paper.thy	Thu Nov 04 13:31:17 2021 +0000
+++ b/thys2/Journal/Paper.thy	Thu Nov 04 13:52:17 2021 +0000
@@ -166,17 +166,31 @@
 
 %TODO: add figure for this?
 
+
+Therefore, we insert a simplification phase
+after each derivation step, as defined below:
 \begin{lemma}
 @{thm blexer_simp_def}
 \end{lemma}
 
+The simplification function is given as follows:
 
 \begin{center}
   \begin{tabular}{lcl}
   @{thm (lhs) bsimp.simps(1)[of  "bs" "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of  "bs" "r\<^sub>1" "r\<^sub>2"]}\\
   @{thm (lhs) bsimp.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\
   @{thm (lhs) bsimp.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\
-  @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
+
+\end{tabular}
+\end{center}
+
+And the two helper functions are:
+\begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) bsimp_AALTs.simps(2)[of  "bs\<^sub>1" "r" ]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of  "bs\<^sub>1" "r" ]}\\
+  @{thm (lhs) bsimp_AALTs.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\
+  @{thm (lhs) bsimp_AALTs.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\
+
 \end{tabular}
 \end{center}
 
@@ -203,11 +217,10 @@
   @{thm[mode=Rule] rrewrite.intros(6)[of "r" "r'" "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\
   @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "rs\<^sub>a" "rs\<^sub>b"]}\\
   @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "rs\<^sub>a" "bs\<^sub>1" "rs\<^sub>1" "rs\<^sub>b"]}\\
-  @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "r\<^sub>2"]}\\
-  @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" "r\<^sub>1"]}\\
-  @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" ]}\\
-  @{thm[mode=Axiom] rrewrite.intros(12)[of "bs" "r\<^sub>1"]}\\
-  @{thm[mode=Rule] rrewrite.intros(13)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\
+  @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\
+  @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\
+  @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" "r\<^sub>1"]}\\
+  @{thm[mode=Rule] rrewrite.intros(12)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\
 
   \end{tabular}
 \end{center}
@@ -252,8 +265,10 @@
 @{thm blexersimp_correctness}
 \end{lemma}
 
+The nice thing about the aove
+\<close>
 
-\<close>
+
 
 section \<open>Introduction\<close>