Changeset 2193


Ignore:
Timestamp:
Jul 17, 2012, 2:12:05 AM (5 years ago)
Author:
sacerdot
Message:

Statement clean-up.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2192 r2193  
    896896         ppc = bitvector_of_nat … (|pre|) ∧
    897897         |code| ≤ 2^16 ∧
    898          True(*(ppc = zero … → code = [])*) ∧
    899898         (nat_of_bitvector … (sigma ppc) = |code| ∨
    900899          sigma ppc = zero … ∧ |code| = 2^16 ∧
     
    924923  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    925924    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
    926     cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #_ #Hfold5 #Hfold3 whd
     925    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * #Hfold1 #Hfold4 #Hfold5 #Hfold3 whd
    927926    <eq_create_label_cost_map whd %
    928927    [2: #ppc #LTppc @Hfold3 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
     
    940939  | * #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
    941940    #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH
    942     * * * #IH1 #IH2 #IH2' #IH3 #IH4
     941    * * #IH1 #IH2 #IH3 #IH4
    943942    cut (|prefix| < |instr_list|)
    944943    [ >prf >length_append normalize <plus_n_Sm @le_S_S // ] #LT_prefix_instr_list
     
    969968    <eq_fetch_pseudo_instruction <eq_create_label_cost_map <EQpc_delta2
    970969    #sigma_pol3 #sigma_pol4
    971     % [ % [% [% ] ] ]
     970    % [ % [% ] ]
    972971    [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat
    973972    | >length_append >length_reverse <EQpc_delta
     
    977976      | * * #IH3a #IH3b #IH3c >IH3b <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction
    978977        >IH3c try % assumption ]
    979     | % (*CSC: Stupid proof of True, drop fake invariant *)
    980978    | >length_append >length_reverse
    981979      cases IH3 -IH3
Note: See TracChangeset for help on using the changeset viewer.