Changeset 2195
- Timestamp:
- Jul 17, 2012, 10:48:45 AM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2194 r2195 255 255 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 256 256 [>eq_assembly_1_pseudoinstruction |2: skip] #OK >OK <EQlen * 257 [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled'; 258 <add_bitvector_of_nat_Sm >add_commutative 259 >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2 260 lapply (eq_f … (bitvector_of_nat 16) … EQ2) -EQ2 261 <add_bitvector_of_nat_plus >bitvector_of_nat_inverse_nat_of_bitvector 262 #X >X #Y @NOT_EMPTY <Y >bitvector_of_nat_exp_zero % ] 257 [2: * #EQ1 #EQ2 258 @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|))))) 259 [1: @lt_to_lt_nat_of_bitvector_add try assumption 260 cases daemon (* XXX: two cases to prove, both true *) 261 |2: cases daemon (* XXX: use monotonicity of sigma *) 262 ] 263 ] 263 264 cases (le_to_or_lt_eq … instr_list_ok) 264 265 [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero … … 282 283 >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption 283 284 @(transitive_le … instr_list_ok') @le_S_S assumption 284 | *#EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]]285 | #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]] 285 286 |2: 286 287 -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
Note: See TracChangeset
for help on using the changeset viewer.