equal
deleted
inserted
replaced
385 "F \<in> Always A ==> (F \<in> Always (-A \<union> B)) = (F \<in> Always B)" |
385 "F \<in> Always A ==> (F \<in> Always (-A \<union> B)) = (F \<in> Always B)" |
386 by (auto simp add: Always_eq_includes_reachable) |
386 by (auto simp add: Always_eq_includes_reachable) |
387 |
387 |
388 (*Delete the nearest invariance assumption (which will be the second one |
388 (*Delete the nearest invariance assumption (which will be the second one |
389 used by Always_Int_I) *) |
389 used by Always_Int_I) *) |
390 lemmas Always_thin = thin_rl [of "F \<in> Always A"] |
390 lemmas Always_thin = thin_rl [of "F \<in> Always A"] for F A |
391 |
391 |
392 |
392 |
393 subsection\<open>Totalize\<close> |
393 subsection\<open>Totalize\<close> |
394 |
394 |
395 lemma reachable_imp_reachable_tot: |
395 lemma reachable_imp_reachable_tot: |