--- a/thys2/ClosedForms.thy	Mon Mar 28 00:59:42 2022 +0100
+++ b/thys2/ClosedForms.thy	Mon Mar 28 20:00:04 2022 +0100
@@ -527,20 +527,23 @@
 lemma frewrite_append:
   shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb"
   apply(induct rs)
-  apply simp+
-  oops
+   apply simp+
+  using frewrite.intros(3) by blast
+  
 
 
 lemma frewrites_cons:
   shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb"
+  apply(induct rsa rsb rule: frewrites.induct)
+   apply simp
+  using frewrite.intros(3) by blast
 
-  oops
 
 lemma frewrites_append:
   shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)"
-  apply(induct rsa rsb rule: frewrites.induct)
+  apply(induct rs)
    apply simp
-  oops
+  by (simp add: frewrites_cons)
 
 
 
@@ -553,9 +556,9 @@
   using frewrite.intros(1) apply blast
     apply(subgoal_tac "(rs @ rsa) \<leadsto>f* (rs @ rsb)")
   using many_steps_later apply blast
-
-
-
+  apply (simp add: frewrites_append)
+  apply (metis append.assoc append_Cons frewrite.intros(2) frewrites_append many_steps_later)
+  using frewrites_cons by auto
 
 
 
@@ -573,8 +576,12 @@
        apply simp+
   using frewrite.intros(1) many_steps_later apply blast
      apply(case_tac "x = x3")
-     apply simp
+      apply simp
   
+  using frewrites_cons apply presburger
+  using frewrite.intros(1) many_steps_later apply fastforce
+  apply(case_tac "rnullable x41")
+  apply simp