Changeset 2314 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Aug 31, 2012, 4:12:35 PM (8 years ago)
Author:
campbell
Message:

Move generic definitions from recent commit to appropriate places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2313 r2314  
    66include "common/Executions.ma".
    77include "utilities/deqsets.ma".
     8include "utilities/listb.ma".
    89
    910discriminator status_class.
     
    23912392] qed.
    23922393
    2393 (* TODO: move *)
    2394 lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
    2395   Exists S (λy. y = x) l →
    2396   x ∈ l.
    2397 #S #x #l elim l
    2398 [ //
    2399 | #h #t #IH
    2400   normalize lapply (eqb_true … x h)
    2401   cases (x==h) *
    2402   [ #E #_ >(E (refl ??)) //
    2403   | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
    2404             | #H @IH @H
    2405             ]
    2406   ]
    2407 ] qed.
    24082394
    24092395(* We need to link the pcs, states of the semantics with the labels and graphs
Note: See TracChangeset for help on using the changeset viewer.