equal
deleted
inserted
replaced
173 by auto |
173 by auto |
174 |
174 |
175 lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union> |
175 lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union> |
176 (d22set (p - 1))"; |
176 (d22set (p - 1))"; |
177 apply (induct p rule: d22set.induct, auto) |
177 apply (induct p rule: d22set.induct, auto) |
178 apply (simp add: SRStar_def d22set.simps, arith) |
178 apply (simp add: SRStar_def d22set.simps) |
179 apply (simp add: SRStar_def d22set.simps, clarify) |
179 apply (simp add: SRStar_def d22set.simps, clarify) |
180 apply (frule aux1) |
180 apply (frule aux1) |
181 apply (frule aux2, auto) |
181 apply (frule aux2, auto) |
182 apply (simp_all add: SRStar_def) |
182 apply (simp_all add: SRStar_def) |
183 apply (simp add: d22set.simps) |
183 apply (simp add: d22set.simps) |