Changeset 1913 for src/ASM/ASMCosts.ma
- Timestamp:
- May 3, 2012, 4:20:21 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1912 r1913 910 910 ∀trace_ends_flag. 911 911 ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. 912 trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace 913 ≤ total_program_size → 912 914 program_counter' = program_counter … start_status → 913 915 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. 919 921 λgood_program_witness: good_program code_memory total_program_size. ?. 920 cases(block_cost' code_memory program_counter [ ] total_program_size total_program_size cost_labels 921 reachable_program_counter_witness good_program_witness true ?) 922 [1: 923 #cost_of_block #block_cost_hyp 924 %{cost_of_block} 925 cases(lookup_opt … cost_labels) in block_cost_hyp; 926 [2: #cost_label] normalize nodelta 927 #hyp assumption 928 |2: 929 @le_plus_n_r 930 ] 922 cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels 923 reachable_program_counter_witness good_program_witness true) 924 #cost_of_block #block_cost_hyp 925 %{cost_of_block} 926 cases(lookup_opt … cost_labels) in block_cost_hyp; 927 [2: #cost_label] normalize nodelta 928 #hyp assumption 931 929 qed. 932 930
Note: See TracChangeset
for help on using the changeset viewer.