Changeset 2197 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jul 17, 2012, 3:23:51 PM (7 years ago)
Author:
sacerdot
Message:

Main lemmas all closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2194 r2197  
    917917          assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    918918         |assembledi| ≤ |assembled| ∧
    919          ∀j:nat. ∀H: j < |assembledi|. K.
     919         ∀j:nat. ∀H: j < |assembledi|. K.
    920920          nth_safe ? j assembledi H =
    921921           nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j)))
     
    951951            assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
    952952           |assembledi| ≤ |reverse … code| ∧
    953            ∀j:nat. ∀H: j < |assembledi|. K.
     953           ∀j:nat. ∀H: j < |assembledi|. K.
    954954            nth_safe ? j assembledi H =
    955955             nth_safe ? (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat ? j))) (reverse … code) K)
     
    10711071      >reverse_append >reverse_reverse
    10721072      cases IH3 -IH3
    1073       [ #IH3 >IH3 <(length_reverse … code) @nth_safe_prepend
     1073      [ #IH3 >IH3 <(length_reverse … code) %
     1074        [ >length_append @monotonic_lt_plus_r assumption
     1075        | @nth_safe_prepend ]
    10741076      | * * #IH3a #IH3b #IH3c >IH3a @⊥
    10751077        cut (|program| = 0)
     
    11121114        >(fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction)
    11131115        @(transitive_le … IH6) //
    1114       | #j #LTj >reverse_append >reverse_reverse #K
    1115         >IH
    1116         [ @shift_nth_prefix
    1117         | >length_reverse
    1118           @(lt_to_le_to_lt …
    1119             (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat … (|assembledi'|)))))
    1120           [ @lt_to_lt_nat_of_bitvector_add try assumption
    1121             [ cases daemon (*CSC: True*)
    1122             | cases daemon (*CSC: True*)
    1123             ]
    1124           | cases IH3 -IH3
    1125             [ #eq_code <eq_code
    1126               @(transitive_le … (nat_of_bitvector … (sigma (add …  ppc' (bitvector_of_nat … 1)))))
    1127               [ cases daemon (*CSC: True*)
    1128               | cases (monotone_sigma … sigma_pol_ok … (add … ppc' (bitvector_of_nat … 1)) ppc ??)
    1129                 try assumption
    1130                 [ #X @X
    1131                 | cases daemon (*CSC: False, sigma ppc = zero! *)
    1132                 | @(transitive_le … ppc_ok) %2 %
    1133                 | cases daemon (*CSC: True*)
    1134                 ]]
    1135             | * * #_ #relevant #_ >relevant
    1136               @(transitive_le … (S ?) … (lt_nat_of_bitvector …)) [%2 % | skip]]]
    1137         ]]]]]
     1116      | #j #LTj >reverse_append >reverse_reverse cases (IH … LTj) -IH #K #IH %
     1117        [ >length_append @(lt_to_le_to_lt … K) //
     1118        | >IH @shift_nth_prefix ]]]]]
    11381119qed.
    11391120
Note: See TracChangeset for help on using the changeset viewer.