- Timestamp:
- Jul 6, 2012, 11:41:40 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2157 r2158 850 850 qed. 851 851 852 853 854 852 definition assembly: 855 853 ∀p: pseudo_assembly_program. … … 958 956 lapply (fst_snd_assembly_1_pseudoinstruction … p2) #EQpc_delta 959 957 cut (pc_delta < 2^16) 960 [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok check fst_eq 958 [ >EQpc_delta 959 @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? p2) 960 @assembly1_pseudoinstruction_lt_2_to_16 ] #pc_delta_ok 961 961 cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd)) 962 962 [ whd in match instruction_size; normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.