--- a/thys2/BasicIdentities.thy	Mon Apr 04 23:56:40 2022 +0100
+++ b/thys2/BasicIdentities.thy	Thu Apr 07 21:31:29 2022 +0100
@@ -363,9 +363,7 @@
    apply(simp_all)
   done
 
-lemma inside_simp_removal:
-  shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
-  sorry
+
 
 lemma set_related_list:
   shows "distinct rs  \<Longrightarrow> length rs = card (set rs)"
@@ -378,15 +376,6 @@
 
 
 
-lemma rders_simp_same_simpders:
-  shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
-  apply(induct s rule: rev_induct)
-   apply simp
-  apply(case_tac "xs = []")
-   apply simp
-  apply(simp add: rders_append rders_simp_append)
-  using inside_simp_removal by blast
-
 
 
 
@@ -432,6 +421,11 @@
   shows "rnullable (rders r s) = rnullable (rders_simp r s)"
   sorry
 
+lemma der_simp_nullability:
+  shows "rnullable r = rnullable (rsimp r)"
+  sorry
+
+
 lemma  first_elem_seqder:
   shows "\<not>rnullable r1p \<Longrightarrow> map rsimp (rder x (RSEQ r1p r2)
                    # rs) = map rsimp ((RSEQ (rder x r1p) r2) # rs) "