diff -r 812e5d112f49 -r 671a83abccf3 thys3/BlexerSimp.thy
--- a/thys3/BlexerSimp.thy	Fri Jul 01 13:02:15 2022 +0100
+++ b/thys3/BlexerSimp.thy	Mon Jul 04 12:27:13 2022 +0100
@@ -94,11 +94,17 @@
   "notZero AZERO = True"
 | "notZero _ = False"
 
+fun tset :: "arexp list \<Rightarrow> rexp set" where
+  "tset rs = set (concat (map turnIntoTerms (map erase rs)))"
+
+
 fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where
   "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else 
                         (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2
                                  | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0)))  )"
 
+abbreviation
+  "p acc r \<equiv> prune6 (set (concat (map turnIntoTerms (map erase acc)) ) ) r Nil"
 
 
 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where
@@ -275,13 +281,17 @@
   using ss6 apply presburger
   by simp
 
+
+
 lemma ss6_realistic:
-  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (concat (map turnIntoTerms (map erase rs1)))))"
+  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (tset rs1))"
   apply(induct rs2 arbitrary: rs1)
    apply simp
-  apply(rename_tac cc cc')
- 
- 
+  apply(rename_tac cc' cc)
+  apply(subgoal_tac "(cc @ a # cc') s\<leadsto>* (cc @ a # dB6 cc' (tset (cc @ [a])))")
+   prefer 2
+  apply (metis append.assoc append.left_neutral append_Cons)
+  apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p cc a) # dB6 cc' (tset (cc @ [a])))") 
   sorry