equal
deleted
inserted
replaced
139 by blast |
139 by blast |
140 |
140 |
141 |
141 |
142 subsubsection \<open>Properties of Preorders\<close> |
142 subsubsection \<open>Properties of Preorders\<close> |
143 |
143 |
|
144 lemma irreflp_on_multp\<^sub>H\<^sub>O[simp]: "irreflp_on B (multp\<^sub>H\<^sub>O R)" |
|
145 by (simp add: irreflp_onI multp\<^sub>H\<^sub>O_def) |
|
146 |
144 lemma totalp_on_multp\<^sub>D\<^sub>M: |
147 lemma totalp_on_multp\<^sub>D\<^sub>M: |
145 "totalp_on A R \<Longrightarrow> (\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A) \<Longrightarrow> totalp_on B (multp\<^sub>D\<^sub>M R)" |
148 "totalp_on A R \<Longrightarrow> (\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A) \<Longrightarrow> totalp_on B (multp\<^sub>D\<^sub>M R)" |
146 by (smt (verit, ccfv_SIG) count_inI in_mono multp\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M not_less_iff_gr_or_eq |
149 by (smt (verit, ccfv_SIG) count_inI in_mono multp\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M not_less_iff_gr_or_eq |
147 totalp_onD totalp_onI) |
150 totalp_onD totalp_onI) |
148 |
151 |