Ignore:
Timestamp:
Aug 10, 2011, 5:17:58 PM (9 years ago)
Author:
campbell
Message:

Show that RTLabs graphs are closed on branch (i.e., all labels in
instructions are in the graph). Rather time consuming and fiddly.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma

    r1104 r1105  
    122122] qed.
    123123
     124lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
     125  lookup tag A (add tag A m i a) j = Some ? v →
     126  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
     127#tag #A #m #i #j #a #v
     128cases (identifier_eq ? i j)
     129[ #E >E >lookup_add_hit #H %1 destruct % //
     130| #NE >lookup_add_miss /2/ @eq_identifier_elim /2/
     131] qed.
     132
    124133(* Extract every identifier, value pair from the map. *)
    125134definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
Note: See TracChangeset for help on using the changeset viewer.