Changeset 2159 for src/ASM

Timestamp:

Jul 6, 2012, 12:05:25 PM (7 years ago)

Author:

sacerdot

Message:

One daemon left, back to original proof.

File:

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

src/ASM/Assembly.ma

@@ -963 +963 @@
       >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ]
     #EQpc_delta2
+    cases (sigma_pol_ok2 … ppc_ok) -sigma_pol_ok2
+    <eq_fetch_pseudo_instruction <eq_create_label_cost_map <EQpc_delta2
+    #sigma_pol3 #sigma_pol4
     % [ % [% [% ] ] ]
     [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat
-    | >length_append >length_reverse <IH3 cases daemon (*CSC: maybe, using monotonicity*)
-    | lapply (sigma_pol_ok2 … ppc_ok) * #sigma_pol_ok3
-      <eq_fetch_pseudo_instruction <eq_create_label_cost_map #sigma_pol4
-       >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta >EQpc_delta2
+    | >length_append >length_reverse <IH3 <EQpc_delta >commutative_plus
+      cases sigma_pol4 [ #LT @(transitive_le … LT) // | * #_ #EQ >EQ % ]
+    | >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta
        #abs >abs in sigma_pol4; *
        [ #abs' cases (absurd ? abs' (not_le_Sn_n …))
        | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1
          >nat_of_bitvector_bitvector_of_nat_inverse // ]
-    | cases (sigma_pol_ok2 … ppc_ok)
-      whd in match instruction_size; normalize nodelta >p2 <eq_fetch_pseudo_instruction
-      <eq_create_label_cost_map
-      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip]
-      #sigma_ok >sigma_ok #sigma_pol_ok3 -sigma_pol_ok2
-      >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol_ok3
-      [ #LT %1 >nat_of_bitvector_add
+    | >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol4
+      [ #LT %1 >sigma_pol3 >nat_of_bitvector_add
         [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption]
         >nat_of_bitvector_bitvector_of_nat_inverse try assumption //
       | * #EQ1 #EQ2 %2 %
         [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus
-          >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero
+          >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X @bitvector_of_nat_exp_zero
         | >commutative_plus assumption ]]
   | cases daemon