Changeset 3576 for LTS/Traces.ma
 Timestamp:
 Jun 19, 2015, 1:56:43 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Traces.ma
r3549 r3576 277 277 ] 278 278 ]. 279 280 lemma eq_ActionLabel_elim : ∀P : bool → Prop.∀p,c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → P (eq_ActionLabel p c1 c2). 281 #P #p * [#f #lab  * [ #lab]  * [ #lab] ] * 282 [1,4,7,10,13: #f' #lab' 2,5,8,14: * [2,4,6,8: #lab'] *: * [2,4,6,8,10,12: #lab'] ] #H1 #H2 283 whd in match eq_ActionLabel; normalize nodelta 284 try(@H2 % #EQ destruct) 285 [ @eq_function_name_elim [ @eq_call_cost_lab_elim [ #H #_ lapply H H ] ]  @eq_return_cost_lab_elim   @eq_fn_label_elim ] 286 normalize nodelta 287 [1,4,6,7,9: try(#EQ destruct) try(#EQ destruct) @H1 % 288 *: * #H @H2 % #EQ destruct cases H % 289 ] 290 qed. 291 292 definition DeqActionLabel ≝ λp.mk_DeqSet (ActionLabel p) (eq_ActionLabel p) ?. 293 @hide_prf #x #y @eq_ActionLabel_elim [ #EQ destruct % //  * #H % #EQ destruct cases H %] 294 qed. 295 296 unification hint 0 ≔ p ; 297 X ≟ (DeqActionLabel p) 298 (*  *) ⊢ 299 (ActionLabel p) ≡ carr X. 300 301 unification hint 0 ≔ p,p1,p2; 302 X ≟ (DeqActionLabel p) 303 (*  *) ⊢ 304 eq_ActionLabel p p1 p2 ≡ eqb X p1 p2. 279 305 280 306 definition is_cost_label : ∀p.ActionLabel p → Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.