Changeset 1903 for src/ASM/ASMCosts.ma
- Timestamp:
- Apr 26, 2012, 4:49:57 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1902 r1903 336 336 ∀n: nat. 337 337 ∀o: nat. 338 ∀v1: Vector addressing_mode_tag n. 339 ∀v2: Vector addressing_mode_tag o. 338 340 ∀Q: addressing_mode → T → Prop. 339 341 ∀fixed_v: Vector addressing_mode_tag (n + o). 340 342 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. 341 ∀v1: Vector addressing_mode_tag n.342 ∀v2: Vector addressing_mode_tag o.343 343 ∀fixed_v_proof: fixed_v = v1 @@ v2. 344 344 ∀subaddressing_mode_proof. 345 345 subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7 346 346 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof. 347 #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 348 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof 349 generalize in match fixed_v_proof; -fixed_v_proof 347 #T #n #o #v1 #v2 348 elim v1 cases v2 349 [1: 350 #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 351 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof 352 #subaddressing_mode_proof destruct normalize 353 #addr #absurd cases absurd 354 |2: 355 #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 356 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof 357 destruct normalize in match ([[]]@@hd:::tl); 358 ] 350 359 cases daemon 351 360 qed.
Note: See TracChangeset
for help on using the changeset viewer.