Changeset 2172 for src/ASM/StatusProofs.ma
- Timestamp:
- Jul 10, 2012, 2:39:38 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/StatusProofs.ma
r2124 r2172 200 200 #x try (#y #H) try #H whd in H; try cases H try % 201 201 whd in match set_arg_8; normalize nodelta 202 whd in match set_arg_8'; normalize nodelta 203 cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta 204 cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta 205 cases (get_index_v bool 4 nu' 0 ?) normalize nodelta 206 try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*) 202 cases (vsplit bool ???) #bit_one #seven_bits normalize nodelta 203 cases (head' bool ??) normalize nodelta 204 try % cases daemon (* XXX: need @(set_bit_addressable_sfr_set_program_counter) *) 207 205 qed. 208 206 … … 349 347 #m #cm #s #addr #byte 350 348 whd in match set_arg_8; normalize nodelta 349 cases daemon (* 351 350 whd in match set_arg_8'; normalize nodelta 352 351 cases addr #subaddressing_modein_proof … … 357 356 cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta 358 357 cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta 359 cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % 358 cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *) 360 359 qed. 361 360 … … 366 365 #m #cm #s #addr #v 367 366 whd in match set_arg_1; normalize nodelta 367 cases daemon (* 368 368 whd in match set_arg_1'; normalize nodelta 369 369 cases addr #subaddressing_modein_proof … … 376 376 cases (get_index_v bool 4 nu ??) normalize nodelta 377 377 (* XXX: try /demod/ try % *) 378 cases daemon 378 cases daemon *) 379 379 qed. 380 380
Note: See TracChangeset
for help on using the changeset viewer.