Changeset 2032 for src/ASM/StatusProofs.ma
 Timestamp:
 Jun 8, 2012, 4:32:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/StatusProofs.ma
r1962 r2032 27 27 #m #s #v 28 28 whd in match write_at_stack_pointer; normalize nodelta 29 cases( split … 4 4 ?) #nu #nl normalize nodelta29 cases(vsplit … 4 4 ?) #nu #nl normalize nodelta 30 30 cases(get_index_v … 4 nu 0 ?) // 31 31 qed. … … 178 178 whd in match set_arg_8; normalize nodelta 179 179 whd in match set_arg_8'; normalize nodelta 180 cases ( split bool 4 4 ?) #nu' #nl' normalize nodelta181 cases ( split bool 1 3 nu') #bit1' #ignore' normalize nodelta180 cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta 181 cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta 182 182 cases (get_index_v bool 4 nu' 0 ?) normalize nodelta 183 183 try % @set_bit_addressable_sfr_set_code_memory … … 201 201 whd in match set_arg_8; normalize nodelta 202 202 whd in match set_arg_8'; normalize nodelta 203 cases ( split bool 4 4 ?) #nu' #nl' normalize nodelta204 cases ( split bool 1 3 nu') #bit1' #ignore' normalize nodelta203 cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta 204 cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta 205 205 cases (get_index_v bool 4 nu' 0 ?) normalize nodelta 206 206 try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*) … … 238 238 = special_function_registers_8051 T cm s. 239 239 #T #cm #s #x whd in ⊢ (??(???%)?); 240 cases ( split ????) #nu #nl normalize nodelta;240 cases (vsplit ????) #nu #nl normalize nodelta; 241 241 cases (get_index_v bool ????) % 242 242 qed. … … 250 250 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s. 251 251 #T #s #x whd in ⊢ (??(??%)?); 252 cases ( split ????) #nu #nl normalize nodelta;252 cases (vsplit ????) #nu #nl normalize nodelta; 253 253 cases (get_index_v bool ????) % 254 254 qed.*) … … 299 299 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s. 300 300 #T #cm #s #x whd in ⊢ (??(???%)?); 301 cases ( split ????) #nu #nl normalize nodelta;301 cases (vsplit ????) #nu #nl normalize nodelta; 302 302 cases (get_index_v bool ????) % 303 303 qed. … … 308 308 = special_function_registers_8052 T cm s. 309 309 #T #cm #s #x whd in ⊢ (??(???%)?); 310 cases ( split ????) #nu #nl normalize nodelta;310 cases (vsplit ????) #nu #nl normalize nodelta; 311 311 cases (get_index_v bool ????) % 312 312 qed. … … 315 315 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s. 316 316 #T #cm #s #x whd in ⊢ (??(???%)?); 317 cases ( split ????) #nu #nl normalize nodelta;317 cases (vsplit ????) #nu #nl normalize nodelta; 318 318 cases (get_index_v bool ????) % 319 319 qed. … … 322 322 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s. 323 323 #T #cm #s #x whd in ⊢ (??(???%)?); 324 cases ( split ????) #nu #nl normalize nodelta;324 cases (vsplit ????) #nu #nl normalize nodelta; 325 325 cases (get_index_v bool ????) % 326 326 qed. … … 356 356 try (#ignore #addr normalize in addr; cases addr) 357 357 normalize nodelta try #_ try /demod/ try % 358 cases ( split bool 4 4 ?) #nu #nl normalize nodelta359 cases ( split bool 1 3 ?) #ignore #three_bits normalize nodelta358 cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta 359 cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta 360 360 cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % 361 361 qed. … … 373 373 try (#addr normalize in addr; cases addr) 374 374 normalize nodelta 375 cases ( split bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %376 cases ( split bool 1 3 ?) #ignore #three_bits normalize nodelta375 cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try % 376 cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta 377 377 cases (get_index_v bool 4 nu ??) normalize nodelta 378 378 (* XXX: try /demod/ try % *) … … 391 391 try (#addr normalize in addr; cases addr) 392 392 normalize nodelta 393 cases ( split bool 8 8 v) #bu #bl normalize nodelta /demod/ %393 cases (vsplit bool 8 8 v) #bu #bl normalize nodelta /demod/ % 394 394 qed. 395 395 … … 413 413 #m #cm #s #v 414 414 whd in match write_at_stack_pointer; normalize nodelta 415 cases ( split bool 4 4 ?) #nu #nl normalize nodelta415 cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta 416 416 cases (get_index_v bool 4 nu ??) normalize nodelta /demod/ % 417 417 qed.
Note: See TracChangeset
for help on using the changeset viewer.