Ignore:
Timestamp:
Mar 11, 2013, 6:50:48 PM (8 years ago)
Author:
piccolo
Message:

ERTLptr to LTL correctness proof started

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/Interference.ma

    r2739 r2845  
    1313{ colouring: vertex → decision
    1414; spilled_no: nat
    15 ; prop_colouring: ∀l. ∀v1, v2: vertex.
     15; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 →
    1616  lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2
    1717; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *)
Note: See TracChangeset for help on using the changeset viewer.