equal
deleted
inserted
replaced
283 lemma single_valued_waits2: |
283 lemma single_valued_waits2: |
284 assumes "vt s" |
284 assumes "vt s" |
285 shows "single_valuedP (waits2 s)" |
285 shows "single_valuedP (waits2 s)" |
286 using assms |
286 using assms |
287 unfolding single_valued_def |
287 unfolding single_valued_def |
288 by (metis Collect_splitD fst_eqD sndI waits2_unique) |
288 by (simp add: Product_Type.Collect_case_prodD waits2_unique) |
289 |
289 |
290 lemma single_valued_holds2: |
290 lemma single_valued_holds2: |
291 assumes "vt s" |
291 assumes "vt s" |
292 shows "single_valuedP (\<lambda>cs th. holds2 s th cs)" |
292 shows "single_valuedP (\<lambda>cs th. holds2 s th cs)" |
293 unfolding single_valued_def holds2_def holds_def by simp |
293 unfolding single_valued_def holds2_def holds_def by simp |