Changeset 2671


Ignore:
Timestamp:
Feb 16, 2013, 5:12:02 PM (6 years ago)
Author:
sacerdot
Message:

simplification

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2657 r2671  
    725725 ≝ λP,x.x.
    726726
    727 definition costlabel_of_as_cost_labels:
    728  ∀code,cost_labels.
    729   as_cost_label (ASM_abstract_status (load_code_memory code) cost_labels)
    730   →Σk:costlabel
    731    .(∃b:BitVector 16.lookup_opt costlabel 16 b cost_labels = Some costlabel k).
    732  #code #cost_labels * #l #Hl %{l} cases Hl #pc #Hl' %{pc} @Hl'
    733 qed.
    734 
    735727lemma costlabel_map_of_as_cost_labels_map_ok:
    736728 ∀ccode1,ccode2,cost_labels_injective,tl,Htl,PRF,PRF2.
     
    754746  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … k).
    755747  ∀trace.
    756   (Σ_{i < |trace|}(tech_cost_of_label cost_labels (map_of_sigma_map … cost_map) codom_dom (map ?? (costlabel_of_as_cost_labels …) trace) i)) =
     748  (Σ_{i < |trace|}(tech_cost_of_label cost_labels (map_of_sigma_map … cost_map) codom_dom trace i)) =
    757749  (Σ_{l ∈ trace}(ASM_cost_map compiled_code cost_labels_injective l)).
    758750* #ccode1 #ccode2 #cost_labels_injective #codom_dom #trace
     
    761753| #tl #hd #IH >append_length >commutative_plus
    762754  >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ]
    763   whd in ⊢ (??%%); <IH <map_append
    764   <(? : | map … hd | = | hd |) [1: <tech_cost_of_label_shift] [2: % | 5: // |3,4: skip]
     755  whd in ⊢ (??%%); <IH
     756  <tech_cost_of_label_shift [2: //]
    765757  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
    766758  [ cases tl -tl #tl #Htl
Note: See TracChangeset for help on using the changeset viewer.