Changeset 1903 for src/ASM/ASMCosts.ma

Timestamp:

Apr 26, 2012, 4:49:57 PM (8 years ago)

Author:

mulligan

Message:

Small changes prior to experiment

File:

• src/ASM/ASMCosts.ma (modified) (1 diff)

src/ASM/ASMCosts.ma

@@ -336 +336 @@
   ∀n: nat.
   ∀o: nat.
+  ∀v1: Vector addressing_mode_tag n.
+  ∀v2: Vector addressing_mode_tag o.
   ∀Q: addressing_mode → T → Prop.
   ∀fixed_v: Vector addressing_mode_tag (n + o).
   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
-  ∀v1: Vector addressing_mode_tag n.
-  ∀v2: Vector addressing_mode_tag o.
   ∀fixed_v_proof: fixed_v = v1 @@ v2.
   ∀subaddressing_mode_proof.
     subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
-  #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
-  #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof
-  generalize in match fixed_v_proof; -fixed_v_proof
+  #T #n #o #v1 #v2
+  elim v1 cases v2
+  [1:
+    #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
+    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
+    #subaddressing_mode_proof destruct normalize
+    #addr #absurd cases absurd
+  |2:
+    #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
+    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
+    destruct normalize in match ([[]]@@hd:::tl);
+  ]
   cases daemon
 qed.