4012   apply(subgoal_tac "good (bders_simp a (aa # list)) \<or> (bders_simp a (aa # list) = AZERO)")

  4012   apply(subgoal_tac "good (bders_simp a (aa # list)) \<or> (bders_simp a (aa # list) = AZERO)")

  4013   apply(auto)

  4013   apply(auto)

  4014       apply(subst (asm) bder_simp_contains_IFF)

  4014       apply(subst (asm) bder_simp_contains_IFF)

  4015        apply(simp)

  4015        apply(simp)

  4016   

  4016   

  4019 lemma

  4018 lemma

  4020   assumes "s \<in> L (erase r)"

  4019   assumes "s \<in> L (erase r)"

  4021   shows "bders_simp r s >> bs \<longleftrightarrow> bders r s >> bs"

  4020   shows "bders_simp r s >> bs \<longleftrightarrow> bders r s >> bs"

  4022   using assms

  4021   using assms

  4023   apply(induct s arbitrary: r bs)

  4022   apply(induct s arbitrary: r bs)