Changeset 2197 for src/ASM/Assembly.ma
 Timestamp:
 Jul 17, 2012, 3:23:51 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2194 r2197 917 917 assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 918 918 assembledi ≤ assembled ∧ 919 ∀j:nat. ∀H: j < assembledi. ∀K.919 ∀j:nat. ∀H: j < assembledi. ∃K. 920 920 nth_safe ? j assembledi H = 921 921 nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j))) … … 951 951 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in 952 952 assembledi ≤ reverse … code ∧ 953 ∀j:nat. ∀H: j < assembledi. ∀K.953 ∀j:nat. ∀H: j < assembledi. ∃K. 954 954 nth_safe ? j assembledi H = 955 955 nth_safe ? (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat ? j))) (reverse … code) K) … … 1071 1071 >reverse_append >reverse_reverse 1072 1072 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 ] 1074 1076  * * #IH3a #IH3b #IH3c >IH3a @⊥ 1075 1077 cut (program = 0) … … 1112 1114 >(fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) 1113 1115 @(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 ]]]]] 1138 1119 qed. 1139 1120
Note: See TracChangeset
for help on using the changeset viewer.