equal
deleted
inserted
replaced
750 by auto |
750 by auto |
751 qed |
751 qed |
752 |
752 |
753 |
753 |
754 lemma rders_simp_bounded: |
754 lemma rders_simp_bounded: |
|
755 fixes "r" |
755 shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N" |
756 shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N" |
756 apply(induct r) |
757 apply(induct r) |
757 apply(rule_tac x = "Suc 0 " in exI) |
758 apply(rule_tac x = "Suc 0 " in exI) |
758 using three_easy_cases0 apply force |
759 using three_easy_cases0 apply force |
759 using three_easy_cases1 apply blast |
760 using three_easy_cases1 apply blast |
765 apply(assumption) |
766 apply(assumption) |
766 apply(assumption) |
767 apply(assumption) |
767 apply (metis alts_closed_form_bounded size_list_estimation') |
768 apply (metis alts_closed_form_bounded size_list_estimation') |
768 using star_closed_form_bounded by blast |
769 using star_closed_form_bounded by blast |
769 |
770 |
770 |
771 corollary rders_simp_finiteness: |
771 |
772 shows "\<forall>r. \<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N" |
772 unused_thms |
773 using rders_simp_bounded by auto |
|
774 |
|
775 |
773 |
776 |
774 |
777 |
775 end |
778 end |