--- a/thys2/ClosedFormsBounds.thy Sat Mar 12 14:33:54 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy Tue Mar 15 16:37:41 2022 +0000
@@ -1,14 +1,11 @@
-
+(**)
theory ClosedFormsBounds
imports "GeneralRegexBound" "ClosedForms"
begin
-
lemma alts_ders_lambda_shape_ders:
shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s"
by (simp add: image_iff)
-
-
lemma rlist_bound:
shows "\<forall>r \<in> set rs. rsize r \<le> N \<Longrightarrow> sum_list (map rsize rs) \<le> N * (length rs)"
apply(induct rs)
@@ -46,20 +43,391 @@
shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))"
using rsimp_aalts_smaller by auto
+lemma no_elem_distinct :
+ shows "a \<notin> set rs \<Longrightarrow> rdistinct rs rset = rdistinct rs (insert a rset)"
+ apply(induct rs arbitrary: rset)
+ apply simp
+ by force
+
+
+
+
+inductive good :: "rrexp \<Rightarrow> bool"
+ where
+"RZERO \<notin> set rs \<Longrightarrow> good (RALTS rs)"
+|"good RZERO"
+|"good RONE"
+|"good (RCHAR c)"
+|"good (RSEQ r1 r2)"
+|"good (RSTAR r0)"
+
+
+lemma after_flts_no0:
+ shows "\<forall>r \<in> set rs. good r \<Longrightarrow> RZERO \<notin> set (rflts rs)"
+ apply(induct rs)
+ apply simp
+ apply(case_tac a)
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ using good.simps apply blast
+ apply simp
+ done
+
lemma flts_has_no_zero:
- shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)"
+ shows "\<forall>r \<in> set rs. good r \<Longrightarrow> rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)"
+ apply(subgoal_tac "RZERO \<notin> set (rflts rs)")
+ apply (meson no_elem_distinct)
+ apply(insert after_flts_no0)
+ by blast
+
+lemma shape_of_alts:
+ shows "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs) \<Longrightarrow> RZERO \<notin> alts_set \<and> RONE \<notin> alts_set"
+ by fastforce
+
+lemma quantified2_implies1:
+ shows "\<forall>r. P \<and> Q \<Longrightarrow> \<forall>r. P"
+ by auto
+
+lemma quantified_quantifiedAB_A:
+ shows " (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) \<Longrightarrow> \<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs"
+ by fastforce
+
+
+
+
+lemma list_distinct_removal:
+ shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rs1) rset = rdistinct rs1 rset"
+ apply(induct rs arbitrary: rset)
+ apply simp
+ by simp
+
+
+lemma rdistinct_mono_list:
+ shows " sum_list (map rsize (rdistinct (x5 @ rs) rset )) \<le>
+ ( sum_list (map rsize x5)) + (sum_list (map rsize (rdistinct rs ((set x5 ) \<union> rset))))"
+ apply(induct x5 arbitrary: rs rset)
+ apply simp
+ apply(case_tac "a \<in> rset")
+ apply simp
+ apply (simp add: add.assoc insert_absorb trans_le_add2)
+ apply simp
+ by (metis Un_insert_right)
+
+
+lemma flts_size_reduction_alts:
+ shows " \<And>a rs noalts_set alts_set corr_set x5.
+ \<lbrakk>\<And>noalts_set alts_set corr_set.
+ (\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs) \<and>
+ (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) \<Longrightarrow>
+ Suc (sum_list (map rsize (rdistinct (rflts rs) (noalts_set \<union> corr_set))))
+ \<le> Suc (sum_list (map rsize (rdistinct rs (insert RZERO (noalts_set \<union> alts_set)))));
+ (\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs) \<and>
+ (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set);
+ a = RALTS x5\<rbrakk>
+ \<Longrightarrow> Suc (sum_list (map rsize (rdistinct (rflts (a # rs)) (noalts_set \<union> corr_set))))
+ \<le> Suc (sum_list
+ (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))))"
+ apply(case_tac "a \<in> alts_set")
+ apply simp
+ apply(subgoal_tac "set x5 \<subseteq> corr_set")
+ apply(subst list_distinct_removal)
+ apply auto[1]
+ apply presburger
+ apply fastforce
+ apply (subgoal_tac "a \<notin> noalts_set")
+ prefer 2
+ apply blast
+ apply simp
+ apply(subgoal_tac "sum_list (map rsize (rdistinct (x5 @ rflts rs) (noalts_set \<union> corr_set)))
+ \<le> sum_list (map rsize x5 ) + sum_list (map rsize (rdistinct (rflts rs) ((set x5) \<union> (noalts_set \<union> corr_set))))")
+ prefer 2
+ using rdistinct_mono_list apply presburger
+ apply(subgoal_tac "insert (RALTS x5) (noalts_set \<union> alts_set) = noalts_set \<union> (insert (RALTS x5) alts_set)")
+ apply(simp only:)
+ apply(subgoal_tac "sum_list (map rsize x5) +
+sum_list (map rsize (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> (set x5))))) \<le>
+Suc (sum_list (map rsize x5) +
+ sum_list
+ (map rsize
+ (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set)))))")
+
+ apply (simp add: Un_left_commute inf_sup_aci(5))
+ apply(subgoal_tac "sum_list (map rsize (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> set x5))))
+\<le> sum_list
+ (map rsize
+ (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set))))")
+ apply linarith
+ apply(subgoal_tac "\<forall>r \<in> insert (RALTS x5) alts_set. \<exists>xs1.( r = RALTS xs1 \<and> set xs1 \<subseteq> corr_set \<union> set x5)")
+ apply presburger
+ apply (meson insert_iff sup.cobounded2 sup.coboundedI1)
+ by blast
+
+
+
- sorry
+lemma flts_vs_nflts1:
+ shows "(\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs)
+ \<and> (\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set))
+\<Longrightarrow> (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set) )))
+ \<le> (sum_list (map rsize (rdistinct rs (insert RZERO (noalts_set \<union> alts_set) ))))"
+ apply(induct rs arbitrary: noalts_set alts_set corr_set)
+ apply simp
+ apply(case_tac a)
+ apply(case_tac "RZERO \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "RZERO \<notin> alts_set")
+ apply simp
+ apply fastforce
+ apply(case_tac "RONE \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "RONE \<notin> alts_set")
+ prefer 2
+ apply fastforce
+ apply(case_tac "RONE \<in> corr_set")
+ apply(subgoal_tac "rflts (a # rs) = RONE # rflts rs")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (RONE # rflts rs) (noalts_set \<union> corr_set) =
+ rdistinct (rflts rs) (noalts_set \<union> corr_set)")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (RONE # rs) (insert RZERO (noalts_set \<union> alts_set)) =
+ RONE # (rdistinct rs (insert RONE (insert RZERO (noalts_set \<union> alts_set)))) ")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (rflts rs) (noalts_set \<union> corr_set) =
+ rdistinct (rflts rs) (insert RONE (noalts_set \<union> corr_set))")
+ apply (simp only:)
+ apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) =
+ insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
+ apply(simp only:)
+ apply(subgoal_tac " (sum_list
+ (map rsize ( rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))
+ \<le> (sum_list
+ (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))")
+ apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
+ apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
+ apply fastforce
+ apply fastforce
+ apply (metis Un_iff insert_absorb)
+ apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1))
+ apply (meson UnCI rdistinct.simps(2))
+ using rflts.simps(4) apply presburger
+ apply simp
+ apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply (metis Un_insert_left insertE rrexp.distinct(15))
+ apply fastforce
+ apply(case_tac "a \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "a \<notin> alts_set")
+ prefer 2
+ apply blast
+ apply(case_tac "a \<in> corr_set")
+ apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)")
+ prefer 2
+ apply fastforce
+ apply(simp only:)
+ apply(subgoal_tac " sum_list
+ (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))
+\<le>
+ sum_list
+ (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set))))")
+
+ apply(subgoal_tac
+"sum_list (map rsize (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)))
+\<le>
+ sum_list (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))")
+ apply fastforce
+ apply simp
+ apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+ apply(simp only:)
+ apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply (metis insertE rrexp.distinct(21))
+ apply blast
+
+ apply fastforce
+ apply force
+ apply simp
+ apply (metis Un_insert_left insert_iff rrexp.distinct(21))
+ apply(case_tac "a \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "a \<notin> alts_set")
+ prefer 2
+ apply blast
+ apply(case_tac "a \<in> corr_set")
+ apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)")
+ prefer 2
+ apply fastforce
+ apply(simp only:)
+ apply(subgoal_tac " sum_list
+ (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))
+\<le>
+ sum_list
+ (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set))))")
+
+ apply(subgoal_tac
+"sum_list (map rsize (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)))
+\<le>
+ sum_list (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))")
+ apply fastforce
+ apply simp
+ apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+ apply(simp only:)
+ apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+ apply(simp only:)
+
+
+ apply (metis insertE rrexp.distinct(25))
+ apply blast
+ apply fastforce
+ apply force
+ apply simp
+
+ apply (metis Un_insert_left insertE rrexp.distinct(25))
+
+ using Suc_le_mono flts_size_reduction_alts apply presburger
+ apply(case_tac "a \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "a \<notin> alts_set")
+ prefer 2
+ apply blast
+ apply(case_tac "a \<in> corr_set")
+ apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)")
+ prefer 2
+ apply fastforce
+ apply(simp only:)
+ apply(subgoal_tac " sum_list
+ (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))
+\<le>
+ sum_list
+ (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set))))")
+
+ apply(subgoal_tac
+"sum_list (map rsize (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)))
+\<le>
+ sum_list (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))")
+ apply fastforce
+ apply simp
+ apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+ apply(simp only:)
+ apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply (metis insertE rrexp.distinct(29))
+
+ apply blast
+
+ apply fastforce
+ apply force
+ apply simp
+ apply (metis Un_insert_left insert_iff rrexp.distinct(29))
+ done
+
+
+
+
lemma flts_vs_nflts:
- shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs
- \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)
+ shows "(\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs)
+ \<and> (\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set))
\<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set) )))
- \<le> Suc (sum_list (map rsize (rdistinct rs (noalts_set \<union> alts_set) )))"
- apply(induct rs arbitrary: noalts_set)
+ \<le> Suc (sum_list (map rsize (rdistinct rs (insert RZERO (noalts_set \<union> alts_set) ))))"
+ apply(induct rs arbitrary: noalts_set alts_set corr_set)
apply simp
+ apply(case_tac a)
+ apply(case_tac "RZERO \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "RZERO \<notin> alts_set")
+ apply simp
+ apply fastforce
+ apply(case_tac "RONE \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "RONE \<notin> alts_set")
+ prefer 2
+ apply fastforce
+ apply(case_tac "RONE \<in> corr_set")
+ apply(subgoal_tac "rflts (a # rs) = RONE # rflts rs")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (RONE # rflts rs) (noalts_set \<union> corr_set) =
+ rdistinct (rflts rs) (noalts_set \<union> corr_set)")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (RONE # rs) (insert RZERO (noalts_set \<union> alts_set)) =
+ RONE # (rdistinct rs (insert RONE (insert RZERO (noalts_set \<union> alts_set)))) ")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (rflts rs) (noalts_set \<union> corr_set) =
+ rdistinct (rflts rs) (insert RONE (noalts_set \<union> corr_set))")
+ apply (simp only:)
+ apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) =
+ insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
+ apply(simp only:)
+ apply(subgoal_tac " Suc (sum_list
+ (map rsize ( rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))
+ \<le> Suc (sum_list
+ (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))")
+ apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
+ apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
+ apply fastforce
+ apply fastforce
+ apply (metis Un_iff insert_absorb)
+ apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1))
+ apply (meson UnCI rdistinct.simps(2))
+ using rflts.simps(4) apply presburger
+ apply simp
+ apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+ apply(simp only:)
+ apply (metis Un_insert_left insertE rrexp.distinct(15))
+ apply fastforce
+ apply(case_tac "a \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "a \<notin> alts_set")
+ prefer 2
+ apply blast
+ apply(case_tac "a \<in> corr_set")
+ apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)")
+ prefer 2
+ apply fastforce
+ apply(simp only:)
+ apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+ apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+ apply(case_tac "a \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "a \<notin> alts_set")
+ prefer 2
+ apply blast
+ apply(case_tac "a \<in> corr_set")
+ apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)")
+ prefer 2
+ apply fastforce
+ apply(simp only:)
+ apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+ apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+ prefer 2
+ apply(case_tac "a \<in> noalts_set")
+ apply simp
+ apply(subgoal_tac "a \<notin> alts_set")
+ prefer 2
+ apply blast
+ apply(case_tac "a \<in> corr_set")
+ apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)")
+ prefer 2
+ apply fastforce
+ apply(simp only:)
+ apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+ apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+ using flts_size_reduction_alts apply presburger
+ done
- sorry
+
+
+
+
+(* apply(rutac x = "\<lambda>a rs noalts_set alts_set corr_set. set xs ")*)
+
lemma distinct_simp_ineq_general:
shows "rsimp ` no_simp = has_simp \<and> finite no_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
@@ -73,10 +441,14 @@
apply(case_tac "rsimp a \<in> no_simp")
apply(subgoal_tac "rsimp a \<in> has_simp")
prefer 2
- apply (simp add: rev_image_eqI rsimp_idem)
- sledgehammer[timeout = 100]
-
- sorry
+ apply (simp add: rev_image_eqI rsimp_idem)
+ apply simp
+ apply (metis finite_insert image_insert insert_absorb trans_le_add2)
+ apply(case_tac "rsimp a \<notin> has_simp")
+ apply simp
+ apply (metis add_mono_thms_linordered_semiring(1) finite.insertI image_insert rsimp_mono)
+ apply simp
+ by (metis finite.insertI image_insert insert_absorb trans_le_add2)
lemma not_mentioned_elem_distinct_strong:
@@ -92,13 +464,40 @@
-
+lemma larger_acc_smaller_distinct_res0:
+ shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))"
+ apply(induct rs arbitrary: ss SS)
+ apply simp
+ apply(case_tac "a \<in> ss")
+ apply(subgoal_tac "a \<in> SS")
+ apply simp
+ apply blast
+ apply(case_tac "a \<in> SS")
+ apply simp
+ apply(subgoal_tac "insert a ss \<subseteq> SS")
+ apply simp
+ apply (simp add: trans_le_add2)
+ apply blast
+ apply(simp)
+ apply(subgoal_tac "insert a ss \<subseteq> insert a SS")
+ apply blast
+ by blast
lemma without_flts_ineq:
shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le>
Suc (sum_list (map rsize (rdistinct ( rs ) {} )))"
- by (metis empty_iff flts_vs_nflts sup_bot_left)
+proof -
+ have " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le>
+ Suc (sum_list (map rsize (rdistinct rs (insert RZERO {}))))"
+ by (metis empty_iff flts_vs_nflts sup_bot_left)
+ also have "... \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
+ by (simp add: larger_acc_smaller_distinct_res0)
+ finally show ?thesis sledgehammer
+ by blast
+qed
+
+
@@ -131,24 +530,7 @@
shows "a \<notin> ss \<Longrightarrow> rdistinct (a # rs) ss = a # rdistinct rs (insert a ss) "
by auto
-lemma larger_acc_smaller_distinct_res0:
- shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))"
- apply(induct rs arbitrary: ss SS)
- apply simp
- apply(case_tac "a \<in> ss")
- apply(subgoal_tac "a \<in> SS")
- apply simp
- apply blast
- apply(case_tac "a \<in> SS")
- apply simp
- apply(subgoal_tac "insert a ss \<subseteq> SS")
- apply simp
- apply (simp add: trans_le_add2)
- apply blast
- apply(simp)
- apply(subgoal_tac "insert a ss \<subseteq> insert a SS")
- apply blast
- by blast
+
lemma larger_acc_smaller_distinct_res:
@@ -393,7 +775,7 @@
-
+unused_thms