Changeset 2159


Ignore:
Timestamp:
Jul 6, 2012, 12:05:25 PM (5 years ago)
Author:
sacerdot
Message:

One daemon left, back to original proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2158 r2159  
    963963      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ]
    964964    #EQpc_delta2
     965    cases (sigma_pol_ok2 … ppc_ok) -sigma_pol_ok2
     966    <eq_fetch_pseudo_instruction <eq_create_label_cost_map <EQpc_delta2
     967    #sigma_pol3 #sigma_pol4
    965968    % [ % [% [% ] ] ]
    966969    [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat
    967     | >length_append >length_reverse <IH3 cases daemon (*CSC: maybe, using monotonicity*)
    968     | lapply (sigma_pol_ok2 … ppc_ok) * #sigma_pol_ok3
    969       <eq_fetch_pseudo_instruction <eq_create_label_cost_map #sigma_pol4
    970        >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta >EQpc_delta2
     970    | >length_append >length_reverse <IH3 <EQpc_delta >commutative_plus
     971      cases sigma_pol4 [ #LT @(transitive_le … LT) // | * #_ #EQ >EQ % ]
     972    | >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta
    971973       #abs >abs in sigma_pol4; *
    972974       [ #abs' cases (absurd ? abs' (not_le_Sn_n …))
    973975       | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1
    974976         >nat_of_bitvector_bitvector_of_nat_inverse // ]
    975     | cases (sigma_pol_ok2 … ppc_ok)
    976       whd in match instruction_size; normalize nodelta >p2 <eq_fetch_pseudo_instruction
    977       <eq_create_label_cost_map
    978       >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip]
    979       #sigma_ok >sigma_ok #sigma_pol_ok3 -sigma_pol_ok2
    980       >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol_ok3
    981       [ #LT %1 >nat_of_bitvector_add
     977    | >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol4
     978      [ #LT %1 >sigma_pol3 >nat_of_bitvector_add
    982979        [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption]
    983980        >nat_of_bitvector_bitvector_of_nat_inverse try assumption //
    984981      | * #EQ1 #EQ2 %2 %
    985982        [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus
    986           >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero
     983          >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X @bitvector_of_nat_exp_zero
    987984        | >commutative_plus assumption ]]
    988985  | cases daemon
Note: See TracChangeset for help on using the changeset viewer.