Changeset 1903


Ignore:
Timestamp:
Apr 26, 2012, 4:49:57 PM (7 years ago)
Author:
mulligan
Message:

Small changes prior to experiment

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1902 r1903  
    336336  ∀n: nat.
    337337  ∀o: nat.
     338  ∀v1: Vector addressing_mode_tag n.
     339  ∀v2: Vector addressing_mode_tag o.
    338340  ∀Q: addressing_mode → T → Prop.
    339341  ∀fixed_v: Vector addressing_mode_tag (n + o).
    340342  ∀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.
    343343  ∀fixed_v_proof: fixed_v = v1 @@ v2.
    344344  ∀subaddressing_mode_proof.
    345345    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
    346346      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  ]
    350359  cases daemon
    351360qed.
Note: See TracChangeset for help on using the changeset viewer.