Ignore:
Timestamp:
Feb 23, 2012, 5:17:32 PM (8 years ago)
Author:
sacerdot
Message:

Minor changes while studying the proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Interference.ma

    r1429 r1730  
    2727; prop_colouring: ∀l. ∀v1, v2: vertex.
    2828   is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
    29 ; prop_colouring2:
     29; prop_colouring2: (*CSC: the exist-guarded premise is just to make the proof more general *)
    3030   ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no
     31(* CSC: useless for the proof and very weak
    3132; prop_colouring3:
    3233   spilled_no = 0 ∨
    3334    ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1)
     35*)
    3436}.
    3537
Note: See TracChangeset for help on using the changeset viewer.