equal
deleted
inserted
replaced
278 lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)" |
278 lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)" |
279 (*by (lifting card_raw_suc)*) |
279 (*by (lifting card_raw_suc)*) |
280 sorry |
280 sorry |
281 |
281 |
282 thm card_raw_cons_gt_0 |
282 thm card_raw_cons_gt_0 |
283 thm mem_card_raw_not_0 |
283 (*thm mem_card_raw_not_0*) |
284 thm not_nil_equiv_cons |
284 thm not_nil_equiv_cons |
285 thm delete_raw.simps |
285 thm delete_raw.simps |
286 (*thm mem_delete_raw*) |
286 (*thm mem_delete_raw*) |
287 thm card_raw_delete_raw |
287 thm card_raw_delete_raw |
288 thm cons_delete_raw |
288 thm cons_delete_raw |