equal
deleted
inserted
replaced
388 then have "f +o O(g) \<subseteq> O(f) + O(g)" |
388 then have "f +o O(g) \<subseteq> O(f) + O(g)" |
389 by (auto del: subsetI) |
389 by (auto del: subsetI) |
390 also have "\<dots> \<subseteq> O(g) + O(g)" |
390 also have "\<dots> \<subseteq> O(g) + O(g)" |
391 proof - |
391 proof - |
392 from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI) |
392 from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI) |
393 thus ?thesis by (auto del: subsetI) |
393 then show ?thesis by (auto del: subsetI) |
394 qed |
394 qed |
395 also have "\<dots> \<subseteq> O(g)" by simp |
395 also have "\<dots> \<subseteq> O(g)" by simp |
396 finally show ?thesis . |
396 finally show ?thesis . |
397 qed |
397 qed |
398 qed |
398 qed |