--- a/thys2/ClosedForms.thy	Wed Mar 09 17:33:08 2022 +0000
+++ b/thys2/ClosedForms.thy	Thu Mar 10 11:18:41 2022 +0000
@@ -35,7 +35,7 @@
 lemma seq_closed_form: shows 
 "rsimp (rders_simp (RSEQ r1 r2) s) = 
 rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # 
-                (map (rders r2) (vsuf s r1)) 
+                (map (rders_simp r2) (vsuf s r1)) 
               )  
       )"
   apply(induct s)
@@ -46,6 +46,17 @@
 lemma seq_closed_form_variant: shows
 "s \<noteq> [] \<Longrightarrow> (rders_simp (RSEQ r1 r2) s) = 
 rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))"
-  sorry
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(subst rders_simp_append)
+  apply(subst rders_simp_one_char)
+  apply(subst rsimp_idem[symmetric])
+  apply(subst rders_simp_one_char[symmetric])
+  apply(subst rders_simp_append[symmetric])
+  apply(insert seq_closed_form)
+  apply(subgoal_tac "rsimp (rders_simp (RSEQ r1 r2) (xs @ [x]))
+ = rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1)))")
+   apply force
+  by presburger
 
 end
\ No newline at end of file