- Timestamp:
- Mar 21, 2013, 9:45:59 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/CostInj.ma
r2601 r2937 1 include "RTLabs/ RTLabs_traces.ma".1 include "RTLabs/CostSpec.ma". 2 2 3 3 (* Check that the RTLabs pc → cost label map is injective for a given RTLabs … … 68 68 [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3) 69 69 [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct 70 | * #_ #PR'' @H1 /3/70 | * #_ #PR'' @H1 % /2/ 71 71 ] 72 72 | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/ … … 78 78 [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct 79 79 @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 ] 81 81 ] 82 82 | #Lcl' cases (lookup_add_cases ??????? Lcl') … … 90 90 [ assumption 91 91 | >(lookup_present_eq ????? L ?) assumption 92 | #E destruct /2/92 | #E destruct @(absurd … PR' FR) 93 93 ] 94 94 ] … … 100 100 ] 101 101 | cases r 102 [ //102 [ whd in ⊢ (% → %); // 103 103 | #m whd in ⊢ (% → %); #H 104 104 #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2
Note: See TracChangeset
for help on using the changeset viewer.