Changeset 2226 for src/RTLabs/CostSpec.ma

Timestamp:

Jul 20, 2012, 6:36:34 PM (8 years ago)

Author:

campbell

Message:

Whole program proof.

File:

• src/RTLabs/CostSpec.ma (modified) (1 diff)

src/RTLabs/CostSpec.ma

@@ -76 +76 @@
 
 definition well_cost_labelled_program : RTLabs_program → Prop ≝
-  λp. All ? (λx. let 〈id,fd〉 ≝ x in
-                 match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p).
+  λp. All ? (λx. match \snd x with [ Internal fn ⇒
+    well_cost_labelled_fn fn ∧ soundly_labelled_fn fn
+  | _ ⇒ True]) (prog_funct … p).