Changeset 1913 for src/ASM/ASMCosts.ma

Timestamp:

May 3, 2012, 4:20:21 PM (9 years ago)

Author:

mulligan

Message:

Got the rest of the file to typecheck as before.

File:

• src/ASM/ASMCosts.ma (modified) (2 diffs)

src/ASM/ASMCosts.ma

@@ -910 +910 @@
         ∀trace_ends_flag.
         ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
+          trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace
+            ≤ total_program_size →
           program_counter' = program_counter … start_status →
             cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
@@ -918 +920 @@
   λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
   λgood_program_witness: good_program code_memory total_program_size. ?.
-  cases(block_cost' code_memory program_counter [ ] total_program_size total_program_size cost_labels
-    reachable_program_counter_witness good_program_witness true ?)
-  [1:
-    #cost_of_block #block_cost_hyp
-    %{cost_of_block}
-    cases(lookup_opt … cost_labels) in block_cost_hyp;
-    [2: #cost_label] normalize nodelta
-    #hyp assumption
-  |2:
-    @le_plus_n_r
-  ]
+  cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
+    reachable_program_counter_witness good_program_witness true)
+  #cost_of_block #block_cost_hyp
+  %{cost_of_block}
+  cases(lookup_opt … cost_labels) in block_cost_hyp;
+  [2: #cost_label] normalize nodelta
+  #hyp assumption
 qed.