Changeset 2937


Ignore:
Timestamp:
Mar 21, 2013, 9:45:59 PM (4 years ago)
Author:
campbell
Message:

Speed up checking of RTLabs/CostInj.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostInj.ma

    r2601 r2937  
    1 include "RTLabs/RTLabs_traces.ma".
     1include "RTLabs/CostSpec.ma".
    22
    33(* Check that the RTLabs pc → cost label map is injective for a given RTLabs
     
    6868      [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3)
    6969        [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct
    70         | * #_ #PR'' @H1 /3/
     70        | * #_ #PR'' @H1 % /2/
    7171        ]
    7272      | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/
     
    7878          [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct
    7979            @lookup_add_hit
    80           | * #NE #PR'' lapply (H1 ?) [/3/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ]
     80          | * #NE #PR'' lapply (H1 ?) [% /2/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ]
    8181          ]
    8282        | #Lcl' cases (lookup_add_cases ??????? Lcl')
     
    9090        [ assumption
    9191        | >(lookup_present_eq ????? L ?) assumption
    92         | #E destruct /2/
     92        | #E destruct @(absurd … PR' FR)
    9393        ]
    9494      ]
     
    100100  ]
    101101| cases r
    102   [ //
     102  [ whd in ⊢ (% → %); //
    103103  | #m whd in ⊢ (% → %); #H
    104104    #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2
Note: See TracChangeset for help on using the changeset viewer.