Ignore:
Timestamp:
Jul 20, 2012, 6:36:34 PM (8 years ago)
Author:
campbell
Message:

Whole program proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostSpec.ma

    r2218 r2226  
    7676
    7777definition well_cost_labelled_program : RTLabs_program → Prop ≝
    78   λp. All ? (λx. let 〈id,fd〉 ≝ x in
    79                  match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p).
     78  λp. All ? (λx. match \snd x with [ Internal fn ⇒
     79    well_cost_labelled_fn fn ∧ soundly_labelled_fn fn
     80  | _ ⇒ True]) (prog_funct … p).
    8081
    8182
Note: See TracChangeset for help on using the changeset viewer.