equal
deleted
inserted
replaced
206 apply(subgoal_tac " (sum_list |
206 apply(subgoal_tac " (sum_list |
207 (map rsize ( rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set))))) |
207 (map rsize ( rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set))))) |
208 \<le> (sum_list |
208 \<le> (sum_list |
209 (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))") |
209 (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))") |
210 apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15)) |
210 apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15)) |
211 apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le) |
211 apply (metis (no_types, opaque_lifting) le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le) |
212 apply fastforce |
212 apply fastforce |
213 apply fastforce |
213 apply fastforce |
214 apply (metis Un_iff insert_absorb) |
214 apply (metis Un_iff insert_absorb) |
215 apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1)) |
215 apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1)) |
216 apply (meson UnCI rdistinct.simps(2)) |
216 apply (meson UnCI rdistinct.simps(2)) |