Changeset 2294 for src/RTLabs


Ignore:
Timestamp:
Aug 13, 2012, 12:21:29 PM (7 years ago)
Author:
campbell
Message:

Make RTLabs cost spec deterministic.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostSpec.ma

    r2288 r2294  
    6363
    6464inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
    65 | bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
    66 | bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
     65| bostc_here : ∀l,n,H.
     66    is_cost_label (lookup_present … g l H) →
     67    bound_on_steps_to_cost g l n
     68| bostc_later : ∀l,n,H.
     69    ¬ is_cost_label (lookup_present … g l H) →
     70    bound_on_steps_to_cost1 g l n →
     71    bound_on_steps_to_cost g l n
    6772with bound_on_steps_to_cost1 : label → nat → Prop ≝
    6873| bostc_step : ∀l,n,H.
Note: See TracChangeset for help on using the changeset viewer.