Changeset 2193 for src/ASM/Assembly.ma

Timestamp:

Jul 17, 2012, 2:12:05 AM (9 years ago)

Author:

sacerdot

Message:

Statement clean-up.

File:

• src/ASM/Assembly.ma (modified) (5 diffs)

src/ASM/Assembly.ma

@@ -896 +896 @@
          ppc = bitvector_of_nat … (|pre|) ∧
          |code| ≤ 2^16 ∧
-         True(*(ppc = zero … → code = [])*) ∧
          (nat_of_bitvector … (sigma ppc) = |code| ∨
           sigma ppc = zero … ∧ |code| = 2^16 ∧
@@ -924 +923 @@
   [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
     >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
-    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #_ #Hfold5 #Hfold3 whd
+    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * #Hfold1 #Hfold4 #Hfold5 #Hfold3 whd
     <eq_create_label_cost_map whd %
     [2: #ppc #LTppc @Hfold3 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
@@ -940 +939 @@
   | * #sigma_pol_ok1 #sigma_pol_ok2 #instr_list_ok cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
     #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH
-    * * * #IH1 #IH2 #IH2' #IH3 #IH4
+    * * #IH1 #IH2 #IH3 #IH4
     cut (|prefix| < |instr_list|)
     [ >prf >length_append normalize <plus_n_Sm @le_S_S // ] #LT_prefix_instr_list
@@ -969 +968 @@
     <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 <EQpc_delta 
@@ -977 +976 @@
       | * * #IH3a #IH3b #IH3c >IH3b <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction
         >IH3c try % assumption ]
-    | % (*CSC: Stupid proof of True, drop fake invariant *)
     | >length_append >length_reverse
       cases IH3 -IH3