--- a/thys2/ClosedForms.thy	Thu Mar 24 21:11:12 2022 +0000
+++ b/thys2/ClosedForms.thy	Fri Mar 25 21:49:53 2022 +0000
@@ -469,29 +469,48 @@
    apply simp
   using rsimpalts_conscons by presburger
 
+lemma no0_flts:
+  shows "RZERO \<notin> set (rflts rs)"
+  apply (induct rs)
+   apply simp
+  apply(case_tac a)
+       apply simp+
+  oops
 
 
 
 lemma distinct_flts_no0:
-  shows "rdistinct (rflts rs) (insert RZERO rset) = rdistinct (rflts rs) rset"
-  apply(induct rs)
+  shows "  rflts (map rsimp (rdistinct rs (insert RZERO rset)))  =
+           rflts (map rsimp (rdistinct rs rset))  "
+  
+  apply(induct rs arbitrary: rset)
    apply simp
   apply(case_tac a)
-  using rflts.simps(2) apply presburger
-  sorry
+  apply simp+
+    apply (smt (verit, ccfv_SIG) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+  prefer 2
+  apply simp  
+  by (smt (verit, ccfv_threshold) Un_insert_right insert_iff list.simps(9) rdistinct.simps(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot rrexp.distinct(7))
+
 
 
 lemma simp_der_flts:
   shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= 
          rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))"
 
-  apply(induct rs arbitrary: rset)
+  apply(induct rs)
    apply simp
   apply(case_tac a)
        apply simp
       apply(case_tac "RZERO \<in> rset")
-       apply simp
-      apply simp
+       apply simp+
+  using distinct_flts_no0 apply presburger
+     apply (case_tac "x = x3")
+  prefer 2
+  apply simp
+  using distinct_flts_no0 apply presburger
+  apply(case_tac "RONE \<in> rset")
+     apply simp+
   
   sorry