Changeset 3102
- Timestamp:
- Apr 6, 2013, 4:11:42 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r3028 r3102 121 121 change with (? → if eq_bv ??? then ? else ? = ?) 122 122 #assm 123 cases (le_to_or_lt_eq … (nat_of_bitvector 16e) bound' ?)123 cases (le_to_or_lt_eq … (nat_of_bitvector ? e) bound' ?) 124 124 [1: 125 125 #e_lt_assm … … 271 271 ∀classify_assm: ASM_classify0 instruction = cl_other. 272 272 ∀pi1 : ℕ. 273 (if match lookup_opt costlabel 16program_counter''' (costlabels prog) with273 (if match lookup_opt ?? program_counter''' (costlabels prog) with 274 274 [None ⇒ true 275 275 |Some _ ⇒ false … … 405 405 change with (ASM_classify0 ? = ?) in classifier_assm; 406 406 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 407 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;408 407 <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) 409 408 qed. … … 463 462 change with (ASM_classify0 ? = ?) in classifier_assm; 464 463 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 465 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;466 464 <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) 467 465 qed. … … 483 481 ∀classify_assm: ASM_classify0 instruction = cl_call. 484 482 (∀pi1:ℕ 485 .if match lookup_opt costlabel 16program_counter'' (costlabels prog) with483 .if match lookup_opt ?? program_counter'' (costlabels prog) with 486 484 [None ⇒ true | Some _ ⇒ false] 487 485 then (∀start_status0:Status (cm prog) … … 600 598 try (change with (ASM_classify0 ? = ?) in classifier_assm;) 601 599 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 602 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;603 600 <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd 604 601 #absurd destruct(absurd) … … 665 662 try (change with (ASM_classify0 ? = ?) in classifier_assm;) 666 663 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 667 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;668 664 <FETCH in classifier_assm; >classify_assm 669 665 #absurd try (destruct(absurd))
Note: See TracChangeset
for help on using the changeset viewer.