3787 

  3787 lemma COUNTEREXAMPLE:

  3788 

  3788   assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"

  3789   shows "bsimp (bder c (bsimp r)) = bsimp (bder c r)"

  3790   apply(simp_all add: assms)

  3791   oops

  3792 

  3793 lemma COUNTEREXAMPLE:

  3794   assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"

  3795   shows "bsimp r = r"

  3796   apply(simp_all add: assms)

  3797   oops

  3798 

  3799 lemma COUNTEREXAMPLE:

  3800   assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"

  3801   shows "bsimp r = XXX"

  3802   and   "bder c r = XXX"

  3803   and   "bsimp (bder c (bsimp r)) = XXX"

  3804   and   "bsimp (bder c r) = XXX"

  3805   apply(simp_all add: assms)

  3806   oops

  3807 

  3808 lemma COUNTEREXAMPLE_contains1:

  3809   assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"

  3810   and   "bsimp (bder c r) >> bs"

  3811   shows "bsimp (bder c (bsimp r)) >> bs"

  3812   using assms 

  3813   apply(auto elim!: contains.cases)

  3814    apply(rule Etrans)

  3815     apply(rule contains.intros)

  3816     apply(rule contains.intros)

  3817    apply(simp)

  3818   apply(rule Etrans)

  3819     apply(rule contains.intros)

  3820     apply(rule contains.intros)

  3821   apply(simp)

  3822   done

  3823 

  3824 lemma COUNTEREXAMPLE_contains2:

  3825   assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"

  3826   and   "bsimp (bder c (bsimp r)) >> bs"

  3827   shows "bsimp (bder c r) >> bs" 

  3828   using assms 

  3829   apply(auto elim!: contains.cases)

  3830    apply(rule Etrans)

  3831     apply(rule contains.intros)

  3832     apply(rule contains.intros)

  3833    apply(simp)

  3834   apply(rule Etrans)

  3835     apply(rule contains.intros)

  3836     apply(rule contains.intros)

  3837   apply(simp)

  3838   done