equal
deleted
inserted
replaced
231 apply (fast intro: BufAC_Cmt_d_req BufAC_Asm_prefix2) |
231 apply (fast intro: BufAC_Cmt_d_req BufAC_Asm_prefix2) |
232 done |
232 done |
233 |
233 |
234 (**** new approach for admissibility, reduces itself to absurdity *************) |
234 (**** new approach for admissibility, reduces itself to absurdity *************) |
235 |
235 |
236 lemma adm_BufAC_Asm: "adm (\<lambda>x. x\<in>BufAC_Asm)" |
236 lemma adm_BufAC_Asm': "adm (\<lambda>x. x\<in>BufAC_Asm)" |
237 apply (rule def_gfp_admI) |
237 apply (rule def_gfp_admI) |
238 apply (rule BufAC_Asm_def [THEN eq_reflection]) |
238 apply (rule BufAC_Asm_def [THEN eq_reflection]) |
239 apply (safe) |
239 apply (safe) |
240 apply (unfold BufAC_Asm_F_def) |
240 apply (unfold BufAC_Asm_F_def) |
241 apply (safe) |
241 apply (safe) |