Changeset 1913


Ignore:
Timestamp:
May 3, 2012, 4:20:21 PM (7 years ago)
Author:
mulligan
Message:

Got the rest of the file to typecheck as before.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1912 r1913  
    910910        ∀trace_ends_flag.
    911911        ∀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 →
    912914          program_counter' = program_counter … start_status →
    913915            cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
     
    918920  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
    919921  λ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
    931929qed.
    932930
Note: See TracChangeset for help on using the changeset viewer.